-- Mathlib/Logic/Function/Basic.lean
theorem surjective_comp_right_iff_injective {γ : Type*} [Nontrivial γ] :
    Surjective (fun g : β → γ ↦ g ∘ f) ↔ Injective f

Proof state:
α : 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, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g => g ∘ f✝) f = fun x => if x = a₂ then c else c'
h₁ : (fun g => g ∘ f✝) f a₁ = if a₁ = a₂ then c else c'
h₂ : (fun g => g ∘ f✝) f a₂ = if a₂ = a₂ then c else c'
⊢ c = c'

Tactic:
simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂

Result:
α : 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, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g => g ∘ f✝) f = fun x => if x = a₂ then c else c'
h₁ : f (f✝ a₁) = c'
h₂ : f (f✝ a₂) = c
⊢ c = c'

Proof state:
α : 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, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g => g ∘ f✝) f = fun x => if x = a₂ then c else c'
h₁ : (fun g => g ∘ f✝) f a₁ = if a₁ = a₂ then c else c'
⊢ c = c'

Tactic:
have h₂ := congr_fun hf a₂

Result:
α : 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, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g => g ∘ f✝) f = fun x => if x = a₂ then c else c'
h₁ : (fun g => g ∘ f✝) f a₁ = if a₁ = a₂ then c else c'
h₂ : (fun g => g ∘ f✝) f a₂ = if a₂ = a₂ then c else c'
⊢ c = c'

Proof state:
α : 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'

Tactic:
simp only [Injective, not_forall] at not_inj

Result:
α : 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, ¬x = x_1
⊢ c = c'

Proof state:
α : 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, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g => g ∘ f✝) f = fun x => if x = a₂ then c else c'
⊢ c = c'

Tactic:
have h₁ := congr_fun hf a₁

Result:
α : 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, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g => g ∘ f✝) f = fun x => if x = a₂ then c else c'
h₁ : (fun g => g ∘ f✝) f a₁ = if a₁ = a₂ then c else c'
⊢ c = c'

Proof state:
α : 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, ¬x = x_1
a₁ a₂ : α
eq : f✝ a₁ = f✝ a₂
ne : ¬a₁ = a₂
f : β → γ
hf : (fun g => g ∘ f✝) f = fun x => if x = a₂ then c else c'
h₁ : f (f✝ a₁) = c'
h₂ : f (f✝ a₂) = c
⊢ c = c'

Tactic:
rw [← h₁, eq, h₂]

Result:
no goals

Proof state:
α : 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, ¬x = x_1
⊢ c = c'

Tactic:
have ⟨a₁, a₂, eq, ne⟩ := not_inj

Result:
α : 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, ¬x = x_1
a₁ a₂ : α
eq : f a₁ = f a₂
ne : ¬a₁ = a₂
⊢ c = c'