awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
Goal:
R_1 : Type u_1
A_1 : Type u_2
L_1 : Type u_3
M : Type u_4
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
inst_3 : LieRing L_1
inst_4 : LieAlgebra R_1 L_1
inst_5 : AddCommGroup M
inst_6 : Module R_1 M
inst_7 : LieRingModule L_1 M
inst_8 : LieModule R_1 L_1 M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst_9 : CommRing R
inst_10 : CommRing A
inst_11 : Algebra R A
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : LieRing L
inst_15 : LieAlgebra R L
inst_16 : LieRing L'
inst_17 : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
⊢ Eq (α := B ⊗[R] L')
    ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
        ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) x : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          y) :
      B ⊗[R] L')
    ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
              ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') x) :
            B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
          (a : B ⊗[R] L') → B ⊗[R] L')
        ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y) :
      B ⊗[R] L')
have refine_1 : ∀ (x : A) (y_1 : L),
  Eq (α := B ⊗[R] L')
    ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
        ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (x ⊗ₜ[R] y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          y) :
      B ⊗[R] L')
    ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
              ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') (x ⊗ₜ[R] y_1)) :
            B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
          (a : B ⊗[R] L') → B ⊗[R] L')
        ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y) :
      B ⊗[R] L')
Tactic: refine x.induction_on (by simp) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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
x : L
⊢ Eq (α := Module.End A (A ⊗[R] M))
    ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → Module.End A (A ⊗[R] M)) (1 ⊗ₜ[R] x) : Module.End A (A ⊗[R] M))
    (LinearMap.baseChange A
        (((toEnd R L M : LieHom.{u_1, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
      A ⊗[R] M →ₗ[A] A ⊗[R] M)
have a : ∀ (x_1 : M),
  Eq (α := A ⊗[R] M)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → Module.End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)) :
                A →ₗ[A] M →ₗ[R] A ⊗[R] M) :
              (a : A) → M →ₗ[R] A ⊗[R] M)
            1 :
          (a : M) → A ⊗[R] M)
        x_1 :
      A ⊗[R] M)
    ((((TensorProduct.AlgebraTensorModule.curry
                  (LinearMap.baseChange A
                    (((toEnd R L M : LieHom.{u_1, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x)) :
                A →ₗ[A] M →ₗ[R] A ⊗[R] M) :
              (a : A) → M →ₗ[R] A ⊗[R] M)
            1 :
          (a : M) → A ⊗[R] M)
        x_1 :
      A ⊗[R] M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (hypothesis)
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
m : A ⊗[R] M
hm :
  Membership.mem (γ := Set (A ⊗[R] M))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (Submodule.baseChange A (↑N : Submodule R M)))))
    m
⊢ Membership.mem (γ := Set (A ⊗[R] M))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (Submodule.baseChange A (↑N : Submodule R M)))))
    ⁅x, m⁆
have hm₁ : Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M)) m
Tactic: rw [Submodule.mem_carrier, SetLike.mem_coe] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (hypothesis)
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
m : A ⊗[R] M
hm : Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M)) m
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M)) ⁅x, m⁆
have 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
Tactic: rw [Submodule.baseChange_eq_span] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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
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
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M)) ⁅x, m⁆
have obtain : ∀
  (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))
    (⁅x,
        (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: obtain ⟨c, rfl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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))
    (⁅x,
        (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)
have refine_1 : ∀ (a : A) (y : L),
  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: refine x.induction_on (by simp) (fun a y ↦ ?_) (fun y z hy hz ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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 (α := 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)
have 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)
Tactic: change toEnd A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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 (α := 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)
have 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)))
Tactic: simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, map_smul, toEnd_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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)))
have 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 sorry ∈
      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 sorry) :
          A ⊗[R] M))
Tactic: refine Submodule.sum_mem _ fun ⟨_, n, hn, h⟩ _ ↦ Submodule.smul_mem _ _ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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 (γ := 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))
have 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)
Tactic: rw [Subtype.coe_mk, ← h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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.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
have 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
Tactic: rw [← Submodule.baseChange_eq_span]
-- Lean 4 proof step from Mathlib.Algebra.Lie.BaseChange (goal)
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)) (baseChange A ⊥) ⊥
have simp : Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) { toSubmodule := ⊥, lie_mem := sorry } ⊥
Tactic: simp only [baseChange, bot_toSubmodule, Submodule.baseChange_bot]