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 : ι
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)
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))
⊢ 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 =
  ∑ x ∈ b.support, HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M) +
    HSMul.hSMul (β := M) z (∑ x ∈ b.support, 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]
-- 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)
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))
simp_rw₅ :
  (P.root : (a : ι) → M) k =
    ∑ x ∈ b.support, HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M) +
      HSMul.hSMul (β := M) z (∑ 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 + z • g) l) ((P.root : (a : ι) → M) l : M) : M)
have simp_rw₆ : (P.root : (a : ι) → M) k =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) z (∑ x ∈ b.support, 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]
-- 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 : ι
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)
⊢ b.height k = b.height i + z • b.height j
have hfg : 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)
Tactic: have hfg : P.root k = ∑ l ∈ b.support, (f + z • g) l • P.root l := by
    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)
hfg :
  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)
⊢ b.height k = b.height i + z • b.height j
have simp_rw : b.height k = ∑ j ∈ b.support, f j + z • b.height j
Tactic: simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, Pi.add_apply, Pi.smul_apply,
    Finset.sum_add_distrib, Finset.smul_sum]
-- 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)
hfg :
  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)
simp_rw : b.height k = ∑ j ∈ b.support, f j + z • b.height j
⊢ b.height k = b.height i + z • b.height j
have simp_rw₁ : b.height k = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
Tactic: simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, Pi.add_apply, Pi.smul_apply,
    Finset.sum_add_distrib, Finset.smul_sum]
-- 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)
hfg :
  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)
simp_rw : b.height k = ∑ j ∈ b.support, f j + z • b.height j
simp_rw₁ : b.height k = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
⊢ b.height k = b.height i + z • b.height j
have simp_rw₂ : ∑ j ∈ b.support, (f + z • g) j = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
Tactic: simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, Pi.add_apply, Pi.smul_apply,
    Finset.sum_add_distrib, Finset.smul_sum]
-- 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)
hfg :
  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)
simp_rw : b.height k = ∑ j ∈ b.support, f j + z • b.height j
simp_rw₁ : b.height k = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₂ : ∑ j ∈ b.support, (f + z • g) j = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
⊢ b.height k = b.height i + z • b.height j
have simp_rw₃ : ∑ x ∈ b.support, (f x + (z • g) x) = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
Tactic: simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, Pi.add_apply, Pi.smul_apply,
    Finset.sum_add_distrib, Finset.smul_sum]
-- 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)
hfg :
  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)
simp_rw : b.height k = ∑ j ∈ b.support, f j + z • b.height j
simp_rw₁ : b.height k = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₂ : ∑ j ∈ b.support, (f + z • g) j = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₃ : ∑ x ∈ b.support, (f x + (z • g) x) = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
⊢ b.height k = b.height i + z • b.height j
have simp_rw₄ : ∑ x ∈ b.support, (f x + z • g x) = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
Tactic: simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, Pi.add_apply, Pi.smul_apply,
    Finset.sum_add_distrib, Finset.smul_sum]
-- 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)
hfg :
  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)
simp_rw : b.height k = ∑ j ∈ b.support, f j + z • b.height j
simp_rw₁ : b.height k = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₂ : ∑ j ∈ b.support, (f + z • g) j = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₃ : ∑ x ∈ b.support, (f x + (z • g) x) = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
simp_rw₄ : ∑ x ∈ b.support, (f x + z • g x) = ∑ j ∈ b.support, f j + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
⊢ b.height k = b.height i + z • b.height j
have simp_rw₅ : HAdd.hAdd (α := ℤ) (∑ x ∈ b.support, f x) (∑ x ∈ b.support, z • g x) =
  ∑ x ∈ b.support, f x + HSMul.hSMul (β := ℤ) z (∑ j ∈ b.support, g j)
Tactic: simp_rw [height_eq_sum hf, height_eq_sum hg, height_eq_sum hfg, Pi.add_apply, Pi.smul_apply,
    Finset.sum_add_distrib, Finset.smul_sum]
-- 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 : ι
⊢ 0 < b.height i ↔ 0 ≤ b.height i
have this : b.height i ≠ 0
Tactic: have := b.height_ne_zero 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 : ι
⊢ b.IsPos i ∨ b.IsPos (-i)
have rw : 0 < b.height i ∨ 0 < -b.height i
Tactic: rw [isPos_iff, isPos_iff, height_reflectionPerm_self]
-- 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 : ι
⊢ 0 < b.height i ∨ 0 < -b.height i
have this : b.height i ≠ 0
Tactic: have := b.height_ne_zero 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 : ι
⊢ b.IsPos (-i) ↔ ¬b.IsPos i
have rw : 0 < -b.height i ↔ ¬0 < b.height i
Tactic: rw [isPos_iff, isPos_iff, height_reflectionPerm_self]
-- 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 : ι
⊢ 0 < -b.height i ↔ ¬0 < b.height i
have this : b.height i ≠ 0
Tactic: have := b.height_ne_zero 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 : ι
h : i ∈ b.support
⊢ b.IsPos i
have rw : LT.lt (α := ℤ) 0 1
Tactic: rw [isPos_iff, height_one_of_mem_support 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 j k : ι
hi : b.IsPos i
hj : b.IsPos j
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ b.IsPos k
have hi₁ : 0 < b.height i
Tactic: rw [isPos_iff] at hi hj ⊢
Cleared hypotheses: hi, hj, 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 : ι
hi : b.IsPos i
hj : b.IsPos j
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi₁ : 0 < b.height i
⊢ b.IsPos k
have hj₁ : 0 < b.height j
Tactic: rw [isPos_iff] at hi hj ⊢
Cleared hypotheses: hi, hj, 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 : ι
hi : 0 < b.height i
hj : 0 < b.height j
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ 0 < b.height k
have rw : 0 < b.height i + b.height j
Tactic: rw [b.height_add 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 : ι
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ b.IsPos k
have hi₁ : 0 < b.height i
Tactic: rw [isPos_iff] at hi
Cleared hypotheses: hi, hj, 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 : ι
hi : 0 < b.height i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ b.IsPos k
have rw : 0 ≤ b.height i - 1
Tactic: rw [isPos_iff', b.height_sub hk, height_one_of_mem_support hj]
-- 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
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
⊢ ∃ j ∈ b.support, 0 < P.pairingIn ℤ j i
have by_contra! : ∀ (contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j 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
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
⊢ False
have suffices : P.pairingIn ℤ i i ≤ 0
Tactic: suffices P.pairingIn ℤ i i ≤ 0 by simp_all
-- 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
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
⊢ P.pairingIn ℤ i 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)),
  P.pairingIn ℤ i 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
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₁ : 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)
⊢ 0 < f
have refine : ¬f < 0
Tactic: refine hf₁.resolve_right ?_
-- 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
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₁ : 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)
⊢ ¬f < 0
have rw : ∀ (contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0) (f : ι → ℤ)
  (h₀ : LT.lt (α := ℤ) 0 (∑ j ∈ b.support, f j)) (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)),
  ¬f < 0
Tactic: rw [isPos_iff, height_eq_sum hf₂] at h₀
Cleared hypotheses: h₀, contra, f, hf₀, hf₁, 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
inst_6 : P.IsCrystallographic
i : ι
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
h₀ : LT.lt (α := ℤ) 0 (∑ j ∈ b.support, f j)
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)
⊢ ¬f < 0
have contrapose! : ∀ (h₀ : f < 0), LE.le (α := ℤ) (∑ j ∈ b.support, f j) 0
Tactic: contrapose! h₀
Cleared hypotheses: h₀