awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial m : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial m : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
have zero : Eq (α := A ⊗[R] MvPolynomial σ R)
  ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
      ((monomial 0 : (a : A) → MvPolynomial σ A) a) :
    A ⊗[R] MvPolynomial σ R)
  (a ⊗ₜ[R] (monomial 0 : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
Tactic: apply @Finsupp.induction σ ℕ _ _ m
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
zero :
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial 0 : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial 0 : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial m : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial m : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
have single_add : ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
  a_1 ∉ f.support →
    b ≠ 0 →
      Eq (α := A ⊗[R] MvPolynomial σ R)
          ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
              ((monomial f : (a : A) → MvPolynomial σ A) a) :
            A ⊗[R] MvPolynomial σ R)
          (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R) →
        Eq (α := A ⊗[R] MvPolynomial σ R)
          ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
              ((monomial (Finsupp.single a_1 b + f) : (a : A) → MvPolynomial σ A) a) :
            A ⊗[R] MvPolynomial σ R)
          (a ⊗ₜ[R] (monomial (Finsupp.single a_1 b + f) : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
Tactic: apply @Finsupp.induction σ ℕ _ _ m
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
h : i ∉ f.support
h_1 : n ≠ 0
hfa :
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial f : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial (Finsupp.single i n + f) : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial (Finsupp.single i n + f) : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
have single_add : HMul.hMul (α := A ⊗[R] MvPolynomial σ R) (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1)
    (1 ⊗ₜ[R] HPow.hPow (α := MvPolynomial σ R) (X i) n) =
  a ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n)
Tactic: simp only [add_comm, monomial_add_single, map_mul, map_pow, aeval_X,
      Algebra.TensorProduct.tmul_pow, one_pow, hfa]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
h : i ∉ f.support
h_1 : n ≠ 0
hfa :
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial f : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
⊢ HMul.hMul (α := A ⊗[R] MvPolynomial σ R) (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1)
      (1 ⊗ₜ[R] HPow.hPow (α := MvPolynomial σ R) (X i) n) =
    a ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n)
have single_add : HMul.hMul (α := A ⊗[R] MvPolynomial σ R) (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1)
    (1 ⊗ₜ[R] HPow.hPow (α := MvPolynomial σ R) (X i) n) =
  (a * 1) ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n)
Tactic: nth_rw 2 [← mul_one a]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
h : i ∉ f.support
h_1 : n ≠ 0
hfa :
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial f : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
⊢ HMul.hMul (α := A ⊗[R] MvPolynomial σ R) (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1)
      (1 ⊗ₜ[R] HPow.hPow (α := MvPolynomial σ R) (X i) n) =
    (a * 1) ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n)
have single_add : Eq (α := A ⊗[R] MvPolynomial σ R)
  ((a * 1) ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n))
  ((a * 1) ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n))
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ Eq (α := MvPolynomial σ R →ₐ[R] A ⊗[R] MvPolynomial σ R)
    (AlgHom.comp
      (AlgHom.restrictScalars R
        (↑(AlgEquiv.symm (algebraTensorAlgEquiv R A)) : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R))
      (mapAlgHom (Algebra.ofId R A)))
    Algebra.TensorProduct.includeRight
have hf : ∀ (i : σ),
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgHom.comp
            (AlgHom.restrictScalars R
              (↑(AlgEquiv.symm (algebraTensorAlgEquiv R A)) : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R))
            (mapAlgHom (Algebra.ofId R A)) :
          (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R)
        (X i) :
      A ⊗[R] MvPolynomial σ R)
    ((Algebra.TensorProduct.includeRight : (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R) (X i) :
      A ⊗[R] MvPolynomial σ R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
a : R
⊢ Eq (α := N ⊗[R] S)
    ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) ((C : (a : R) → MvPolynomial σ R) a) :
      N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : N ⊗[R] S)
