awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
zero :
  (IsTensorProduct.lift h F : (a : N) → Q) 0 = HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) 0 : Q)
zero₁ : 0 = HSMul.hSMul (β := Q) r 0
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) r 0) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) 0 : Q)
have zero₂ : Eq.{u_3 + 1} (α := Q) 0 0
Tactic: rw [smul_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
s : S
m : M
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
have tmul : (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) (r * s) ((f : (a : M) → N) m : N)) =
  HSMul.hSMul (β := Q) r
    ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
Tactic: rw [← mul_smul, hF, hF, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
s : S
m : M
tmul :
  (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) (r * s) ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
have tmul₁ : HSMul.hSMul (β := Q) (r * s) ((g : (a : M) → Q) m : Q) =
  HSMul.hSMul (β := Q) r
    ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
Tactic: rw [← mul_smul, hF, hF, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
s : S
m : M
tmul :
  (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) (r * s) ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
tmul₁ :
  HSMul.hSMul (β := Q) (r * s) ((g : (a : M) → Q) m : Q) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
have tmul₂ : HSMul.hSMul (β := Q) (r * s) ((g : (a : M) → Q) m : Q) = r • HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
Tactic: rw [← mul_smul, hF, hF, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
s : S
m : M
tmul :
  (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) (r * s) ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
tmul₁ :
  HSMul.hSMul (β := Q) (r * s) ((g : (a : M) → Q) m : Q) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
tmul₂ : HSMul.hSMul (β := Q) (r * s) ((g : (a : M) → Q) m : Q) = r • HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) r
      ((IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) : Q)
have tmul₃ : r • HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q) = r • HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
Tactic: rw [← mul_smul, hF, hF, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
x₁ x₂ : N
e₁ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₁) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
e₂ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₂) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • (x₁ + x₂)) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) (x₁ + x₂) : Q)
have add : (IsTensorProduct.lift h F : (a : N) → Q) (r • (x₁ + x₂)) =
  r •
    HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
      ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
Tactic: rw [map_add, smul_add, map_add, smul_add, e₁, e₂]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
x₁ x₂ : N
e₁ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₁) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
e₂ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₂) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
add :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • (x₁ + x₂)) =
    r •
      HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
        ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • (x₁ + x₂)) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) (x₁ + x₂) : Q)
have add₁ : (IsTensorProduct.lift h F : (a : N) → Q) (r • x₁ + r • x₂) =
  r •
    HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
      ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
Tactic: rw [map_add, smul_add, map_add, smul_add, e₁, e₂]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
x₁ x₂ : N
e₁ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₁) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
e₂ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₂) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
add :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • (x₁ + x₂)) =
    r •
      HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
        ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
add₁ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₁ + r • x₂) =
    r •
      HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
        ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • (x₁ + x₂)) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) (x₁ + x₂) : Q)
have add₂ : HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) (r • x₁) : Q)
    ((IsTensorProduct.lift h F : (a : N) → Q) (r • x₂) : Q) =
  r •
    HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
      ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
Tactic: rw [map_add, smul_add, map_add, smul_add, e₁, e₂]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
x₁ x₂ : N
e₁ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₁) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
e₂ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₂) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
add :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • (x₁ + x₂)) =
    r •
      HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
        ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
add₁ :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x₁ + r • x₂) =
    r •
      HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
        ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
add₂ :
  HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) (r • x₁) : Q)
      ((IsTensorProduct.lift h F : (a : N) → Q) (r • x₂) : Q) =
    r •
      HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q)
        ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • (x₁ + x₂)) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) (x₁ + x₂) : Q)
have add₃ : HAdd.hAdd (α := Q) (β := Q) ((IsTensorProduct.lift h F : (a : N) → Q) (r • x₁) : Q)
    ((IsTensorProduct.lift h F : (a : N) → Q) (r • x₂) : Q) =
  HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₁ : Q) +
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x₂ : Q)
Tactic: rw [map_add, smul_add, map_add, smul_add, e₁, e₂]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
x : N
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
⊢ (IsTensorProduct.lift h F : (a : N) → Q) (r • x) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x : Q)
have zero : (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) r 0) =
  HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) 0 : Q)
Tactic: induction x using h.inductionOn with
      | zero => rw [smul_zero, map_zero, smul_zero]
      | tmul s m =>
        change h.lift F (r • s • f m) = r • h.lift F (s • f m)
        rw [← mul_smul, hF, hF, mul_smul]
      | add x₁ x₂ e₁ e₂ => rw [map_add, smul_add, map_add, smul_add, e₁, e₂]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
inst_11 : Module R Q
inst_12 : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
⊢ Eq.{u_3 + 1} (α := Q) ((h.lift g : (a : N) → Q) ((f : (a : M) → N) x : N) : Q) ((g : (a : M) → Q) x : Q)
have hF : ∀ (s : S) (m : M),
  (h.lift g : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
    HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
Tactic: have hF : ∀ (s : S) (m : M), h.lift g (s • f m) = s • g m := h.lift_eq _
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
inst_11 : Module R Q
inst_12 : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF :
  ∀ (s : S) (m : M),
    (h.lift g : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((h.lift g : (a : N) → Q) ((f : (a : M) → N) x : N) : Q) ((g : (a : M) → Q) x : Q)
have h₁ : (f : (a : M) → N) x = HSMul.hSMul.{v₃, v₂, v₂} (α := S) (β := N) 1 ((f : (a : M) → N) x : N)
Tactic: convert! hF 1 x