awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
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)
contra : ∀ (i : ι), LE.le (α := ℤ) (0 i) ((-Nat.cast ∘ f) i)
⊢ False
have contra₁ : f = 0
Tactic: replace contra : f = 0 := by ext i; simpa using contra i
Cleared hypotheses: contra
-- 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 : ι
f : ι → ℤ
heq :
  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 = ∑ j ∈ b.support, f j
have suffices : ∀ j ∈ b.support,
  sorry.choose (p := fun (f : ι → ℤ) ↦
      Function.support f ⊆ (↑b.support : Set ι) ∧
        (0 < f ∨ f < 0) ∧
          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))
      j =
    f j
Tactic: suffices ∀ j ∈ b.support, (b.exists_root_eq_sum_int i).choose j = f j from
    Finset.sum_congr rfl this
-- 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 : ι
f : ι → ℤ
heq :
  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)
j : ι
hj : j ∈ b.support
⊢ ⋯.choose (p := fun (f : ι → ℤ) ↦
      Function.support f ⊆ (↑b.support : Set ι) ∧
        (0 < f ∨ f < 0) ∧
          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))
      j =
    f j
have h : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
  (∑ j ∈ b.support,
      HSMul.hSMul (β := M)
        (sorry.choose (p := fun (f : ι → ℤ) ↦
          Function.support f ⊆ (↑b.support : Set ι) ∧
            (0 < f ∨ f < 0) ∧
              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))
          j)
        ((P.root : (a : ι) → M) j : M) :
    M)
Tactic: obtain ⟨-, -, h⟩ := (b.exists_root_eq_sum_int i).choose_spec
-- 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 : ι
f : ι → ℤ
heq :
  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)
j : ι
hj : j ∈ b.support
h :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support,
        HSMul.hSMul (β := M)
          (⋯.choose (p := fun (f : ι → ℤ) ↦
            Function.support f ⊆ (↑b.support : Set ι) ∧
              (0 < f ∨ f < 0) ∧
                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))
            j)
          ((P.root : (a : ι) → M) j : M) :
      M)
⊢ ⋯.choose (p := fun (f : ι → ℤ) ↦
      Function.support f ⊆ (↑b.support : Set ι) ∧
        (0 < f ∨ f < 0) ∧
          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))
      j =
    f j
have rw : ∀
  (heq :
    Eq.{u_3 + 1} (α := M)
      (∑ a : ↥b.support,
        HSMul.hSMul (β := M)
          (sorry.choose (p := fun (f : ι → ℤ) ↦
            Function.support f ⊆ (↑b.support : Set ι) ∧
              (0 < f ∨ f < 0) ∧
                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))
            (↑a : ι))
          ((P.root : (a : ι) → M) (↑a : ι) : M))
      (∑ a : ↥b.support, HSMul.hSMul (β := M) (f (↑a : ι)) ((P.root : (a : ι) → M) (↑a : ι) : M)))
  (j : ι) (hj : j ∈ b.support)
  (h :
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
      (∑ j ∈ b.support,
          HSMul.hSMul (β := M)
            (sorry.choose (p := fun (f : ι → ℤ) ↦
              Function.support f ⊆ (↑b.support : Set ι) ∧
                (0 < f ∨ f < 0) ∧
                  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))
              j)
            ((P.root : (a : ι) → M) j : M) :
        M)),
  sorry.choose (p := fun (f : ι → ℤ) ↦
      Function.support f ⊆ (↑b.support : Set ι) ∧
        (0 < f ∨ f < 0) ∧
          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))
      j =
    f j
Tactic: rw [h, b.support.sum_subtype (p := (· ∈ b.support)) (by simp) (F := inferInstance),
    b.support.sum_subtype (p := (· ∈ b.support)) (by simp) (F := inferInstance)] at heq
Cleared hypotheses: heq, j, hj, h
-- 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 : ι
f : ι → ℤ
heq :
  Eq.{u_3 + 1} (α := M)
    (∑ a : ↥b.support,
      HSMul.hSMul (β := M)
        (⋯.choose (p := fun (f : ι → ℤ) ↦
          Function.support f ⊆ (↑b.support : Set ι) ∧
            (0 < f ∨ f < 0) ∧
              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))
          (↑a : ι))
        ((P.root : (a : ι) → M) (↑a : ι) : M))
    (∑ a : ↥b.support, HSMul.hSMul (β := M) (f (↑a : ι)) ((P.root : (a : ι) → M) (↑a : ι) : M))
j : ι
hj : j ∈ b.support
h :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support,
        HSMul.hSMul (β := M)
          (⋯.choose (p := fun (f : ι → ℤ) ↦
            Function.support f ⊆ (↑b.support : Set ι) ∧
              (0 < f ∨ f < 0) ∧
                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))
            j)
          ((P.root : (a : ι) → M) j : M) :
      M)
