awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
⊢ Epi f
have refine_2 : Epi (X := Abelian.image f) (Abelian.image.ι f)
Tactic: suffices Epi (Abelian.image.ι f) by
        rw [← Abelian.image.fac f]
        exact epi_comp _ _
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (hypothesis)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
⊢ Epi (X := Abelian.image f) (Abelian.image.ι f)
have hf₁ : CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (Abelian.image.ι f) ≠ 0
Tactic: rw [← Abelian.image.fac f] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (Abelian.image.ι f) ≠ 0
⊢ Epi (X := Abelian.image f) (Abelian.image.ι f)
have refine_2 : let ι : Abelian.image f ⟶ V := Abelian.image.ι f;
∀ (hf : Abelian.factorThruImage f ≫ ι ≠ 0), Epi ι
Tactic: set ι := Abelian.image.ι f
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (hypothesis)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
habs : φ ≫ ι = 0
⊢ False
have hιφ : 𝟙 (Abelian.image f) = ι ≫ φ
Tactic: have hιφ : 𝟙 _ = ι ≫ φ := (Injective.comp_factorThru (𝟙 _) ι).symm
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (hypothesis)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
habs : φ ≫ ι = 0
hιφ : 𝟙 (Abelian.image f) = ι ≫ φ
⊢ False
have hιφ₁ : 𝟙 (Abelian.image f) ≫ ι = (ι ≫ φ) ≫ ι
Tactic: apply_fun (· ≫ ι) at hιφ
Cleared hypotheses: hιφ
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (hypothesis)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
⊢ Epi ι
have hφι : φ ≫ ι ≠ 0
Tactic: have hφι : φ ≫ ι ≠ 0 := by
        intro habs
        have hιφ : 𝟙 _ = ι ≫ φ := (Injective.comp_factorThru (𝟙 _) ι).symm
        apply_fun (· ≫ ι) at hιφ
        simp_all
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
hφι : φ ≫ ι ≠ 0
⊢ Epi ι
have refine_2 : ∀ (c : k) (hc : c • φ ≫ ι = 𝟙 V), Epi ι
Tactic: obtain ⟨c, hc⟩ : ∃ c : k, c • _ = 𝟙 V := (finrank_eq_one_iff_of_nonzero' _ hφι).mp h (𝟙 V)
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
hφι : φ ≫ ι ≠ 0
c : k
hc : c • φ ≫ ι = 𝟙 V
⊢ Epi ι
have refine_2 : ∀ {R : FDRep k G} (g : V ⟶ R) (hg : ι ≫ g = 0), g = 0
Tactic: refine Preadditive.epi_of_cancel_zero _ (fun g hg ↦ ?_)
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (hypothesis)
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
hφι : φ ≫ ι ≠ 0
c : k
hc : c • φ ≫ ι = 𝟙 V
R : FDRep k G
g : V ⟶ R
hg : ι ≫ g = 0
⊢ g = 0
have hc₁ : (c • φ ≫ ι) ≫ g = 𝟙 V ≫ g
Tactic: apply_fun (· ≫ g) at hc
Cleared hypotheses: hc
-- 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
⊢ NeZero.{u} (R := k) (↑(Nat.card G) : k)
have rw : NeZero.{u} (R := k) (↑(Fintype.card G) : k)
Tactic: rw [← @Fintype.card_eq_nat_card G (by assumption)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (hypothesis)
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
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have this : NeZero.{u} (R := k) (↑(Nat.card G) : k)
Tactic: have : NeZero (Nat.card G : k) := by
      rw [← @Fintype.card_eq_nat_card G (by assumption)]
      exact NeZero.charZero
-- 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 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have have : ∀ (this : Invertible (α := k) (↑(Nat.card G) : k)),
  Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
Tactic: have := invertibleOfNonzero (NeZero.ne (Nat.card G : k))
-- 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 : Invertible (α := k) (↑(Nat.card G) : k)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have have : ∀ (this : Invertible (α := k) (↑(Fintype.card G) : k)),
  Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
Tactic: have := invertibleOfNonzero (NeZero.ne (Fintype.card G : k))
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (hypothesis)
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 : Invertible (α := k) (↑(Fintype.card G) : k)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have this₁ : HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _)
    (∑ g : G, V.character g * V.character g⁻¹) =
  1
Tactic: have : ⅟(Nat.card G : k) • ∑ g, V.character g * V.character g⁻¹ = 1 := by
      simpa only [Nonempty.intro (Iso.refl V), ↓reduceIte, Fintype.card_eq_nat_card]
      using char_orthonormal V V
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (hypothesis)
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⁻¹) =
    1
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have 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)
Tactic: apply_fun (· * (Fintype.card G : k)) at this
Cleared hypotheses: this
-- 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)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have 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)
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
-- 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)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have 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)
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
-- 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)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have 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)
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
-- 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)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have 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)
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
-- 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)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have 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)
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
-- 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)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have 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)
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