-- 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
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₂
hx₂ : (∃ x, f x = x₂) ∧ x₂ ∈ J₂
hy : ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂✝⟩⁆ = y
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:
obtain ⟨⟨z₂, hz₂⟩, hz₂'⟩ := hx₂

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₁
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}

Proof state:
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'
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}

Tactic:
rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩, 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
⊢ y ∈ (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
⊢ (fun a => f a) ⁅↑⟨z₁, hz₁⟩, ↑⟨z₂, hz₂⟩⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
have hz₁' : f z₁ ∈ f.idealRange ⊓ J₁ := by
  rw [LieSubmodule.mem_inf]; exact ⟨f.mem_idealRange z₁, hz₁⟩

Result:
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₁
⊢ (fun a => f a) ⁅↑⟨z₁, hz₁⟩, ↑⟨z₂, hz₂⟩⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

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
⊢ 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}))

Tactic:
congr

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} = ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

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

Tactic:
rw [LieSubmodule.mem_inf]

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
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₁
⊢ f z₂ ∈ f.idealRange ∧ f z₂ ∈ J₂