⊢ ⋯.choose (p := fun (f : ι → ℤ) ↦
      Function.support f ⊆ (↑b.support : Set ι) ∧
        (0 < f ∨ f < 0) ∧
          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))
      j =
    f j
have aux : ∀ (j : ↥b.support),
  (sorry.choose (p := fun (f : ι → ℤ) ↦
          Function.support f ⊆ (↑b.support : Set ι) ∧
            (0 < f ∨ f < 0) ∧
              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)) ∘
        Subtype.val (p := fun (x : ι) ↦ x ∈ (↑b.support : Set ι)))
      j =
    (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑b.support : Set ι))) j
Tactic: have aux (j : b.support) := Fintype.linearIndependent_iffₛ.mp
      (b.linearIndepOn_root.restrict_scalars' ℤ) ((b.exists_root_eq_sum_int i).choose ∘ (↑))
      (f ∘ (↑)) (by simpa) 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 : ι
⊢ b.height i ≠ 0
have 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 ≠ 0
Tactic: obtain ⟨f, hf₀, hf₁, 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 : ι
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 ≠ 0
have rw : Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
Tactic: rw [height_eq_sum hf₂]
-- 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 : ι
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)
⊢ Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
have inl : ∀ (pos : 0 < f), Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
Tactic: rcases hf₁ with pos | neg
Cleared hypotheses: hf₁
-- 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 : ι
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)
inl : ∀ (pos : 0 < f), Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
⊢ Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
have inr : ∀ (neg : f < 0), Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
Tactic: rcases hf₁ with pos | neg
Cleared hypotheses: hf₁
-- 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 : ι
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)
pos : 0 < f
⊢ Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
have inl : ∃ i ∈ b.support, 0 < f i
Tactic: refine (Finset.sum_pos' (fun i _ ↦ pos.le i) ?_).ne'
-- 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 : ι
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)
pos : 0 < f
⊢ ∃ i ∈ b.support, 0 < f i
have inl : ∀ (contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0), False
Tactic: by_contra! contra
-- 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 : ι
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)
pos : 0 < f
contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0
j : ι
⊢ f j = 0
have pos₁ : ∀ (hj : j ∈ Function.support f), f j = 0
Tactic: by_cases hj : j ∈ f.support
-- 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 : ι
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)
pos : 0 < f
contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0
j : ι
pos₁ : ∀ (hj : j ∈ Function.support f), f j = 0
⊢ f j = 0
have neg : ∀ (hj : j ∉ Function.support f), f j = 0
Tactic: by_cases hj : j ∈ f.support
-- 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 : ι
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)
pos : 0 < f
contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0
⊢ False
have contra₁ : ∀ (j : ι), f j = 0
Tactic: replace contra (j : ι) : f j = 0 := by
      by_cases hj : j ∈ f.support
      · exact le_antisymm (contra j (hf₀ hj)) (pos.le j)
      · simpa using hj
Cleared hypotheses: contra
-- 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 : ι
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
⊢ Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
have inr : ∃ i ∈ b.support, f i < 0
Tactic: refine (Finset.sum_neg' (fun i _ ↦ neg.le i) ?_).ne
-- 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 : ι
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
⊢ ∃ i ∈ b.support, f i < 0
have inr : ∀ (contra : ∀ (i : ι) (_ : i ∈ b.support), 0 ≤ f i), False
Tactic: by_contra! contra
-- 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 : ι
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
have pos : ∀ (hj : j ∈ Function.support f), f j = 0
Tactic: by_cases hj : j ∈ f.support
-- 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 : ι
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
⊢ f j = 0
have neg₁ : ∀ (hj : j ∉ Function.support f), f j = 0
Tactic: by_cases hj : j ∈ f.support
-- 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 : ι
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
⊢ False
have contra₁ : ∀ (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
Cleared hypotheses: contra
-- 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 : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ b.height (-i) = -b.height i
have 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
Tactic: obtain ⟨f, hf₀, hf₁, hf₂⟩ := b.exists_root_eq_sum_int i
-- 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 : ι
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)
⊢ b.height (-i) = -b.height i
have 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)
Tactic: have hf₃ : P.root (-i) = ∑ j ∈ b.support, (-f) j • P.root j := by simpa
-- 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 : ι
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)
have rw : (P.root : (a : ι) → M) i =
  HSMul.hSMul (α := ℤ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℤ) i 1 i : ℤ) ((P.root : (a : ι) → M) i : M)
Tactic: rw [Finset.sum_eq_single_of_mem i hi (by simp_all)]
-- 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 : ι
hi : i ∈ b.support
⊢ b.height i = 1
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)
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
-- 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 : ι
hi : i ∈ b.support
⊢ b.height i = 1
have 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)
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]
-- 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 : ι
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)
⊢ b.height i = 1
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
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]
-- 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)
⊢ b.height k = b.height i + 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 + 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 : ι
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)
⊢ b.height k = b.height i + 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 + b.height j
Tactic: obtain ⟨g, -, -, hg⟩ := b.exists_root_eq_sum_int j