-- Mathlib/Algebra/Lie/BaseChange.lean
lemma lie_baseChange {I : LieIdeal R L} {N : LieSubmodule R L M} :
    ⁅I, N⁆.baseChange A = ⁅I.baseChange A, N.baseChange A⁆

Proof state:
case refine_2.intro.intro.intro.intro.mem.intro.intro.mem.intro.intro
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ baseChange A I
y : L
hy : y ∈ I
m : A ⊗[R] M
hm : m ∈ baseChange A N
m' : M
hm' : m' ∈ N
⊢ 1 ⊗ₜ[R] ⁅y, m'⁆ ∈ Submodule.span A s

Tactic:
apply Submodule.subset_span

Result:
case refine_2.intro.intro.intro.intro.mem.intro.intro.mem.intro.intro.a
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ baseChange A I
y : L
hy : y ∈ I
m : A ⊗[R] M
hm : m ∈ baseChange A N
m' : M
hm' : m' ∈ N
⊢ 1 ⊗ₜ[R] ⁅y, m'⁆ ∈ s

Proof state:
case refine_2.intro.intro.intro.intro.mem.intro.intro.smul
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ baseChange A I
y : L
hy : y ∈ I
m : A ⊗[R] M
hm : m ∈ baseChange A N
a : A
u : A ⊗[R] M
hx✝ : u ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
hu : ⁅1 ⊗ₜ[R] y, u⁆ ∈ Submodule.span A s
⊢ a • ⁅1 ⊗ₜ[R] y, u⁆ ∈ Submodule.span A s

Tactic:
exact Submodule.smul_mem _ a hu

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ baseChange A I
m : A ⊗[R] M
hm : m ∈ baseChange A N
⊢ ⁅x, m⁆ ∈ ↑(Submodule.span A s)

Tactic:
revert m

Result:
case refine_2.intro.intro.intro.intro
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ baseChange A I
⊢ ∀ m ∈ baseChange A N, ⁅x, m⁆ ∈ ↑(Submodule.span A s)

Proof state:
case refine_2.intro.intro.intro.intro.mem.intro.intro.smul
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ baseChange A I
y : L
hy : y ∈ I
m : A ⊗[R] M
hm : m ∈ baseChange A N
⊢ ∀ (a : A) (x : A ⊗[R] M) (hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)),
    (fun m' x => ⁅1 ⊗ₜ[R] y, m'⁆ ∈ Submodule.span A s) x hx →
      (fun m' x => ⁅1 ⊗ₜ[R] y, m'⁆ ∈ Submodule.span A s) (a • x) ⋯

Tactic:
intro a u _ hu

Result:
case refine_2.intro.intro.intro.intro.mem.intro.intro.smul
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ baseChange A I
y : L
hy : y ∈ I
m : A ⊗[R] M
hm : m ∈ baseChange A N
a : A
u : A ⊗[R] M
hx✝ : u ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
hu : ⁅1 ⊗ₜ[R] y, u⁆ ∈ Submodule.span A s
⊢ ⁅1 ⊗ₜ[R] y, a • u⁆ ∈ Submodule.span A s

Proof state:
case refine_1.intro.intro.intro.intro
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : L
hx : x ∈ I
m : M
hm : m ∈ N
⊢ 1 ⊗ₜ[R] ⁅x, m⁆ ∈ {x | ∃ x_1 ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x_1, n⁆ = x}

Tactic:
exact ⟨1 ⊗ₜ x, tmul_mem_baseChange_of_mem 1 hx,
       1 ⊗ₜ m, tmul_mem_baseChange_of_mem 1 hm, by simp⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.smul
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x✝ : A ⊗[R] L
hx✝¹ : x✝ ∈ baseChange A I
a : A
x : A ⊗[R] L
hx✝ : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hx : ∀ m' ∈ baseChange A N, ⁅x, m'⁆ ∈ Submodule.span A s
m' : A ⊗[R] M
hm' : m' ∈ baseChange A N
⊢ ⁅a • x, m'⁆ ∈ Submodule.span A s

Tactic:
rw [smul_lie]

Result:
case refine_2.intro.intro.intro.intro.smul
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x✝ : A ⊗[R] L
hx✝¹ : x✝ ∈ baseChange A I
a : A
x : A ⊗[R] L
hx✝ : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hx : ∀ m' ∈ baseChange A N, ⁅x, m'⁆ ∈ Submodule.span A s
m' : A ⊗[R] M
hm' : m' ∈ baseChange A N
⊢ a • ⁅x, m'⁆ ∈ Submodule.span A s