case intro
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ↑f
h₂ : IsLieAbelian L₁
y : L₂
u : L₁
⊢ ⁅↑f u, y⁆ = 0
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ↑f
h₂ : IsLieAbelian L₁
x y : L₂
⊢ ⁅x, y⁆ = 0
obtain ⟨u, rfl⟩ := h₁ x
case intro.intro
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ↑f
h₂ : IsLieAbelian L₁
u v : L₁
⊢ ⁅↑f u, ↑f v⁆ = 0
case intro
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ↑f
h₂ : IsLieAbelian L₁
y : L₂
u : L₁
⊢ ⁅↑f u, y⁆ = 0
obtain ⟨v, rfl⟩ := h₁ y
no goals
case intro.intro
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective ↑f
h₂ : IsLieAbelian L₁
u v : L₁
⊢ ⁅↑f u, ↑f v⁆ = 0
rw [← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]