awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Denumerable (hypothesis)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
m : (↑s : Type)
hmax : t.maximum = (↑m : WithBot (↑s : Type))
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
have wf : (↑m : ℕ) < x
Tactic: have wf : ↑m < x := by simpa using hmt.mp (List.maximum_mem hmax)
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
m : (↑s : Type)
hmax : t.maximum = (↑m : WithBot (↑s : Type))
wf : (↑m : ℕ) < x
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
have coe : ∀ (a : ℕ) (hmax : t.maximum = (↑(ofNat s a) : WithBot (↑s : Type))) (wf : (↑(ofNat s a) : ℕ) < x),
  ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
Tactic: rcases ofNat_surjective m with ⟨a, rfl⟩
Cleared hypotheses: m, hmax, wf
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
a : ℕ
hmax : t.maximum = (↑(ofNat s a) : WithBot (↑s : Type))
wf : (↑(ofNat s a) : ℕ) < x
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
have coe : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx ≤ ofNat s (a + 1)
Tactic: refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
have cases : ∀ (x_1 : WithBot (↑s : Type)) (hmax : t.maximum = x_1),
  ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
Tactic: cases hmax : List.maximum t with
    | bot =>
      refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (a := (⊥ : s)) ?_)⟩
      rwa [← List.maximum_eq_bot.1 hmax, hmt]
    | coe m =>
      have wf : ↑m < x := by simpa using hmt.mp (List.maximum_mem hmax)
      rcases ofNat_surjective m with ⟨a, rfl⟩
      refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩
      exact le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
