-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem map_bracket_eq {I₁ I₂ : LieIdeal R L} (h : Function.Surjective f) :
    map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆

Proof state:
case h.intro.mk.intro.mk.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₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L'
h₂ : z₂ ∈ map f I₂
y₁ : ↥I₁
h₁ : f ↑y₁ ∈ map f I₁
⊢ ⁅↑⟨f ↑y₁, h₁⟩, ↑⟨z₂, h₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
obtain ⟨y₂, rfl⟩ := mem_map_of_surjective h h₂

Result:
case h.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₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
y₁ : ↥I₁
h₁ : f ↑y₁ ∈ map f I₁
y₂ : ↥I₂
h₂ : f ↑y₂ ∈ map f I₂
⊢ ⁅↑⟨f ↑y₁, h₁⟩, ↑⟨f ↑y₂, h₂⟩⁆ ∈ ⇑↑f '' {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'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
this : ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆
⊢ map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆

Tactic:
exact le_antisymm (map_bracket_le f) this

Result:
no goals

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'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆

Tactic:
suffices ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆ by exact le_antisymm (map_bracket_le f) this

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'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆

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

Tactic:
apply Submodule.span_mono

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'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ⇑↑f '' {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'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
y₁ : ↥I₁
h₁ : f ↑y₁ ∈ map f I₁
y₂ : ↥I₂
h₂ : f ↑y₂ ∈ map f I₂
⊢ ↑f ⁅↑y₁, ↑y₂⁆ = ⁅↑⟨f ↑y₁, h₁⟩, ↑⟨f ↑y₂, h₂⟩⁆

Tactic:
apply f.map_lie

Result:
no goals

Proof state:
case h.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₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
y₁ : ↥I₁
h₁ : f ↑y₁ ∈ map f I₁
y₂ : ↥I₂
h₂ : f ↑y₂ ∈ map f I₂
⊢ ⁅↑⟨f ↑y₁, h₁⟩, ↑⟨f ↑y₂, h₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
exact ⟨⁅(y₁ : L), (y₂ : L)⁆, ⟨y₁, y₂, rfl⟩, by apply f.map_lie⟩

Result:
no goals

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'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆

Tactic:
rw [← LieSubmodule.toSubmodule_le_toSubmodule, coe_map_of_surjective h,
  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'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ Submodule.span R (⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x})

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'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rintro x ⟨⟨z₁, h₁⟩, ⟨z₂, h₂⟩, rfl⟩

Result:
case h.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₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
z₁ : L'
h₁ : z₁ ∈ map f I₁
z₂ : L'
h₂ : z₂ ∈ map f I₂
⊢ ⁅↑⟨z₁, h₁⟩, ↑⟨z₂, h₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case h.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₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
z₁ : L'
h₁ : z₁ ∈ map f I₁
z₂ : L'
h₂ : z₂ ∈ map f I₂
⊢ ⁅↑⟨z₁, h₁⟩, ↑⟨z₂, h₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
obtain ⟨y₁, rfl⟩ := mem_map_of_surjective h h₁

Result:
case h.intro.mk.intro.mk.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₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L'
h₂ : z₂ ∈ map f I₂
y₁ : ↥I₁
h₁ : f ↑y₁ ∈ map f I₁
⊢ ⁅↑⟨f ↑y₁, h₁⟩, ↑⟨z₂, h₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}