awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
rw : LE.le (α := ℤ) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) 0
⊢ P.pairingIn ℤ i i ≤ 0

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
refine : ∀ j ∈ b.support, f j • P.pairingIn ℤ j i ≤ 0
⊢ LE.le (α := ℤ) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) 0

Tactic:
refine Finset.sum_nonpos fun j _ ↦ ?_

Premises used: Finset.sum_nonpos
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
j : ι
h : j ∈ b.support
pos : ∀ (hj : j ∈ Function.support f), f j • P.pairingIn ℤ j i ≤ 0
neg : ∀ (hj : j ∉ Function.support f), f j • P.pairingIn ℤ j i ≤ 0
⊢ f j • P.pairingIn ℤ j i ≤ 0

Tactic:
by_cases hj : j ∈ Function.support f

Premises used: Function.support
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
j : ι
h : j ∈ b.support
hj : j ∈ Function.support f
⊢ f j • P.pairingIn ℤ j i ≤ 0

Tactic:
smul_nonpos_of_nonneg_of_nonpos (hf₁.le j) (contra j (hf₀ hj))

Premises used: LT.lt.le, smul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
j : ι
h : j ∈ b.support
hj : j ∈ Function.support f
⊢ f j • P.pairingIn ℤ j i ≤ 0

Tactic:
exact smul_nonpos_of_nonneg_of_nonpos (hf₁.le j) (contra j (hf₀ hj))

Premises used: LT.lt.le, smul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
j : ι
h : j ∈ b.support
hj : j ∉ Function.support f
⊢ f j • P.pairingIn ℤ j i ≤ 0

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
inl : ∀ (hi : b.IsPos i), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
inr : ∀ (hi : b.IsPos (-i)), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

Tactic:
rcases IsPos.or_neg b i with hi | hi

Premises used: RootPairing.Base.IsPos.or_neg
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
hi : b.IsPos i
inl : ∀ (j : ι) (hj : j ∈ b.support) (hj₀ : 0 < P.pairingIn ℤ j i), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

Tactic:
obtain ⟨j, hj, hj₀⟩ := hi.exists_mem_support_pos_pairingIn

Premises used: RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j : ι
hj : j ∈ b.support
hj₀ : 0 < P.pairingIn ℤ j i
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

Tactic:
⟨j, hj, hj₀.ne'⟩

Premises used: LT.lt.ne', And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j : ι
hj : j ∈ b.support
hj₀ : 0 < P.pairingIn ℤ j i
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

Tactic:
exact ⟨j, hj, hj₀.ne'⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
hi : b.IsPos (-i)
inr : ∀ (j : ι) (hj : j ∈ b.support) (hj₀ : 0 < P.pairingIn ℤ j (-i)), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

Tactic:
obtain ⟨j, hj, hj₀⟩ := hi.exists_mem_support_pos_pairingIn

Premises used: RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
hi : b.IsPos (-i)
j : ι
hj : j ∈ b.support
hj₀ : 0 < P.pairingIn ℤ j (-i)
⊢ P.pairingIn ℤ j i ≠ 0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i : ι
hi : b.IsPos (-i)
j : ι
hj : j ∈ b.support
hj₀ : 0 < P.pairingIn ℤ j (-i)
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

Tactic:
exact ⟨j, hj, by aesop⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)

Tactic:
IsReduced.linearIndependent P hij.symm fun contra ↦ ?_

Premises used: Ne.symm, RootPairing.IsReduced.linearIndependent
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
refine : ∀ (contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)), False
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)

Tactic:
refine IsReduced.linearIndependent P hij.symm fun contra ↦ ?_

Premises used: Ne.symm, RootPairing.IsReduced.linearIndependent
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)
this : InvolutiveNeg ι := P.indexNeg
rw : j = -i
⊢ i = -j

Tactic:
rw [eq_comm, neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg, eq_comm
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)
this : InvolutiveNeg ι := P.indexNeg
⊢ j = -i

Tactic:
simpa using contra
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)
this : InvolutiveNeg ι := P.indexNeg
⊢ i = -j

Tactic:
replace contra : i = -j := by rw [eq_comm, neg_eq_iff_eq_neg]; simpa using contra
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
this : InvolutiveNeg ι := P.indexNeg
contra : i = -j
⊢ LT.lt (α := ℤ) 0 (-1)

Tactic:
rw [contra, isPos_iff, height_reflectionPerm_self, height_one_of_mem_support hj] at hi

Premises used: RootPairing.Base.height_reflectionPerm_self, RootPairing.Base.height_one_of_mem_support, RootPairing.Base.isPos_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
this : InvolutiveNeg ι := P.indexNeg
contra : i = -j
hi₁ : LT.lt (α := ℤ) 0 (-1)
⊢ i = -j

Tactic:
rw [contra, isPos_iff, height_reflectionPerm_self, height_one_of_mem_support hj] at hi

Premises used: RootPairing.Base.height_reflectionPerm_self, RootPairing.Base.height_one_of_mem_support, RootPairing.Base.isPos_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
this : InvolutiveNeg ι := P.indexNeg
hi : LT.lt (α := ℤ) 0 (-1)
contra : i = -j
⊢ False

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)

Tactic:
replace hij : LinearIndependent R ![P.root j, P.root i] := by
    refine IsReduced.linearIndependent P hij.symm fun contra ↦ ?_
    letI := P.indexNeg
    replace contra : i = -j := by rw [eq_comm, neg_eq_iff_eq_neg]; simpa using contra
    rw [contra, isPos_iff, height_reflectionPerm_self, height_one_of_mem_support hj] at hi
    lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (α := ℤ) (β := M) 0 ((P.root : (a : ι) → M) j : M))
hij :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
⊢ b.IsPos k

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M))
hij :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
rw :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M)) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M))
⊢ (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M))

Tactic:
rw [hk]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M))
hij :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
⊢ HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M)) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M))

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑w : ℤ) 1) ((P.root : (a : ι) → M) j : M))
hij :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M)))

Tactic:
replace hk : P.root i + (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι} (hi : b.IsPos i)
    (hk :
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))
    (hij :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)),
    b.IsPos k
i k : ι
hi : b.IsPos i
hij :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
hk :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) (w + 1) ((P.root : (a : ι) → M) j : M)))
simp :
  ∀ (hk : w + 1 ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i),
    w ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (α := ℤ) (β := M) (↑w : ℤ) ((P.root : (a : ι) → M) j : M)))

Tactic:
simp only [natCast_zsmul, root_add_nsmul_mem_range_iff_le_chainTopCoeff hij] at hk ⊢

Premises used: natCast_zsmul, RootPairing.root_add_nsmul_mem_range_iff_le_chainTopCoeff