awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst : Nonempty γ
h : ∃ (e : β → γ), g = e ∘ f
x x_1 : α
hf : f x = f x_1
rw :
  (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x =
    (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x_1
rw₁ :
  Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x) =
    (Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h ∘ f) x_1
rw₂ :
  Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x) =
    Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x_1)
⊢ g x = g x_1
have rw₃ : Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x_1) =
  Classical.choose (p := fun (x : β → γ) ↦ g = x ∘ f) h (f x_1)
Tactic: rw [Classical.choose_spec h, comp_apply, comp_apply, hf]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : Eq (α := β → γ) ((fun (g : α → γ) ↦ extend f g e') g₁) ((fun (g : α → γ) ↦ extend f g e') g₂)
⊢ g₁ = g₂
have refine : ∀ (x : α), g₁ x = g₂ x
Tactic: refine funext fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : Eq (α := β → γ) ((fun (g : α → γ) ↦ extend f g e') g₁) ((fun (g : α → γ) ↦ extend f g e') g₂)
x : α
⊢ g₁ x = g₂ x
have H : Eq.{u_3} (α := γ) ((fun (g : α → γ) ↦ extend f g e') g₁ (f x)) ((fun (g : α → γ) ↦ extend f g e') g₂ (f x))
Tactic: have H := congr_fun hg (f x)
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f
have refine : ∀ (not_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
Tactic: refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
not_inj : ¬Injective f
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
⊢ c = c'
have not_inj₁ : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1
Tactic: simp only [Injective, not_forall] at not_inj
Cleared hypotheses: not_inj
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1
⊢ c = c'
have have : ∀ (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂), c = c'
Tactic: have ⟨a₁, a₂, eq, ne⟩ := not_inj
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1
a₁ a₂ : α
eq : f a₁ = f a₂
ne : ¬a₁ = a₂
⊢ c = c'
have have : ∀ (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c'), c = c'
Tactic: have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
⊢ c = c'
have h₁ : (fun (g : β → γ) ↦ g ∘ f_1) f a₁ = if a₁ = a₂ then c else c'
Tactic: have h₁ := congr_fun hf a₁
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : (fun (g : β → γ) ↦ g ∘ f_1) f a₁ = if a₁ = a₂ then c else c'
⊢ c = c'
have h₂ : (fun (g : β → γ) ↦ g ∘ f_1) f a₂ = if a₂ = a₂ then c else c'
Tactic: have h₂ := congr_fun hf a₂
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : (fun (g : β → γ) ↦ g ∘ f_1) f a₁ = if a₁ = a₂ then c else c'
h₂ : (fun (g : β → γ) ↦ g ∘ f_1) f a₂ = if a₂ = a₂ then c else c'
⊢ c = c'
have h₃ : f (f_1 a₁) = c'
Tactic: simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (hypothesis)
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : (fun (g : β → γ) ↦ g ∘ f_1) f a₁ = if a₁ = a₂ then c else c'
h₂ : (fun (g : β → γ) ↦ g ∘ f_1) f a₂ = if a₂ = a₂ then c else c'
h₃ : f (f_1 a₁) = c'
⊢ c = c'
have h₄ : f (f_1 a₂) = c
Tactic: simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : f (f_1 a₁) = c'
h₂ : f (f_1 a₂) = c
⊢ c = c'
have rw : c = f (f_1 a₁)
Tactic: rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : f (f_1 a₁) = c'
h₂ : f (f_1 a₂) = c
rw : c = f (f_1 a₁)
⊢ c = c'
have rw₁ : c = f (f_1 a₂)
Tactic: rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f_1 : α → β
γ : Type u_4
inst : Nontrivial γ
surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f_1
c c' : γ
not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f_1 x = f_1 x_1), ¬x = x_1
a₁ a₂ : α
eq : f_1 a₁ = f_1 a₂
ne : ¬a₁ = a₂
f : β → γ
hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f_1) f) fun (x : α) ↦ if x = a₂ then c else c'
h₁ : f (f_1 a₁) = c'
h₂ : f (f_1 a₂) = c
rw : c = f (f_1 a₁)
rw₁ : c = f (f_1 a₂)
⊢ c = c'
have rw₂ : c = c
Tactic: rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f
have refine : ∀ (not_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
Tactic: classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
refine : ∀ (not_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f
have refine₁ : ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
  (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1), c = c'
Tactic: classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
refine : ∀ (not_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
refine₁ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1), c = c'
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f
have refine₂ : ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
  (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂),
  c = c'
Tactic: classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
refine : ∀ (not_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
refine₁ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1), c = c'
refine₂ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂),
    c = c'
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f
have refine₃ : ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
  (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
  (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c'), c = c'
Tactic: classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
refine : ∀ (not_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
refine₁ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1), c = c'
refine₂ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂),
    c = c'
refine₃ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c'), c = c'
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f
have refine₄ : ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
  (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
  (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c')
  (h₁ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₁ = if a₁ = a₂ then c else c'), c = c'
Tactic: classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
refine : ∀ (not_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
refine₁ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1), c = c'
refine₂ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂),
    c = c'
refine₃ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c'), c = c'
refine₄ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c')
    (h₁ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₁ = if a₁ = a₂ then c else c'), c = c'
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f
have refine₅ : ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
  (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
  (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c')
  (h₁ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₁ = if a₁ = a₂ then c else c')
  (h₂ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₂ = if a₂ = a₂ then c else c'), c = c'
Tactic: classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst : Nontrivial γ
refine : ∀ (not_inj : ¬Injective f) (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ), c = c'
refine₁ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1), c = c'
refine₂ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂),
    c = c'
refine₃ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c'), c = c'
refine₄ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c')
    (h₁ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₁ = if a₁ = a₂ then c else c'), c = c'
refine₅ :
  ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
    (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
    (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c')
    (h₁ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₁ = if a₁ = a₂ then c else c')
    (h₂ : (fun (g : β → γ) ↦ g ∘ f) f_1 a₂ = if a₂ = a₂ then c else c'), c = c'
⊢ (Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) ↔ Injective f
have refine₆ : ∀ (surj : Surjective (β := α → γ) fun (g : β → γ) ↦ g ∘ f) (c c' : γ)
  (not_inj : ∃ (x : α), ∃ (x_1 : α), ∃ (x_2 : f x = f x_1), ¬x = x_1) (a₁ a₂ : α) (eq : f a₁ = f a₂) (ne : ¬a₁ = a₂)
  (f_1 : β → γ) (hf : Eq (α := α → γ) ((fun (g : β → γ) ↦ g ∘ f) f_1) fun (x : α) ↦ if x = a₂ then c else c')
  (h₁ : f_1 (f a₁) = c') (h₂ : f_1 (f a₂) = c), c = c'
Tactic: classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
⊢ curry (update (β := fun (a : α × α') ↦ β) f aa' b) =
    update (β := fun (a : α) ↦ α' → β) (curry f) aa'.fst (update (β := fun (a : α') ↦ β) (curry f aa'.fst) aa'.snd b)
have h : ∀ (a : α) (a' : α'),
  curry (update (β := fun (a : α × α') ↦ β) f aa' b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) aa'.fst (update (β := fun (a : α') ↦ β) (curry f aa'.fst) aa'.snd b) a
      a'
Tactic: ext a a'
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
⊢ curry (update (β := fun (a : α × α') ↦ β) f aa' b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) aa'.fst (update (β := fun (a : α') ↦ β) (curry f aa'.fst) aa'.snd b) a
      a'
have h : ∀ (a₂ : α) (a₂' : α'),
  curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
Tactic: let ⟨a₂, a₂'⟩ := aa'
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
have h : curry (update (β := fun (a : α × α') ↦ β) f (a, a₂') b) a a' =
  update (β := fun (a : α) ↦ α' → β) (curry f) (a, a₂').fst
    (update (β := fun (a : α') ↦ β) (curry f (a, a₂').fst) (a, a₂').snd b) a a'
Tactic: obtain rfl | ha := eq_or_ne a a₂
Cleared hypotheses: a₂
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
h :
  curry (update (β := fun (a : α × α') ↦ β) f (a, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a₂').fst) (a, a₂').snd b) a a'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
have h₁ : ∀ (ha : a ≠ a₂),
  curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
Tactic: obtain rfl | ha := eq_or_ne a a₂
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a₂').fst) (a, a₂').snd b) a a'
have h : curry (update (β := fun (a : α × α') ↦ β) f (a, a') b) a a' =
  update (β := fun (a : α) ↦ α' → β) (curry f) (a, a').fst
    (update (β := fun (a : α') ↦ β) (curry f (a, a').fst) (a, a').snd b) a a'
Tactic: obtain rfl | ha' := eq_or_ne a' a₂'
Cleared hypotheses: a₂'
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
h :
  curry (update (β := fun (a : α × α') ↦ β) f (a, a') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a').fst) (a, a').snd b) a a'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a₂').fst) (a, a₂').snd b) a a'
have h₁ : ∀ (ha' : a' ≠ a₂'),
  curry (update (β := fun (a : α × α') ↦ β) f (a, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a, a₂').fst) (a, a₂').snd b) a a'
Tactic: obtain rfl | ha' := eq_or_ne a' a₂'
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
have h : curry (update (β := fun (a : α × α') ↦ β) f (a₂, a') b) a a' =
  update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a').fst
    (update (β := fun (a : α') ↦ β) (curry f (a₂, a').fst) (a₂, a').snd b) a a'
Tactic: obtain rfl | ha' := eq_or_ne a' a₂'
Cleared hypotheses: a₂'
-- Lean 4 proof step from Mathlib.Logic.Function.Basic (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
h :
  curry (update (β := fun (a : α × α') ↦ β) f (a₂, a') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a').fst) (a₂, a').snd b) a a'
⊢ curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
have h₁ : ∀ (ha' : a' ≠ a₂'),
  curry (update (β := fun (a : α × α') ↦ β) f (a₂, a₂') b) a a' =
    update (β := fun (a : α) ↦ α' → β) (curry f) (a₂, a₂').fst
      (update (β := fun (a : α') ↦ β) (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
Tactic: obtain rfl | ha' := eq_or_ne a' a₂'