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
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 ι)
h : ¬f ≤ 0
h' : 0 < f
⊢ 0 ≤ f

Tactic:
le_of_lt h'

Premises used: le_of_lt
-- 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 ι)
h : ¬f ≤ 0
h' : 0 < f
⊢ 0 ≤ f

Tactic:
exact le_of_lt h'

Premises used: le_of_lt
-- 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 ι)
h : ¬f ≤ 0
h' : f < 0
refine_1 : False
⊢ 0 ≤ f

Tactic:
exfalso
-- 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 ι)
h : ¬f ≤ 0
h' : f < 0
⊢ False

Tactic:
h (le_of_lt h')

Premises used: le_of_lt
-- 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 ι)
h : ¬f ≤ 0
h' : f < 0
⊢ False

Tactic:
exact h (le_of_lt h')

Premises used: le_of_lt
-- 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 ι)
h : ¬f ≤ 0
refine_2 : ∀ (h : ∀ (i : ι), f i ≤ 0 i), f ≤ 0
⊢ ∃ (i : ι), 0 i < f i

Tactic:
contrapose! h
-- 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 ι)
h : ∀ (i : ι), f i ≤ 0 i
⊢ f ≤ 0

Tactic:
h
-- 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 ι)
h : ∀ (i : ι), f i ≤ 0 i
⊢ f ≤ 0

Tactic:
exact h
-- 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 ι)
rw :
  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))
⊢ 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))

Tactic:
rw [← neg_mem_range_root_iff]

Premises used: RootPairing.neg_mem_range_root_iff
-- 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 ι)
⊢ 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))

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 :
  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 ι)
⊢ 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))

Tactic:
replace hf : ∑ j ∈ b.support, (-f) j • P.root j ∈ range P.root := by
    rw [← neg_mem_range_root_iff]; 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 ι)
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))
⊢ Function.support (-f) ⊆ (↑b.support : Set ι)

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 ι)
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))
⊢ ¬-f ≤ 0 ↔ 0 < -f

Tactic:
have := b.not_nonpos_iff_pos_of_sum_mem_range_root (-f) hf (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 : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
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))
this : ¬-f ≤ 0 ↔ 0 < -f
⊢ ¬0 ≤ f ↔ f < 0

Tactic:
simp_all
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
inl :
  ∀ (hi : j ∈ b.support),
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) j : M) ∉
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
inr :
  ∀ (hij : j ≠ i),
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
⊢ HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)

Tactic:
rcases eq_or_ne j i with rfl | hij

Premises used: eq_or_ne, rfl
-- 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
j : ι
hj hi : j ∈ b.support
⊢ HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)

Tactic:
simpa only [sub_self, mem_range, not_exists] using fun k ↦ P.ne_zero k

Premises used: Set.mem_range, RootPairing.ne_zero, sub_self, not_exists
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
⊢ {i, j} ⊆ b.support

Tactic:
aesop (add simp Finset.insert_subset_iff)

Premises used: Finset.insert_subset_iff
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
⊢ {i, j} ⊆ b.support

Tactic:
have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
⊢ {i, j} ⊆ b.support

Tactic:
lia
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
⊢ ∀ x ∈ b.support, x ∉ {i, j} → HSMul.hSMul (β := M) (f x) ((P.root : (a : ι) → M) x : M) = 0

Tactic:
aesop
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
⊢ i ∉ {j}

Tactic:
grind
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
rw :
  HSMul.hSMul (β := M) (f i) ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)

Tactic:
rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop),
      Finset.sum_insert (by grind), Finset.sum_singleton]

Premises used: Finset.sum_singleton, Finset.sum_subset, Finset.sum_insert
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
⊢ HSMul.hSMul (β := M) (f i) ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)

Tactic:
simp [f, hij, sub_eq_add_neg]

Premises used: sub_eq_add_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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
⊢ ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)

Tactic:
have hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j := by
    have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
    rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop),
      Finset.sum_insert (by grind), Finset.sum_singleton]
    simp [f, hij, sub_eq_add_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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
hf :
  ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
contra rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ 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))

Tactic:
rwa [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
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
hf :
  ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
contra :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ Function.support f ⊆ (↑b.support : Set ι)

Tactic:
aesop
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
hf :
  ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
contra :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
inr : ∀ (pos : 0 < f), False
inr₁ : ∀ (neg : f < 0), False
⊢ False

Tactic:
rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg

Premises used: RootPairing.Base.pos_or_neg_of_sum_smul_root_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
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
hf :
  ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
contra :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
pos : 0 < f
⊢ False

Tactic:
simpa [hij, f] using le_of_lt pos j

Premises used: le_of_lt
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
hf :
  ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
contra :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
neg : f < 0
⊢ False

Tactic:
simpa [hij, f] using le_of_lt neg i

Premises used: le_of_lt
-- 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 j : ι
hi : i ∈ b.support
hj : j ∈ b.support
⊢ HSub.hSub (α := N) (β := N) ((P.coroot : (a : ι) → N) i : N) ((P.coroot : (a : ι) → N) j : N) ∉
    range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)

Tactic:
b.flip.sub_notMem_range_root hi hj

Premises used: Set.Mem, RootPairing.Base.flip, RootPairing.Base.sub_notMem_range_root
-- 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 : IsDomain R
inst_7 : P.IsCrystallographic
inst_8 : Finite ι
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
by_contra! : ∀ (h : 0 < P.pairingIn ℤ i j), False
⊢ P.pairingIn ℤ i j ≤ 0

Tactic:
by_contra! h
-- 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 : IsDomain R
inst_7 : P.IsCrystallographic
inst_8 : Finite ι
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
h : 0 < P.pairingIn ℤ i j
⊢ False

Tactic:
b.sub_notMem_range_root hi hj <| P.root_sub_root_mem_of_pairingIn_pos h hij

Premises used: RootPairing.root_sub_root_mem_of_pairingIn_pos, RootPairing.Base.sub_notMem_range_root
-- 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 : IsDomain R
inst_7 : P.IsCrystallographic
inst_8 : Finite ι
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
h : 0 < P.pairingIn ℤ i j
⊢ False

Tactic:
exact b.sub_notMem_range_root hi hj <| P.root_sub_root_mem_of_pairingIn_pos h hij

Premises used: RootPairing.root_sub_root_mem_of_pairingIn_pos, RootPairing.Base.sub_notMem_range_root
-- 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 : IsDomain R
inst_7 : P.IsCrystallographic
inst_8 : Finite ι
i j : ↥b.support
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) (↑j : ι) = 0

Tactic:
chainBotCoeff_eq_zero_iff.mpr <| Or.inr <| b.sub_notMem_range_root j.property i.property

Premises used: Iff.mpr, RootPairing.Base.sub_notMem_range_root, RootPairing.chainBotCoeff_eq_zero_iff, Or.inr, Subtype.property
-- 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 : IsDomain R
inst_7 : P.IsCrystallographic
inst_8 : Finite ι
i j : ↥b.support
hij : i ≠ j
rw :
  (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) (↑j : ι)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) (↑j : ι)) : ℤ)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) (↑j : ι)) : ℤ)
⊢ (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) (↑j : ι)) : ℤ) =
    -P.pairingIn ℤ (↑j : ι) (↑i : ι)

Tactic:
rw [← chainTopCoeff_sub_chainBotCoeff (b.linearIndependent_pair_of_ne hij)]

Premises used: RootPairing.Base.linearIndependent_pair_of_ne, RootPairing.chainTopCoeff_sub_chainBotCoeff