<commit_before>/-
Copyright (c) 2017 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: <NAME>
-/

section subtype
variables {α : Sort*} {β : α → Prop}

protected lemma subtype.eq' : ∀ {a1 a2 : {x // β x}}, a1.val = a2.val → a1 = a2
| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl

lemma subtype.ext {a1 a2 : {x // β x}} : a1 = a2 ↔ a1.val = a2.val :=
⟨congr_arg _, subtype.eq'⟩

theorem subtype.val_injective : function.injective (@subtype.val _ β) :=
λ a b, subtype.eq'

@[simp] theorem subtype.coe_eta {α : Type*} {β : α → Prop}
 (a : {a // β a}) (h : β a) : subtype.mk ↑a h = a := subtype.eta _ _

@[simp] theorem subtype.coe_mk {α : Type*} {β : α → Prop}
 (a h) : (@subtype.mk α β a h : α) = a := rfl

@[simp] theorem subtype.mk_eq_mk {α : Type*} {β : α → Prop}
 {a h a' h'} : @subtype.mk α β a h = @subtype.mk α β a' h' ↔ a = a' :=<commit_msg>feat(data/subtype): subtype.coe_ext<commit_after>/-
Copyright (c) 2017 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: <NAME>
-/

section subtype
variables {α : Sort*} {β : α → Prop}

protected lemma subtype.eq' : ∀ {a1 a2 : {x // β x}}, a1.val = a2.val → a1 = a2
| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl

lemma subtype.ext {a1 a2 : {x // β x}} : a1 = a2 ↔ a1.val = a2.val :=
⟨congr_arg _, subtype.eq'⟩

lemma subtype.coe_ext {a1 a2 : {x // β x}} : a1 = a2 ↔ (a1 : α) = a2 :=
subtype.ext

theorem subtype.val_injective : function.injective (@subtype.val _ β) :=
λ a b, subtype.eq'

@[simp] theorem subtype.coe_eta {α : Type*} {β : α → Prop}
 (a : {a // β a}) (h : β a) : subtype.mk ↑a h = a := subtype.eta _ _

@[simp] theorem subtype.coe_mk {α : Type*} {β : α → Prop}
 (a h) : (@subtype.mk α β a h : α) = a := rfl

@[simp] theorem subtype.mk_eq_mk {α : Type*} {β : α → Prop}
 {a h a' h'} : @subtype.mk α β a h = @subtype.mk α β a' h' ↔ a = a' :=
{'fraction_non_alphanumeric': 0.1919191919191919, 'fraction_numerical': 0.024455077086656035, 'mean_word_length': 2.937238493723849, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '869538', 'n_tokens_mistral': 883, 'n_tokens_neox': 820, 'n_words': 293}