-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Group G
inst_2 : IsAlgClosed k
inst_3 : CharZero k
inst_4 : Fintype G
V : FDRep k G
h : Simple V
this_1 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
this_2 : Invertible (α := k) (↑(Nat.card G) : k)
this_3 : Invertible (α := k) (↑(Fintype.card G) : k)
this :
  HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _)
        (∑ g : G, V.character g * V.character g⁻¹) *
      (↑(Fintype.card G) : k) =
    HMul.hMul (α := k) 1 (↑(Fintype.card G) : k)
rwa :
  ∀
    (this :
      (↑(Fintype.card G) : k) *
          HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _)
            (∑ g : G, V.character g * V.character g⁻¹) =
        HMul.hMul (α := k) 1 (↑(Fintype.card G) : k)),
    Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
rwa₁ :
  ∀
    (this :
      HSMul.hSMul (α := k) (↑(Fintype.card G) : k)
          (HSMul.hSMul (α := k) (β := k)
            (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _)
            (∑ g : G, V.character g * V.character g⁻¹)) =
        HMul.hMul (α := k) 1 (↑(Fintype.card G) : k)),
    Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
rwa₂ :
  ∀
    (this :
      HSMul.hSMul (β := k)
          (HMul.hMul (α := k) (↑(Fintype.card G) : k)
            (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _))
          (∑ g : G, V.character g * V.character g⁻¹) =
        HMul.hMul (α := k) 1 (↑(Fintype.card G) : k)),
    Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
rwa₃ :
  ∀
    (this :
      HSMul.hSMul (β := k)
          (HMul.hMul (α := k) (↑(Nat.card G) : k)
            (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _))
          (∑ g : G, V.character g * V.character g⁻¹) =
        HMul.hMul (α := k) 1 (↑(Nat.card G) : k)),
    Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
rwa₄ :
  ∀
    (this :
      HSMul.hSMul (α := k) (β := k) 1 (∑ g : G, V.character g * V.character g⁻¹) =
        HMul.hMul (α := k) 1 (↑(Nat.card G) : k)),
    Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
rwa₅ :
  ∀ (this : HMul.hMul (α := k) 1 (∑ g : G, V.character g * V.character g⁻¹) = HMul.hMul (α := k) 1 (↑(Nat.card G) : k)),
    Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
rwa₆ :
  ∀ (this : ∑ g : G, V.character g * V.character g⁻¹ = HMul.hMul (α := k) 1 (↑(Nat.card G) : k)),
    Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have rwa₇ : ∀ (this : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)),
  Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
Tactic: rwa [mul_comm, ← smul_eq_mul, smul_smul, Fintype.card_eq_nat_card, mul_invOf_self, smul_eq_mul,
      one_mul, one_mul] at this
Cleared hypotheses: this