awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
contra : f = 0
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)

Tactic:
simp [hf', contra]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
contra : f = 0
⊢ False

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

Premises used: RootPairing.ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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)
suffices :
  ∀ 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
⊢ b.height i = ∑ j ∈ b.support, f j

Tactic:
suffices ∀ j ∈ b.support, (b.exists_root_eq_sum_int i).choose j = f j from
    Finset.sum_congr rfl this
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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
⊢ 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)

Tactic:
obtain ⟨-, -, h⟩ := (b.exists_root_eq_sum_int i).choose_spec

Premises used: Exists.choose_spec, RootPairing.Base.exists_root_eq_sum_int
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
heq :
  Eq.{u_3 + 1} (α := 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))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : 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)
⊢ ∀ (x : ι), x ∈ b.support ↔ (fun (x : ι) ↦ x ∈ b.support) x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : 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)
⊢ ∀ (x : ι), x ∈ b.support ↔ (fun (x : ι) ↦ x ∈ b.support) x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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)
rw :
  ∀
    (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
⊢ ⋯.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

Premises used: Finset.sum_subtype, RootPairing.Base.support
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
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_1 : ι
hj : j_1 ∈ 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)
j : ↥b.support
⊢ Eq.{u_3 + 1} (α := M)
    (∑ i_1 : (↑(↑b.support : Set ι) : Type u_1),
      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)) ∘
            Subtype.val (p := fun (x : ι) ↦ x ∈ (↑b.support : Set ι)))
          i_1)
        ((P.root : (a : ι) → M) (↑i_1 : ι) : M))
    (∑ i : (↑(↑b.support : Set ι) : Type u_1),
      HSMul.hSMul (β := M) ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑b.support : Set ι))) i)
        ((P.root : (a : ι) → M) (↑i : ι) : M))

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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)
⊢ ∀ (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)) ∘
          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
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
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)
aux :
  ∀ (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)) ∘
          Subtype.val (p := fun (x : ι) ↦ x ∈ (↑b.support : Set ι)))
        j =
      (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑b.support : Set ι))) j
⊢ ⋯.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:
simpa using aux ⟨j, hj⟩

Premises used: Subtype.mk
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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
⊢ b.height i ≠ 0

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

Premises used: RootPairing.Base.exists_root_eq_sum_int
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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)
rw : Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
⊢ b.height i ≠ 0

Tactic:
rw [height_eq_sum hf₂]

Premises used: RootPairing.Base.height_eq_sum
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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
inr : ∀ (neg : f < 0), Ne (α := ℤ) (∑ j ∈ b.support, f j) 0
⊢ Ne (α := ℤ) (∑ j ∈ b.support, f j) 0

Tactic:
rcases hf₁ with pos | neg
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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

Tactic:
(Finset.sum_pos' (fun i _ ↦ pos.le i) ?_).ne'

Premises used: Finset.sum_pos', LT.lt.le, LT.lt.ne'
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
pos : 0 < f
inl : ∃ i ∈ b.support, 0 < f i
⊢ Ne (α := ℤ) (∑ j ∈ b.support, f j) 0

Tactic:
refine (Finset.sum_pos' (fun i _ ↦ pos.le i) ?_).ne'

Premises used: Finset.sum_pos', LT.lt.le, LT.lt.ne'
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
pos : 0 < f
inl : ∀ (contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0), False
⊢ ∃ i ∈ b.support, 0 < f i

Tactic:
by_contra! contra
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
pos : 0 < f
contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0
j : ι
pos₁ : ∀ (hj : j ∈ Function.support f), f j = 0
neg : ∀ (hj : j ∉ Function.support f), f j = 0
⊢ f j = 0

Tactic:
by_cases hj : j ∈ f.support

Premises used: Function.support
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
pos : 0 < f
contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0
j : ι
hj : j ∈ Function.support f
⊢ f j = 0

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

Premises used: LT.lt.le, le_antisymm
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
pos : 0 < f
contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0
j : ι
hj : j ∈ Function.support f
⊢ f j = 0

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

Premises used: LT.lt.le, le_antisymm
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
pos : 0 < f
contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0
j : ι
hj : j ∉ Function.support f
⊢ f j = 0

Tactic:
simpa using hj
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
pos : 0 < f
contra : ∀ (i : ι) (_ : i ∈ b.support), f i ≤ 0
⊢ ∀ (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
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
pos : 0 < f
contra : ∀ (j : ι), f j = 0
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)

Tactic:
simp [hf₂, contra]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf₂ :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
pos : 0 < f
contra : ∀ (j : ι), f j = 0
⊢ False

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

Premises used: RootPairing.ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : CharZero R
i : ι
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

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

Premises used: LT.lt.le, Finset.sum_neg', LT.lt.ne