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
N : LieSubmodule R L M
x : A ⊗[R] L
c :
  (↑(↑(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)) :
      Type (max u_2 u_4)) →₀
    A
hm :
  Membership.mem (α := A ⊗[R] M) (γ := 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)))
    ((Finsupp.linearCombination A
            (Subtype.val (p := fun (x : A ⊗[R] M) ↦
              x ∈
                (↑(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)))) :
          (a :
              (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)) :
                  Type (max u_2 u_4)) →₀
                A) →
            A ⊗[R] M)
        c :
      A ⊗[R] M)
⊢ Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (Bracket.bracket (L := A ⊗[R] L) 0
        ((Finsupp.linearCombination A
              (Subtype.val (p := fun (x : A ⊗[R] M) ↦
                x ∈
                  (↑(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)))) :
            (a :
                (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                        Set (A ⊗[R] M)) :
                    Type (max u_2 u_4)) →₀
                  A) →
              A ⊗[R] M)
          c) :
      A ⊗[R] 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
N : LieSubmodule R L M
x : A ⊗[R] L
c :
  (↑(↑(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)) :
      Type (max u_2 u_4)) →₀
    A
hm :
  Membership.mem (α := A ⊗[R] M) (γ := 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)))
    ((Finsupp.linearCombination A
            (Subtype.val (p := fun (x : A ⊗[R] M) ↦
              x ∈
                (↑(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)))) :
          (a :
              (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)) :
                  Type (max u_2 u_4)) →₀
                A) →
            A ⊗[R] M)
        c :
      A ⊗[R] M)
a : A
y : L
refine_1 :
  Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    ((((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → Module.End A (A ⊗[R] M)) (a ⊗ₜ[R] y) :
            Module.End A (A ⊗[R] M)) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        ((Finsupp.linearCombination A
              (Subtype.val (p := fun (x : A ⊗[R] M) ↦
                x ∈
                  (↑(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)))) :
            (a :
                (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                        Set (A ⊗[R] M)) :
                    Type (max u_2 u_4)) →₀
                  A) →
              A ⊗[R] M)
          c) :
      A ⊗[R] M)
⊢ Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y)
        ((Finsupp.linearCombination A
              (Subtype.val (p := fun (x : A ⊗[R] M) ↦
                x ∈
                  (↑(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)))) :
            (a :
                (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                        Set (A ⊗[R] M)) :
                    Type (max u_2 u_4)) →₀
                  A) →
              A ⊗[R] M)
          c) :
      A ⊗[R] M)

Tactic:
change toEnd A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _

Premises used: LieModule.toEnd, TensorProduct, DFunLike.coe
-- 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
N : LieSubmodule R L M
x : A ⊗[R] L
c :
  (↑(↑(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)) :
      Type (max u_2 u_4)) →₀
    A
hm :
  Membership.mem (α := A ⊗[R] M) (γ := 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)))
    ((Finsupp.linearCombination A
            (Subtype.val (p := fun (x : A ⊗[R] M) ↦
              x ∈
                (↑(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)))) :
          (a :
              (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)) :
                  Type (max u_2 u_4)) →₀
                A) →
            A ⊗[R] M)
        c :
      A ⊗[R] M)
a : A
y : L
refine_1 :
  Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (∑ x ∈ c.support,
      HSMul.hSMul (α := A)
        ((c :
              (a :
                  (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                        Set (A ⊗[R] M)) :
                    Type (max u_2 u_4))) →
                A)
            x :
          A)
        (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y) (↑x : A ⊗[R] M)))
⊢ Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    ((((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → Module.End A (A ⊗[R] M)) (a ⊗ₜ[R] y) :
            Module.End A (A ⊗[R] M)) :
          (a : A ⊗[R] M) → A ⊗[R] M)
        ((Finsupp.linearCombination A
              (Subtype.val (p := fun (x : A ⊗[R] M) ↦
                x ∈
                  (↑(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)))) :
            (a :
                (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                        Set (A ⊗[R] M)) :
                    Type (max u_2 u_4)) →₀
                  A) →
              A ⊗[R] M)
          c) :
      A ⊗[R] M)

