-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem comap_bracket_eq {J₁ J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) :
    comap f ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ⁅comap f J₁, comap f J₂⁆ ⊔ f.ker

Proof state:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
y x₁ : L'
hx₁ : x₁ ∈ f.idealRange ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ f.idealRange ⊓ J₂
hy : ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ = y
z₁ : L
hz₁' : f z₁ ∈ J₁
hz₁ : f z₁ = x₁
hz₂' : x₂ ∈ J₂
z₂ : L
hz₂ : f z₂ = x₂
⊢ ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ ∈ (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rw [← hz₂] at hz₂'

Result:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
y x₁ : L'
hx₁ : x₁ ∈ f.idealRange ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ f.idealRange ⊓ J₂
hy : ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ = y
z₁ : L
hz₁' : f z₁ ∈ J₁
hz₁ : f z₁ = x₁
z₂ : L
hz₂' : f z₂ ∈ J₂
hz₂ : f z₂ = x₂
⊢ ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ ∈ (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
simp only [LieHom.coe_toLinearMap, Set.mem_setOf_eq]

Result:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
y x₁ : L'
hx₁ : x₁ ∈ f.idealRange ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ f.idealRange ⊓ J₂
hy : ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ = y
z₁ : L
hz₁' : f z₁ ∈ J₁
hz₁ : f z₁ = x₁
z₂ : L
hz₂' : f z₂ ∈ J₂
hz₂ : f z₂ = x₂
⊢ ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ ∈ (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
refine ⟨⁅z₁, z₂⁆, ⟨⟨z₁, hz₁'⟩, ⟨z₂, hz₂'⟩, rfl⟩, ?_⟩

Result:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
y x₁ : L'
hx₁ : x₁ ∈ f.idealRange ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ f.idealRange ⊓ J₂
hy : ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, 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₂⁆ = ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆

Proof state:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ comap f ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ⁅comap f J₁, comap f J₂⁆ ⊔ f.ker

Tactic:
rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule,
  LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, ← Submodule.comap_map_eq,
  LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.lieIdeal_oper_eq_linear_span,
  LinearMap.map_span]

Result:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ Submodule.comap (↑f) (Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) =
    Submodule.comap (↑f) (Submodule.span R (⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}))

Proof state:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
ext y

Result:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
y : L'
⊢ y ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ y ∈ (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
y x₁ : L'
hx₁ : x₁ ∈ f.idealRange ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ f.idealRange ⊓ J₂
hy : ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ = y
⊢ y ∈ (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rw [← hy]

Result:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
y x₁ : L'
hx₁ : x₁ ∈ f.idealRange ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ f.idealRange ⊓ J₂
hy : ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ = y
⊢ ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ ∈ (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
y x₁ : L'
hx₁ : x₁ ∈ f.idealRange ⊓ J₁
x₂ : L'
hx₂ : x₂ ∈ f.idealRange ⊓ J₂
hy : ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ = y
⊢ ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆ ∈ (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rw [LieSubmodule.mem_inf, f.mem_idealRange_iff h] at hx₁ hx₂

Result:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
y x₁ : L'
hx₁✝ : x₁ ∈ f.idealRange ⊓ J₁
hx₁ : (∃ x, f x = x₁) ∧ x₁ ∈ J₁
x₂ : L'
hx₂✝ : x₂ ∈ f.idealRange ⊓ J₂
hx₂ : (∃ x, f x = x₂) ∧ x₂ ∈ J₂
hy : ⁅↑⟨x₁, hx₁✝⟩, ↑⟨x₂, hx₂✝⟩⁆ = y
⊢ ⁅↑⟨x₁, hx₁✝⟩, ↑⟨x₂, hx₂✝⟩⁆ ∈ (fun a => f a) '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
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 : ⁅↑⟨z₁, hz₁⟩, ↑⟨z₂, hz₂⟩⁆ = x
hz₁' : f z₁ ∈ f.idealRange ⊓ J₁
hz₂' : f z₂ ∈ f.idealRange ⊓ J₂
⊢ (fun a => f a) ⁅↑⟨z₁, hz₁⟩, ↑⟨z₂, hz₂⟩⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
use ⟨f z₁, hz₁'⟩, ⟨f z₂, hz₂'⟩

Result:
case 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'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
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 : ⁅↑⟨z₁, hz₁⟩, ↑⟨z₂, hz₂⟩⁆ = x
hz₁' : f z₁ ∈ f.idealRange ⊓ J₁
hz₂' : f z₂ ∈ f.idealRange ⊓ J₂
⊢ ⁅↑⟨f z₁, hz₁'⟩, ↑⟨f z₂, hz₂'⟩⁆ = (fun a => f a) ⁅↑⟨z₁, hz₁⟩, ↑⟨z₂, hz₂⟩⁆