-- Mathlib/Algebra/Lie/Normalizer.lean
theorem lie_mem_sup_of_mem_normalizer {x y z : L} (hx : x ∈ H.normalizer) (hy : y ∈ (R ∙ x) ⊔ ↑H)
    (hz : z ∈ (R ∙ x) ⊔ ↑H) : ⁅y, z⁆ ∈ (R ∙ x) ⊔ ↑H

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
u₁ : L
hu₁ : u₁ ∈ Submodule.span R {x}
v : L
hv : v ∈ H
u₂ : L
hu₂ : u₂ ∈ Submodule.span R {x}
w : L
hw : w ∈ H
⊢ ⁅u₁ + v, u₂ + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Tactic:
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hu₁

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
u₂ : L
hu₂ : u₂ ∈ Submodule.span R {x}
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
⊢ ⁅t • x + v, u₂ + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.refine_1
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅v, x⁆ ∈ H

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅x, w⁆ ∈ H

Tactic:
exacts [(H.mem_normalizer_iff' x).mp hx v hv, (H.mem_normalizer_iff x).mp hx w hw]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y z : L
hx : x ∈ H.normalizer
hy : y ∈ Submodule.span R {x} ⊔ H.toSubmodule
hz : z ∈ Submodule.span R {x} ⊔ H.toSubmodule
⊢ ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Tactic:
rw [Submodule.mem_sup] at hy hz

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y z : L
hx : x ∈ H.normalizer
hy : ∃ y_1 ∈ Submodule.span R {x}, ∃ z ∈ H.toSubmodule, y_1 + z = y
hz : ∃ y ∈ Submodule.span R {x}, ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
⊢ ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅t • x + v, s • x + w⁆ ∈ H.toSubmodule

Tactic:
simp only [LieSubalgebra.mem_toSubmodule, smul_lie, add_lie, zero_add, lie_add, smul_zero,
  lie_smul, lie_self]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ s • ⁅v, x⁆ + (t • ⁅x, w⁆ + ⁅v, w⁆) ∈ H

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y z : L
hx : x ∈ H.normalizer
hy : ∃ y_1 ∈ Submodule.span R {x}, ∃ z ∈ H.toSubmodule, y_1 + z = y
hz : ∃ y ∈ Submodule.span R {x}, ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
⊢ ⁅y, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Tactic:
obtain ⟨u₁, hu₁, v, hv : v ∈ H, rfl⟩ := hy

Result:
case intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x z : L
hx : x ∈ H.normalizer
hz : ∃ y ∈ Submodule.span R {x}, ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
u₁ : L
hu₁ : u₁ ∈ Submodule.span R {x}
v : L
hv : v ∈ H
⊢ ⁅u₁ + v, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
u₂ : L
hu₂ : u₂ ∈ Submodule.span R {x}
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
⊢ ⁅t • x + v, u₂ + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Tactic:
obtain ⟨s, rfl⟩ := Submodule.mem_span_singleton.mp hu₂

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅t • x + v, s • x + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ s • ⁅v, x⁆ + (t • ⁅x, w⁆ + ⁅v, w⁆) ∈ H

Tactic:
refine H.add_mem (H.smul_mem s ?_) (H.add_mem (H.smul_mem t ?_) (H.lie_mem hv hw))

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.refine_1
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅v, x⁆ ∈ H

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a.refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅x, w⁆ ∈ H

Proof state:
case intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x z : L
hx : x ∈ H.normalizer
hz : ∃ y ∈ Submodule.span R {x}, ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
u₁ : L
hu₁ : u₁ ∈ Submodule.span R {x}
v : L
hv : v ∈ H
⊢ ⁅u₁ + v, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Tactic:
obtain ⟨u₂, hu₂, w, hw : w ∈ H, rfl⟩ := hz

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
u₁ : L
hu₁ : u₁ ∈ Submodule.span R {x}
v : L
hv : v ∈ H
u₂ : L
hu₂ : u₂ ∈ Submodule.span R {x}
w : L
hw : w ∈ H
⊢ ⁅u₁ + v, u₂ + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅t • x + v, s • x + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule

Tactic:
apply Submodule.mem_sup_right

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ Submodule.span R {x}
s : R
hu₂ : s • x ∈ Submodule.span R {x}
⊢ ⁅t • x + v, s • x + w⁆ ∈ H.toSubmodule