awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
pos :
  x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
      (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr l) 1)
⊢ ∃ (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:
refine ⟨l, x * (P.chainBotCoeff i k + 1), hl, ?_⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
pos :
  ∀ (m : ↥b.support),
    (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inl m) =
      HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
        (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
        (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr l) 1) (Sum.inl m)
pos₁ :
  ∀ (m : ι),
    (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inr m) =
      HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
        (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
        (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr l) 1) (Sum.inr m)
⊢ x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
      (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr l) 1)

Tactic:
ext (m | m)
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
m : ↥b.support
⊢ (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inl m) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
      (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr l) 1) (Sum.inl m)

Tactic:
simp [e, -indexNeg_neg, hki]

Premises used: RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
m : ι
pos :
  ∀
    (hl :
      (P.root : (a : ι) → M) m =
        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) (Sum.inr m) =
      HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
        (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
        (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr m) 1) (Sum.inr m)
pos₁ :
  ∀ (hml : m ≠ l),
    (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inr m) =
      HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
        (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
        (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr l) 1) (Sum.inr m)
⊢ (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inr m) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
      (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr l) 1) (Sum.inr m)

Tactic:
rcases eq_or_ne m l with rfl | hml

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
m : ι
hl :
  (P.root : (a : ι) → M) m =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
rw :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((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)))
⊢ (P.root : (a : ι) → M) m =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)

Tactic:
rw [hl, hk₁]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
m : ι
hl :
  (P.root : (a : ι) → M) m =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
⊢ HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((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:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
m : ι
hl :
  (P.root : (a : ι) → M) m =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
⊢ (P.root : (a : ι) → M) m =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)

Tactic:
replace hl : P.root m = P.root i + P.root k := by rw [hl, hk₁]; module
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
m : ι
hl :
  (P.root : (a : ι) → M) m =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)
⊢ (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inr m) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
      (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr m) 1) (Sum.inr m)

Tactic:
simp [e, -indexNeg_neg, hl, mul_add]

Premises used: mul_add, RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
m : ι
hml : m ≠ l
contra :
  (P.root : (a : ι) → M) m =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)
rw :
  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))) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) l : M)

Tactic:
rw [hl, contra, hk₁]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
m : ι
hml : m ≠ l
contra :
  (P.root : (a : ι) → M) m =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : 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))) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
m : ι
hml : m ≠ l
⊢ (P.root : (a : ι) → M) m ≠
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)

Tactic:
replace hl : P.root m ≠ P.root i + P.root k :=
            fun contra ↦ hml (P.root.injective <| by rw [hl, contra, hk₁]; module)
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
l m : ι
hml : m ≠ l
hl :
  (P.root : (a : ι) → M) m ≠
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)
⊢ (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inr m) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R)
      (x * (chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k + 1))
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr l) 1) (Sum.inr m)

Tactic:
simp [e, -indexNeg_neg, hml, hl]

Premises used: RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
hij :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
neg : x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 = 0
⊢ 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:
left
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
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)
hki : k ≠ -(↑i : ι)
hij :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
neg :
  ∀ (l : ↥b.support),
    (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inl l) = 0 (Sum.inl l)
neg₁ : ∀ (l : ι), (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inr l) = 0 (Sum.inr l)
⊢ x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 = 0

Tactic:
ext (l | l)