R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ Submodule.comap (↑f) (Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}) =
    Submodule.comap (↑f) (Submodule.span R (↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}))
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ comap f ⁅LieHom.idealRange f ⊓ J₁, LieHom.idealRange f ⊓ J₂⁆ = ⁅comap f J₁, comap f J₂⁆ ⊔ LieHom.ker f
rw [← LieSubmodule.coe_toSubmodule_eq_iff, comap_coeSubmodule,
  LieSubmodule.sup_coe_toSubmodule, f.ker_coeSubmodule, ← Submodule.comap_map_eq,
  LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.lieIdeal_oper_eq_linear_span,
  LinearMap.map_span]
case e_p.e_s
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ Submodule.comap (↑f) (Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}) =
    Submodule.comap (↑f) (Submodule.span R (↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}))
congr
case e_p.e_s
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
simp only [LieHom.coe_toLinearMap, Set.mem_setOf_eq]
case e_p.e_s.h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
⊢ y ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ↔ y ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
ext y
case e_p.e_s.h.mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
⊢ y ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → y ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}

case e_p.e_s.h.mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
⊢ y ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → y ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
⊢ y ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ↔ y ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
constructor
case e_p.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
⊢ y ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
⊢ y ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → y ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩, hy⟩
case e_p.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
⊢ y ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rw [← hy]
case e_p.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁✝ : x₁ ∈ LieHom.idealRange f ⊓ J₁
hx₁ : (∃ x, ↑f x = x₁) ∧ x₁ ∈ J₁
x₂ : L'
hx₂✝ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hx₂ : (∃ x, ↑f x = x₂) ∧ x₂ ∈ J₂
hy : ⁅↑{ val := x₁, property := hx₁✝ }, ↑{ val := x₂, property := hx₂✝ }⁆ = y
⊢ ⁅↑{ val := x₁, property := hx₁✝ }, ↑{ val := x₂, property := hx₂✝ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
erw [LieSubmodule.mem_inf, f.mem_idealRange_iff h] at hx₁ hx₂
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂✝ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hx₂ : (∃ x, ↑f x = x₂) ∧ x₂ ∈ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂✝ }⁆ = y
hz₁' : x₁ ∈ J₁
z₁ : L
hz₁ : ↑f z₁ = x₁
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂✝ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁✝ : x₁ ∈ LieHom.idealRange f ⊓ J₁
hx₁ : (∃ x, ↑f x = x₁) ∧ x₁ ∈ J₁
x₂ : L'
hx₂✝ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hx₂ : (∃ x, ↑f x = x₂) ∧ x₂ ∈ J₂
hy : ⁅↑{ val := x₁, property := hx₁✝ }, ↑{ val := x₂, property := hx₂✝ }⁆ = y
⊢ ⁅↑{ val := x₁, property := hx₁✝ }, ↑{ val := x₂, property := hx₂✝ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
obtain ⟨⟨z₁, hz₁⟩, hz₁'⟩ := hx₁
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂✝ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hx₂ : (∃ x, ↑f x = x₂) ∧ x₂ ∈ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂✝ }⁆ = y
z₁ : L
hz₁' : ↑f z₁ ∈ J₁
hz₁ : ↑f z₁ = x₁
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂✝ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂✝ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hx₂ : (∃ x, ↑f x = x₂) ∧ x₂ ∈ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂✝ }⁆ = y
hz₁' : x₁ ∈ J₁
z₁ : L
hz₁ : ↑f z₁ = x₁
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂✝ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rw [← hz₁] at hz₁'
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
z₁ : L
hz₁' : ↑f z₁ ∈ J₁
hz₁ : ↑f z₁ = x₁
hz₂' : x₂ ∈ J₂
z₂ : L
hz₂ : ↑f z₂ = x₂
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂✝ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hx₂ : (∃ x, ↑f x = x₂) ∧ x₂ ∈ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂✝ }⁆ = y
z₁ : L
hz₁' : ↑f z₁ ∈ J₁
hz₁ : ↑f z₁ = x₁
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂✝ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
obtain ⟨⟨z₂, hz₂⟩, hz₂'⟩ := hx₂
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
z₁ : L
hz₁' : ↑f z₁ ∈ J₁
hz₁ : ↑f z₁ = x₁
z₂ : L
hz₂' : ↑f z₂ ∈ J₂
hz₂ : ↑f z₂ = x₂
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
z₁ : L
hz₁' : ↑f z₁ ∈ J₁
hz₁ : ↑f z₁ = x₁
hz₂' : x₂ ∈ J₂
z₂ : L
hz₂ : ↑f z₂ = x₂
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rw [← hz₂] at hz₂'
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
z₁ : L
hz₁' : ↑f z₁ ∈ J₁
hz₁ : ↑f z₁ = x₁
z₂ : L
hz₂' : ↑f z₂ ∈ J₂
hz₂ : ↑f z₂ = x₂
⊢ (fun a => ↑f a) ⁅z₁, z₂⁆ = ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
z₁ : L
hz₁' : ↑f z₁ ∈ J₁
hz₁ : ↑f z₁ = x₁
z₂ : L
hz₂' : ↑f z₂ ∈ J₂
hz₂ : ↑f z₂ = x₂
⊢ ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
refine ⟨⁅z₁, z₂⁆, ⟨⟨z₁, hz₁'⟩, ⟨z₂, hz₂'⟩, rfl⟩, ?_⟩
no goals
case e_p.e_s.h.mp.intro.mk.intro.mk.intro.intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y x₁ : L'
hx₁ : x₁ ∈ LieHom.idealRange f ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ LieHom.idealRange f ⊓ J₂
hy : ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆ = y
z₁ : L
hz₁' : ↑f z₁ ∈ J₁
hz₁ : ↑f z₁ = x₁
z₂ : L
hz₂' : ↑f z₂ ∈ J₂
hz₂ : ↑f z₂ = x₂
⊢ (fun a => ↑f a) ⁅z₁, z₂⁆ = ⁅↑{ val := x₁, property := hx₁ }, ↑{ val := x₂, property := hx₂ }⁆
simp only [hz₁, hz₂, Submodule.coe_mk, LieHom.map_lie]
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
⊢ y ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
⊢ y ∈ (fun a => ↑f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → y ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rintro ⟨x, ⟨⟨z₁, hz₁⟩, ⟨z₂, hz₂⟩, hx⟩, hy⟩
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
⊢ (fun a => ↑f a) ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
⊢ y ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rw [← hy, ← hx]
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
hz₁' : ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
⊢ (fun a => ↑f a) ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
⊢ (fun a => ↑f a) ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
have hz₁' : f z₁ ∈ f.idealRange ⊓ J₁ := by
  rw [LieSubmodule.mem_inf]; exact ⟨f.mem_idealRange, hz₁⟩
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
hz₁' : ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
hz₂' : ↑f z₂ ∈ LieHom.idealRange f ⊓ J₂
⊢ (fun a => ↑f a) ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
hz₁' : ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
⊢ (fun a => ↑f a) ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
have hz₂' : f z₂ ∈ f.idealRange ⊓ J₂ := by
  rw [LieSubmodule.mem_inf]; exact ⟨f.mem_idealRange, hz₂⟩
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
hz₁' : ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
hz₂' : ↑f z₂ ∈ LieHom.idealRange f ⊓ J₂
⊢ ⁅↑{ val := ↑f z₁, property := hz₁' }, ↑{ val := ↑f z₂, property := hz₂' }⁆ =
    (fun a => ↑f a) ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
hz₁' : ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
hz₂' : ↑f z₂ ∈ LieHom.idealRange f ⊓ J₂
⊢ (fun a => ↑f a) ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
use ⟨f z₁, hz₁'⟩, ⟨f z₂, hz₂'⟩
no goals
case e_p.e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
hz₁' : ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
hz₂' : ↑f z₂ ∈ LieHom.idealRange f ⊓ J₂
⊢ ⁅↑{ val := ↑f z₁, property := hz₁' }, ↑{ val := ↑f z₂, property := hz₂' }⁆ =
    (fun a => ↑f a) ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆
simp only [Submodule.coe_mk, LieHom.map_lie]
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
⊢ ↑f z₁ ∈ LieHom.idealRange f ∧ ↑f z₁ ∈ J₁
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
⊢ ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
rw [LieSubmodule.mem_inf]
no goals
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
⊢ ↑f z₁ ∈ LieHom.idealRange f ∧ ↑f z₁ ∈ J₁
exact ⟨f.mem_idealRange, hz₁⟩
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
hz₁' : ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
⊢ ↑f z₂ ∈ LieHom.idealRange f ∧ ↑f z₂ ∈ J₂
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
hz₁' : ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
⊢ ↑f z₂ ∈ LieHom.idealRange f ⊓ J₂
rw [LieSubmodule.mem_inf]
no goals
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
y : L'
x : L
hy : (fun a => ↑f a) x = y
z₁ : L
hz₁ : z₁ ∈ comap f J₁
z₂ : L
hz₂ : z₂ ∈ comap f J₂
hx : ⁅↑{ val := z₁, property := hz₁ }, ↑{ val := z₂, property := hz₂ }⁆ = x
hz₁' : ↑f z₁ ∈ LieHom.idealRange f ⊓ J₁
⊢ ↑f z₂ ∈ LieHom.idealRange f ∧ ↑f z₂ ∈ J₂
exact ⟨f.mem_idealRange, hz₂⟩