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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this : HMul.hMul (α := R) (↑z : R) (↑w : R) = 1
⊢ z * w = 1

Tactic:
norm_cast at 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this : z * w = 1
⊢ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1

Tactic:
rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at this

Premises used: Int.mul_eq_one_iff_eq_one_or_neg_one
-- 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
inl : z = 1 → w = 1 → z = 1 ∨ z = -1
inr : z = -1 → w = -1 → z = 1 ∨ z = -1
inl₁ : z = 1 → w = 1 → z = 1 ∨ z = -1
inr₁ : z = -1 → w = -1 → z = 1 ∨ z = -1
inl₂ : z = 1 → w = 1 → ¬z = 1 → z = -1
inr₂ : z = -1 → w = -1 → ¬z = 1 → z = -1
inl₃ : z = 1 → w = 1 → ¬z = 1 → z = -1
⊢ z = 1 ∨ z = -1

Tactic:
tauto
-- 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
f : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
obtain :
  ∀ (k : ι)
    (hk :
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)),
    0 < f ∨ f < 0
⊢ 0 < f ∨ f < 0

Tactic:
obtain ⟨k, hk⟩ := hf
-- 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
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hf₀ : Function.support (M := ℤ) 0 ⊆ (↑b.support : Set ι)
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (α := ℤ) (β := M) (0 j) ((P.root : (a : ι) → M) j : M) : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)

Tactic:
simp [hk]
-- 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
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hf₀ : Function.support (M := ℤ) 0 ⊆ (↑b.support : Set ι)
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (α := ℤ) (β := M) (0 j) ((P.root : (a : ι) → M) j : M) : M)
⊢ False

Tactic:
exact P.ne_zero k <| by simp [hk]

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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
⊢ f ≠ 0

Tactic:
have hf' : f ≠ 0 := by rintro rfl; exact P.ne_zero k <| by simp [hk]
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
inl :
  ∀
    (hk' :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) k : M)),
    0 < f ∨ f < 0
inr :
  ∀
    (hk' :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) k : M)),
    0 < f ∨ f < 0
⊢ 0 < f ∨ f < 0

Tactic:
rcases b.root_mem_or_neg_mem k with hk' | hk'

Premises used: RootPairing.Base.root_mem_or_neg_mem
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) k : M)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))

Tactic:
rw [hk] at hk'
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) k : M)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))

Tactic:
rw [hk] at hk'
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
inl : 0 < f
⊢ 0 < f ∨ f < 0

Tactic:
left
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ 0 < f

Tactic:
this f hk' hf₀ hf'
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ 0 < f

Tactic:
exact this f hk' hf₀ hf'
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
inr : f < 0
⊢ 0 < f ∨ f < 0

Tactic:
right
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))

Tactic:
hk'
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
h :
  Eq.{u_3 + 1} (α := M) (∑ j ∈ b.support, HSMul.hSMul (β := M) ((-f) j) ((P.root : (a : ι) → M) j : M))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) ((-f) j) ((P.root : (a : ι) → M) j : M))

Tactic:
convert! hk'
-- 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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ Eq.{u_3 + 1} (α := M) (∑ j ∈ b.support, HSMul.hSMul (β := M) ((-f) j) ((P.root : (a : ι) → M) j : M))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))

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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ Function.support (-f) ⊆ (↑b.support : Set ι)

Tactic:
simpa only [support_neg]

Premises used: Function.support_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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ -f ≠ 0

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
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ f < 0

Tactic:
simpa using this (-f) (by convert! hk'; simp) (by simpa only [support_neg]) (by simpa)

Premises used: Neg.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
f : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
suffices :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
⊢ 0 < f ∨ f < 0

Tactic:
suffices ∀ (f : ι → ℤ)
      (hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support))
      (hf₀ : f.support ⊆ b.support) (hf' : f ≠ 0), 0 < f by
    obtain ⟨k, hk⟩ := hf
    have hf' : f ≠ 0 := by rintro rfl; exact P.ne_zero k <| by simp [hk]
    rcases b.root_mem_or_neg_mem k with hk' | hk' <;> rw [hk] at hk'
    · left; exact this f hk' hf₀ hf'
    · right; simpa using this (-f) (by convert! hk'; simp) (by simpa only [support_neg]) (by 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
f_1 : ι → ℤ
hf_1 :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
this :
  Eq.{u_3 + 1} (α := M) (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))

Tactic:
rwa [this]