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
i : ι
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)
neg : f < 0
inr : ∃ i ∈ b.support, f i < 0
⊢ Ne (α := ℤ) (∑ j ∈ b.support, f j) 0

Tactic:
refine (Finset.sum_neg' (fun i _ ↦ neg.le i) ?_).ne

Premises used: LT.lt.le, Finset.sum_neg', LT.lt.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
i : ι
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)
neg : f < 0
inr : ∀ (contra : ∀ (i : ι) (_ : i ∈ b.support), 0 ≤ f i), False
⊢ ∃ i ∈ b.support, f i < 0

Tactic:
by_contra! 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
i : ι
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)
neg : f < 0
contra : ∀ (i : ι) (_ : i ∈ b.support), 0 ≤ f i
j : ι
pos : ∀ (hj : j ∈ Function.support f), f j = 0
neg₁ : ∀ (hj : j ∉ Function.support f), f j = 0
⊢ f j = 0

Tactic:
by_cases hj : j ∈ f.support

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
i : ι
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)
neg : f < 0
contra : ∀ (i : ι) (_ : i ∈ b.support), 0 ≤ f i
j : ι
hj : j ∈ Function.support f
⊢ f j = 0

Tactic:
le_antisymm (neg.le j) (contra j (hf₀ hj))

Premises used: LT.lt.le, le_antisymm
-- 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
i : ι
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)
neg : f < 0
contra : ∀ (i : ι) (_ : i ∈ b.support), 0 ≤ f i
j : ι
hj : j ∈ Function.support f
⊢ f j = 0

Tactic:
exact le_antisymm (neg.le j) (contra j (hf₀ hj))

Premises used: LT.lt.le, le_antisymm
-- 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
i : ι
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)
neg : f < 0
contra : ∀ (i : ι) (_ : i ∈ b.support), 0 ≤ f i
j : ι
hj : j ∉ Function.support f
⊢ f j = 0

Tactic:
simpa using hj
-- 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
i : ι
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)
neg : f < 0
contra : ∀ (i : ι) (_ : i ∈ b.support), 0 ≤ f i
⊢ ∀ (j : ι), f j = 0

Tactic:
replace contra (j : ι) : f j = 0 := by
      by_cases hj : j ∈ f.support
      · exact le_antisymm (neg.le j) (contra j (hf₀ hj))
      · simpa using hj
-- 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
i : ι
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)
neg : f < 0
contra : ∀ (j : ι), f j = 0
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)

Tactic:
simp [hf₂, 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
i : ι
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)
neg : f < 0
contra : ∀ (j : ι), f j = 0
⊢ False

Tactic:
exact P.ne_zero i <| by simp [hf₂, contra]

Premises used: RootPairing.ne_zero
-- 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
i : ι
this : InvolutiveNeg ι := P.indexNeg
obtain :
  ∀ (f : ι → ℤ) (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf₁ : 0 < f ∨ f < 0)
    (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)),
    b.height (-i) = -b.height i
⊢ b.height (-i) = -b.height i

Tactic:
obtain ⟨f, hf₀, hf₁, hf₂⟩ := b.exists_root_eq_sum_int i

Premises used: RootPairing.Base.exists_root_eq_sum_int
-- 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
i : ι
this : InvolutiveNeg ι := P.indexNeg
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
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)
⊢ 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)

Tactic:
simpa
-- 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
i : ι
this : InvolutiveNeg ι := P.indexNeg
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
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)
⊢ 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)

Tactic:
have hf₃ : P.root (-i) = ∑ j ∈ b.support, (-f) j • P.root j := by simpa
-- 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
i : ι
this : InvolutiveNeg ι := P.indexNeg
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₁ : 0 < f ∨ f < 0
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₃ :
  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)
⊢ b.height (-i) = -b.height i

Tactic:
simp only [height_eq_sum hf₂, height_eq_sum hf₃, Pi.neg_apply, Finset.sum_neg_distrib]

Premises used: RootPairing.Base.height_eq_sum, Finset.sum_neg_distrib, Pi.neg_apply
-- 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
i : ι
hi : i ∈ b.support
⊢ ∀ b_1 ∈ b.support,
    b_1 ≠ i →
      HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 b_1 : ℤ) ((P.root : (a : ι) → M) b_1 : M) = 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
i : ι
hi : i ∈ b.support
rw :
  (P.root : (a : ι) → M) i =
    HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 i : ℤ) ((P.root : (a : ι) → M) i : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support,
        HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 j : ℤ) ((P.root : (a : ι) → M) j : M) :
      M)

Tactic:
rw [Finset.sum_eq_single_of_mem i hi (by simp_all)]

Premises used: Finset.sum_eq_single_of_mem
-- 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
i : ι
hi : i ∈ b.support
⊢ (P.root : (a : ι) → M) i =
    HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 i : ℤ) ((P.root : (a : ι) → M) i : M)

Tactic:
simp
-- 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
i : ι
hi : i ∈ b.support
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support,
        HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 j : ℤ) ((P.root : (a : ι) → M) j : M) :
      M)

Tactic:
have : P.root i = ∑ j ∈ b.support, (Pi.single i 1 : ι → ℤ) j • P.root j := by
    rw [Finset.sum_eq_single_of_mem i hi (by simp_all)]; simp
-- 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
i : ι
hi : i ∈ b.support
this :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support,
        HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 j : ℤ) ((P.root : (a : ι) → M) j : M) :
      M)
⊢ b.height i = 1

Tactic:
simpa [height_eq_sum this]

Premises used: RootPairing.Base.height_eq_sum
-- 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
i : ι
hi : i ∈ b.support
have :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support,
        HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 j : ℤ) ((P.root : (a : ι) → M) j : M) :
      M)
