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
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)
h₁ : (f : (a : M) → N) x = HSMul.hSMul.{v₃, v₂, v₂} (α := S) (β := N) 1 ((f : (a : M) → N) x : N)
⊢ 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₂ : (g : (a : M) → Q) x = HSMul.hSMul.{v₃, u_3, u_3} (α := S) (β := Q) 1 ((g : (a : M) → Q) x : Q)
Tactic: convert! hF 1 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
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)
⊢ (f : (a : M) → N) x = HSMul.hSMul.{v₃, v₂, v₂} (α := S) (β := N) 1 ((f : (a : M) → N) x : N)
have h₁ : Eq.{v₂ + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
Tactic: rw [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
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)
⊢ (g : (a : M) → Q) x = HSMul.hSMul.{v₃, u_3, u_3} (α := S) (β := Q) 1 ((g : (a : M) → Q) x : Q)
have h₁ : Eq.{u_3 + 1} (α := Q) ((g : (a : M) → Q) x : Q) ((g : (a : M) → Q) x : Q)
Tactic: rw [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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
⊢ g₁ = g₂
have h₁ : ∀ (x : N), Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
Tactic: ext 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
have h₁ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) 0 : Q) ((g₂ : (a : N) → Q) 0 : Q)
Tactic: refine h.inductionOn 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
h₁ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) 0 : Q) ((g₂ : (a : N) → Q) 0 : Q)
h₂ :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
have h₃ : ∀ (s : S) (n : N),
  Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n : Q) ((g₂ : (a : N) → Q) n : Q) →
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (s • n) : Q) ((g₂ : (a : N) → Q) (s • n) : Q)
Tactic: refine h.inductionOn 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
h₁ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) 0 : Q) ((g₂ : (a : N) → Q) 0 : Q)
h₂ :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
h₃ :
  ∀ (s : S) (n : N),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n : Q) ((g₂ : (a : N) → Q) n : Q) →
      Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (s • n) : Q) ((g₂ : (a : N) → Q) (s • n) : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
have h₄ : ∀ (n₁ n₂ : N),
  Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n₁ : Q) ((g₂ : (a : N) → Q) n₁ : Q) →
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n₂ : Q) ((g₂ : (a : N) → Q) n₂ : Q) →
      Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (n₁ + n₂) : Q) ((g₂ : (a : N) → Q) (n₁ + n₂) : Q)