have C : Eq (α := N ⊗[R] S) ((algebraMap R N : (a : R) → N) a ⊗ₜ[R] 1 : N ⊗[R] S)
  (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
Tactic: simp only [algHom_C, Algebra.TensorProduct.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
a : R
⊢ Eq (α := N ⊗[R] S) ((algebraMap R N : (a : R) → N) a ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
have C : Eq (α := N ⊗[R] S) (HMul.hMul (α := N) (β := N) ((algebraMap R N : (a : R) → N) a : N) (1 : N) ⊗ₜ[R] 1 : N ⊗[R] S)
  (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
Tactic: rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
a : R
C :
  Eq (α := N ⊗[R] S) (HMul.hMul (α := N) (β := N) ((algebraMap R N : (a : R) → N) a : N) (1 : N) ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
⊢ Eq (α := N ⊗[R] S) ((algebraMap R N : (a : R) → N) a ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
have C₁ : Eq (α := N ⊗[R] S) (HSMul.hSMul (β := N) a 1 ⊗ₜ[R] 1 : N ⊗[R] S) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
Tactic: rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
a : R
C :
  Eq (α := N ⊗[R] S) (HMul.hMul (α := N) (β := N) ((algebraMap R N : (a : R) → N) a : N) (1 : N) ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
C₁ :
  Eq (α := N ⊗[R] S) (HSMul.hSMul (β := N) a 1 ⊗ₜ[R] 1 : N ⊗[R] S) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
⊢ Eq (α := N ⊗[R] S) ((algebraMap R N : (a : R) → N) a ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
have C₂ : Eq (α := N ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a)
Tactic: rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
a : R
C :
  Eq (α := N ⊗[R] S) (HMul.hMul (α := N) (β := N) ((algebraMap R N : (a : R) → N) a : N) (1 : N) ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
C₁ :
  Eq (α := N ⊗[R] S) (HSMul.hSMul (β := N) a 1 ⊗ₜ[R] 1 : N ⊗[R] S) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
C₂ : Eq (α := N ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a)
⊢ Eq (α := N ⊗[R] S) ((algebraMap R N : (a : R) → N) a ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
have C₃ : Eq (α := N ⊗[R] S) (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) (1 : S))
  (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a)
Tactic: rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
a : R
C :
  Eq (α := N ⊗[R] S) (HMul.hMul (α := N) (β := N) ((algebraMap R N : (a : R) → N) a : N) (1 : N) ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
C₁ :
  Eq (α := N ⊗[R] S) (HSMul.hSMul (β := N) a 1 ⊗ₜ[R] 1 : N ⊗[R] S) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
C₂ : Eq (α := N ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a)
C₃ :
  Eq (α := N ⊗[R] S) (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) (1 : S))
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a)
⊢ Eq (α := N ⊗[R] S) ((algebraMap R N : (a : R) → N) a ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
have C₄ : Eq (α := N ⊗[R] S) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
  (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
Tactic: rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
p : MvPolynomial σ R
⊢ Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S)
have C : ∀ (a : R),
  Eq (α := N ⊗[R] S)
    ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) ((C : (a : R) → MvPolynomial σ R) a) :
      N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : N ⊗[R] S)
Tactic: induction p using MvPolynomial.induction_on with
  | C a =>
    simp only [algHom_C, Algebra.TensorProduct.algebraMap_apply]
    rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
  | add p q hp hq => simp [hp, hq, tmul_add]
  | mul_X p i h => simp [h]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := N ⊗[R] S)
      ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
        N ⊗[R] S)
      (1 ⊗ₜ[R]
          (aeval f : (a : MvPolynomial σ R) → S) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) :
        N ⊗[R] S)
⊢ Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S)
have add : ∀ (p q : MvPolynomial σ R)
  (hp :
    Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
      (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S))
  (hq :
    Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) q : N ⊗[R] S)
      (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) q : N ⊗[R] S)),
  Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) (p + q) : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) (p + q) : N ⊗[R] S)
Tactic: induction p using MvPolynomial.induction_on with
  | C a =>
    simp only [algHom_C, Algebra.TensorProduct.algebraMap_apply]
    rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
  | add p q hp hq => simp [hp, hq, tmul_add]
  | mul_X p i h => simp [h]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := N ⊗[R] S)
      ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
        N ⊗[R] S)
      (1 ⊗ₜ[R]
          (aeval f : (a : MvPolynomial σ R) → S) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) :
        N ⊗[R] S)
add :
  ∀ (p q : MvPolynomial σ R)
    (hp :
      Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
        (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S))
    (hq :
      Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) q : N ⊗[R] S)
        (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) q : N ⊗[R] S)),
    Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) (p + q) : N ⊗[R] S)
      (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) (p + q) : N ⊗[R] S)
⊢ Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S)
have mul_X : ∀ (p : MvPolynomial σ R) (i : σ)
  (h :
    Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
      (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S)),
  Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) (p * X i) : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) (p * X i) : N ⊗[R] S)
Tactic: induction p using MvPolynomial.induction_on with
  | C a =>
    simp only [algHom_C, Algebra.TensorProduct.algebraMap_apply]
    rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
  | add p q hp hq => simp [hp, hq, tmul_add]
  | mul_X p i h => simp [h]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Nontrivial (hypothesis)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
ha : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
inst_5 : IsDomain A
inst_6 : IsDomain B
⊢ Nontrivial (A ⊗[R] B)
have this : IsDomain R
Tactic: haveI := ha.isDomain _
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Pi (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
x y : A ⊗[R] ((i : ι) → B i)
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (x * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          x :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
have zero : ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
      (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
    (0 * y) =
  HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
    (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        0 :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        y :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Pi (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
x y : A ⊗[R] ((i : ι) → B i)
zero :
  ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (0 * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          0 :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (x * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          x :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
have tmul : ∀ (x : A) (y_1 : (i : ι) → B i),
  ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (x ⊗ₜ[R] y_1 * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
Tactic: induction x
Cleared hypotheses: x