G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ diff (MonoidHom.id { x // x ∈ H }) α (op ↑h • β) = diff (MonoidHom.id { x // x ∈ H }) α β * h ^ index H
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
⊢ diff (MonoidHom.id { x // x ∈ H }) α (op ↑h • β) = diff (MonoidHom.id { x // x ∈ H }) α β * h ^ index H
letI := H.fintypeQuotientOfFiniteIndex
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ (let α_1 := toEquiv (_ : ↑α ∈ leftTransversals ↑H);
    let β_1 := toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H);
    ∏ q : G ⧸ H,
      ↑(MonoidHom.id { x // x ∈ H })
        { val := (↑(↑α_1 q))⁻¹ * ↑(↑β_1 q),
          property :=
            (_ :
              (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ *
                  ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q) ∈
                H) }) =
    ∏ x : G ⧸ H,
      ↑(MonoidHom.id { x // x ∈ H })
          { val := (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) x))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) x),
            property :=
              (_ :
                (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) x))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) x) ∈
                  H) } *
        h
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ diff (MonoidHom.id { x // x ∈ H }) α (op ↑h • β) = diff (MonoidHom.id { x // x ∈ H }) α β * h ^ index H
rw [diff, diff, index_eq_card, ←Finset.card_univ, ←Finset.prod_const, ←Finset.prod_mul_distrib]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ ↑(MonoidHom.id { x // x ∈ H })
      {
        val :=
          (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ * ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q),
        property :=
          (_ :
            (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ *
                ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q) ∈
              H) } =
    ↑(MonoidHom.id { x // x ∈ H })
        { val := (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) q),
          property :=
            (_ :
              (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) q) ∈
                H) } *
      h
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ (let α_1 := toEquiv (_ : ↑α ∈ leftTransversals ↑H);
    let β_1 := toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H);
    ∏ q : G ⧸ H,
      ↑(MonoidHom.id { x // x ∈ H })
        { val := (↑(↑α_1 q))⁻¹ * ↑(↑β_1 q),
          property :=
            (_ :
              (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ *
                  ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q) ∈
                H) }) =
    ∏ x : G ⧸ H,
      ↑(MonoidHom.id { x // x ∈ H })
          { val := (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) x))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) x),
            property :=
              (_ :
                (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) x))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) x) ∈
                  H) } *
        h
refine' Finset.prod_congr rfl fun q _ => _
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q) = ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) q) * ↑h
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ ↑(MonoidHom.id { x // x ∈ H })
      {
        val :=
          (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ * ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q),
        property :=
          (_ :
            (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ *
                ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q) ∈
              H) } =
    ↑(MonoidHom.id { x // x ∈ H })
        { val := (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) q),
          property :=
            (_ :
              (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) q) ∈
                H) } *
      h
simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, coe_mk, mul_assoc, mul_right_inj]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ q = op ↑h • q
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q) = ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) q) * ↑h
rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, unop_op, mul_left_inj, ←Subtype.ext_iff,
  Equiv.apply_eq_iff_eq, inv_smul_eq_iff]
no goals
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ q = op ↑h • q
exact self_eq_mul_right.mpr ((QuotientGroup.eq_one_iff _).mpr h.2)