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

Tactic:
exact ⟨f.mem_idealRange z₁, hz₁⟩

Result:
no goals

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

Tactic:
rintro ⟨x, ⟨⟨z₁, hz₁⟩, ⟨z₂, hz₂⟩, hx⟩, hy⟩

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

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

Tactic:
obtain ⟨⟨z₁, hz₁⟩, hz₁'⟩ := hx₁

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
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
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:
constructor

Result:
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}

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

Tactic:
rw [← hy, ← hx]

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
⊢ (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
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₂

Tactic:
exact ⟨f.mem_idealRange z₂, hz₂⟩

Result:
no goals

Proof state:
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₂⟩⁆

Tactic:
simp only [Submodule.coe_mk, LieHom.map_lie]

Result:
no goals

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₂
⊢ (fun a => f a) ⁅z₁, z₂⁆ = ⁅↑⟨x₁, hx₁⟩, ↑⟨x₂, hx₂⟩⁆

Tactic:
simp only [hz₁, hz₂, Submodule.coe_mk, LieHom.map_lie]

Result:
no goals