Tactic: refine h.inductionOn 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) 0 : Q) ((g₂ : (a : N) → Q) 0 : Q)
have h₁ : Eq.{u_3 + 1} (α := Q) (0 : Q) ((g₂ : (a : N) → Q) 0 : Q)
Tactic: rw [map_zero, map_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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
h₁ : Eq.{u_3 + 1} (α := Q) (0 : Q) ((g₂ : (a : N) → Q) 0 : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) 0 : Q) ((g₂ : (a : N) → Q) 0 : Q)
have h₂ : Eq.{u_3 + 1} (α := Q) 0 0
Tactic: rw [map_zero, map_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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
s : S
n : N
e' : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n : Q) ((g₂ : (a : N) → Q) n : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (s • n) : Q) ((g₂ : (a : N) → Q) (s • n) : Q)
have h₁ : HSMul.hSMul (β := Q) s ((g₁ : (a : N) → Q) n : Q) = (g₂ : (a : N) → Q) (s • n)
Tactic: rw [g₁.map_smul, g₂.map_smul, 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
s : S
n : N
e' : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n : Q) ((g₂ : (a : N) → Q) n : Q)
h₁ : HSMul.hSMul (β := Q) s ((g₁ : (a : N) → Q) n : Q) = (g₂ : (a : N) → Q) (s • n)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (s • n) : Q) ((g₂ : (a : N) → Q) (s • n) : Q)
have h₂ : HSMul.hSMul (β := Q) s ((g₁ : (a : N) → Q) n : Q) = HSMul.hSMul (β := Q) s ((g₂ : (a : N) → Q) n : Q)
Tactic: rw [g₁.map_smul, g₂.map_smul, 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x : N
s : S
n : N
e' : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) n : Q) ((g₂ : (a : N) → Q) n : Q)
h₁ : HSMul.hSMul (β := Q) s ((g₁ : (a : N) → Q) n : Q) = (g₂ : (a : N) → Q) (s • n)
h₂ : HSMul.hSMul (β := Q) s ((g₁ : (a : N) → Q) n : Q) = HSMul.hSMul (β := Q) s ((g₂ : (a : N) → Q) n : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (s • n) : Q) ((g₂ : (a : N) → Q) (s • n) : Q)
have h₃ : HSMul.hSMul (β := Q) s ((g₂ : (a : N) → Q) n : Q) = HSMul.hSMul (β := Q) s ((g₂ : (a : N) → Q) n : Q)
Tactic: rw [g₁.map_smul, g₂.map_smul, 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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x_1 x y : N
e₁ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
e₂ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) y : Q) ((g₂ : (a : N) → Q) y : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (x + y) : Q) ((g₂ : (a : N) → Q) (x + y) : Q)
have h₁ : HAdd.hAdd (α := Q) (β := Q) ((g₁ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) = (g₂ : (a : N) → Q) (x + y)
Tactic: rw [map_add, map_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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x_1 x y : N
e₁ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
e₂ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) y : Q) ((g₂ : (a : N) → Q) y : Q)
h₁ : HAdd.hAdd (α := Q) (β := Q) ((g₁ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) = (g₂ : (a : N) → Q) (x + y)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (x + y) : Q) ((g₂ : (a : N) → Q) (x + y) : Q)
have h₂ : HAdd.hAdd (α := Q) (β := Q) ((g₁ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) =
  HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q)
Tactic: rw [map_add, map_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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x_1 x y : N
e₁ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
e₂ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) y : Q) ((g₂ : (a : N) → Q) y : Q)
h₁ : HAdd.hAdd (α := Q) (β := Q) ((g₁ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) = (g₂ : (a : N) → Q) (x + y)
h₂ :
  HAdd.hAdd (α := Q) (β := Q) ((g₁ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) =
    HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (x + y) : Q) ((g₂ : (a : N) → Q) (x + y) : Q)
have h₃ : HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) =
  HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q)
Tactic: rw [map_add, map_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
Q : Type u_3
inst_9 : AddCommMonoid Q
inst_10 : Module S Q
g₁ g₂ : N →ₗ[S] Q
e :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
      ((g₂ : (a : N) → Q) ((f : (a : M) → N) x : N) : Q)
x_1 x y : N
e₁ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) x : Q)
e₂ : Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) y : Q) ((g₂ : (a : N) → Q) y : Q)
h₁ : HAdd.hAdd (α := Q) (β := Q) ((g₁ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) = (g₂ : (a : N) → Q) (x + y)
h₂ :
  HAdd.hAdd (α := Q) (β := Q) ((g₁ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) =
    HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q)
h₃ :
  HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₁ : (a : N) → Q) y : Q) =
    HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q)
⊢ Eq.{u_3 + 1} (α := Q) ((g₁ : (a : N) → Q) (x + y) : Q) ((g₂ : (a : N) → Q) (x + y) : Q)
have h₄ : HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q) =
  HAdd.hAdd (α := Q) (β := Q) ((g₂ : (a : N) → Q) x : Q) ((g₂ : (a : N) → Q) y : Q)
Tactic: rw [map_add, map_add, e₁, e₂]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
⊢ IsTensorProduct (M₁ := S) (M₂ := M) (M := S ⊗[R] M)
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ v₃)} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : 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] S ⊗[R] M))) :
            (M →ₗ[R] S ⊗[R] M) →ₗ[S] S →ₗ[S] M →ₗ[R] S ⊗[R] M) :
          (a : M →ₗ[R] S ⊗[R] M) → S →ₗ[S] M →ₗ[R] S ⊗[R] M)
        ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)))
