-- 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
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x
mem :
  ∀ (u : L) (hu : u ∈ range b.e),
    Membership.mem (γ := 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)))
      u
zero :
  Membership.mem (γ := 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)))
    0
add :
  ∀ (x y : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x →
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) y →
        ∀
          (hu :
            Membership.mem (γ := 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)))
              x)
          (hv :
            Membership.mem (γ := 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)))
              y),
          Membership.mem (γ := 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)))
            (x + y)
smul :
  ∀ (t : R) (x : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) x →
      ∀
        (hu :
          Membership.mem (γ := 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)))
            x),
        Membership.mem (γ := 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)))
          (t • x)
lie :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u →
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v →
        ∀
          (hu :
            Membership.mem (γ := 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)))
              u)
          (hv :
            Membership.mem (γ := 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)))
              v),
          Membership.mem (γ := 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)))
            ⁅u, v⁆
⊢ Membership.mem (γ := 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)))
    x

Tactic:
induction hx using lieSpan_induction with
  | mem u hu =>
    obtain ⟨i, rfl⟩ := hu
    apply LieSubmodule.mem_iSup_of_mem (Pi.single i 1)
    simp only [ne_eq, Pi.single_eq_zero_iff, one_ne_zero, not_false_eq_true, nsmul_eq_mul, iSup_pos,
      LieModule.mem_genWeightSpace, Finset.sum_apply, Pi.mul_apply, Pi.natCast_apply,
      Subtype.forall, toEnd_mk]
    exact fun y hy ↦ ⟨1, by simp [Pi.single_apply]⟩
  | zero => simp
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    let s : Set (b.cartan → R) := {χ | ∃ n : ι → ℕ, n ≠ 0 ∧ χ = ∑ i, n i • b.baseSupp i}
    have hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s := by
      rintro - ⟨n₁, hn₁, rfl⟩ - ⟨n₂, hn₂, rfl⟩
      refine ⟨n₁ + n₂, by simp [hn₁], ?_⟩
      ext; simp [add_smul, Finset.sum_add_distrib]
    let e : {n : ι → ℕ | n ≠ 0} ≃ s :=
      .ofBijective (fun n ↦ ⟨∑ i, n.val i • b.baseSupp i, n.val, n.property, by ext; simp⟩) <| by
      refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
      · ext i
        have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
        refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i
        ext v
        rw [Subtype.mk.injEq] at h
        simpa using congr_fun h v
      · use ⟨χ.property.choose, χ.property.choose_spec.1⟩
        ext i
        simpa using congr_fun χ.property.choose_spec.2.symm i
    replace hu : u ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hu; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    replace hv : v ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace b.cartan χ := by
      convert! hv; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    convert! mem_biSup_genWeightSpace_of hs hu hv
    rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl

Premises used: Pi.mul_apply, iSup_subtype', LieModule.mem_genWeightSpace, Finset.sum_apply, LieSubalgebra.toEnd_mk, Subtype.forall, iSup_pos, Pi.natCast_apply, ne_eq, nsmul_eq_mul, Pi.single_eq_zero_iff, one_ne_zero, not_false_eq_true, rfl