-- Mathlib/Algebra/Lie/Submodule.lean
theorem coe_map_of_surjective (h : Function.Surjective f) :
    LieSubmodule.toSubmodule (I.map f) = (LieSubmodule.toSubmodule I).map (f : L →ₗ[R] L')

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
x y : L'
hy : y ∈ __src✝.carrier
⊢ ⁅x, y⁆ ∈ __src✝.carrier

Tactic:
have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [hy]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
x y : L'
hy : y ∈ __src✝.carrier
hy' : ∃ x ∈ I, f x = y
⊢ ⁅x, y⁆ ∈ __src✝.carrier

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ∃ N, ↑N = Submodule.map ↑f ↑I

Tactic:
exact ⟨J, rfl⟩

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
⊢ ↑(map f I) = Submodule.map ↑f ↑I

Tactic:
let J : LieIdeal R L' :=
  { (I : Submodule R L).map (f : L →ₗ[R] L') with
    lie_mem := fun {x y} hy ↦ by
      have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [hy]
      obtain ⟨z₂, hz₂, rfl⟩ := hy'
      obtain ⟨z₁, rfl⟩ := h x
      simp only [LieHom.coe_toLinearMap, SetLike.mem_coe, Set.mem_image,
        LieSubmodule.mem_toSubmodule, Submodule.mem_carrier, Submodule.map_coe]
      use ⁅z₁, z₂⁆
      exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩ }

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ↑(map f I) = Submodule.map ↑f ↑I

Proof state:
case intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ __src✝.carrier
z₁ : L
⊢ ⁅f z₁, f z₂⁆ ∈ __src✝.carrier

Tactic:
simp only [LieHom.coe_toLinearMap, SetLike.mem_coe, Set.mem_image,
  LieSubmodule.mem_toSubmodule, Submodule.mem_carrier, Submodule.map_coe]

Result:
case intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ __src✝.carrier
z₁ : L
⊢ ∃ x ∈ (toLieSubalgebra R L I).toSubmodule, f x = ⁅f z₁, f z₂⁆

Proof state:
case intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
x : L'
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ __src✝.carrier
⊢ ⁅x, f z₂⁆ ∈ __src✝.carrier

Tactic:
obtain ⟨z₁, rfl⟩ := h x

Result:
case intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ __src✝.carrier
z₁ : L
⊢ ⁅f z₁, f z₂⁆ ∈ __src✝.carrier

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
x y : L'
hy : y ∈ __src✝.carrier
⊢ ∃ x ∈ I, f x = y

Tactic:
simpa [hy]

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
x y : L'
hy : y ∈ __src✝.carrier
hy' : ∃ x ∈ I, f x = y
⊢ ⁅x, y⁆ ∈ __src✝.carrier

Tactic:
obtain ⟨z₂, hz₂, rfl⟩ := hy'

Result:
case intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
x : L'
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ __src✝.carrier
⊢ ⁅x, f z₂⁆ ∈ __src✝.carrier

Proof state:
case h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ __src✝.carrier
z₁ : L
⊢ ⁅z₁, z₂⁆ ∈ (toLieSubalgebra R L I).toSubmodule ∧ f ⁅z₁, z₂⁆ = ⁅f z₁, f z₂⁆

Tactic:
exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ __src✝.carrier
z₁ : L
⊢ ∃ x ∈ (toLieSubalgebra R L I).toSubmodule, f x = ⁅f z₁, f z₂⁆

Tactic:
use ⁅z₁, z₂⁆

Result:
case h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
z₂ : L
hz₂ : z₂ ∈ I
hy : f z₂ ∈ __src✝.carrier
z₁ : L
⊢ ⁅z₁, z₂⁆ ∈ (toLieSubalgebra R L I).toSubmodule ∧ f ⁅z₁, z₂⁆ = ⁅f z₁, f z₂⁆

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ↑(map f I) = Submodule.map ↑f ↑I

Tactic:
rw [map, toLieSubalgebra_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ∃ N, ↑N = Submodule.map ↑f ↑I