awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.BaseChange
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
x_1 : 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_1 ⊗ₜ[R] y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
          (a : A ⊗[R] L) → A ⊗[R] L)
        0))
    ((((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_1 ⊗ₜ[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') 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.BaseChange
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
x_1 : A
y_1 : L
x_2 : A
x_3 : 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_1 ⊗ₜ[R] y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (x_2 ⊗ₜ[R] x_3)) :
      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_1 ⊗ₜ[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') (x_2 ⊗ₜ[R] x_3)) :
      B ⊗[R] L')

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.BaseChange
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
x_1 : A
y_1 : L
x_2 x_3 : A ⊗[R] L
h1 :
  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_1 ⊗ₜ[R] y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          x_2) :
      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_1 ⊗ₜ[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') x_2) :
      B ⊗[R] L')
h2 :
  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_1 ⊗ₜ[R] y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          x_3) :
      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_1 ⊗ₜ[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') x_3) :
      B ⊗[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_1 ⊗ₜ[R] y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (x_2 + x_3)) :
      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_1 ⊗ₜ[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') (x_2 + x_3)) :
      B ⊗[R] L')

Tactic:
simp [h1, h2]
-- Module: Mathlib.Algebra.Lie.BaseChange
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
x_1 : 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_1 ⊗ₜ[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_1 ⊗ₜ[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 y.induction_on (by simp) (fun _ _ ↦ by simp) (fun _ _ h1 h2 ↦ by simp [h1, h2])
-- Module: Mathlib.Algebra.Lie.BaseChange
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 x_1 y_1 : 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_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          0))
      ((((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_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') 0)) →
    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) y_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
              (a : A ⊗[R] L) → A ⊗[R] L)
            0))
        ((((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') 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') 0)) →
      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_1 + y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
              (a : A ⊗[R] L) → A ⊗[R] L)
            0))
        ((((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_1 + 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') 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.BaseChange
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 x_1 y_1 : A ⊗[R] L
x_2 : A
x_3 : L
h :
  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_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
            (a : A ⊗[R] L) → A ⊗[R] L)
          (x_2 ⊗ₜ[R] x_3)) :
      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_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') (x_2 ⊗ₜ[R] x_3)) :
      B ⊗[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) y_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
              (a : A ⊗[R] L) → A ⊗[R] L)
            (x_2 ⊗ₜ[R] x_3)) :
        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') 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') (x_2 ⊗ₜ[R] x_3)) :
        B ⊗[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_1 + y_1) : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
              (a : A ⊗[R] L) → A ⊗[R] L)
            (x_2 ⊗ₜ[R] x_3)) :
        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_1 + 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') (x_2 ⊗ₜ[R] x_3)) :
        B ⊗[R] L')

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Lie.BaseChange
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 x_1 y_1 : 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_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_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') →
    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) 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') 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') →
      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_1 + 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_1 + 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 y.induction_on (by simp) (fun _ _ h ↦ by simp [h]) (by simp_all)
-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : LieRing L
inst_6 : LieAlgebra R L
inst_7 : LieRing L'
inst_8 : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
a : A
x : L
⊢ Eq (α := B ⊗[R] L') ((map f g : (a : A ⊗[R] L) → B ⊗[R] L') (a ⊗ₜ[R] x) : B ⊗[R] L')
    ((f : (a : A) → B) a ⊗ₜ[R] (g : (a : L) → L') x : B ⊗[R] L')

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, 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
x : L
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)
⊢ 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)

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
x : L
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:
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
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 (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M)) m

Tactic:
rw [Submodule.mem_carrier, SetLike.mem_coe] at hm ⊢

Premises used: SetLike.mem_coe, Submodule.mem_carrier
-- 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
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.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

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
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
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)
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (Submodule.baseChange A (↑N : Submodule R M)) ⁅x, m⁆

Tactic:
obtain ⟨c, rfl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp hm

Premises used: Finsupp.mem_span_iff_linearCombination, Iff.mp, rfl