awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : (↑s : Type)
rw : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (List.range (↑x : ℕ))).length = #({y ∈ range (↑x : ℕ) | y ∈ s})
⊢ toFunAux (s := s) x = #({y ∈ range (↑x : ℕ) | y ∈ s})

Tactic:
rw [toFunAux, List.countP_eq_length_filter]

Premises used: List.countP_eq_length_filter, _private.0.Nat.Subtype.toFunAux
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : (↑s : Type)
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (List.range (↑x : ℕ))).length = #({y ∈ range (↑x : ℕ) | y ∈ s})

Tactic:
rfl
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
rw : ∀ (x : ℕ), x ∉ {y ∈ range (↑(ofNat s 0) : ℕ) | y ∈ s}
⊢ toFunAux (s := s) (ofNat s 0) = 0

Tactic:
rw [toFunAux_eq, card_eq_zero, eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem, Finset.card_eq_zero, _private.0.Nat.Subtype.toFunAux_eq
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
hn : n ∈ {y ∈ range (↑(ofNat s 0) : ℕ) | y ∈ s}
⊢ n < (↑⊥ : ℕ) ∧ n ∈ s

Tactic:
rw [mem_filter, ofNat, mem_range] at hn

Premises used: Finset.mem_range, Nat.Subtype.ofNat, Finset.mem_filter
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
hn : n < (↑⊥ : ℕ) ∧ n ∈ s
⊢ False

Tactic:
bot_le.not_gt (show (⟨n, hn.2⟩ : s) < ⊥ from hn.1)

Premises used: LE.le.not_gt, And.left, bot_le
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
hn : n < (↑⊥ : ℕ) ∧ n ∈ s
⊢ False

Tactic:
exact bot_le.not_gt (show (⟨n, hn.2⟩ : s) < ⊥ from hn.1)

Premises used: LE.le.not_gt, And.left, bot_le
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
⊢ toFunAux (s := s) (ofNat s n) = n

Tactic:
have ih : toFunAux (ofNat s n) = n := right_inverse_aux n
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
⊢ (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}

Tactic:
simp
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
⊢ (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}

Tactic:
have h₁ : (ofNat s n : ℕ) ∉ {x ∈ range (ofNat s n) | x ∈ s} := by simp
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
simp :
  ∀ (a : ℕ), a < (↑(succ (s := s) (ofNat s n)) : ℕ) ∧ a ∈ s ↔ a = (↑(ofNat s n) : ℕ) ∨ a < (↑(ofNat s n) : ℕ) ∧ a ∈ s
⊢ {x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s} =
    insert (↑(ofNat s n) : ℕ) ({x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s})

Tactic:
simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]

Premises used: Finset.mem_insert, Finset.ext_iff, Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
m : ℕ
h : m < (↑(succ (s := s) (ofNat s n)) : ℕ) ∧ m ∈ s
simp : m = (↑(ofNat s n) : ℕ) ∨ m < (↑(ofNat s n) : ℕ)
⊢ m = (↑(ofNat s n) : ℕ) ∨ m < (↑(ofNat s n) : ℕ) ∧ m ∈ s

Tactic:
simp only [h.2, and_true]

Premises used: and_true, And.right
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
m : ℕ
h : m < (↑(succ (s := s) (ofNat s n)) : ℕ) ∧ m ∈ s
⊢ m = (↑(ofNat s n) : ℕ) ∨ m < (↑(ofNat s n) : ℕ)

Tactic:
Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1))

Premises used: lt_or_eq_of_le, Nat.Subtype.lt_succ_iff_le, Or.symm, And.left, Iff.mp
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
m : ℕ
h : m < (↑(succ (s := s) (ofNat s n)) : ℕ) ∧ m ∈ s
⊢ m = (↑(ofNat s n) : ℕ) ∨ m < (↑(ofNat s n) : ℕ)

Tactic:
exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1))

Premises used: lt_or_eq_of_le, Nat.Subtype.lt_succ_iff_le, Or.symm, And.left, Iff.mp
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
⊢ ∀ (a : ℕ), a < (↑(succ (s := s) (ofNat s n)) : ℕ) ∧ a ∈ s ↔ a = (↑(ofNat s n) : ℕ) ∨ a < (↑(ofNat s n) : ℕ) ∧ a ∈ s

