-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem smul_diff_smul' [hH : Normal H] (g : Gᵐᵒᵖ) :
    diff (MonoidHom.id H) (g • α) (g • β) =
      ⟨g.unop⁻¹ * (diff (MonoidHom.id H) α β : H) * g.unop,
        hH.mem_comm ((congr_arg (· ∈ H) (mul_inv_cancel_left _ _)).mpr (SetLike.coe_mem _))⟩

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : H.IsCommutative
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H := { toFun := fun h => ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) = ⟨(unop g)⁻¹ * ↑(diff (MonoidHom.id ↥H) α β) * unop g, ⋯⟩

Tactic:
refine (Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun x ↦ ?_).trans (map_prod ϕ _ _).symm

Result:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : H.IsCommutative
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H := { toFun := fun h => ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
x : G ⧸ H
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv x))⁻¹ * ↑(⋯.leftQuotientEquiv x), ⋯⟩ =
    ϕ
      ((MonoidHom.id ↥H)
        ⟨(↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x)))⁻¹ * ↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x)),
          ⋯⟩)

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : H.IsCommutative
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H := { toFun := fun h => ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
x : G ⧸ H
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv x))⁻¹ * ↑(⋯.leftQuotientEquiv x), ⋯⟩ =
    ϕ
      ((MonoidHom.id ↥H)
        ⟨(↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x)))⁻¹ * ↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x)),
          ⋯⟩)

Tactic:
simp only [ϕ, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, mul_inv_rev, mul_assoc,
  MonoidHom.id_apply, toPerm_symm_apply, MonoidHom.coe_mk, OneHom.coe_mk]

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : H.IsCommutative
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) = ⟨(unop g)⁻¹ * ↑(diff (MonoidHom.id ↥H) α β) * unop g, ⋯⟩

Tactic:
letI := H.fintypeQuotientOfFiniteIndex

Result:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : H.IsCommutative
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) = ⟨(unop g)⁻¹ * ↑(diff (MonoidHom.id ↥H) α β) * unop g, ⋯⟩

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : H.IsCommutative
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
h₁ h₂ : ↥H
⊢ { toFun := fun h => ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯ }.toFun (h₁ * h₂) =
    { toFun := fun h => ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯ }.toFun h₁ *
      { toFun := fun h => ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯ }.toFun h₂

Tactic:
simp only [Subtype.ext_iff, coe_mk, coe_mul, mul_assoc, mul_inv_cancel_left]

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : H.IsCommutative
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ (fun h => ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩) 1 = 1

Tactic:
rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]

Result:
no goals