-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem smul_diff' (h : H) :
    diff (MonoidHom.id H) α (op (h : G) • β) = diff (MonoidHom.id H) α β * h ^ H.index

Proof state:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ ↑(⋯.leftQuotientEquiv q) = ↑(⋯.leftQuotientEquiv q) * ↑h

Tactic:
rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, MulOpposite.unop_op, mul_left_inj,
  ← Subtype.ext_iff, Equiv.apply_eq_iff_eq, inv_smul_eq_iff]

Result:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ q = op ↑h • q

Proof state:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ * h

Tactic:
simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, mul_assoc, mul_right_inj]

Result:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ ↑(⋯.leftQuotientEquiv q) = ↑(⋯.leftQuotientEquiv q) * ↑h

Proof state:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ ∏ q : G ⧸ H, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    ∏ x : G ⧸ H, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv x))⁻¹ * ↑(⋯.leftQuotientEquiv x), ⋯⟩ * h

Tactic:
refine Finset.prod_congr rfl fun q _ => ?_

Result:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ * h

Proof state:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ q = op ↑h • q

Tactic:
exact self_eq_mul_right.mpr ((QuotientGroup.eq_one_iff _).mpr h.2)

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ diff (MonoidHom.id ↥H) α (op ↑h • β) = diff (MonoidHom.id ↥H) α β * h ^ H.index

Tactic:
rw [diff, diff, index_eq_card, Nat.card_eq_fintype_card,
    ← Finset.card_univ, ← Finset.prod_const, ← Finset.prod_mul_distrib]

Result:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ ∏ q : G ⧸ H, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    ∏ x : G ⧸ H, (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv x))⁻¹ * ↑(⋯.leftQuotientEquiv x), ⋯⟩ * h

Proof state:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
⊢ diff (MonoidHom.id ↥H) α (op ↑h • β) = diff (MonoidHom.id ↥H) α β * h ^ H.index

Tactic:
letI := H.fintypeQuotientOfFiniteIndex

Result:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
⊢ diff (MonoidHom.id ↥H) α (op ↑h • β) = diff (MonoidHom.id ↥H) α β * h ^ H.index