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 : IsDomain R
inst_7 : P.IsCrystallographic
inst_8 : Finite ι
i j : ↥b.support
hij : i ≠ j
⊢ (↑(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 : ι)) : ℤ)

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 : P.IsRootSystem
change :
  LE.le.{u_3} (α := Submodule R M) ⊤
    (span R
      (range.{u_3, u_1 + 1} (ι := ↥b.support)
        ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))))
⊢ LE.le.{u_3} (α := Submodule R M) ⊤
    (span R (range fun (x : (↑(↑b.support : Set ι) : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι)))

Tactic:
change ⊤ ≤ span R (range <| P.root ∘ ((↑) : b.support → ι))

Premises used: Function.comp, RootPairing.root, Submodule.span, Set.range, Subtype.val, DFunLike.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 : P.IsRootSystem
⊢ LE.le.{u_3} (α := Submodule R M) ⊤
    (span R
      (range.{u_3, u_1 + 1} (ι := ↥b.support)
        ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))))

Tactic:
simp [range_comp]

Premises used: Set.range_comp
-- 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 : P.IsRootSystem
i : ↥b.support
⊢ Eq.{u_3 + 1} (α := M) ((b.toWeightBasis : (a : ↥b.support) → M) i : M) ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
simp [toWeightBasis]

Premises used: RootPairing.Base.toWeightBasis
-- 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 : P.IsRootSystem
i : ↥b.support
⊢ Eq (α := Finsupp.{u_1, u_2} (↥b.support) R)
    ((b.toWeightBasis.repr : (a : M) → ↥b.support →₀ R) ((P.root : (a : ι) → M) (↑i : ι)) :
      Finsupp.{u_1, u_2} (↥b.support) R)
    (Finsupp.single i 1 : Finsupp.{u_1, u_2} (↥b.support) R)

Tactic:
simp [← LinearEquiv.eq_symm_apply]

Premises used: LinearEquiv.eq_symm_apply
-- 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 : P.IsRootSystem
i : ↥b.support
⊢ Eq.{u_4 + 1} (α := N) ((b.toCoweightBasis : (a : ↥b.support) → N) i : N) ((P.coroot : (a : ι) → N) (↑i : ι) : N)

Tactic:
b.flip.toWeightBasis_apply (P := P.flip) i

Premises used: Set.Mem, setOf, RootPairing.Base.flip, RootPairing.Base.toWeightBasis_apply
-- 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 : P.IsRootSystem
i : ↥b.support
⊢ Eq (α := Finsupp.{u_1, u_2} (↥b.support) R)
    ((b.toCoweightBasis.repr : (a : N) → ↥b.support →₀ R) ((P.coroot : (a : ι) → N) (↑i : ι)) :
      Finsupp.{u_1, u_2} (↥b.support) R)
    (Finsupp.single i 1 : Finsupp.{u_1, u_2} (↥b.support) R)

Tactic:
simp [← LinearEquiv.eq_symm_apply]

Premises used: LinearEquiv.eq_symm_apply
-- 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 : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
inl :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) i : M)),
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        (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) (f j) ((P.root : (a : ι) → M) j : M) : M))
inr :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) i : M)),
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        (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) (f j) ((P.root : (a : ι) → M) j : M) : M))
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (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) (f j) ((P.root : (a : ι) → M) j : M) : M))

Tactic:
rcases b.root_mem_or_neg_mem i with hi | hi

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
i : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) i : M)
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 ι) ∧
        (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) (f j) ((P.root : (a : ι) → M) j : M) : M))
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (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) (f j) ((P.root : (a : ι) → M) j : M) : M))

Tactic:
obtain ⟨f, hf, hf'⟩ := this _ 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
i : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) i : M)
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 ι) ∧
      (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) (f j) ((P.root : (a : ι) → M) j : M) : M))

Tactic:
⟨f, hf, Or.inl hf'⟩

Premises used: And.intro, Exists.intro, Or.inl
-- 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 : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) i : M)
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 ι) ∧
      (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) (f j) ((P.root : (a : ι) → M) j : M) : M))

Tactic:
exact ⟨f, hf, Or.inl 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 : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) i : 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 ι) ∧
        (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) (f j) ((P.root : (a : ι) → M) j : M) : M))
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (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) (f j) ((P.root : (a : ι) → M) j : M) : M))

Tactic:
obtain ⟨f, hf, hf'⟩ := this _ 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
i : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) i : M)
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 ι) ∧
      (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) (f j) ((P.root : (a : ι) → M) j : M) : M))

Tactic:
⟨f, hf, Or.inr hf'⟩

Premises used: And.intro, Exists.intro, Or.inr
-- 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 : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) i : M)
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 ι) ∧
      (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) (f j) ((P.root : (a : ι) → M) j : M) : M))

Tactic:
exact ⟨f, hf, Or.inr 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 : ι
suffices :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (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) (f j) ((P.root : (a : ι) → M) j : M) : M))

Tactic:
suffices ∀ m ∈ AddSubmonoid.closure (P.root '' b.support),
    ∃ f : ι → ℕ, f.support ⊆ b.support ∧ m = ∑ j ∈ b.support, f j • P.root j by
    rcases b.root_mem_or_neg_mem i with hi | hi
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inl hf'⟩
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inr 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
⊢ Function.support (M := ℕ) 0 ⊆ (↑b.support : Set ι) ∧
    Eq.{u_3 + 1} (α := M) 0 (∑ j ∈ b.support, HSMul.hSMul (α := ℕ) (β := M) (0 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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
refine_1 :
  ∀ (x : M) (h : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)) x),
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
refine_2 :
  ∀ (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 : ι → ℕ),
        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)
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)

Tactic:
refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm
-- 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
j : ι
hj : j ∈ (↑b.support : Set ι)
⊢ Function.support (M := ℕ) (Pi.single (M := fun (a : ι) ↦ ℕ) j 1) ⊆ (↑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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
j : ι
hj : j ∈ (↑b.support : Set ι)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
    (∑ j_1 ∈ b.support,
        HSMul.hSMul (α := ℕ) (β := M) (Pi.single (M := fun (a : ι) ↦ ℕ) j 1 j_1 : ℕ) ((P.root : (a : ι) → M) j_1 : M) :
      M)

Tactic:
aesop (add simp Pi.single_apply)

Premises used: Pi.single_apply
-- 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
j : ι
hj : j ∈ (↑b.support : Set ι)
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M)
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)

Tactic:
exact ⟨Pi.single j 1, by simpa, by aesop (add simp Pi.single_apply)⟩
-- 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 : M
refine_2 :
  ∀ (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 : ι → ℕ),
        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)
⊢ ∀ (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 : ι → ℕ),
        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:
_