-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem h_apply_fromCoset_nin_range (x : B) (hx : x ∈ f.hom.range) (b : B) (hb : b ∉ f.hom.range) :
    h x (fromCoset ⟨b • f.hom.range, b, rfl⟩) = fromCoset ⟨(x * b) • ↑f.hom.range, x * b, rfl⟩

Proof state:
case h.e'_5
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
r : x * b ∈ (Hom.hom f).range
⊢ b = x⁻¹ * (x * b)

Tactic:
rw [← mul_assoc, inv_mul_cancel, one_mul]

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩ ≠ ∞

Tactic:
simp

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ (h x) (fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩

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

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

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

Tactic:
simp only [tau, MonoidHom.coe_mk, Equiv.toFun_as_coe, Equiv.coe_trans, Function.comp_apply]

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞)
      ((g x)
        ((Equiv.symm (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞)) (fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩))) =
    fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞) ((g x) (fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩)) =
    fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩

Tactic:
simp only [g_apply_fromCoset, leftCoset_assoc]

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞) (fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩) =
    fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞) (fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩) =
    fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩

Tactic:
refine Equiv.swap_apply_of_ne_of_ne (fromCoset_ne_of_nin_range _ fun r => hb ?_) (by simp)

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
r : x * b ∈ (Hom.hom f).range
⊢ b ∈ (Hom.hom f).range

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ ≠ ∞

Tactic:
simp

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
r : x * b ∈ (Hom.hom f).range
⊢ b ∈ (Hom.hom f).range

Tactic:
convert Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r

Result:
case h.e'_5
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
r : x * b ∈ (Hom.hom f).range
⊢ b = x⁻¹ * (x * b)

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞)
      ((g x)
        ((Equiv.symm (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞)) (fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩))) =
    fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩

Tactic:
rw [Equiv.symm_swap,
  @Equiv.swap_apply_of_ne_of_ne X' _ (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) ∞
    (fromCoset ⟨b • ↑f.hom.range, b, rfl⟩) (fromCoset_ne_of_nin_range _ hb) (by simp)]

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ (Equiv.swap (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) ∞) ((g x) (fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩)) =
    fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