Tactic:
simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, map_smul, toEnd_apply_apply]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, map_sum, LieModule.toEnd_apply_apply, map_smul
-- 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
N : LieSubmodule R L M
x : A ⊗[R] L
c :
  (↑(↑(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)) :
      Type (max u_2 u_4)) →₀
    A
hm :
  Membership.mem (α := A ⊗[R] M) (γ := 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)))
    ((Finsupp.linearCombination A
            (Subtype.val (p := fun (x : A ⊗[R] M) ↦
              x ∈
                (↑(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)))) :
          (a :
              (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)) :
                  Type (max u_2 u_4)) →₀
                A) →
            A ⊗[R] M)
        c :
      A ⊗[R] M)
a : A
y : L
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (∑ x ∈ c.support,
      HSMul.hSMul (α := A)
        ((c :
              (a :
                  (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                        Set (A ⊗[R] M)) :
                    Type (max u_2 u_4))) →
                A)
            x :
          A)
        (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y) (↑x : A ⊗[R] M)))

Tactic:
Submodule.sum_mem _ fun ⟨_, n, hn, h⟩ _ ↦ Submodule.smul_mem _ _ ?_

Premises used: Set.Mem, Bracket.bracket, Submodule.sum_mem, LieSubmodule.toSubmodule, Membership.mem, _private.0.LieSubmodule.baseChange.match_1, Subtype.mk, And.intro, Submodule.baseChange, Exists.intro, HSMul.hSMul, TensorProduct.tmul, Subtype.val, DFunLike.coe, 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
N : LieSubmodule R L M
x : A ⊗[R] L
c :
  (↑(↑(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)) :
      Type (max u_2 u_4)) →₀
    A
hm :
  Membership.mem (α := A ⊗[R] M) (γ := 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)))
    ((Finsupp.linearCombination A
            (Subtype.val (p := fun (x : A ⊗[R] M) ↦
              x ∈
                (↑(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)))) :
          (a :
              (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)) :
                  Type (max u_2 u_4)) →₀
                A) →
            A ⊗[R] M)
        c :
      A ⊗[R] M)
a : A
y : L
refine_1 :
  ∀
    (x :
      (↑(↑(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)) :
        Type (max u_2 u_4)))
    (val : A ⊗[R] M) (n : M) (hn : n ∈ (↑(↑N : Submodule R M) : Set M))
    (h : ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M) n = val),
    Subtype.mk (p := fun (x : A ⊗[R] M) ↦
          x ∈
            (↑(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)))
          val ⋯ ∈
        c.support →
      Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
        (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y)
          (↑(Subtype.mk (p := fun (x : A ⊗[R] M) ↦
                x ∈
                  (↑(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)))
                val ⋯) :
            A ⊗[R] M))
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (∑ x ∈ c.support,
      HSMul.hSMul (α := A)
        ((c :
              (a :
                  (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                        Set (A ⊗[R] M)) :
                    Type (max u_2 u_4))) →
                A)
            x :
          A)
        (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y) (↑x : A ⊗[R] M)))

Tactic:
refine Submodule.sum_mem _ fun ⟨_, n, hn, h⟩ _ ↦ Submodule.smul_mem _ _ ?_

Premises used: Submodule.sum_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
N : LieSubmodule R L M
x : A ⊗[R] L
c :
  (↑(↑(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)) :
      Type (max u_2 u_4)) →₀
    A
hm :
  Membership.mem (α := A ⊗[R] M) (γ := 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)))
    ((Finsupp.linearCombination A
            (Subtype.val (p := fun (x : A ⊗[R] M) ↦
              x ∈
                (↑(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)))) :
          (a :
              (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)) :
                  Type (max u_2 u_4)) →₀
                A) →
            A ⊗[R] M)
        c :
      A ⊗[R] M)
a : A
y : L
x_1 :
  (↑(↑(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)) :
    Type (max u_2 u_4))
val : A ⊗[R] M
n : M
hn : n ∈ (↑(↑N : Submodule R M) : Set M)
h : ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M) n = val
h_1 :
  Subtype.mk (p := fun (x : A ⊗[R] M) ↦
      x ∈
        (↑(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)))
      val ⋯ ∈
    c.support
