awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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
⊢ 𝟙 (Abelian.image f) = ι ≫ φ

Tactic:
have hιφ : 𝟙 _ = ι ≫ φ := (Injective.comp_factorThru (𝟙 _) ι).symm
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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) = ι ≫ φ
⊢ 𝟙 (Abelian.image f) ≫ ι = (ι ≫ φ) ≫ ι

Tactic:
apply_fun (· ≫ ι) at hιφ

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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

Tactic:
simp_all
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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)) ι
⊢ φ ≫ ι ≠ 0

Tactic:
have hφι : φ ≫ ι ≠ 0 := by
        intro habs
        have hιφ : 𝟙 _ = ι ≫ φ := (Injective.comp_factorThru (𝟙 _) ι).symm
        apply_fun (· ≫ ι) at hιφ
        simp_all
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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), c • φ ≫ ι = 𝟙 V

Tactic:
(finrank_eq_one_iff_of_nonzero' _ hφι).mp h (𝟙 V)

Premises used: CategoryTheory.CategoryStruct.id, Iff.mp, finrank_eq_one_iff_of_nonzero'
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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
refine_2 : ∀ (c : k) (hc : c • φ ≫ ι = 𝟙 V), Epi ι
⊢ Epi ι

Tactic:
obtain ⟨c, hc⟩ : ∃ c : k, c • _ = 𝟙 V := (finrank_eq_one_iff_of_nonzero' _ hφι).mp h (𝟙 V)

Premises used: CategoryTheory.CategoryStruct.id, Iff.mp, finrank_eq_one_iff_of_nonzero'
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 ι

Tactic:
Preadditive.epi_of_cancel_zero _ (fun g hg ↦ ?_)

Premises used: CategoryTheory.Preadditive.epi_of_cancel_zero
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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
refine_2 : ∀ {R : FDRep k G} (g : V ⟶ R) (hg : ι ≫ g = 0), g = 0
⊢ Epi ι

Tactic:
refine Preadditive.epi_of_cancel_zero _ (fun g hg ↦ ?_)

Premises used: CategoryTheory.Preadditive.epi_of_cancel_zero
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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
⊢ (c • φ ≫ ι) ≫ g = 𝟙 V ≫ g

Tactic:
apply_fun (· ≫ g) at hc

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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
R : FDRep k G
g : V ⟶ R
hg : ι ≫ g = 0
hc : (c • φ ≫ ι) ≫ g = 𝟙 V ≫ g
⊢ g = 0

Tactic:
simpa [hg] using hc.symm

Premises used: Eq.symm
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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
⊢ Fintype G

Tactic:
assumption
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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
rw : NeZero.{u} (R := k) (↑(Fintype.card G) : k)
⊢ NeZero.{u} (R := k) (↑(Nat.card G) : k)

Tactic:
rw [← @Fintype.card_eq_nat_card G (by assumption)]

Premises used: Fintype.card_eq_nat_card
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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) (↑(Fintype.card G) : k)

Tactic:
NeZero.charZero

Premises used: NeZero.charZero
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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) (↑(Fintype.card G) : k)

Tactic:
exact NeZero.charZero

Premises used: NeZero.charZero
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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)

Tactic:
have : NeZero (Nat.card G : k) := by
      rw [← @Fintype.card_eq_nat_card G (by assumption)]
      exact NeZero.charZero
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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)
have :
  ∀ (this : Invertible (α := k) (↑(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)

Tactic:
have := invertibleOfNonzero (NeZero.ne (Nat.card G : k))
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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)
have :
  ∀ (this : Invertible (α := k) (↑(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)

Tactic:
have := invertibleOfNonzero (NeZero.ne (Fintype.card G : k))
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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)
⊢ HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _)
      (∑ g : G, V.character g * V.character g⁻¹) =
    1

Tactic:
simpa only [Nonempty.intro (Iso.refl V), ↓reduceIte, Fintype.card_eq_nat_card]
      using char_orthonormal V V

Premises used: CategoryTheory.Iso.refl, Nonempty.intro, reduceIte, FDRep.char_orthonormal, Fintype.card_eq_nat_card
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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)
⊢ 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
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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
⊢ 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

Premises used: HMul.hMul, Fintype.card, Nat.cast
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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)
have :
  HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _)
      (∑ g : G, V.character g * V.character g⁻¹) =
    1
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),
    Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have₂ :
  HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _)
      (∑ g : G, V.character g * V.character g⁻¹) =
    1
have₃ 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),
    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)),
    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:
classical
    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
    apply_fun (· * (Fintype.card G : k)) at this
    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

Premises used: HMul.hMul, smul_smul, Fintype.card, mul_invOf_self, Nat.cast, mul_comm, smul_eq_mul, one_mul, Fintype.card_eq_nat_card
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
⊢ Fintype G

Tactic:
assumption
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
rw : NeZero.{u} (R := k) (↑(Fintype.card G) : k)
⊢ NeZero.{u} (R := k) (↑(Nat.card G) : k)

Tactic:
rw [← @Fintype.card_eq_nat_card G (by assumption)]

Premises used: Fintype.card_eq_nat_card
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
⊢ NeZero.{u} (R := k) (↑(Fintype.card G) : k)

Tactic:
NeZero.charZero

Premises used: NeZero.charZero
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
⊢ NeZero.{u} (R := k) (↑(Fintype.card G) : k)

