-- 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
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
⊢ ∀ (x : A ⊗[R] L) (h : x ∈ ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)),
    (fun x' x => ∀ m' ∈ baseChange A N, ⁅x', m'⁆ ∈ Submodule.span A s) x ⋯

Tactic:
rintro _ ⟨y : L, hy : y ∈ I, rfl⟩ m hm

Result:
case refine_2.intro.intro.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
⊢ ⁅((TensorProduct.mk R A L) 1) y, m⁆ ∈ Submodule.span A s

Proof state:
case refine_2.intro.intro.intro.intro.mem.intro.intro.add
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
⊢ ∀ (x y_1 : A ⊗[R] M) (hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N))
    (hy : y_1 ∈ 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) y_1 hy →
        (fun m' x => ⁅1 ⊗ₜ[R] y, m'⁆ ∈ Submodule.span A s) (x + y_1) ⋯

Tactic:
intro u v _ _ hu hv

Result:
case refine_2.intro.intro.intro.intro.mem.intro.intro.add
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
u v : A ⊗[R] M
hx✝ : u ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
hy✝ : v ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
hu : ⁅1 ⊗ₜ[R] y, u⁆ ∈ Submodule.span A s
hv : ⁅1 ⊗ₜ[R] y, v⁆ ∈ Submodule.span A s
⊢ ⁅1 ⊗ₜ[R] y, u + v⁆ ∈ Submodule.span A s

Proof state:
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, 1 ⊗ₜ[R] m⁆ = 1 ⊗ₜ[R] ⁅x, m⁆

Tactic:
simp

Result:
no goals

Proof state:
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

Tactic:
exact ⟨y, hy, m', hm', rfl⟩

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.add
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
⊢ ∀ (x y : A ⊗[R] L) (hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I))
    (hy : y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)),
    (fun x' x => ∀ m' ∈ baseChange A N, ⁅x', m'⁆ ∈ Submodule.span A s) x hx →
      (fun x' x => ∀ m' ∈ baseChange A N, ⁅x', m'⁆ ∈ Submodule.span A s) y hy →
        (fun x' x => ∀ m' ∈ baseChange A N, ⁅x', m'⁆ ∈ Submodule.span A s) (x + y) ⋯

Tactic:
intro x y _ _ hx hy m' hm'

Result:
case refine_2.intro.intro.intro.intro.add
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
x y : A ⊗[R] L
hx✝ : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hx : ∀ m' ∈ baseChange A N, ⁅x, m'⁆ ∈ Submodule.span A s
hy : ∀ m' ∈ baseChange A N, ⁅y, m'⁆ ∈ Submodule.span A s
m' : A ⊗[R] M
hm' : m' ∈ baseChange A N
⊢ ⁅x + y, m'⁆ ∈ Submodule.span A s