awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
simp : Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) { toSubmodule := ⊥, lie_mem := ⋯ } ⊥
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A ⊥) ⊥

Tactic:
simp only [baseChange, bot_toSubmodule, Submodule.baseChange_bot]

Premises used: LieSubmodule.bot_toSubmodule, Submodule.baseChange_bot, LieSubmodule.baseChange
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) { toSubmodule := ⊥, lie_mem := ⋯ } ⊥

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
simp : Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) { toSubmodule := ⊤, lie_mem := ⋯ } ⊤
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A ⊤) ⊤

Tactic:
simp only [baseChange, top_toSubmodule, Submodule.baseChange_top]

Premises used: LieSubmodule.top_toSubmodule, LieSubmodule.baseChange, Submodule.baseChange_top
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) { toSubmodule := ⊤, lie_mem := ⋯ } ⊤

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
h :
  ∀ (x : A ⊗[R] M),
    Membership.mem (γ := Set (A ⊗[R] M))
        (Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
          {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m})
        x ↔
      x ∈ s
⊢ Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
x : A ⊗[R] M
⊢ Membership.mem (γ := Set (A ⊗[R] M))
      (Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
        {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m})
      x ↔
    x ∈ s

Tactic:
simp [s]
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
⊢ Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s

Tactic:
have : (TensorProduct.mk R A M 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s := by ext; simp [s]
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
rw :
  Eq (α := Submodule A (A ⊗[R] M)) (Submodule.span A s)
    (Submodule.span A
      {x : A ⊗[R] M |
        ∃ (x_1 : A ⊗[R] L),
          Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
            ∃ (n : A ⊗[R] M),
              Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x})
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A ⁅I, N⁆)
    (Bracket.bracket (L := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (baseChange A I) (baseChange A N))

Tactic:
rw [← toSubmodule_inj, coe_baseChange, lieIdeal_oper_eq_linear_span',
    Submodule.baseChange_span, this, lieIdeal_oper_eq_linear_span']

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.toSubmodule_inj, Submodule.baseChange_span, LieSubmodule.coe_baseChange
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
⊢ Eq (α := Submodule A (A ⊗[R] M)) (Submodule.span A s)
    (Submodule.span A
      {x : A ⊗[R] M |
        ∃ (x_1 : A ⊗[R] L),
          Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
            ∃ (n : A ⊗[R] M),
              Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x})

Tactic:
le_antisymm (Submodule.span_mono ?_) (Submodule.span_le.mpr ?_)

Premises used: Iff.mpr, le_antisymm, Submodule.span_mono, Submodule.span_le
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
refine_1 :
  s ⊆
    {x : A ⊗[R] M |
      ∃ (x_1 : A ⊗[R] L),
        Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
          ∃ (n : A ⊗[R] M),
            Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x}
refine_2 :
  {x : A ⊗[R] M |
      ∃ (x_1 : A ⊗[R] L),
        Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
          ∃ (n : A ⊗[R] M),
            Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x} ⊆
    (↑(Submodule.span A s) : Set (A ⊗[R] M))
⊢ Eq (α := Submodule A (A ⊗[R] M)) (Submodule.span A s)
    (Submodule.span A
      {x : A ⊗[R] M |
        ∃ (x_1 : A ⊗[R] L),
          Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
            ∃ (n : A ⊗[R] M),
              Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x})

Tactic:
refine le_antisymm (Submodule.span_mono ?_) (Submodule.span_le.mpr ?_)

Premises used: Iff.mpr, le_antisymm, Submodule.span_mono, Submodule.span_le
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : L
hx : x ∈ I
m : M
hm : m ∈ N
⊢ Eq (α := A ⊗[R] M) (Bracket.bracket (L := A ⊗[R] L) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] m)) (1 ⊗ₜ[R] ⁅x, m⁆)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : L
hx : x ∈ I
m : M
hm : m ∈ N
⊢ Membership.mem (γ := Set (A ⊗[R] M))
    {x : A ⊗[R] M |
      ∃ (x_1 : A ⊗[R] L),
        Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x_1 ∧
          ∃ (n : A ⊗[R] M),
            Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) n ∧ ⁅x_1, n⁆ = x}
    (1 ⊗ₜ[R] ⁅x, m⁆)

Tactic:
exact ⟨1 ⊗ₜ x, tmul_mem_baseChange_of_mem 1 hx,
           1 ⊗ₜ m, tmul_mem_baseChange_of_mem 1 hm, by simp⟩
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (baseChange A I) x
m : A ⊗[R] M
hm : Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) m
refine_2 :
  ∀
    (hx :
      Membership.mem (γ := Submodule A (A ⊗[R] L))
        (Submodule.span A
          (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
                (↑I : Submodule R L)) :
            Set (A ⊗[R] L)))
        x)
    (m : A ⊗[R] M)
    (hm :
      Membership.mem (γ := Submodule A (A ⊗[R] M))
        (Submodule.span A
          (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                (↑N : Submodule R M)) :
            Set (A ⊗[R] M)))
        m),
    ⁅x, m⁆ ∈ (↑(Submodule.span A s) : Set (A ⊗[R] M))
