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
r : S
x : S ⊗[R] M
refine_1 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r 0) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
have refine_2 : ∀ (x : S) (y : M),
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r (x ⊗ₜ[R] y)) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- 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
r : S
x : S ⊗[R] M
refine_1 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r 0) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
refine_2 :
  ∀ (x : S) (y : M),
    (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r (x ⊗ₜ[R] y)) =
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
have refine_3 : ∀ (x y : S ⊗[R] M),
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) →
    (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) =
        HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N) →
      (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
        HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x + y) : N)
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- 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
r : S
x : S ⊗[R] M
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r 0) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
have refine_1 : (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 =
  HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
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
r : S
x : S ⊗[R] M
refine_1 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r 0) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
have refine_1₁ : 0 = HSMul.hSMul (β := N) r 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
r : S
x : S ⊗[R] M
refine_1 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
refine_1₁ : 0 = HSMul.hSMul (β := N) r 0
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (HSMul.hSMul (β := S ⊗[R] M) r 0) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) 0 : N)
have refine_1₂ : Eq.{v₂ + 1} (α := N) 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
r : S
x_1 x y : S ⊗[R] M
hx :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
hy :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x + y) : N)
have refine_3 : (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
  r •
    HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
Tactic: rw [map_add, smul_add, map_add, smul_add, hx, hy]
-- 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
r : S
x_1 x y : S ⊗[R] M
hx :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
hy :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x + y) : N)
have refine_3₁ : (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x + r • y) =
  r •
    HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
Tactic: rw [map_add, smul_add, map_add, smul_add, hx, hy]
-- 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
r : S
x_1 x y : S ⊗[R] M
hx :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
hy :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₁ :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x + r • y) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x + y) : N)
have refine_3₂ : HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) : N)
    ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
  r •
    HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
Tactic: rw [map_add, smul_add, map_add, smul_add, hx, hy]
-- 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
r : S
x_1 x y : S ⊗[R] M
hx :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
hy :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₁ :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x + r • y) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₂ :
  HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x + y) : N)
have refine_3₃ : HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) : N)
    ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
  HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
Tactic: rw [map_add, smul_add, map_add, smul_add, hx, hy]
-- 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
r : S
x_1 x y : S ⊗[R] M
hx :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
hy :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₁ :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x + r • y) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₂ :
  HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₃ :
  HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x + y) : N)
have refine_3₄ : HAdd.hAdd (β := N) (HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N))
    ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
  HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
Tactic: rw [map_add, smul_add, map_add, smul_add, hx, hy]
-- 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
r : S
x_1 x y : S ⊗[R] M
hx :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
hy :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3 :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₁ :
  (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x + r • y) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₂ :
  HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
    r •
      HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
        ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₃ :
  HAdd.hAdd (α := N) (β := N) ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) : N)
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
refine_3₄ :
  HAdd.hAdd (β := N) (HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N))
      ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • y) : N) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
      HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
⊢ (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • (x + y)) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (x + y) : N)
have refine_3₅ : HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N) =
  HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N) +
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) y : N)
Tactic: rw [map_add, smul_add, map_add, smul_add, hx, hy]
-- 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
m : M
⊢ Eq (α := S ⊗[R] M) ((h.equiv.symm : (a : N) → S ⊗[R] M) ((f : (a : M) → N) m) : S ⊗[R] M) (1 ⊗ₜ[R] m : S ⊗[R] M)
have rw : Eq.{v₂ + 1} (α := N) ((f : (a : M) → N) m : N) ((h.equiv : (a : S ⊗[R] M) → N) (1 ⊗ₜ[R] m) : N)
Tactic: rw [h.equiv.symm_apply_eq, h.equiv_tmul, one_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
m : M
rw : Eq.{v₂ + 1} (α := N) ((f : (a : M) → N) m : N) ((h.equiv : (a : S ⊗[R] M) → N) (1 ⊗ₜ[R] m) : N)
⊢ Eq (α := S ⊗[R] M) ((h.equiv.symm : (a : N) → S ⊗[R] M) ((f : (a : M) → N) m) : S ⊗[R] M) (1 ⊗ₜ[R] m : S ⊗[R] M)
have rw₁ : (f : (a : M) → N) m = HSMul.hSMul.{v₃, v₂, v₂} (α := S) (β := N) 1 ((f : (a : M) → N) m : N)
Tactic: rw [h.equiv.symm_apply_eq, h.equiv_tmul, one_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
m : M
rw : Eq.{v₂ + 1} (α := N) ((f : (a : M) → N) m : N) ((h.equiv : (a : S ⊗[R] M) → N) (1 ⊗ₜ[R] m) : N)
rw₁ : (f : (a : M) → N) m = HSMul.hSMul.{v₃, v₂, v₂} (α := S) (β := N) 1 ((f : (a : M) → N) m : N)
⊢ Eq (α := S ⊗[R] M) ((h.equiv.symm : (a : N) → S ⊗[R] M) ((f : (a : M) → N) m) : S ⊗[R] M) (1 ⊗ₜ[R] m : S ⊗[R] M)
have rw₂ : Eq.{v₂ + 1} (α := N) ((f : (a : M) → N) m : N) ((f : (a : M) → N) m : N)
Tactic: rw [h.equiv.symm_apply_eq, h.equiv_tmul, one_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
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), Eq.{v₂ + 1} (α := N) ((e : (a : S ⊗[R] M) → N) (1 ⊗ₜ[R] x) : N) ((f : (a : M) → N) x : N)
⊢ IsBaseChange S f
have apply : ∀ (x : S) (y : M),
  Eq.{v₂ + 1} (α := N) ((LinearEquiv.restrictScalars R e : (a : S ⊗[R] M) → N) (x ⊗ₜ[R] y) : N)
    (((((↑R :
                    {S M : Type v₃} →
                      {M₂ : Type (max v₁ v₂)} →
                        [inst : Semiring R] →
                          [inst_9 : Semiring S] →
                            [inst_10 : AddCommMonoid M] →
                              [inst_11 : AddCommMonoid M₂] →
                                [inst_12 : Module R M] →
                                  [inst_13 : Module R M₂] →
                                    [inst_14 : Module S M] →
                                      [inst_15 : 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] N))) :
                        (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
                      (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
                    f) :
                (a : S) → M →ₗ[R] N)
              x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
Tactic: apply IsTensorProduct.of_equiv (e.restrictScalars R)
-- 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
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
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ (↑eM : M →ₗ[R] P) = (↑(LinearEquiv.restrictScalars R eN) : N →ₗ[R] Q) ∘ₗ f
⊢ IsTensorProduct.{u_1, v₃, v₁, v₂} (M₁ := S) (M₂ := M) (M := N)
      ((↑R :
          {S M : Type v₃} →
            {M₂ : Type (max v₁ 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] N))) : (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
            (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
          f)) ↔
    IsTensorProduct.{u_1, v₃, u_2, u_3} (M₁ := S) (M₂ := P) (M := Q)
      ((↑R :
          {S M : Type v₃} →
            {M₂ : Type (max u_2 u_3)} →
              [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 (P →ₗ[R] Q))) : (P →ₗ[R] Q) →ₗ[S] S →ₗ[S] P →ₗ[R] Q) :
            (a : P →ₗ[R] Q) → S →ₗ[S] P →ₗ[R] Q)
          f'))
have this : ∀ (m : M),
  Eq.{u_3 + 1} (α := Q) ((f' : (a : P) → Q) ((eM : (a : M) → P) m : P) : Q)
    ((eN : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
Tactic: have (m : M) : f' (eM m) = eN (f m) := LinearMap.congr_fun comm m