awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
h₅ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M))
m : ι
hm :
  (P.root : (a : ι) → M) m =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M)
l' : ι
hl' :
  (P.root : (a : ι) → M) l' =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
hk :
  (P.root : (a : ι) → M) k =
    HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M)
aux₃ :
  ∀ (x : ι) (hx : x ≠ m),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))
aux₄ :
  ∀ (x : ι) (hx : x ≠ l'),
    ¬((P.root : (a : ι) → M) x =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
        (P.root : (a : ι) → M) k =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M))
rw :
  (P.root : (a : ι) → M) k =
    HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M)
⊢ (P.root : (a : ι) → M) k =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l' : M) ((P.root : (a : ι) → M) (↑j : ι) : M)
have rw₁ : HSub.hSub (β := M) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
    ((P.root : (a : ι) → M) (↑j : ι) : M) =
  HSub.hSub (β := M) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
    ((P.root : (a : ι) → M) (↑j : ι) : M)
Tactic: rw [hl', hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst_10 : P.IsReduced
inst_11 : P.IsIrreducible
hij' : (↑i : ι) ≠ (↑j : ι)
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ (↑j : ι)
h₄ : l ≠ -(↑i : ι)
h₅ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M))
m : ι
hm :
  (P.root : (a : ι) → M) m =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M)
l' : ι
hl' :
  (P.root : (a : ι) → M) l' =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M)
hk :
  (P.root : (a : ι) → M) k =
    HSub.hSub (β := M)
      (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑j : ι) : M)
aux₃ :
  ∀ (x : ι) (hx : x ≠ m),
    ¬((P.root : (a : ι) → M) x =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑j : ι) : M) ∧
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))
aux₄ :
  ∀ (x : ι) (hx : x ≠ l'),
    ¬((P.root : (a : ι) → M) x =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
        (P.root : (a : ι) → M) k =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑j : ι) : M))
⊢ HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) m) : R) 1 *
      HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) l) : R) 1 =
    HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) l') : R) 1 *
      HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) 1
have this₁ : (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) m + 1) *
    (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) l + 1) =
  (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑j : ι) l' + 1) *
    (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l + 1)
Tactic: have := chainBotCoeff_mul_chainTopCoeff i.property j.property hij' hl'.symm hm.symm h₅
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
n : ℕ
h : j ≠ -(↑i : ι)
⊢ (e i ^ n).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ n).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
have this : Module.IsReflexive R M
Tactic: have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
n : ℕ
h : j ≠ -(↑i : ι)
this : Module.IsReflexive R M
⊢ (e i ^ n).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ n).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
have this₁ : IsAddTorsionFree M
Tactic: have : IsAddTorsionFree M := .of_isTorsionFree R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
n_1 : ℕ
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
n : ℕ
⊢ (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
have rw : e i *ᵥ e i ^ n *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr j) 1 = e i *ᵥ (e i ^ n).col (Sum.inr j)
Tactic: rw [pow_succ', ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
n : ℕ
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
⊢ (e i ^ n).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ n).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
have aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
Tactic: have aux (n : ℕ) : (e i ^ (n + 1)).col (.inr j) = (e i).mulVec ((e i ^ n).col (.inr j)) := by
    rw [pow_succ', ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]; simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
⊢ (HPow.hPow (β := ℕ) (e i) 0).col (Sum.inr j) =
    HSMul.hSMul (α := ℕ) (β := (j : ↥b.support ⊕ ι) → R) 1 (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr j) 1)
have h₁ : ∀ (x : ↥b.support ⊕ ι),
  (HPow.hPow (β := ℕ) (e i) 0).col (Sum.inr j) x =
    HSMul.hSMul (α := ℕ) (β := (j : ↥b.support ⊕ ι) → R) 1 (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr j) 1)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
ih :
  (e i ^ n).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ n).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
⊢ (e i ^ (n + 1)).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ (n + 1)).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
have succ : ∀ (hn : (e i ^ n).col (Sum.inr j) = 0),
  (e i ^ (n + 1)).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ (n + 1)).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
Tactic: rcases ih with hn | ⟨k, x, hk₁, hk₂⟩
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
ih :
  (e i ^ n).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ n).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
succ :
  ∀ (hn : (e i ^ n).col (Sum.inr j) = 0),
    (e i ^ (n + 1)).col (Sum.inr j) = 0 ∨
      ∃ (k : ι) (x : ℕ),
        (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
          (e i ^ (n + 1)).col (Sum.inr j) =
            HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
⊢ (e i ^ (n + 1)).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ (n + 1)).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
have succ₁ : ∀ (k : ι) (x : ℕ)
  (hk₁ :
    (P.root : (a : ι) → M) k =
      HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M)))
  (hk₂ :
    (e i ^ n).col (Sum.inr j) =
      HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)),
  (e i ^ (n + 1)).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ (n + 1)).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
Tactic: rcases ih with hn | ⟨k, x, hk₁, hk₂⟩
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
hn : (e i ^ n).col (Sum.inr j) = 0
⊢ (e i ^ (n + 1)).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ (n + 1)).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
have succ : (e i ^ (n + 1)).col (Sum.inr j) = 0
Tactic: left
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
⊢ (e i ^ (n + 1)).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ (n + 1)).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
have succ : x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 = 0 ∨
  ∃ (k_1 : ι) (x_1 : ℕ),
    (P.root : (a : ι) → M) k_1 =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
          (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
      x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
        HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x_1 (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k_1) 1)
Tactic: rw [aux, hk₂, Matrix.mulVec_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n x : ℕ
hk₁ :
  (P.root : (a : ι) → M) (-(↑i : ι)) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr (-(↑i : ι))) 1)
⊢ (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
have simp : ∀
  (hk₁ :
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
          (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))) =
      0),
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HAdd.hAdd (β := M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
        ((P.root : (a : ι) → M) (↑i : ι) : M)) =
    0
Tactic: simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self, neg_eq_iff_add_eq_zero,
          add_smul, one_smul] at hk₁ ⊢
Cleared hypotheses: hk₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n x : ℕ
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr (-(↑i : ι))) 1)
hk₁ :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
        (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))) =
    0
⊢ HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HAdd.hAdd (β := M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
        ((P.root : (a : ι) → M) (↑i : ι) : M)) =
    0
have rw : HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
    (HAdd.hAdd (β := M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
      ((P.root : (a : ι) → M) (↑i : ι) : M)) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M)))
Tactic: rw [← hk₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n x : ℕ
hk₁ :
  (P.root : (a : ι) → M) (-(↑i : ι)) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr (-(↑i : ι))) 1)
⊢ False
have hk₃ : (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
Tactic: replace hk₁ : P.root (-j) = (n + 1) • P.root i := by
        simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self, neg_eq_iff_add_eq_zero,
          add_smul, one_smul] at hk₁ ⊢
        rw [← hk₁]
        module
Cleared hypotheses: hk₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n x : ℕ
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr (-(↑i : ι))) 1)
hk₁ : (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ False
have inl : ∀
  (hk₂ :
    (HPow.hPow (β := ℕ) (e i) 0).col (Sum.inr j) =
      HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x
        (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr (-(↑i : ι))) 1))
  (hk₁ :
    (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (HAdd.hAdd (α := ℕ) 0 1) ((P.root : (a : ι) → M) (↑i : ι) : M)),
  False
Tactic: rcases n.eq_zero_or_pos with rfl | hn
Cleared hypotheses: n, hk₂, hk₁