⊢ ⁅x, m⁆ ∈ (↑(Submodule.span A s) : Set (A ⊗[R] M))

Tactic:
rw [mem_baseChange_iff] at hx hm

Premises used: LieSubmodule.mem_baseChange_iff
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x
m : A ⊗[R] M
hm :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    m
⊢ ∀ (y : A ⊗[R] M)
    (hy :
      Membership.mem (γ := Submodule A (A ⊗[R] M))
        (Submodule.span A
          (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                (↑N : Submodule R M)) :
            Set (A ⊗[R] M)))
        y),
    (fun (x : A ⊗[R] L) (m : A ⊗[R] M)
          (x_1 :
            Membership.mem (γ := Submodule A (A ⊗[R] L))
              (Submodule.span A
                (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
                      (↑I : Submodule R L)) :
                  Set (A ⊗[R] L)))
              x)
          (x_2 :
            Membership.mem (γ := Submodule A (A ⊗[R] M))
              (Submodule.span A
                (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                      (↑N : Submodule R M)) :
                  Set (A ⊗[R] M)))
              m) ↦
        Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x, m⁆)
      0 y ⋯ hy

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x
m : A ⊗[R] M
hm :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    m
⊢ ∀ (x : A ⊗[R] L)
    (hx :
      Membership.mem (γ := Submodule A (A ⊗[R] L))
        (Submodule.span A
          (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
                (↑I : Submodule R L)) :
            Set (A ⊗[R] L)))
        x),
    (fun (x : A ⊗[R] L) (m : A ⊗[R] M)
          (x_1 :
            Membership.mem (γ := Submodule A (A ⊗[R] L))
              (Submodule.span A
                (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
                      (↑I : Submodule R L)) :
                  Set (A ⊗[R] L)))
              x)
          (x_2 :
            Membership.mem (γ := Submodule A (A ⊗[R] M))
              (Submodule.span A
                (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
                      (↑N : Submodule R M)) :
                  Set (A ⊗[R] M)))
              m) ↦
        Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x, m⁆)
      x 0 hx ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x_1 : A ⊗[R] L
hx_1 :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x_1
m : A ⊗[R] M
hm :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    m
x : L
hx : x ∈ (↑(↑I : Submodule R L) : Set L)
y : M
hy : y ∈ (↑(↑N : Submodule R M) : Set M)
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] ⁅x, y⁆)
    (Bracket.bracket (L := A ⊗[R] L)
      (((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1 : (a : L) → A ⊗[R] L) x : A ⊗[R] L)
      (((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M) y))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x_1 : A ⊗[R] L
hx_1 :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x_1
m : A ⊗[R] M
hm :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    m
x : L
hx : x ∈ (↑(↑I : Submodule R L) : Set L)
y : M
hy : y ∈ (↑(↑N : Submodule R M) : Set M)
⊢ Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s)
    (Bracket.bracket (L := A ⊗[R] L)
        (((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1 : (a : L) → A ⊗[R] L) x : A ⊗[R] L)
        (((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M) y) :
      A ⊗[R] M)

Tactic:
exact Submodule.subset_span ⟨x, hx, y, hy, by simp⟩
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x
m : A ⊗[R] M
hm :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    m
x_1 y : A ⊗[R] L
z : A ⊗[R] M
hx_1 :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x_1
hy :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    y
hz :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    z
h : Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x_1, z⁆
h_1 : Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅y, z⁆
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x_1 + y, z⁆

Tactic:
simp [add_mem, Submodule.smul_mem, *]

Premises used: AddMemClass.add_mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m : A ⊗[R] M | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this :
  Set.image (α := M) (⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M)
      {m : M | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} =
    s
x : A ⊗[R] L
hx :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x
m : A ⊗[R] M
hm :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    m
x_1 : A ⊗[R] L
y z : A ⊗[R] M
hx_1 :
  Membership.mem (γ := Submodule A (A ⊗[R] L))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A L : (a : A) → L →ₗ[R] A ⊗[R] L) 1)
            (↑I : Submodule R L)) :
        Set (A ⊗[R] L)))
    x_1
hy :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    y
hz :
  Membership.mem (γ := Submodule A (A ⊗[R] M))
    (Submodule.span A
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1)
            (↑N : Submodule R M)) :
        Set (A ⊗[R] M)))
    z
h : Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x_1, y⁆
h_1 : Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x_1, z⁆
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.span A s) ⁅x_1, y + z⁆

Tactic:
simp [add_mem, Submodule.smul_mem, *]

Premises used: AddMemClass.add_mem, Submodule.smul_mem