-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem mono_lie (h₁ : I ≤ J) (h₂ : N ≤ N') : ⁅I, N⁆ ≤ ⁅J, N'⁆

Proof state:
case a
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N

Tactic:
rintro m' ⟨⟨x, hx⟩, ⟨n, hn⟩, hm⟩

Result:
case a.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = m'
⊢ m' ∈ ↑N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N_1 → m ∈ N_1
⊢ ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N

Tactic:
intro N hN

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
⊢ m ∈ N

Proof state:
case a.intro.mk.intro.mk.a
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = m'
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
use ⟨x, h₁ hx⟩, ⟨n, h₂ hn⟩

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : m ∈ ⁅I, N⁆
⊢ m ∈ ⁅J, N'⁆

Tactic:
rw [lieIdeal_oper_eq_span, mem_lieSpan] at h

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N_1 → m ∈ N_1
⊢ m ∈ ⁅J, N'⁆

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N_1 → m ∈ N_1
⊢ m ∈ ⁅J, N'⁆

Tactic:
rw [lieIdeal_oper_eq_span, mem_lieSpan]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N_1 → m ∈ N_1
⊢ ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N

Proof state:
case a.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = m'
⊢ m' ∈ ↑N

Tactic:
rw [← hm]

Result:
case a.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = m'
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ ∈ ↑N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
⊢ ⁅I, N⁆ ≤ ⁅J, N'⁆

Tactic:
intro m h

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : m ∈ ⁅I, N⁆
⊢ m ∈ ⁅J, N'⁆

Proof state:
case a.intro.mk.intro.mk
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = m'
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ ∈ ↑N

Tactic:
apply hN

Result:
case a.intro.mk.intro.mk.a
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N✝
hm : ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = m'
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
⊢ m ∈ N

Tactic:
apply h

Result:
case a
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N✝ N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N✝ ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
N : LieSubmodule R L M
hN : {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N