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
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)
⊢ P.pairingIn ℤ i i ≤ 0
have hf₃ : 0 < f
Tactic: replace hf₁ : 0 < f := by
    refine hf₁.resolve_right ?_
    rw [isPos_iff, height_eq_sum hf₂] at h₀
    contrapose! h₀
    exact Finset.sum_nonpos fun i _ ↦ h₀.le i
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
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) : R)
have simp_rw : P.pairing i i = (algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i)
Tactic: simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]
-- 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₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
simp_rw : P.pairing i i = (algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i)
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) : R)
have simp_rw₁ : P.pairing i i = ∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i)
Tactic: simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]
-- 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₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
simp_rw : P.pairing i i = (algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i)
simp_rw₁ : P.pairing i i = ∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i)
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) : R)
have simp_rw₂ : Eq.{u_2 + 1} (α := R)
  ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      ((P.coroot : (a : ι) → N) i : N) :
    R)
  (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
Tactic: simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]
-- 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₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
simp_rw : P.pairing i i = (algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i)
simp_rw₁ : P.pairing i i = ∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i)
simp_rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) : R)
have simp_rw₃ : Eq.{u_2 + 1} (α := R)
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) i : N) :
    R)
  (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
Tactic: simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]
-- 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₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
simp_rw : P.pairing i i = (algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i)
simp_rw₁ : P.pairing i i = ∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i)
simp_rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
simp_rw₃ :
  Eq.{u_2 + 1} (α := R)
    (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) : R)
have simp_rw₄ : Eq.{u_2 + 1} (α := R)
  ((∑ x ∈ b.support, (P.toLinearMap : (a : M) → N →ₗ[R] R) (HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M)) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) i : N) :
    R)
  (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
Tactic: simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]
-- 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₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
simp_rw : P.pairing i i = (algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i)
simp_rw₁ : P.pairing i i = ∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i)
simp_rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
simp_rw₃ :
  Eq.{u_2 + 1} (α := R)
    (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
simp_rw₄ :
  Eq.{u_2 + 1} (α := R)
    ((∑ x ∈ b.support,
            (P.toLinearMap : (a : M) → N →ₗ[R] R) (HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M)) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) : R)
have simp_rw₅ : Eq.{u_2 + 1} (α := R)
  ((∑ x ∈ b.support,
          HSMul.hSMul (β := N →ₗ[R] R) (f x)
            ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) x) : N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) i : N) :
    R)
  (∑ x ∈ b.support, HSMul.hSMul (β := R) (f x) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ x i) : R) : R)
Tactic: simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]
-- 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₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
simp_rw : P.pairing i i = (algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i)
simp_rw₁ : P.pairing i i = ∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i)
simp_rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
simp_rw₃ :
  Eq.{u_2 + 1} (α := R)
    (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
simp_rw₄ :
  Eq.{u_2 + 1} (α := R)
    ((∑ x ∈ b.support,
            (P.toLinearMap : (a : M) → N →ₗ[R] R) (HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M)) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, (algebraMap ℤ R : (a : ℤ) → R) (f x • P.pairingIn ℤ x i) : R)
simp_rw₅ :
  Eq.{u_2 + 1} (α := R)
    ((∑ x ∈ b.support,
            HSMul.hSMul (β := N →ₗ[R] R) (f x)
              ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) x) : N →ₗ[R] R) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) i : N) :
      R)
    (∑ x ∈ b.support, HSMul.hSMul (β := R) (f x) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ x i) : R) : R)
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) : R)
have simp_rw₆ : Eq.{u_2 + 1} (α := R)
  ((∑ i ∈ b.support,
      (⇑(HSMul.hSMul (β := N →ₗ[R] R) (f i)
            ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R)) :
        (a : N) → R))
    ((P.coroot : (a : ι) → N) i))
  (∑ x ∈ b.support, HSMul.hSMul (β := R) (f x) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ x i) : R))
Tactic: simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]
-- 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
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
⊢ P.pairingIn ℤ i i ≤ 0
have this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
Tactic: have : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i :=
    algebraMap_injective ℤ R <| by
      simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]
-- 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₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
⊢ P.pairingIn ℤ i i ≤ 0
have rw : LE.le (α := ℤ) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) 0
Tactic: rw [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
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
⊢ LE.le (α := ℤ) (∑ j ∈ b.support, f j • P.pairingIn ℤ j i) 0
have refine : ∀ j ∈ b.support, f j • P.pairingIn ℤ j i ≤ 0
Tactic: refine Finset.sum_nonpos fun 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
inst_6 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ (j : ι) (_ : j ∈ b.support), P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
j : ι
h : j ∈ b.support
⊢ f j • P.pairingIn ℤ j i ≤ 0
have pos : ∀ (hj : j ∈ Function.support f), f j • P.pairingIn ℤ j i ≤ 0
Tactic: by_cases hj : j ∈ Function.support f
-- 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₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
j : ι
h : j ∈ b.support
pos : ∀ (hj : j ∈ Function.support f), f j • P.pairingIn ℤ j i ≤ 0
⊢ f j • P.pairingIn ℤ j i ≤ 0
have neg : ∀ (hj : j ∉ Function.support f), f j • P.pairingIn ℤ j i ≤ 0
Tactic: by_cases hj : j ∈ Function.support f
-- 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 : ι
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
have inl : ∀ (hi : b.IsPos i), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
Tactic: rcases IsPos.or_neg b i with hi | hi
-- 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 : ι
inl : ∀ (hi : b.IsPos i), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
have inr : ∀ (hi : b.IsPos (-i)), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
Tactic: rcases IsPos.or_neg b i with hi | hi
-- 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 : ι
hi : b.IsPos i
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
have inl : ∀ (j : ι) (hj : j ∈ b.support) (hj₀ : 0 < P.pairingIn ℤ j i), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
Tactic: obtain ⟨j, hj, hj₀⟩ := hi.exists_mem_support_pos_pairingIn
-- 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 : ι
hi : b.IsPos (-i)
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
have inr : ∀ (j : ι) (hj : j ∈ b.support) (hj₀ : 0 < P.pairingIn ℤ j (-i)), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
Tactic: obtain ⟨j, hj, hj₀⟩ := hi.exists_mem_support_pos_pairingIn
-- 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 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
have refine : ∀ (contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)), False
Tactic: refine IsReduced.linearIndependent P hij.symm fun 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 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)
this : InvolutiveNeg ι := P.indexNeg
⊢ i = -j
have rw : j = -i
Tactic: rw [eq_comm, neg_eq_iff_eq_neg]
-- 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
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)
this : InvolutiveNeg ι := P.indexNeg
⊢ False
have contra₁ : i = -j
Tactic: replace contra : i = -j := by rw [eq_comm, neg_eq_iff_eq_neg]; simpa using contra
Cleared hypotheses: contra
-- 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
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hi : b.IsPos i
hj : j ∈ b.support
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) j : M))
this : InvolutiveNeg ι := P.indexNeg
contra : i = -j
⊢ False
have hi₁ : LT.lt (α := ℤ) 0 (-1)
Tactic: rw [contra, isPos_iff, height_reflectionPerm_self, height_one_of_mem_support hj] at hi
Cleared hypotheses: hi, contra