Tactic:
exact fun m =>
        ⟨fun h => by
          simp only [h.2, and_true]
          exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)),
         fun h =>
          h.elim (fun h => h.symm ▸ ⟨lt_succ_self _, (ofNat s n).prop⟩) fun h =>
            ⟨h.1.trans (lt_succ_self _), h.2⟩⟩
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
⊢ {x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s} =
    insert (↑(ofNat s n) : ℕ) ({x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s})

Tactic:
have h₂ : {x ∈ range (succ (ofNat s n)) | x ∈ s} =
        insert ↑(ofNat s n) {x ∈ range (ofNat s n) | x ∈ s} := by
      simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]
      exact fun m =>
        ⟨fun h => by
          simp only [h.2, and_true]
          exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)),
         fun h =>
          h.elim (fun h => h.symm ▸ ⟨lt_succ_self _, (ofNat s n).prop⟩) fun h =>
            ⟨h.1.trans (lt_succ_self _), h.2⟩⟩
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
h₂ :
  {x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s} =
    insert (↑(ofNat s n) : ℕ) ({x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s})
simp :
  ∀ (ih : #({y ∈ range (↑(ofNat s n) : ℕ) | y ∈ s}) = n),
    #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1
⊢ toFunAux (s := s) (ofNat s (n + 1)) = n + 1

Tactic:
simp only [toFunAux_eq, ofNat] at ih ⊢

Premises used: Nat.Subtype.ofNat, _private.0.Nat.Subtype.toFunAux_eq
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
h₂ :
  {x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s} =
    insert (↑(ofNat s n) : ℕ) ({x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s})
ih : #({y ∈ range (↑(ofNat s n) : ℕ) | y ∈ s}) = n
rhs : n + 1
| #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1

Tactic:
rhs
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
h₂ :
  {x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s} =
    insert (↑(ofNat s n) : ℕ) ({x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s})
ih : #({y ∈ range (↑(ofNat s n) : ℕ) | y ∈ s}) = n
rw : #({x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s})
| n + 1

Tactic:
rw [← ih, ← card_insert_of_notMem h₁, ← h₂]

Premises used: Finset.card_insert_of_notMem
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
h₂ :
  {x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s} =
    insert (↑(ofNat s n) : ℕ) ({x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s})
ih : #({y ∈ range (↑(ofNat s n) : ℕ) | y ∈ s}) = n
rw : #({x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s})
| #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1

Tactic:
rhs
      rw [← ih, ← card_insert_of_notMem h₁, ← h₂]

Premises used: Finset.card_insert_of_notMem
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
h₁ : (↑(ofNat s n) : ℕ) ∉ {x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s}
h₂ :
  {x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s} =
    insert (↑(ofNat s n) : ℕ) ({x ∈ range (↑(ofNat s n) : ℕ) | x ∈ s})
ih : #({y ∈ range (↑(ofNat s n) : ℕ) | y ∈ s}) = n
conv : #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1
conv₁ :
  #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = #({x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s})
⊢ #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1

Tactic:
conv =>
      rhs
      rw [← ih, ← card_insert_of_notMem h₁, ← h₂]

Premises used: Finset.card_insert_of_notMem
-- Module: Mathlib.Logic.Denumerable
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
inst_1 : Infinite α
this_1 : DecidablePred fun (x : ℕ) ↦ x ∈ Set.range.{0, u_3 + 1} (ι := α) encode := decidableRangeEncode α
this_2 : Infinite (↑(Set.range.{0, u_3 + 1} (ι := α) encode) : Type) := ⋯
this : Denumerable (↑(Set.range.{0, u_3 + 1} (ι := α) encode) : Type) :=
  Subtype.denumerable (Set.range.{0, u_3 + 1} (ι := α) encode)
⊢ Denumerable α

Tactic:
exact Denumerable.ofEquiv (Set.range (@encode α _)) (equivRangeEncode α)

Premises used: Set.Elem, Encodable.equivRangeEncode, Encodable.encode, Set.range, Denumerable.ofEquiv
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_3
inst : Countable α
inst_1 : Infinite α
⊢ Nonempty.{u_3 + 1} (Denumerable α)

Tactic:
(nonempty_encodable α).map fun h => @Denumerable.ofEncodableOfInfinite _ h _

Premises used: Denumerable.ofEncodableOfInfinite, nonempty_encodable, Nonempty.map
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_3
⊢ Nonempty.{u_3 + 1} (Denumerable α) ↔ Countable α ∧ Infinite α

Tactic:
⟨fun ⟨_⟩ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ nonempty_denumerable _⟩

Premises used: inferInstance, _private.0.nonempty_denumerable_iff.match_1, _private.0.nonempty_denumerable_iff.match_2, And, And.intro, Iff.intro, Countable, Nonempty, Infinite, nonempty_denumerable, Denumerable
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Countable α
inst_1 : Infinite α
inst_2 : Countable β
inst_3 : Infinite β
intro : ∀ (val : Denumerable α), Nonempty (α ≃ β)
⊢ Nonempty (α ≃ β)

Tactic:
cases nonempty_denumerable α

Premises used: nonempty_denumerable
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Countable α
inst_1 : Infinite α
inst_2 : Countable β
inst_3 : Infinite β
val : Denumerable α
intro : ∀ (val : Denumerable β), Nonempty (α ≃ β)
⊢ Nonempty (α ≃ β)

Tactic:
cases nonempty_denumerable β

Premises used: nonempty_denumerable
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Countable α
inst_1 : Infinite α
inst_2 : Countable β
inst_3 : Infinite β
val : Denumerable α
val_1 : Denumerable β
⊢ Nonempty (α ≃ β)

Tactic:
⟨(Denumerable.eqv _).trans (Denumerable.eqv _).symm⟩

Premises used: Denumerable.eqv, Equiv.trans, Nonempty.intro, Equiv.symm
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Countable α
inst_1 : Infinite α
inst_2 : Countable β
inst_3 : Infinite β
val : Denumerable α
val_1 : Denumerable β
⊢ Nonempty (α ≃ β)

Tactic:
exact ⟨(Denumerable.eqv _).trans (Denumerable.eqv _).symm⟩
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
f g : α ↪ β
h : f.toFun = g.toFun
mk :
  ∀ (toFun : α → β) (inj' : Injective toFun) (h : { toFun := toFun, inj' := inj' : α ↪ β }.toFun = g.toFun),
    { toFun := toFun, inj' := inj' : α ↪ β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
g : α ↪ β
toFun : α → β
inj' : Injective toFun
h : { toFun := toFun, inj' := inj' : α ↪ β }.toFun = g.toFun
mk :
  ∀ (toFun_1 : α → β) (inj'_1 : Injective toFun_1)
    (h : { toFun := toFun, inj' := inj' : α ↪ β }.toFun = { toFun := toFun_1, inj' := inj'_1 }.toFun),
    { toFun := toFun, inj' := inj' : α ↪ β } = { toFun := toFun_1, inj' := inj'_1 }
⊢ { toFun := toFun, inj' := inj' : α ↪ β } = g

Tactic:
cases g
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
toFun : α → β
inj' : Injective toFun
toFun_1 : α → β
inj'_1 : Injective toFun_1
h : { toFun := toFun, inj' := inj' : α ↪ β }.toFun = { toFun := toFun_1, inj' := inj'_1 }.toFun
⊢ { toFun := toFun, inj' := inj' : α ↪ β } = { toFun := toFun_1, inj' := inj'_1 }

Tactic:
congr
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
f g : α ↪ β
h : f.toFun = g.toFun
mk mk₁ :
  ∀ (toFun : α → β) (inj' : Injective toFun) (h : { toFun := toFun, inj' := inj' : α ↪ β }.toFun = g.toFun),
    { toFun := toFun, inj' := inj' : α ↪ β } = g
mk₂ mk₃ :
  ∀ (toFun : α → β) (inj' : Injective toFun) (toFun_1 : α → β) (inj'_1 : Injective toFun_1)
    (h : { toFun := toFun, inj' := inj' : α ↪ β }.toFun = { toFun := toFun_1, inj' := inj'_1 }.toFun),
    { toFun := toFun, inj' := inj' : α ↪ β } = { toFun := toFun_1, inj' := inj'_1 }
⊢ f = g

Tactic:
{ cases f; cases g; congr }
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
⊢ (∃ (f : α → β), Surjective f) ↔ Nonempty (α → β) ∧ Nonempty (β ↪ α)

Tactic:
⟨fun ⟨f, h⟩ ↦ ⟨⟨f⟩, ⟨⟨_, injective_surjInv h⟩⟩⟩, fun ⟨h, ⟨e⟩⟩ ↦ (nonempty_fun.mp h).elim
    (fun _ ↦ ⟨isEmptyElim, (isEmptyElim <| e ·)⟩) fun _ ↦ ⟨_, invFun_surjective e.inj'⟩⟩

Premises used: Function.invFun, isEmptyElim, Exists, Function.Embedding.mk, nonempty_fun, Function.invFun_surjective, Function.Embedding.inj', _private.0.Function.exists_surjective_iff.match_1, Function.surjInv, Nonempty.intro, Function.Embedding, And, And.intro, Iff.intro, Exists.intro, Iff.mp, Nonempty, Function.Embedding.toFun, Or.elim, Function.injective_surjInv, DFunLike.coe, Function.Surjective, _private.0.Function.exists_surjective_iff.match_2
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
f : α ≃ β
⊢ Eq (α := (a : α) → β) (⇑f.toEmbedding : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
f : α ≃ β
a : α
⊢ Eq.{v} (α := β) ((f.toEmbedding : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
x x_1 : α ≃ β
h : x.toEmbedding = x_1.toEmbedding
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : Eq (α := (a : α) → β) (⇑x.toEmbedding : (a : α) → β) (⇑x_1.toEmbedding : (a : α) → β)),
    Eq (α := (a : α) → β) (⇑x : (a : α) → β) (⇑x_1 : (a : α) → β)
⊢ x = x_1

Tactic:
rwa [DFunLike.ext'_iff] at h ⊢

Premises used: DFunLike.ext'_iff
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
⊢ Injective (β := α → β) fun (f : α ↪ β) ↦ (⇑f : (a : α) → β)

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f g : α ↪ β
h : ∀ (x : α), Eq.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : IsEmpty α
a : α ↪ β
h :
  ∀ (v : α),
    Eq.{u_2} (α := β) ((a : (a : α) → β) v : β)
      (({ toFun := fun (a : α) ↦ isEmptyElim (p := fun (x : α) ↦ β) a, inj' := ⋯ } : (a : α) → β) v : β)
⊢ a = { toFun := fun (a : α) ↦ isEmptyElim (p := fun (x : α) ↦ β) a, inj' := ⋯ }

Tactic:
ext v
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : IsEmpty α
a : α ↪ β
v : α
⊢ Eq.{u_2} (α := β) ((a : (a : α) → β) v : β)
    (({ toFun := fun (a : α) ↦ isEmptyElim (p := fun (x : α) ↦ β) a, inj' := ⋯ } : (a : α) → β) v : β)

Tactic:
isEmptyElim v

Premises used: isEmptyElim
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
inst : IsEmpty α
a : α ↪ β
v : α
⊢ Eq.{u_2} (α := β) ((a : (a : α) → β) v : β)
    (({ toFun := fun (a : α) ↦ isEmptyElim (p := fun (x : α) ↦ β) a, inj' := ⋯ } : (a : α) → β) v : β)

Tactic:
exact isEmptyElim v
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α ↪ β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
i : Injective f
⊢ (⇑{ toFun := f, inj' := i : α ↪ β } : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
inj : Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ { toFun := (⇑f : (a : α) → β), inj' := inj : α ↪ β } = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α ↪ β
⊢ Injective.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
EmbeddingLike.injective f

Premises used: EmbeddingLike.injective
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α ↪ β
x y : α
⊢ Eq.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x = y

Tactic:
EmbeddingLike.apply_eq_iff_eq f

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
⊢ Eq.{u_1} (α := (a : α) → α) (⇑(Embedding.refl α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α ↪ β
g : β ↪ γ
⊢ Eq (α := (a : α) → γ) (⇑(f.trans g) : (a : α) → γ)
    (comp.{u_1, u_2, u_3} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
⊢ (Embedding.refl α).trans f = f

Tactic:
rfl

Premises used: Function.Embedding.trans, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
⊢ f.trans (Embedding.refl β) = f

Tactic:
rfl

Premises used: Function.Embedding.trans, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α ↪ β
g : β ↪ γ
h : γ ↪ δ
⊢ (f.trans g).trans h = f.trans (g.trans h)

Tactic:
rfl

Premises used: Function.Embedding.trans, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
⊢ Eq.{max 1 u_1} { toFun := id, inj' := ⋯ } (Embedding.refl α)

Tactic:
rfl

Premises used: Function.Embedding.refl, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : β → γ
hf : Injective f
hg : Injective g
⊢ { toFun := f, inj' := hf : α ↪ β }.trans { toFun := g, inj' := hg : β ↪ γ } = { toFun := g ∘ f, inj' := ⋯ }

Tactic:
rfl

Premises used: Function.Embedding.trans, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ Eq.{max 1 u_1} (e.toEmbedding.trans e.symm.toEmbedding) (Embedding.refl α)

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ Eq.{max 1 u_2} (e.symm.toEmbedding.trans e.toEmbedding) (Embedding.refl β)

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Type u_2
x : α ≃ β
H :
  ∀ (x_1 : α),
    Eq.{u_2 + 1} (α := β)
      (((fun (f : { f : α ↪ β // Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }) ↦
                (↑f : α ↪ β).equivOfSurjective ⋯)
              ((fun (f : α ≃ β) ↦
                  (Subtype.mk (p := fun (f : α ↪ β) ↦ Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β))
                      f.toEmbedding ⋯ :
                    { f : α ↪ β // Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }))
                x) :
            (a : α) → β)
          x_1 :
        β)
      ((x : (a : α) → β) x_1 : β)
⊢ (fun (f : { f : α ↪ β // Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }) ↦
        (↑f : α ↪ β).equivOfSurjective ⋯)
      ((fun (f : α ≃ β) ↦
          (Subtype.mk (p := fun (f : α ↪ β) ↦ Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β))
              f.toEmbedding ⋯ :
            { f : α ↪ β // Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Type u_2
x : α ≃ β
x_1 : α
⊢ Eq.{u_2 + 1} (α := β)
    (((fun (f : { f : α ↪ β // Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }) ↦
              (↑f : α ↪ β).equivOfSurjective ⋯)
            ((fun (f : α ≃ β) ↦
                (Subtype.mk (p := fun (f : α ↪ β) ↦ Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β))
                    f.toEmbedding ⋯ :
                  { f : α ↪ β // Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }))
              x) :
          (a : α) → β)
        x_1 :
      β)
    ((x : (a : α) → β) x_1 : β)

Tactic:
rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst : (a' : α) → Decidable (a' = a)
inst_1 : (a' : α) → Decidable ((f : (a : α) → β) a' = b)
x y : α
h :
  Eq.{u_2} (α := β)
    ((fun (a' : α) ↦
        if a' = a then b else if (f : (a : α) → β) a' = b then (f : (a : α) → β) a else (f : (a : α) → β) a')
      x)
    ((fun (a' : α) ↦
        if a' = a then b else if (f : (a : α) → β) a' = b then (f : (a : α) → β) a else (f : (a : α) → β) a')
      y)
⊢ x = y

Tactic:
grind
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst : (a' : α) → Decidable (a' = a)
inst_1 : (a' : α) → Decidable ((f : (a : α) → β) a' = b)
⊢ (f.setValue a b : (a : α) → β) a = b

Tactic:
simp [setValue]

Premises used: Function.Embedding.setValue
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a a' : α
b : β
inst : (a' : α) → Decidable (a' = a)
inst_1 : (a' : α) → Decidable ((f : (a : α) → β) a' = b)
⊢ (f.setValue a b : (a : α) → β) a' = b ↔ a' = a

Tactic:
(setValue f a b).injective.eq_iff' <| setValue_eq ..

Premises used: Function.Embedding.setValue_eq, Function.Injective.eq_iff', Function.Embedding.setValue, Function.Embedding.injective
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
c : α
inst : (a' : α) → Decidable (a' = a)
inst_1 : (a' : α) → Decidable ((f : (a : α) → β) a' = b)
hc : c ≠ a
hb : (f : (a : α) → β) c ≠ b
⊢ Eq.{u_2} (α := β) ((f.setValue a b : (a : α) → β) c : β) ((f : (a : α) → β) c : β)

Tactic:
simp [setValue, hc, hb]

Premises used: Function.Embedding.setValue
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a c : α
inst : (a' : α) → Decidable (a' = a)
inst_1 : (a' : α) → Decidable (Eq.{u_2} (α := β) ((f : (a : α) → β) a' : β) ((f : (a : α) → β) c : β))
⊢ Eq.{u_2} (α := β) ((f.setValue a ((f : (a : α) → β) c) : (a : α) → β) c : β) ((f : (a : α) → β) a : β)

Tactic:
simp [setValue]

Premises used: Function.Embedding.setValue
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
p : α → Prop
x : Subtype p
⊢ (subtype p : (a : Subtype p) → α) x = (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
p : α → Prop
⊢ Injective.{max 1 u_1, u_1} (α := Subtype p) (β := α) (⇑(subtype p) : (a : Subtype p) → α)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
p : α → Prop
⊢ Eq (α := (self : Subtype p) → α) (⇑(subtype p) : (a : Subtype p) → α) (Subtype.val (p := p))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
inst : Setoid α
⊢ Eq.{u_1} (α := Quotient inst → α) (⇑(quotientOut α) : (a : Quotient inst) → α) Quotient.out

Tactic:
rfl

Premises used: Quot.out, Quotient.out, Quotient, Classical.choose, rfl