awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
have 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)
Tactic: simp_rw [Pi.add_apply, add_smul, Finset.sum_add_distrib, ← hf, ← hg, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [Pi.add_apply, add_smul, Finset.sum_add_distrib, ← hf, ← hg, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
⊢ 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)
have 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))
Tactic: simp_rw [Pi.add_apply, add_smul, Finset.sum_add_distrib, ← hf, ← hg, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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))
⊢ 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)
have 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)
Tactic: simp_rw [Pi.add_apply, add_smul, Finset.sum_add_distrib, ← hf, ← hg, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (hypothesis)
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)
⊢ b.height k = b.height i + b.height j
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
⊢ b.height k = b.height i + b.height j
have simp_rw : b.height k = ∑ j ∈ b.support, f j + 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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
⊢ b.height k = b.height i + b.height j
have simp_rw₁ : b.height k = HAdd.hAdd (α := ℤ) (∑ j ∈ b.support, f j) (∑ j ∈ b.support, g j)
Tactic: simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, ← Finset.sum_add_distrib,
    Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
⊢ b.height k = b.height i + b.height j
have simp_rw₂ : ∑ j ∈ b.support, (f + g) j = HAdd.hAdd (α := ℤ) (∑ j ∈ b.support, f j) (∑ j ∈ b.support, g j)
Tactic: simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, ← Finset.sum_add_distrib,
    Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
⊢ b.height k = b.height i + b.height j
have simp_rw₃ : Eq (α := ℤ) (∑ j ∈ b.support, (f + g) j) (∑ x ∈ b.support, (f x + g x))
Tactic: simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, ← Finset.sum_add_distrib,
    Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (hypothesis)
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
⊢ b.height k = b.height i - b.height j
have hk₁ : (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]
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
⊢ b.height k = b.height i - b.height j
have rw : b.height k = b.height i + -b.height j
Tactic: rw [sub_eq_add_neg, ← b.height_reflectionPerm_self, b.height_add hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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
⊢ b.height k = b.height i - b.height j
have rw₁ : b.height k = b.height i + b.height (-j)
Tactic: rw [sub_eq_add_neg, ← b.height_reflectionPerm_self, b.height_add hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
⊢ b.height k = b.height i - b.height j
have rw₂ : b.height i + b.height (-j) = b.height i + b.height (-j)
Tactic: rw [sub_eq_add_neg, ← b.height_reflectionPerm_self, b.height_add hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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))
⊢ b.height k = b.height i + z • b.height j
have 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
Tactic: obtain ⟨f, -, -, hf⟩ := b.exists_root_eq_sum_int i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
⊢ b.height k = b.height i + z • b.height j
have 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
Tactic: obtain ⟨g, -, -, hg⟩ := b.exists_root_eq_sum_int j
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
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 + z • g) l) ((P.root : (a : ι) → M) l : M) : M)
have simp_rw : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
  (∑ x ∈ b.support, HSMul.hSMul (β := M) (f x + (z • g) x) ((P.root : (a : ι) → M) x : M) : M)
Tactic: simp_rw [Pi.add_apply, Pi.smul_apply, add_smul, smul_assoc, Finset.sum_add_distrib,
      ← Finset.smul_sum, ← hf, ← hg, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
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 + (z • g) x) ((P.root : (a : ι) → M) x : M) : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + z • g) l) ((P.root : (a : ι) → M) l : M) : M)
have simp_rw₁ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
  (∑ x ∈ b.support, HSMul.hSMul (β := M) (f x + z • g x) ((P.root : (a : ι) → M) x : M) : M)
Tactic: simp_rw [Pi.add_apply, Pi.smul_apply, add_smul, smul_assoc, Finset.sum_add_distrib,
      ← Finset.smul_sum, ← hf, ← hg, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
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 + (z • 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 + z • g x) ((P.root : (a : ι) → M) x : M) : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + z • g) l) ((P.root : (a : ι) → M) l : M) : M)
have 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) (z • g x) ((P.root : (a : ι) → M) x : M)) :
    M)
Tactic: simp_rw [Pi.add_apply, Pi.smul_apply, add_smul, smul_assoc, Finset.sum_add_distrib,
      ← Finset.smul_sum, ← hf, ← hg, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
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 + (z • 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 + z • 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) (z • g x) ((P.root : (a : ι) → M) x : M)) :
      M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + z • g) l) ((P.root : (a : ι) → M) l : M) : M)
have 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) +
        z • HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M)) :
    M)
Tactic: simp_rw [Pi.add_apply, Pi.smul_apply, add_smul, smul_assoc, Finset.sum_add_distrib,
      ← Finset.smul_sum, ← hf, ← hg, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
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)
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 + (z • 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 + z • 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) (z • 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) +
          z • HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M)) :
      M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ l ∈ b.support, HSMul.hSMul (β := M) ((f + z • g) l) ((P.root : (a : ι) → M) l : M) : M)
have 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, z • HSMul.hSMul (β := M) (g x) ((P.root : (a : ι) → M) x : M))
Tactic: simp_rw [Pi.add_apply, Pi.smul_apply, add_smul, smul_assoc, Finset.sum_add_distrib,
      ← Finset.smul_sum, ← hf, ← hg, hk]