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_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 : ι)
suffices :
  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:
suffices ∑ j, f' j • P.root j = ∑ j ∈ b.support, f j • P.root j by rwa [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
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 : ι)
rw :
  Eq.{u_3 + 1} (α := M) (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
    (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (f (↑i : ι)) ((P.root : (a : ι) → M) (↑i : ι) : 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:
rw [← b.support.sum_finset_coe]

Premises used: RootPairing.Base.support, Finset.sum_finset_coe
-- 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 : ι)
⊢ Eq.{u_3 + 1} (α := M) (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
    (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (f (↑i : ι)) ((P.root : (a : ι) → M) (↑i : ι) : M))

Tactic:
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
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 : ι)
⊢ 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:
replace hf : ∑ j, f' j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support) := by
    suffices ∑ j, f' j • P.root j = ∑ j ∈ b.support, f j • P.root j by rwa [this]
    rw [← b.support.sum_finset_coe]; 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
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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
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))
⊢ ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℕ),
    Eq.{u_3 + 1} (α := M)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (c i) ((P.root : (a : ι) → M) (↑i : ι) : M))
      (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))

Tactic:
rw [← span_nat_eq_addSubmonoidClosure, mem_toAddSubmonoid,
    Fintype.mem_span_image_iff_exists_fun] at hf

Premises used: Fintype.mem_span_image_iff_exists_fun, Submodule.mem_toAddSubmonoid, Submodule.span_nat_eq_addSubmonoidClosure
-- 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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
hf :
  ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℕ),
    Eq.{u_3 + 1} (α := M)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (c i) ((P.root : (a : ι) → M) (↑i : ι) : M))
      (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
obtain :
  ∀ (c : (↑(↑b.support : Set ι) : Type u_1) → ℕ)
    (hc :
      Eq.{u_3 + 1} (α := M)
        (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (c i) ((P.root : (a : ι) → M) (↑i : ι) : M))
        (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))),
    0 < f
⊢ 0 < f

Tactic:
obtain ⟨c, hc⟩ := 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_1 : ι → ℤ
hf :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc :
  Eq.{u_3 + 1} (α := M)
    (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (c i) ((P.root : (a : ι) → M) (↑i : ι) : M))
    (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
i : ↥b.support
⊢ Eq.{u_3 + 1} (α := M)
    (∑ i : (↑(↑b.support : Set ι) : Type u_1),
      HSMul.hSMul (β := M) ((Int.ofNat ∘ c) i) ((P.root : (a : ι) → M) (↑i : ι) : M))
    (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (f' 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
f_1 : ι → ℤ
hf :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc :
  Eq.{u_3 + 1} (α := M)
    (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (c i) ((P.root : (a : ι) → M) (↑i : ι) : M))
    (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
⊢ ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i

Tactic:
replace hc (i : b.support) : c i = f' i := Fintype.linearIndependent_iffₛ.mp
    (b.linearIndepOn_root.restrict_scalars' ℤ) (Int.ofNat ∘ c) f' (by simpa) i
-- 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 :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
pos : ∀ (hi : i ∈ b.support), 0 i ≤ f i
neg : ∀ (hi : i ∉ b.support), 0 i ≤ f i
⊢ 0 i ≤ f i

Tactic:
by_cases hi : i ∈ b.support

Premises used: 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
f_1 : ι → ℤ
hf :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∈ b.support
pos : 0 ≤ f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i hi)
⊢ 0 i ≤ f i

Tactic:
change 0 ≤ f' ⟨i, hi⟩

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
f_1 : ι → ℤ
hf :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∈ b.support
⊢ 0 ≤ f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i hi)

Tactic:
simp [← hc]
-- 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 :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∉ b.support
contrapose : ∀ (hi : i ∈ Function.support f), i ∈ b.support
⊢ i ∉ Function.support f

Tactic:
contrapose hi
-- 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 :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∈ Function.support f
⊢ i ∈ b.support

Tactic:
hf₀ hi
-- 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 :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∈ Function.support f
⊢ i ∈ b.support

Tactic:
exact hf₀ hi
-- 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 :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∉ b.support
⊢ i ∉ Function.support f

Tactic:
replace hi : i ∉ f.support := by contrapose hi; exact hf₀ hi
-- 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 :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∉ Function.support f
⊢ 0 i ≤ f i

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
f_1 : ι → ℤ
hf :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
⊢ 0 ≤ f

Tactic:
have aux : 0 ≤ f := by
    intro i
    by_cases hi : i ∈ b.support
    · change 0 ≤ f' ⟨i, hi⟩
      simp [← hc]
    · replace hi : i ∉ f.support := by contrapose hi; exact hf₀ hi
      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
f_1 : ι → ℤ
hf :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
aux : 0 ≤ f
⊢ 0 < f

Tactic:
Pi.lt_def.mpr ⟨aux, ?_⟩

Premises used: Iff.mpr, Pi.lt_def, And.intro
-- 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 :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
aux : 0 ≤ f
refine : ∃ (i : ι), 0 i < f i
⊢ 0 < f

Tactic:
refine Pi.lt_def.mpr ⟨aux, ?_⟩

Premises used: Iff.mpr, Pi.lt_def, And.intro
-- 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 :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
aux : 0 ≤ f
by_contra! : ∀ (contra : ∀ (i : ι), f i ≤ 0 i), False
⊢ ∃ (i : ι), 0 i < 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
f_1 : ι → ℤ
hf :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
aux : 0 ≤ f
contra : ∀ (i : ι), f i ≤ 0 i
⊢ f = 0

Tactic:
replace contra : f = 0 := le_antisymm contra aux
-- 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 :
  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₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
aux : 0 ≤ f
contra : f = 0
⊢ False

Tactic:
contradiction
-- 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 : ¬f ≤ 0 ↔ 0 ≤ f ∧ ∃ (i : ι), 0 i < f i
⊢ ¬f ≤ 0 ↔ 0 < f

Tactic:
rw [Pi.lt_def]

Premises used: Pi.lt_def
-- 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_1 : 0 ≤ f ∧ ∃ (i : ι), 0 i < f i
contra : f ≤ 0
h : 0 ≤ f
i : ι
hi : 0 i < f i
⊢ False

Tactic:
simp [le_antisymm contra h] at hi

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

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, ⟨i, hi⟩⟩ contra ↦ by simp [le_antisymm contra h] at hi⟩
-- 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_1 : ∀ (h' : 0 < f), 0 ≤ f
refine_1₁ : ∀ (h' : f < 0), 0 ≤ f
⊢ 0 ≤ f

Tactic:
rcases b.pos_or_neg_of_sum_smul_root_mem f hf hf₀ with h' | h'

Premises used: RootPairing.Base.pos_or_neg_of_sum_smul_root_mem