-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem agree : f.hom.range = { x | h x = g x }

Proof state:
case refine_1
A B : Grp
f : A ⟶ B
b : ↑B
⊢ b ∈ ↑(Hom.hom f).range → b ∈ {x | h x = g x}

Tactic:
rintro ⟨a, rfl⟩

Result:
case refine_1.intro
A B : Grp
f : A ⟶ B
a : ↑A
⊢ (Hom.hom f) a ∈ {x | h x = g x}

Proof state:
case refine_2
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
⊢ False

Tactic:
have eq1 : (h b) (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) =
    fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ := by
  change ((τ).symm.trans (g b)).trans τ _ = _
  dsimp [tau]
  simp [g_apply_infinity f]

Result:
case refine_2
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
⊢ False

Proof state:
case pos
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨(ConcreteCategory.hom f) a • y • ↑(Hom.hom f).range, ⋯⟩

Tactic:
simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m), smul_smul]

Result:
no goals

Proof state:
case refine_1.intro.H.infinity
A B : Grp
f : A ⟶ B
a : ↑A
⊢ (h ((ConcreteCategory.hom f) a)) ∞ = (g ((ConcreteCategory.hom f) a)) ∞

Tactic:
rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]

Result:
no goals

Proof state:
case refine_2
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
eq2 : (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩
⊢ False

Tactic:
exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, DFunLike.congr_fun hb])

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩) ∞)
      ((g b) ((Equiv.swap (fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩) ∞) (fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩))) =
    fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩

Tactic:
simp [g_apply_infinity f]

Result:
no goals

Proof state:
case refine_1.intro
A B : Grp
f : A ⟶ B
a : ↑A
⊢ (Hom.hom f) a ∈ {x | h x = g x}

Tactic:
change h (f a) = g (f a)

Result:
case refine_1.intro
A B : Grp
f : A ⟶ B
a : ↑A
⊢ h ((ConcreteCategory.hom f) a) = g ((ConcreteCategory.hom f) a)

Proof state:
case neg
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∉ (Hom.hom f).range
⊢ fromCoset ⟨((ConcreteCategory.hom f) a * y) • ↑(Hom.hom f).range, ⋯⟩ =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
simp only [leftCoset_assoc]

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
⊢ (((Equiv.symm τ).trans (g b)).trans τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
dsimp [tau]

Result:
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩) ∞)
      ((g b) ((Equiv.swap (fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩) ∞) (fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩))) =
    fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
⊢ (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
change ((τ).symm.trans (g b)).trans τ _ = _

Result:
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
⊢ (((Equiv.symm τ).trans (g b)).trans τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Proof state:
case refine_1.intro.H.fromCoset.mk.intro
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
by_cases m : y ∈ f.hom.range

Result:
case pos
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

case neg
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∉ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Proof state:
case pos
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩ =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
change fromCoset _ = fromCoset ⟨f a • (y • _), _⟩

Result:
case pos
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨(ConcreteCategory.hom f) a • y • ↑(Hom.hom f).range, ⋯⟩

Proof state:
case refine_2
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
⊢ False

Tactic:
have eq2 :
    g b (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ :=
  rfl

Result:
case refine_2
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
eq2 : (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩
⊢ False

Proof state:
case neg
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∉ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]

Result:
case neg
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∉ (Hom.hom f).range
⊢ fromCoset ⟨((ConcreteCategory.hom f) a * y) • ↑(Hom.hom f).range, ⋯⟩ =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
eq2 : (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩
⊢ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩

Tactic:
rw [← eq1, ← eq2, DFunLike.congr_fun hb]

Result:
no goals

Proof state:
case refine_1.intro.H.fromCoset.mk.intro
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩) =
    (g ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩)

Tactic:
rw [g_apply_fromCoset]

Result:
case refine_1.intro.H.fromCoset.mk.intro
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Proof state:
case refine_1.intro
A B : Grp
f : A ⟶ B
a : ↑A
⊢ h ((ConcreteCategory.hom f) a) = g ((ConcreteCategory.hom f) a)

Tactic:
ext ⟨⟨_, ⟨y, rfl⟩⟩⟩

Result:
case refine_1.intro.H.fromCoset.mk.intro
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩) =
    (g ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩)

case refine_1.intro.H.infinity
A B : Grp
f : A ⟶ B
a : ↑A
⊢ (h ((ConcreteCategory.hom f) a)) ∞ = (g ((ConcreteCategory.hom f) a)) ∞