⊢ Set.range (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) ∘ ofNat s) = s
have rw : Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) '' Set.range (ofNat s) = s
Tactic: rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
rw : Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) '' Set.range (ofNat s) = s
⊢ Set.range (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) ∘ ofNat s) = s
have rw₁ : Set.image (α := { x : ℕ // x ∈ s }) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s)) Set.univ = s
Tactic: rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
rw : Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) '' Set.range (ofNat s) = s
rw₁ : Set.image (α := { x : ℕ // x ∈ s }) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s)) Set.univ = s
⊢ Set.range (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) ∘ ofNat s) = s
have rw₂ : Set.range (ι := { x : ℕ // x ∈ s }) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s)) = s
Tactic: rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
rw : Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) '' Set.range (ofNat s) = s
rw₁ : Set.image (α := { x : ℕ // x ∈ s }) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s)) Set.univ = s
rw₂ : Set.range (ι := { x : ℕ // x ∈ s }) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s)) = s
⊢ Set.range (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) ∘ ofNat s) = s
have rw₃ : s = s
Tactic: rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : (↑s : Type)
⊢ toFunAux (s := s) x = #({y ∈ range (↑x : ℕ) | y ∈ s})
have rw : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (List.range (↑x : ℕ))).length = #({y ∈ range (↑x : ℕ) | y ∈ s})
Tactic: rw [toFunAux, List.countP_eq_length_filter]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
⊢ toFunAux (s := s) (ofNat s 0) = 0
have rw : ∀ (x : ℕ), x ∉ {y ∈ range (↑(ofNat s 0) : ℕ) | y ∈ s}
Tactic: rw [toFunAux_eq, card_eq_zero, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (hypothesis)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
hn : n ∈ {y ∈ range (↑(ofNat s 0) : ℕ) | y ∈ s}
⊢ False
have hn₁ : n < (↑⊥ : ℕ) ∧ n ∈ s
Tactic: rw [mem_filter, ofNat, mem_range] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Logic.Denumerable (hypothesis)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
⊢ toFunAux (s := s) (ofNat s (n + 1)) = n + 1
have ih : toFunAux (s := s) (ofNat s n) = n
Tactic: have ih : toFunAux (ofNat s n) = n := right_inverse_aux n
-- Lean 4 proof step from Mathlib.Logic.Denumerable (hypothesis)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
ih : toFunAux (s := s) (ofNat s n) = n
⊢ toFunAux (s := s) (ofNat s (n + 1)) = n + 1
have h₁ : (↑(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
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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})
have simp : ∀ (a : ℕ), a < (↑(succ (s := s) (ofNat s n)) : ℕ) ∧ a ∈ s ↔ a = (↑(ofNat s n) : ℕ) ∨ a < (↑(ofNat s n) : ℕ) ∧ a ∈ s
Tactic: simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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) : ℕ) ∧ m ∈ s
have simp : m = (↑(ofNat s n) : ℕ) ∨ m < (↑(ofNat s n) : ℕ)
Tactic: simp only [h.2, and_true]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (hypothesis)
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}
⊢ toFunAux (s := s) (ofNat s (n + 1)) = n + 1
have h₂ : {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⟩⟩
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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})
⊢ toFunAux (s := s) (ofNat s (n + 1)) = n + 1
have simp : ∀ (ih : #({y ∈ range (↑(ofNat s n) : ℕ) | y ∈ s}) = n),
  #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1
Tactic: simp only [toFunAux_eq, ofNat] at ih ⊢
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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
| #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1
have rhs : n + 1
Tactic: rhs
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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
| n + 1
have rw : #({x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s})
Tactic: rw [← ih, ← card_insert_of_notMem h₁, ← h₂]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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
| #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1
have rw : #({x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s})
Tactic: rhs
      rw [← ih, ← card_insert_of_notMem h₁, ← h₂]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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
⊢ #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1
have conv : #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1
Tactic: conv =>
      rhs
      rw [← ih, ← card_insert_of_notMem h₁, ← h₂]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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
⊢ #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = n + 1
have conv₁ : #({y ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | y ∈ s}) = #({x ∈ range (↑(succ (s := s) (ofNat s n)) : ℕ) | x ∈ s})
Tactic: conv =>
      rhs
      rw [← ih, ← card_insert_of_notMem h₁, ← h₂]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Countable α
inst_1 : Infinite α
inst_2 : Countable β
inst_3 : Infinite β
⊢ Nonempty (α ≃ β)
have intro : ∀ (val : Denumerable α), Nonempty (α ≃ β)
Tactic: cases nonempty_denumerable α
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Countable α
inst_1 : Infinite α
inst_2 : Countable β
inst_3 : Infinite β
val : Denumerable α
⊢ Nonempty (α ≃ β)
have intro : ∀ (val : Denumerable β), Nonempty (α ≃ β)
Tactic: cases nonempty_denumerable β
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Sort u
β : Sort v
f g : α ↪ β
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : α → β) (inj' : Injective toFun) (h : { toFun := toFun, inj' := inj' : α ↪ β }.toFun = g.toFun),
  { toFun := toFun, inj' := inj' : α ↪ β } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Sort u
β : Sort v
g : α ↪ β
toFun : α → β
inj' : Injective toFun
h : { toFun := toFun, inj' := inj' : α ↪ β }.toFun = g.toFun
⊢ { toFun := toFun, inj' := inj' : α ↪ β } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Sort u
β : Sort v
f g : α ↪ β
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : α → β) (inj' : Injective toFun) (h : { toFun := toFun, inj' := inj' : α ↪ β }.toFun = g.toFun),
  { toFun := toFun, inj' := inj' : α ↪ β } = g
Tactic: { cases f; cases g; congr }
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
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
⊢ f = g
have 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 }
Tactic: { cases f; cases g; congr }
Cleared hypotheses: f, g, h
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Sort u
β : Sort v
x x_1 : α ≃ β
h : x.toEmbedding = x_1.toEmbedding
⊢ x = x_1
have rwa : ∀ (h : Eq (α := (a : α) → β) (⇑x.toEmbedding : (a : α) → β) (⇑x_1.toEmbedding : (a : α) → β)),
  Eq (α := (a : α) → β) (⇑x : (a : α) → β) (⇑x_1 : (a : α) → β)
Tactic: rwa [DFunLike.ext'_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
inst : IsEmpty α
a : α ↪ β
⊢ a = { toFun := fun (a : α) ↦ isEmptyElim (p := fun (x : α) ↦ β) a, inj' := ⋯ }
have h : ∀ (v : α),
  Eq.{u_2} (α := β) ((a : (a : α) → β) v : β)
    (({ toFun := fun (a : α) ↦ isEmptyElim (p := fun (x : α) ↦ β) a, inj' := sorry } : (a : α) → β) v : β)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Sort u_1
β : Type u_2
x : α ≃ β
⊢ (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
have H : ∀ (x_1 : α),
  Eq.{u_2 + 1} (α := β)
    (((fun (f : { f : α ↪ β // Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }) ↦
              (↑f : α ↪ β).equivOfSurjective sorry)
            ((fun (f : α ≃ β) ↦
                (Subtype.mk (p := fun (f : α ↪ β) ↦ Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β))
                    f.toEmbedding sorry :
                  { f : α ↪ β // Surjective.{u_1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }))
              x) :
          (a : α) → β)
        x_1 :
      β)
    ((x : (a : α) → β) x_1 : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
one : Type u_1
α : Type u_2
inst : Unique one
f : one ↪ α
⊢ (fun (a : α) ↦ ({ toFun := fun (x : one) ↦ a, inj' := ⋯ } : one ↪ α))
      ((fun (f : one ↪ α) ↦ ((f : (a : one) → α) default : α)) f) =
    f
have h : ∀ (x : one),
  Eq.{u_2 + 1} (α := α)
    (((fun (a : α) ↦ ({ toFun := fun (x : one) ↦ a, inj' := sorry } : one ↪ α))
            ((fun (f : one ↪ α) ↦ ((f : (a : one) → α) default : α)) f) :
          (a : one) → α)
        x :
      α)
    ((f : (a : one) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Sort u
γ : Sort w
inst : Inhabited γ
⊢ Eq (α := (α → γ) ↪ α → γ) (Embedding.refl α).arrowCongrLeft (Embedding.refl (α → γ))
have h : ∀ (x : α → γ) (x_1 : α),
  Eq.{w} (α := γ) (((Embedding.refl α).arrowCongrLeft : (a : α → γ) → α → γ) x x_1 : γ)
    ((Embedding.refl (α → γ) : (a : α → γ) → α → γ) x x_1 : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
⊢ Eq (α := (α₁ → γ) ↪ α₃ → γ) (Embedding.trans e₁₂.arrowCongrLeft e₂₃.arrowCongrLeft) (e₁₂.trans e₂₃).arrowCongrLeft
have h : ∀ (f : α₁ → γ) (a : α₃),
  Eq.{w} (α := γ) ((Embedding.trans e₁₂.arrowCongrLeft e₂₃.arrowCongrLeft : (a : α₁ → γ) → α₃ → γ) f a : γ)
    (((e₁₂.trans e₂₃).arrowCongrLeft : (a : α₁ → γ) → α₃ → γ) f a : γ)
Tactic: ext f a
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ Eq.{w} (α := γ) ((Embedding.trans e₁₂.arrowCongrLeft e₂₃.arrowCongrLeft : (a : α₁ → γ) → α₃ → γ) f a : γ)
    (((e₁₂.trans e₂₃).arrowCongrLeft : (a : α₁ → γ) → α₃ → γ) f a : γ)
have h : extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
    (fun (a : α₃) ↦ default) a =
  extend (comp.{u, v, x} (β := α₂) (⇑e₂₃ : (a : α₂) → α₃) (⇑e₁₂ : (a : α₁) → α₂)) f (fun (a : α₃) ↦ default) a
Tactic: simp only [trans_apply, arrowCongrLeft_apply, Pi.default_def, coe_trans]
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
      (fun (a : α₃) ↦ default) a =
    extend (comp.{u, v, x} (β := α₂) (⇑e₂₃ : (a : α₂) → α₃) (⇑e₁₂ : (a : α₁) → α₂)) f (fun (a : α₃) ↦ default) a
have h : extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
    (fun (a : α₃) ↦ default) a =
  extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃)
    (extend (⇑e₁₂ : (a : α₁) → α₂) f ((fun (a : α₃) ↦ default) ∘ (⇑e₂₃ : (a : α₂) → α₃))) (fun (a : α₃) ↦ default) a
Tactic: rw [e₁₂.injective.extend_comp e₂₃.injective, Function.comp_def]
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
h :
  extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
      (fun (a : α₃) ↦ default) a =
    extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃)
      (extend (⇑e₁₂ : (a : α₁) → α₂) f ((fun (a : α₃) ↦ default) ∘ (⇑e₂₃ : (a : α₂) → α₃))) (fun (a : α₃) ↦ default) a
⊢ extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
      (fun (a : α₃) ↦ default) a =
    extend (comp.{u, v, x} (β := α₂) (⇑e₂₃ : (a : α₂) → α₃) (⇑e₁₂ : (a : α₁) → α₂)) f (fun (a : α₃) ↦ default) a
have h₁ : extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
    (fun (a : α₃) ↦ default) a =
  extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (x : α₂) ↦ default)
    (fun (a : α₃) ↦ default) a
Tactic: rw [e₁₂.injective.extend_comp e₂₃.injective, Function.comp_def]
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
⊢ (fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) ((fun (f : α ↪ γ) ↦ Embedding.congr h h' f) x) = x
have h₁ : ∀ (x_1 : α),
  Eq.{u_3} (α := γ)
    (((fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) ((fun (f : α ↪ γ) ↦ Embedding.congr h h' f) x) : (a : α) → γ)
        x_1 :
      γ)
    ((x : (a : α) → γ) x_1 : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
⊢ (fun (f : α ↪ γ) ↦ Embedding.congr h h' f) ((fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) x) = x
have h₁ : ∀ (x_1 : β),
  Eq.{u_4} (α := δ)
    (((fun (f : α ↪ γ) ↦ Embedding.congr h h' f) ((fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) x) : (a : β) → δ)
        x_1 :
      δ)
    ((x : (a : β) → δ) x_1 : δ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
⊢ Eq (α := α₂ ↪ γ₂) ((ea.embeddingCongr ec : (a : α₁ ↪ γ₁) → α₂ ↪ γ₂) (f.trans g) : α₂ ↪ γ₂)
    (Embedding.trans.{u_4, u_5, u_6} (β := β₂) ((ea.embeddingCongr eb : (a : α₁ ↪ β₁) → α₂ ↪ β₂) f)
        ((eb.embeddingCongr ec : (a : β₁ ↪ γ₁) → β₂ ↪ γ₂) g) :
      α₂ ↪ γ₂)
have h : ∀ (x : α₂),
  Eq.{u_6} (α := γ₂) ((((ea.embeddingCongr ec : (a : α₁ ↪ γ₁) → α₂ ↪ γ₂) (f.trans g) : α₂ ↪ γ₂) : (a : α₂) → γ₂) x : γ₂)
    ((Embedding.trans.{u_4, u_5, u_6} (β := β₂) ((ea.embeddingCongr eb : (a : α₁ ↪ β₁) → α₂ ↪ β₂) f)
            ((eb.embeddingCongr ec : (a : β₁ ↪ γ₁) → β₂ ↪ γ₂) g) :
          (a : α₂) → γ₂)
        x :
      γ₂)
Tactic: ext