-- Mathlib/Algebra/Lie/TensorProduct.lean
theorem lieIdeal_oper_eq_tensor_map_range :
    ⁅I, N⁆ = ((toModuleHom R L M).comp (mapIncl I N : I ⊗[R] N →ₗ⁅R,L⁆ L ⊗[R] M)).range

Proof state:
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩ = x ⊗ₜ[R] n

Tactic:
rfl

Result:
no goals

Proof state:
case h.left
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

Tactic:
use ⟨x, hx⟩, ⟨n, hn⟩

Result:
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩ = x ⊗ₜ[R] n

Proof state:
case e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rw [← h]

Result:
case e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case e_s.h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ m ∈ ⇑↑(toModuleHom R L M) '' {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

Tactic:
constructor

Result:
case e_s.h.mp
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → m ∈ ⇑↑(toModuleHom R L M) '' {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

case e_s.h.mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ m ∈ ⇑↑(toModuleHom R L M) '' {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t} → m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t} ∧ ↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆

Tactic:
constructor

Result:
case h.left
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

case h.right
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆

Proof state:
case e_s
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = ⇑↑(toModuleHom R L M) '' {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

Tactic:
ext m

Result:
case e_s.h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ m ∈ ⇑↑(toModuleHom R L M) '' {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

Proof state:
case e_s.h.mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ m ∈ ⇑↑(toModuleHom R L M) '' {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t} → m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
rintro ⟨t, ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩, h⟩

Result:
case e_s.h.mpr.intro.intro.intro.mk.intro.mk
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case e_s.h.mp
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} → m ∈ ⇑↑(toModuleHom R L M) '' {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

Tactic:
rintro ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩

Result:
case e_s.h.mp.intro.mk.intro.mk
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ ∈ ⇑↑(toModuleHom R L M) '' {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

Proof state:
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩)

Tactic:
rfl

Result:
no goals