Tactic:
exact NeZero.charZero

Premises used: NeZero.charZero
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
⊢ 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
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
this : NeZero.{u} (R := k) (↑(Nat.card G) : k)
have : ∀ (this : Invertible (α := k) (↑(Fintype.card G) : k)), Simple V
⊢ Simple V

Tactic:
have := invertibleOfNonzero (NeZero.ne (Fintype.card G : k))
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
this_1 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
this : Invertible (α := k) (↑(Fintype.card G) : k)
have : ∀ (this : Invertible (α := k) (↑(Nat.card G) : k)), Simple V
⊢ Simple V

Tactic:
have := invertibleOfNonzero (NeZero.ne (Nat.card G : k))
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
this_1 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
this_2 : Invertible (α := k) (↑(Fintype.card G) : k)
this : Invertible (α := k) (↑(Nat.card G) : k)
⊢ HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ g : G, V.character g * V.character g⁻¹) =
    (↑(Module.finrank k (V ⟶ V)) : k)

Tactic:
have eq := FDRep.scalar_product_char_eq_finrank_equivariant V V
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
this_1 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
this_2 : Invertible (α := k) (↑(Fintype.card G) : k)
this : Invertible (α := k) (↑(Nat.card G) : k)
eq :
  HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (∑ g : G, V.character g * V.character g⁻¹) =
    (↑(Module.finrank k (V ⟶ V)) : k)
⊢ HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (↑(Nat.card G) : k) =
    (↑(Module.finrank k (V ⟶ V)) : k)

Tactic:
rw [h] at eq
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
this_1 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
this_2 : Invertible (α := k) (↑(Fintype.card G) : k)
this : Invertible (α := k) (↑(Nat.card G) : k)
eq :
  HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(Fintype.card G) : k) _)
      (↑(Nat.card G) : k) =
    (↑(Module.finrank k (V ⟶ V)) : k)
⊢ Eq.{u + 1} (α := k) 1 (↑(Module.finrank k (V ⟶ V)) : k)

Tactic:
simp only [invOf_eq_inv, smul_eq_mul, inv_mul_cancel_of_invertible, Fintype.card_eq_nat_card]
      at eq

Premises used: inv_mul_cancel_of_invertible, invOf_eq_inv, smul_eq_mul, Fintype.card_eq_nat_card
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
this_1 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
this_2 : Invertible (α := k) (↑(Fintype.card G) : k)
this : Invertible (α := k) (↑(Nat.card G) : k)
eq : Eq.{u + 1} (α := k) 1 (↑(Module.finrank k (V ⟶ V)) : k)
rw : Module.finrank k (V ⟶ V) = 1
rw₁ : Eq.{u + 1} (α := k) (↑(Module.finrank k (V ⟶ V)) : k) (↑1 : k)
rw₂ : Eq.{u + 1} (α := k) 1 (↑1 : k)
rw₃ rw₄ : Eq.{u + 1} (α := k) 1 1
⊢ Simple V

Tactic:
rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]

Premises used: Nat.cast_inj, FDRep.simple_iff_end_is_rank_one, Nat.cast_one
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g g₁ : G
h : (QuotientGroup.rightRel S : G → G → Prop) g₁ g
rcases : ∀ (s : ↥S), (fun (m : ↥S) ↦ m • g) s * g⁻¹ ∈ S
⊢ g₁ * g⁻¹ ∈ S

Tactic:
rcases h with ⟨s, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g : G
s : ↥S
⊢ (fun (m : ↥S) ↦ m • g) s * g⁻¹ ∈ S

Tactic:
mul_inv_cancel_right s.1 g ▸ s.2

Premises used: mul_inv_cancel_right, Set.Mem, Eq.rec, Eq.symm, Subtype.val, Subtype.property
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g : G
s : ↥S
⊢ (fun (m : ↥S) ↦ m • g) s * g⁻¹ ∈ S

Tactic:
exact mul_inv_cancel_right s.1 g ▸ s.2
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g : G
a : (↑A : Type w)
rw :
  (((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * g⁻¹) ⋯) :
          (↑A : Type w) →ₗ[k] (↑A : Type w)) :
        (a : (↑A : Type w)) → (↑A : Type w))
      a =
    a
hc : (QuotientGroup.rightRel S : G → G → Prop) g g
⊢ (A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g = a

Tactic:
rw [indToCoindAux, LinearMap.pi_apply, dif_pos]

Premises used: dif_pos, LinearMap.pi_apply, Rep.indToCoindAux
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g : G
a : (↑A : Type w)
⊢ (((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * g⁻¹) ⋯) :
          (↑A : Type w) →ₗ[k] (↑A : Type w)) :
        (a : (↑A : Type w)) → (↑A : Type w))
      a =
    a

Tactic:
simp [← S.1.one_def]

Premises used: Submonoid.one_def, Subgroup.toSubmonoid
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g : G
a : (↑A : Type w)
⊢ (QuotientGroup.rightRel S : G → G → Prop) g g

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : (↑A : Type w)
h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₁ g
⊢ Eq.{w + 1} (α := (↑A : Type w)) ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₁ : (↑A : Type w))
    (0 : (↑A : Type w))

Tactic:
simp [indToCoindAux, dif_neg h]

Premises used: dif_neg, Rep.indToCoindAux