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 : 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)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have 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)
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 : Invertible (α := k) (↑(Fintype.card G) : k)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
have have : HSMul.hSMul (α := k) (β := k) (@Invertible.invOf _ MulZeroClass.toMul InvOneClass.toOne (↑(Nat.card G) : k) _)
    (∑ g : G, V.character g * V.character g⁻¹) =
  1
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
-- 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 : 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
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
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)
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
-- 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 : 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)
⊢ Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
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⁻¹) *
        (↑(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)
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
-- 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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
⊢ 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 : Eq.{u + 1} (α := k) (∑ g : G, V.character g * V.character g⁻¹) (↑(Nat.card G) : k)
⊢ Simple V
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 : 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)
⊢ Simple V
have have : ∀ (this : Invertible (α := k) (↑(Fintype.card G) : k)), Simple V
Tactic: have := invertibleOfNonzero (NeZero.ne (Fintype.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 : 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)
⊢ Simple V
have have : ∀ (this : Invertible (α := k) (↑(Nat.card G) : k)), Simple V
Tactic: have := invertibleOfNonzero (NeZero.ne (Nat.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 : 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)
⊢ Simple V
have 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)
Tactic: have eq := FDRep.scalar_product_char_eq_finrank_equivariant 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 : 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)
⊢ Simple V
have 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)
Tactic: rw [h] at eq
Cleared hypotheses: eq
-- 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 : 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)
⊢ Simple V
have eq₁ : 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
Cleared hypotheses: eq
-- 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 : 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)
⊢ Simple V
have rw : Module.finrank k (V ⟶ V) = 1
Tactic: rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]
-- 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 : 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
⊢ Simple V
have rw₁ : Eq.{u + 1} (α := k) (↑(Module.finrank k (V ⟶ V)) : k) (↑1 : k)
Tactic: rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]
-- 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 : 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)
⊢ Simple V
have rw₂ : Eq.{u + 1} (α := k) 1 (↑1 : k)
Tactic: rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]
-- 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 : 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)
⊢ Simple V
have rw₃ : Eq.{u + 1} (α := k) 1 1
Tactic: rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
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
⊢ g₁ * g⁻¹ ∈ S
have rcases : ∀ (s : ↥S), (fun (m : ↥S) ↦ m • g) s * g⁻¹ ∈ S
Tactic: rcases h with ⟨s, rfl⟩
Cleared hypotheses: g₁, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
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.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g = a
have rw : (((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * g⁻¹) sorry) :
        (↑A : Type w) →ₗ[k] (↑A : Type w)) :
      (a : (↑A : Type w)) → (↑A : Type w))
    a =
  a
Tactic: rw [indToCoindAux, LinearMap.pi_apply, dif_pos]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
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
⊢ (A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g = a
have hc : (QuotientGroup.rightRel S : G → G → Prop) g g
Tactic: rw [indToCoindAux, LinearMap.pi_apply, dif_pos]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
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)
s : ↥S
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * g₁) : (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₁ : (↑A : Type w)) :
      (↑A : Type w))
have inl : ∀ (s₁ : ↥S),
  Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * (fun (m : ↥S) ↦ m • g) s₁) :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g) s₁) : (↑A : Type w)) :
      (↑A : Type w))
Tactic: rcases em ((QuotientGroup.rightRel S).r g₁ g) with ⟨s₁, rfl⟩ | h
Cleared hypotheses: g₁
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
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)
s : ↥S
inl :
  ∀ (s₁ : ↥S),
    Eq.{w + 1} (α := (↑A : Type w))
      ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * (fun (m : ↥S) ↦ m • g) s₁) :
        (↑A : Type w))
      ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (↑A : Type w))
          ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g) s₁) :
            (↑A : Type w)) :
        (↑A : Type w))
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * g₁) : (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₁ : (↑A : Type w)) :
      (↑A : Type w))
have inr : ∀ (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 ((↑s : G) * g₁) : (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₁ : (↑A : Type w)) :
      (↑A : Type w))
Tactic: rcases em ((QuotientGroup.rightRel S).r g₁ g) with ⟨s₁, rfl⟩ | h
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
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)
s s₁ : ↥S
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * (fun (m : ↥S) ↦ m • g) s₁) :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g) s₁) : (↑A : Type w)) :
      (↑A : Type w))
have inl : Eq (α := (↑A : Type w))
  ((if h : (QuotientGroup.rightRel S : G → G → Prop) ((↑s : G) * s₁ • g) g then
          (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
            (Subtype.mk (p := fun (x : G) ↦ x ∈ S) ((↑s : G) * s₁ • g * g⁻¹) sorry)
        else 0 :
        (a : (↑A : Type w)) → (↑A : Type w))
      a :
    (↑A : Type w))
  ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
        (a : (↑A : Type w)) → (↑A : Type w))
      ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g) g then
              (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
                (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g * g⁻¹) sorry)
            else 0 :
            (a : (↑A : Type w)) → (↑A : Type w))
          a :
        (↑A : Type w)) :
    (↑A : Type w))
Tactic: simp only [indToCoindAux, LinearMap.pi_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
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)
s s₁ : ↥S
⊢ Eq (α := (↑A : Type w))
    ((if h : (QuotientGroup.rightRel S : G → G → Prop) ((↑s : G) * s₁ • g) g then
            (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) ((↑s : G) * s₁ • g * g⁻¹) ⋯)
          else 0 :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g) g then
                (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
                  (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g * g⁻¹) ⋯)
              else 0 :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w)) :
      (↑A : Type w))
have inl : Eq (α := (↑A : Type w))
  ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
            (Subtype.mk (p := fun (x : G) ↦ x ∈ S) ((↑s : G) * s₁ • g * g⁻¹) sorry) :
          (↑A : Type w) →ₗ[k] (↑A : Type w)) :
        (a : (↑A : Type w)) → (↑A : Type w))
      a :
    (↑A : Type w))
  ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
        (a : (↑A : Type w)) → (↑A : Type w))
      ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g * g⁻¹) sorry) :
              (↑A : Type w) →ₗ[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (↑A : Type w))
          a :
        (↑A : Type w)) :
    (↑A : Type w))
Tactic: rw [dif_pos ⟨s * s₁, mul_assoc ..⟩, dif_pos ⟨s₁, rfl⟩]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
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)
s : ↥S
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 ((↑s : G) * g₁) : (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₁ : (↑A : Type w)) :
      (↑A : Type w))
have inr : ¬(QuotientGroup.rightRel S : G → G → Prop) ((↑s : G) * g₁) g
Tactic: rw [indToCoindAux_of_not_rel _ _ _ h, indToCoindAux_of_not_rel, map_zero]