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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
refine_2 :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x →
    ∀
      (hy :
        Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
          y),
      (∃ (f : ι → ℕ),
          Function.support f ⊆ (↑b.support : Set ι) ∧
            x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
        (∃ (f : ι → ℕ),
            Function.support f ⊆ (↑b.support : Set ι) ∧
              y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
          ∃ (f : ι → ℕ),
            Function.support f ⊆ (↑b.support : Set ι) ∧
              x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
⊢ ∀
    (hx :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x)
    (hy :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y),
    (∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
      (∃ (f : ι → ℕ),
          Function.support f ⊆ (↑b.support : Set ι) ∧
            y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
        ∃ (f : ι → ℕ),
          Function.support f ⊆ (↑b.support : Set ι) ∧
            x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)

Tactic:
_
-- 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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
refine_2 :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y →
    (∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
      (∃ (f : ι → ℕ),
          Function.support f ⊆ (↑b.support : Set ι) ∧
            y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
        ∃ (f : ι → ℕ),
          Function.support f ⊆ (↑b.support : Set ι) ∧
            x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
⊢ ∀
    (hy :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y),
    (∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
      (∃ (f : ι → ℕ),
          Function.support f ⊆ (↑b.support : Set ι) ∧
            y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
        ∃ (f : ι → ℕ),
          Function.support f ⊆ (↑b.support : Set ι) ∧
            x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)

Tactic:
_
-- 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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y
refine_2 :
  ∀ (f : ι → ℕ) (hf : Function.support f ⊆ (↑b.support : Set ι))
    (hf' : x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)),
    (∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
⊢ (∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
    (∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)

Tactic:
⟨f, 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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' : x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
refine_2 :
  ∀ (g : ι → ℕ) (hg : Function.support g ⊆ (↑b.support : Set ι))
    (hg' : y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M)),
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
⊢ (∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)

Tactic:
⟨g, hg, hg'⟩
-- 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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' : x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
g : ι → ℕ
hg : Function.support g ⊆ (↑b.support : Set ι)
hg' : y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M)
⊢ x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) ((f + g) j) ((P.root : (a : ι) → M) j : M)

Tactic:
simp [hf', hg', add_smul, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, add_smul
-- 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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' : x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
g : ι → ℕ
hg : Function.support g ⊆ (↑b.support : Set ι)
hg' : y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M)
refine_2 : Function.support (f + g) ⊆ (↑b.support : Set ι)
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)

Tactic:
refine ⟨f + g, ?_, by simp [hf', hg', add_smul, Finset.sum_add_distrib]⟩
-- 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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' : x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
g : ι → ℕ
hg : Function.support g ⊆ (↑b.support : Set ι)
hg' : y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M)
⊢ Function.support (f + g) ⊆ (↑b.support : Set ι)

Tactic:
(support_add f g).trans <| union_subset_iff.mpr ⟨hf, hg⟩

Premises used: Iff.mpr, Set.union_subset_iff, HasSubset.Subset.trans, Function.support_add, 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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' : x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
g : ι → ℕ
hg : Function.support g ⊆ (↑b.support : Set ι)
hg' : y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M)
⊢ Function.support (f + g) ⊆ (↑b.support : Set ι)

Tactic:
exact (support_add f g).trans <| union_subset_iff.mpr ⟨hf, hg⟩

Premises used: Iff.mpr, Set.union_subset_iff, HasSubset.Subset.trans, Function.support_add, 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
i : ι
inl :
  ∀ (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)),
    ∃ (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)
inr :
  ∀ (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)),
    ∃ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨f, hf, hf' | hf'⟩ := b.exists_root_eq_sum_nat_or_neg i

Premises used: RootPairing.Base.exists_root_eq_sum_nat_or_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)
⊢ Function.support (M := ℤ) (Nat.cast ∘ 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
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)
x : ι
⊢ LE.le (α := (fun (i : ι) ↦ ℤ) x) (0 x) ((Nat.cast ∘ f) 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 : ι → ℕ
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)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (α := ℤ) (β := M) ((Nat.cast ∘ f) j) ((P.root : (a : ι) → M) j : M) : M)

Tactic:
simp [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 : ι
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)
inl : ∃ (i : ι), LT.lt (α := ℤ) (0 i) ((Nat.cast ∘ f) i)
⊢ ∃ (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)

Tactic:
refine ⟨Nat.cast ∘ f, by simpa, Or.inl <| Pi.lt_def.mpr ⟨fun _ ↦ by simp, ?_⟩, by simp [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 : ι
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)
inl : ∀ (contra : ∀ (i : ι), LE.le (α := ℤ) ((Nat.cast ∘ f) i) (0 i)), False
⊢ ∃ (i : ι), LT.lt (α := ℤ) (0 i) ((Nat.cast ∘ 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)
contra : ∀ (i : ι), LE.le (α := ℤ) ((Nat.cast ∘ f) i) (0 i)
h : ∀ (i : ι), f i = 0 i
⊢ f = 0

Tactic:
ext 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
i_1 : ι
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i_1 : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
contra : ∀ (i : ι), LE.le (α := ℤ) ((Nat.cast ∘ f) i) (0 i)
i : ι
⊢ f i = 0 i

Tactic:
simpa using contra 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
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 : ∀ (i : ι), LE.le (α := ℤ) ((Nat.cast ∘ f) i) (0 i)
⊢ f = 0

Tactic:
replace contra : f = 0 := by ext i; simpa using contra 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
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 : ι → ℕ
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)
⊢ Function.support (M := ℤ) (-Nat.cast ∘ 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
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)
x : ι
⊢ LE.le (α := (fun (i : ι) ↦ ℤ) x) ((-Nat.cast ∘ f) x) (0 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 : ι → ℕ
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)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    (∑ j ∈ b.support, HSMul.hSMul (α := ℤ) (β := M) ((-Nat.cast ∘ f) j) ((P.root : (a : ι) → M) j : M) : M)

Tactic:
simp [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 : ι
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)
inr : ∃ (i : ι), LT.lt (α := ℤ) ((-Nat.cast ∘ f) i) (0 i)
⊢ ∃ (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)

Tactic:
refine ⟨-Nat.cast ∘ f, by simpa, Or.inr <| Pi.lt_def.mpr ⟨fun _ ↦ by simp, ?_⟩, by simp [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 : ι
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)
inr : ∀ (contra : ∀ (i : ι), LE.le (α := ℤ) (0 i) ((-Nat.cast ∘ f) i)), False
⊢ ∃ (i : ι), LT.lt (α := ℤ) ((-Nat.cast ∘ f) i) (0 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)
contra : ∀ (i : ι), LE.le (α := ℤ) (0 i) ((-Nat.cast ∘ f) i)
h : ∀ (i : ι), f i = 0 i
⊢ f = 0

Tactic:
ext 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
i_1 : ι
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i_1 : M)
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
contra : ∀ (i : ι), LE.le (α := ℤ) (0 i) ((-Nat.cast ∘ f) i)
i : ι
⊢ f i = 0 i

Tactic:
simpa using contra 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
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 : ∀ (i : ι), LE.le (α := ℤ) (0 i) ((-Nat.cast ∘ f) i)
⊢ f = 0

Tactic:
replace contra : f = 0 := by ext i; simpa using contra i