A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
r : ¬Function.Surjective ↑f
⊢ False
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
⊢ Function.Surjective ↑f
by_contra r
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
r : ¬∀ (b : ↑B), ∃ a, ↑f a = b
⊢ False
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
r : ¬Function.Surjective ↑f
⊢ False
dsimp [Function.Surjective] at r
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
r : ∃ b, ∀ (a : ↑A), ↑f a ≠ b
⊢ False
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
r : ¬∀ (b : ↑B), ∃ a, ↑f a = b
⊢ False
push_neg at r
case intro
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
b : ↑B
hb : ∀ (a : ↑A), ↑f a ≠ b
⊢ False
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
r : ∃ b, ∀ (a : ↑A), ↑f a ≠ b
⊢ False
rcases r with ⟨b, hb⟩
no goals
case intro
A B : GroupCat
f : A ⟶ B
inst✝ : Epi f
b : ↑B
hb : ∀ (a : ↑A), ↑f a ≠ b
⊢ False
exact
  SurjectiveOfEpiAuxs.g_ne_h f b (fun ⟨c, hc⟩ => hb _ hc)
    ((cancel_epi f).1 (SurjectiveOfEpiAuxs.comp_eq f))