have h : Eq (α := S →ₗ[R] M →ₗ[R] S ⊗[R] M)
  ((↑R :
      {S M : Type v₃} →
        {M₂ : Type (max v₁ v₃)} →
          [inst : Semiring R] →
            [inst_5 : Semiring S] →
              [inst_6 : AddCommMonoid M] →
                [inst_7 : AddCommMonoid M₂] →
                  [inst_8 : Module R M] →
                    [inst_9 : Module R M₂] →
                      [inst_10 : Module S M] →
                        [inst_11 : 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] S ⊗[R] M))) :
          (M →ₗ[R] S ⊗[R] M) →ₗ[S] S →ₗ[S] M →ₗ[R] S ⊗[R] M) :
        (a : M →ₗ[R] S ⊗[R] M) → S →ₗ[S] M →ₗ[R] S ⊗[R] M)
      ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)))
  (mk R S M)
Tactic: convert! TensorProduct.isTensorProduct R S M using 1
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
⊢ Eq (α := S →ₗ[R] M →ₗ[R] S ⊗[R] M)
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ v₃)} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : 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] S ⊗[R] M))) :
            (M →ₗ[R] S ⊗[R] M) →ₗ[S] S →ₗ[S] M →ₗ[R] S ⊗[R] M) :
          (a : M →ₗ[R] S ⊗[R] M) → S →ₗ[S] M →ₗ[R] S ⊗[R] M)
        ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)))
    (mk R S M)
have h : ∀ (s : S) (x : M),
  Eq (α := S ⊗[R] M)
    (((((↑R :
                    {S M : Type v₃} →
                      {M₂ : Type (max v₁ v₃)} →
                        [inst : Semiring R] →
                          [inst_5 : Semiring S] →
                            [inst_6 : AddCommMonoid M] →
                              [inst_7 : AddCommMonoid M₂] →
                                [inst_8 : Module R M] →
                                  [inst_9 : Module R M₂] →
                                    [inst_10 : Module S M] →
                                      [inst_11 : 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] S ⊗[R] M))) :
                        (M →ₗ[R] S ⊗[R] M) →ₗ[S] S →ₗ[S] M →ₗ[R] S ⊗[R] M) :
                      (a : M →ₗ[R] S ⊗[R] M) → S →ₗ[S] M →ₗ[R] S ⊗[R] M)
                    ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
                (a : S) → M →ₗ[R] S ⊗[R] M)
              s :
            M →ₗ[R] S ⊗[R] M) :
          (a : M) → S ⊗[R] M)
        x :
      S ⊗[R] M)
    ((((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) s : M →ₗ[R] S ⊗[R] M) : (a : M) → S ⊗[R] M) x : S ⊗[R] M)
Tactic: ext s x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
s : S
x : M
⊢ HSMul.hSMul (β := S ⊗[R] M) s (1 ⊗ₜ[R] x) = s ⊗ₜ[R] x
have h : Eq (α := S ⊗[R] M) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] x) (s ⊗ₜ[R] x)
Tactic: rw [TensorProduct.smul_tmul']
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
S : Type v₃
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : Module R M
s : S
x : M
⊢ Eq (α := S ⊗[R] M) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] x) (s ⊗ₜ[R] x)
have h : HSMul.hSMul (β := S) s 1 = s
Tactic: congr 1
-- 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) : S ⊗[R] M →ₗ[R] N).toFun (r • x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) ((↑(IsTensorProduct.equiv h) : S ⊗[R] M →ₗ[R] N).toFun x)
have change : (IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) (r • x) =
  HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
Tactic: change h.equiv (r • x) = r • h.equiv 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) (r • x) =
    HSMul.hSMul (β := N) r ((IsTensorProduct.equiv h : (a : S ⊗[R] M) → N) x : N)
have 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)
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_