refine_1 :
  Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y)
        (((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M) n) :
      A ⊗[R] M)
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y)
      (↑(Subtype.mk (p := fun (x : A ⊗[R] M) ↦
            x ∈
              (↑(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)))
            val ⋯) :
        A ⊗[R] M))

Tactic:
rw [Subtype.coe_mk, ← h]

Premises used: Subtype.coe_mk
-- 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
N : LieSubmodule R L M
x : A ⊗[R] L
c :
  (↑(↑(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)) :
      Type (max u_2 u_4)) →₀
    A
hm :
  Membership.mem (α := A ⊗[R] M) (γ := 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)))
    ((Finsupp.linearCombination A
            (Subtype.val (p := fun (x : A ⊗[R] M) ↦
              x ∈
                (↑(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)))) :
          (a :
              (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)) :
                  Type (max u_2 u_4)) →₀
                A) →
            A ⊗[R] M)
        c :
      A ⊗[R] M)
a : A
y : L
x_1 :
  (↑(↑(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)) :
    Type (max u_2 u_4))
val : A ⊗[R] M
n : M
hn : n ∈ (↑(↑N : Submodule R M) : Set M)
h : ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M) n = val
h_1 :
  Subtype.mk (p := fun (x : A ⊗[R] M) ↦
      x ∈
        (↑(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)))
      val ⋯ ∈
    c.support
⊢ Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y)
        (((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M) n) :
      A ⊗[R] M)

Tactic:
Submodule.tmul_mem_baseChange_of_mem _ (N.lie_mem hn)

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, List.foldl, LieSubmodule.lie_mem, Submodule.tmul_mem_baseChange_of_mem, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux
-- 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
N : LieSubmodule R L M
x : A ⊗[R] L
c :
  (↑(↑(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)) :
      Type (max u_2 u_4)) →₀
    A
hm :
  Membership.mem (α := A ⊗[R] M) (γ := 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)))
    ((Finsupp.linearCombination A
            (Subtype.val (p := fun (x : A ⊗[R] M) ↦
              x ∈
                (↑(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)))) :
          (a :
              (↑(↑(Submodule.map ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (↑N : Submodule R M)) :
                      Set (A ⊗[R] M)) :
                  Type (max u_2 u_4)) →₀
                A) →
            A ⊗[R] M)
        c :
      A ⊗[R] M)
a : A
y : L
x_1 :
  (↑(↑(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)) :
    Type (max u_2 u_4))
val : A ⊗[R] M
n : M
hn : n ∈ (↑(↑N : Submodule R M) : Set M)
h : ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M) n = val
h_1 :
  Subtype.mk (p := fun (x : A ⊗[R] M) ↦
      x ∈
        (↑(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)))
      val ⋯ ∈
    c.support
⊢ Membership.mem (α := A ⊗[R] M) (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M))
    (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] y)
        (((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M) n) :
      A ⊗[R] M)

Tactic:
exact Submodule.tmul_mem_baseChange_of_mem _ (N.lie_mem hn)

Premises used: LieSubmodule.lie_mem, Submodule.tmul_mem_baseChange_of_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
N : LieSubmodule R L M
⊢ Eq (α := Submodule A (A ⊗[R] M)) (↑(baseChange A N) : Submodule A (A ⊗[R] M))
    (Submodule.baseChange A (↑N : Submodule R M))

Tactic:
rfl

Premises used: LinearMap.range, Submodule.baseChange, rfl, Submodule.copy
-- 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
N : LieSubmodule R L M
a : A
m : M
hm : m ∈ N
⊢ Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) (a ⊗ₜ[R] m)

Tactic:
(N : Submodule R M).tmul_mem_baseChange_of_mem a hm

Premises used: Set.Mem, Submodule.tmul_mem_baseChange_of_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
N : LieSubmodule R L M
m : A ⊗[R] M
rw :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) m ↔
    Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M)) m
⊢ Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) m ↔
    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

Tactic:
rw [← Submodule.baseChange_eq_span]

Premises used: Submodule.baseChange_eq_span
-- 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
N : LieSubmodule R L M
m : A ⊗[R] M
⊢ Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (baseChange A N) m ↔
    Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M)) m

Tactic:
rfl