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
⊢ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} =
    Submodule.span R (↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t})
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
⊢ ⁅I, N⁆ = LieModuleHom.range (LieModuleHom.comp (toModuleHom R L M) (mapIncl I N))
rw [← coe_toSubmodule_eq_iff, lieIdeal_oper_eq_linear_span, LieModuleHom.coeSubmodule_range,
  LieModuleHom.coe_linearMap_comp, LinearMap.range_comp, mapIncl_def, coe_linearMap_map,
  TensorProduct.map_range_eq_span_tmul, Submodule.map_span]
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
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
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
⊢ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} =
    Submodule.span R (↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t})
congr
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 ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ↔ m ∈ ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
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
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
ext m
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 ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → m ∈ ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) 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] ↑↑(incl N) n = t} → m ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
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 ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ↔ m ∈ ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
constructor
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
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ ∈
    ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
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 ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → m ∈ ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
rintro ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩
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 ⊗ₜ[R] n ∈ {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t} ∧
    ↑↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆
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
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ ∈
    ↑↑(toModuleHom R L M) '' {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t}
use x ⊗ₜ n
case e_s.h.mp.intro.mk.intro.mk.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] ↑↑(incl N) n = t}

case e_s.h.mp.intro.mk.intro.mk.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) = ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆
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 ⊗ₜ[R] n ∈ {t | ∃ m n, ↑↑(incl I) m ⊗ₜ[R] ↑↑(incl N) n = t} ∧
    ↑↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆
constructor
case e_s.h.mp.intro.mk.intro.mk.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
⊢ ↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn } = x ⊗ₜ[R] n
case e_s.h.mp.intro.mk.intro.mk.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] ↑↑(incl N) n = t}
use ⟨x, hx⟩, ⟨n, hn⟩
no goals
case e_s.h.mp.intro.mk.intro.mk.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
⊢ ↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn } = x ⊗ₜ[R] n
simp
no goals
case e_s.h.mp.intro.mk.intro.mk.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) = ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆
simp
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) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) = m
⊢ m ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
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] ↑↑(incl N) n = t} → m ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rintro ⟨t, ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩, h⟩
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) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) = m
⊢ ↑↑(toModuleHom R L M) (↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) ∈
    {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
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) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) = m
⊢ m ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rw [← h]
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) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) = m
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ =
    ↑↑(toModuleHom R L M) (↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn })
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) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) = m
⊢ ↑↑(toModuleHom R L M) (↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) ∈
    {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
use ⟨x, hx⟩, ⟨n, hn⟩
no goals
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) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn }) = m
⊢ ⁅↑{ val := x, property := hx }, ↑{ val := n, property := hn }⁆ =
    ↑↑(toModuleHom R L M) (↑↑(incl I) { val := x, property := hx } ⊗ₜ[R] ↑↑(incl N) { val := n, property := hn })
simp