have₁ :
  ∀
    (this :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
        (∑ j ∈ b.support,
            HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 j : ℤ) ((P.root : (a : ι) → M) j : M) :
          M)),
    b.height i = 1
have₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support,
        HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 j : ℤ) ((P.root : (a : ι) → M) j : M) :
      M)
have₃ have₄ :
  ∀
    (this :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
        (∑ j ∈ b.support,
            HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 j : ℤ) ((P.root : (a : ι) → M) j : M) :
          M)),
    b.height i = 1
⊢ b.height i = 1

Tactic:
classical
  have : P.root i = ∑ j ∈ b.support, (Pi.single i 1 : ι → ℤ) j • P.root j := by
    rw [Finset.sum_eq_single_of_mem i hi (by simp_all)]; simp
  simpa [height_eq_sum 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
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
obtain :
  ∀ (f : ι → ℤ)
    (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)),
    b.height k = b.height i + b.height j
⊢ b.height k = b.height i + b.height j

Tactic:
obtain ⟨f, -, -, hf⟩ := b.exists_root_eq_sum_int i

Premises used: RootPairing.Base.exists_root_eq_sum_int
-- 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
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
f : ι → ℤ
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)
obtain :
  ∀ (g : ι → ℤ)
    (hg :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)),
    b.height k = b.height i + b.height j
⊢ b.height k = b.height i + b.height j

Tactic:
obtain ⟨g, -, -, hg⟩ := b.exists_root_eq_sum_int j

Premises used: RootPairing.Base.exists_root_eq_sum_int
-- 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
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
f : ι → ℤ
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)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
simp_rw :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ x ∈ b.support, HSMul.hSMul (β := M) (f x + g x) ((P.root : (a : ι) → M) x : M) : M)
simp_rw₁ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ x ∈ b.support,
        (HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M) +
          HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M)) :
      M)
simp_rw₂ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (∑ x ∈ b.support, HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M))
      (∑ x ∈ b.support, HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M))
simp_rw₃ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M)
      (∑ x ∈ b.support, HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M) : M)
simp_rw₄ :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + g) l) ((P.root : (a : ι) → M) l : M) : M)

Tactic:
simp_rw [Pi.add_apply, add_smul, Finset.sum_add_distrib, ← hf, ← hg, hk]

Premises used: Finset.sum_add_distrib, Pi.add_apply, add_smul
-- 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
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
f : ι → ℤ
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)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + g) l) ((P.root : (a : ι) → M) l : M) : M)

Tactic:
have hfg : P.root k = ∑ l ∈ b.support, (f + g) l • P.root l := by
    simp_rw [Pi.add_apply, add_smul, Finset.sum_add_distrib, ← hf, ← hg, 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
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
f : ι → ℤ
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)
g : ι → ℤ
hg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)
hfg :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + g) l) ((P.root : (a : ι) → M) l : M) : M)
simp_rw : b.height k = ∑ j ∈ b.support, f j + b.height j
simp_rw₁ : b.height k = HAdd.hAdd (α := ℤ) (∑ j ∈ b.support, f j) (∑ j ∈ b.support, g j)
simp_rw₂ : ∑ j ∈ b.support, (f + g) j = HAdd.hAdd (α := ℤ) (∑ j ∈ b.support, f j) (∑ j ∈ b.support, g j)
simp_rw₃ : Eq (α := ℤ) (∑ j ∈ b.support, (f + g) j) (∑ x ∈ b.support, (f x + g x))
⊢ b.height k = b.height i + b.height j

Tactic:
simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, ← Finset.sum_add_distrib,
    Pi.add_apply]

Premises used: RootPairing.Base.height_eq_sum, Finset.sum_add_distrib, Pi.add_apply
-- 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
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
this : InvolutiveNeg ι := P.indexNeg
⊢ (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) (-j) : M)

Tactic:
simpa [← sub_eq_add_neg]

Premises used: sub_eq_add_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
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
this : InvolutiveNeg ι := P.indexNeg
⊢ (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) (-j) : M)

Tactic:
replace hk : P.root k = P.root i + P.root (-j) := by simpa [← sub_eq_add_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
i j k : ι
this : InvolutiveNeg ι := P.indexNeg
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) (-j) : M)
rw : b.height k = b.height i + -b.height j
rw₁ : b.height k = b.height i + b.height (-j)
rw₂ rw₃ : b.height i + b.height (-j) = b.height i + b.height (-j)
⊢ b.height k = b.height i - b.height j

Tactic:
rw [sub_eq_add_neg, ← b.height_reflectionPerm_self, b.height_add hk]

Premises used: RootPairing.Base.height_reflectionPerm_self, sub_eq_add_neg, RootPairing.Base.height_add
-- 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
i j k : ι
z : ℤ
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))
obtain :
  ∀ (f : ι → ℤ)
    (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)),
    b.height k = b.height i + z • b.height j
⊢ b.height k = b.height i + z • b.height j

Tactic:
obtain ⟨f, -, -, hf⟩ := b.exists_root_eq_sum_int i

Premises used: RootPairing.Base.exists_root_eq_sum_int
-- 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
i j k : ι
z : ℤ
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))
f : ι → ℤ
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)
obtain :
  ∀ (g : ι → ℤ)
    (hg :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M) : M)),
    b.height k = b.height i + z • b.height j
⊢ b.height k = b.height i + z • b.height j

Tactic:
obtain ⟨g, -, -, hg⟩ := b.exists_root_eq_sum_int j

Premises used: RootPairing.Base.exists_root_eq_sum_int