awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
⊢ Disjoint sU sV

Tactic:
Set.disjoint_iff_forall_ne.mpr fun f hf g hg ↦ ?_

Premises used: Iff.mpr, Set.disjoint_iff_forall_ne
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
refine : ∀ (f : ↥b.cartan → R) (hf : f ∈ sU) (g : ↥b.cartan → R) (hg : g ∈ sV), f ≠ g
⊢ Disjoint sU sV

Tactic:
refine Set.disjoint_iff_forall_ne.mpr fun f hf g hg ↦ ?_

Premises used: Iff.mpr, Set.disjoint_iff_forall_ne
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥b.cartan → R
hf : f ∈ sU
hg : f ∈ sV
⊢ ∃ (n : ι → ℕ), n ≠ 0 ∧ f = -(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)

Tactic:
simpa [hsU] using hf
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥b.cartan → R
hf : f ∈ sU
hg : f ∈ sV
obtain : ∀ (n : ι → ℕ) (hn : n ≠ 0) (hn' : f = -(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)), False
⊢ False

Tactic:
obtain ⟨n, hn, hn'⟩ : ∃ n : ι → ℕ, n ≠ 0 ∧ f = -∑ i, n i • b.baseSupp i := by
      simpa [hsU] using hf
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥b.cartan → R
hf : f ∈ sU
hg : f ∈ sV
n : ι → ℕ
hn : n ≠ 0
hn' : f = -(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)
⊢ ∃ (m : ι → ℕ), m ≠ 0 ∧ f = (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R)

Tactic:
simpa [hsV] using hg
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥b.cartan → R
hf : f ∈ sU
hg : f ∈ sV
n : ι → ℕ
hn : n ≠ 0
hn' : f = -(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)
obtain :
  ∀ (m : ι → ℕ) (hm : m ≠ 0) (hf : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sU)
    (hg : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sV)
    (hn' :
      Eq (α := ↥b.cartan → R) (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R)
        (-(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R))),
    False
⊢ False

Tactic:
obtain ⟨m, hm, rfl⟩ : ∃ m : ι → ℕ, m ≠ 0 ∧ f = ∑ i, m i • b.baseSupp i := by
      simpa [hsV] using hg

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sU
hg : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sV
hn' :
  Eq (α := ↥b.cartan → R) (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R)
    (-(⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R))
⊢ HAdd.hAdd (α := ↥b.cartan → R) (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R)
      (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R) =
    0

Tactic:
rw [eq_neg_iff_add_eq_zero] at hn'

Premises used: eq_neg_iff_add_eq_zero
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sU
hg : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sV
hn' :
  HAdd.hAdd (α := ↥b.cartan → R) (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R)
      (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R) =
    0
⊢ Eq (α := (a : ↥b.cartan) → R)
    (⇑(HAdd.hAdd (α := Dual.{u_2, u_3} R ↥b.cartan) (∑ i : ι, m i • b.baseSupp i) (∑ i : ι, n i • b.baseSupp i)) :
      (a : ↥b.cartan) → R)
    0

Tactic:
change ⇑(∑ i, m i • b.baseSupp i + ∑ i, n i • b.baseSupp i) = 0 at hn'

Premises used: LieAlgebra.Basis.baseSupp, Finset.univ, HAdd.hAdd, HSMul.hSMul, Finset.sum
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sU
hg : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sV
hn' :
  Eq (α := (a : ↥b.cartan) → R)
    (⇑(HAdd.hAdd (α := Dual.{u_2, u_3} R ↥b.cartan) (∑ i : ι, m i • b.baseSupp i) (∑ i : ι, n i • b.baseSupp i)) :
      (a : ↥b.cartan) → R)
    0
⊢ Eq (α := LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥b.cartan) R)
    (∑ x : ι, HSMul.hSMul (α := R) (↑((m + n) x) : R) (b.baseSupp x)) 0

Tactic:
simp_rw [LinearMap.coe_zero_iff, ← Finset.sum_add_distrib, ← add_smul, ← Pi.add_apply,
        ← Nat.cast_smul_eq_nsmul R] at hn'

Premises used: Finset.sum_add_distrib, Pi.add_apply, add_smul, Nat.cast_smul_eq_nsmul, LinearMap.coe_zero_iff
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sU
hg : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sV
hn' :
  Eq (α := LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥b.cartan) R)
    (∑ x : ι, HSMul.hSMul (α := R) (↑((m + n) x) : R) (b.baseSupp x)) 0
⊢ Eq (α := Dual.{u_2, u_3} R ↥b.cartan) (∑ i : ι, HSMul.hSMul (α := R) ((Nat.cast ∘ (m + n)) i) (b.baseSupp i)) 0

Tactic:
hn'
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : Fintype ι
inst_5 : IsDomain R
inst_6 : CharZero R
inst_7 : IsTorsionFree R L
U : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan
        (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
hU :
  U =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑((-b.baseSupp) i) : (a : ↥b.cartan) → R))
V : LieSubmodule R (↥b.cartan) L :=
  ⨆ (n : ι → ℕ),
    ⨆ (_ : n ≠ 0),
      rootSpace b.cartan (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
hV :
  V =
    ⨆ (n : ι → ℕ),
      ⨆ (_ : n ≠ 0),
        rootSpace b.cartan
          (∑ i : ι, HSMul.hSMul (β := (a : ↥b.cartan) → R) (n i) (⇑(b.baseSupp i) : (a : ↥b.cartan) → R))
s0 : Set (↥b.cartan → R) := {0}
hs0 : s0 = {0}
sU : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
hsU : sU = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • (-b.baseSupp) i) : (a : ↥b.cartan) → R)}
sV : Set (↥b.cartan → R) :=
  {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hsV : sV = {f : ↥b.cartan → R | ∃ (n : ι → ℕ), n ≠ 0 ∧ f = (⇑(∑ i : ι, n i • b.baseSupp i) : (a : ↥b.cartan) → R)}
hs0' : rootSpace b.cartan 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
n : ι → ℕ
hn : n ≠ 0
m : ι → ℕ
hm : m ≠ 0
hf : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sU
hg : (⇑(∑ i : ι, m i • b.baseSupp i) : (a : ↥b.cartan) → R) ∈ sV
hn' :
  Eq (α := LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥b.cartan) R)
    (∑ x : ι, HSMul.hSMul (α := R) (↑((m + n) x) : R) (b.baseSupp x)) 0
⊢ Eq (α := Dual.{u_2, u_3} R ↥b.cartan) (∑ i : ι, HSMul.hSMul (α := R) ((Nat.cast ∘ (m + n)) i) (b.baseSupp i)) 0

Tactic:
exact hn'