-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem map_bracket_eq [LieModule R L M] : map f ⁅I, N⁆ = ⁅I, map f N⁆

Proof state:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ map f ⁅I, N⁆ = ⁅I, map f N⁆

Tactic:
rw [← toSubmodule_inj, toSubmodule_map, lieIdeal_oper_eq_linear_span,
  lieIdeal_oper_eq_linear_span, Submodule.map_span]

Result:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R (⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case e_s.h.mpr
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → m ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rintro ⟨x, ⟨m₂, hm₂ : m₂ ∈ map f N⟩, rfl⟩

Result:
case e_s.h.mpr.intro.intro.mk
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
x : ↥I
m₂ : M₂
hm₂ : m₂ ∈ map f N
⊢ ⁅↑x, ↑⟨m₂, hm₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case e_s.h
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
⊢ m ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
constructor

Result:
case e_s.h.mp
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
⊢ m ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

case e_s.h.mpr
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → m ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case e_s
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
ext m

Result:
case e_s.h
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
⊢ m ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.span R (⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) = Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
congr

Result:
case e_s
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case e_s.h.mp
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
⊢ m ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rintro ⟨-, ⟨⟨x, ⟨n, hn⟩, rfl⟩, hm⟩⟩

Result:
case e_s.h.mp.intro.intro.intro.intro.mk
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
x : ↥I
n : M
hn : n ∈ N
hm : ↑f ⁅↑x, ↑⟨n, hn⟩⁆ = m
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case e_s.h.mpr.intro.intro.mk
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
x : ↥I
m₂ : M₂
hm₂ : m₂ ∈ map f N
⊢ ⁅↑x, ↑⟨m₂, hm₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
obtain ⟨n, hn, rfl⟩ := (mem_map m₂).mp hm₂

Result:
case e_s.h.mpr.intro.intro.mk.intro.intro
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
x : ↥I
n : M
hn : n ∈ N
hm₂ : f n ∈ map f N
⊢ ⁅↑x, ↑⟨f n, hm₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}