awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
h : ¬k < n
neg :
  HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0) 0 =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
neg₁ :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
    (if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0)
⊢ HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
have neg₂ : Eq.{u_1 + 1} (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0) (if k = n then 1 else 0)
Tactic: rw [Finset.sum_eq_zero fun x _ ↦ if_neg (by cases x; lia), add_zero, dif_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Monic (R := MvPolynomial (Fin n) R) (freeMonic R n)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin n) R →ₐ[R] S
⊢ (fun (p : MonicDegreeEq S n) ↦ (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
      ((fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom) f) =
    f
have hf : ∀ (i : Fin n),
  Eq.{u_2 + 1} (α := S)
    (((fun (p : MonicDegreeEq S n) ↦
              (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
            ((fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
              f) :
          (a : MvPolynomial (Fin n) R) → S)
        (X i) :
      S)
    ((f : (a : MvPolynomial (Fin n) R) → S) (X i) : S)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
this : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p : S[X]).coeff i
⊢ (fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
      ((fun (p : MonicDegreeEq S n) ↦
          (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
        p) =
    p
have a : ∀ (i : ℕ),
  Polynomial.coeff
      (↑((fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
            ((fun (p : MonicDegreeEq S n) ↦
                (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
              p)) :
        S[X])
      i =
    (↑p : S[X]).coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
⊢ (fun (f : MvPolynomial (Fin n) R →ₐ[R] S) ↦ MonicDegreeEq.map (MonicDegreeEq.freeMonic R n) f.toRingHom)
      ((fun (p : MonicDegreeEq S n) ↦
          (aeval fun (x : Fin n) ↦ (↑p : S[X]).coeff (↑x : ℕ) : MvPolynomial (Fin n) R →ₐ[R] S))
        p) =
    p
have suffices : ∀ i ≥ n, (if i = n then 1 else 0) = (↑p : S[X]).coeff i
Tactic: suffices ∀ i ≥ n, (if i = n then 1 else 0) = p.1.coeff i by
      ext i; simp +contextual [coeff_freeMonic, apply_dite, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
i : ℕ
hi : i ≥ n
⊢ (if i = n then 1 else 0) = (↑p : S[X]).coeff i
have pos : ∀ (hi' : i = n), 1 = (↑p : S[X]).coeff i
Tactic: split_ifs with hi'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
i : ℕ
hi : i ≥ n
pos : ∀ (hi' : i = n), 1 = (↑p : S[X]).coeff i
⊢ (if i = n then 1 else 0) = (↑p : S[X]).coeff i
have neg : ∀ (hi' : ¬i = n), 0 = (↑p : S[X]).coeff i
Tactic: split_ifs with hi'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n : ℕ
p : MonicDegreeEq S n
g : S →ₐ[R] T
⊢ Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (↑g : S →+* T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    (g.comp ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p) :
      MvPolynomial (Fin n) R →ₐ[R] T)
have obtain : ∀ (f : MvPolynomial (Fin n) R →ₐ[R] S),
  Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (MonicDegreeEq.map ((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f)
          (↑g : S →+* T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    (g.comp
        ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
          ((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n) f)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
Tactic: obtain ⟨f, rfl⟩ := (mapEquivMonic R S n).surjective p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n : ℕ
p : MonicDegreeEq S n
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
⊢ Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (algebraMap S T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    (AlgHom.comp (IsScalarTower.toAlgHom R S T)
        ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p) :
      MvPolynomial (Fin n) R →ₐ[R] T)
have rw : Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
  ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
      (p.map (algebraMap S T)) :
    MvPolynomial (Fin n) R →ₐ[R] T)
  ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
      (p.map (↑(IsScalarTower.toAlgHom R S T) : S →+* T)) :
    MvPolynomial (Fin n) R →ₐ[R] T)
Tactic: rw [← mapEquivMonic_symm_map, IsScalarTower.coe_toAlgHom]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n : ℕ
p : MonicDegreeEq S n
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
rw :
  Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (algebraMap S T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (↑(IsScalarTower.toAlgHom R S T) : S →+* T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
⊢ Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
    ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
        (p.map (algebraMap S T)) :
      MvPolynomial (Fin n) R →ₐ[R] T)
    (AlgHom.comp (IsScalarTower.toAlgHom R S T)
        ((Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p) :
      MvPolynomial (Fin n) R →ₐ[R] T)
have rw₁ : Eq (α := MvPolynomial (Fin n) R →ₐ[R] T)
  ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
      (p.map (algebraMap S T)) :
    MvPolynomial (Fin n) R →ₐ[R] T)
  ((Equiv.symm (mapEquivMonic R T n) : (a : MonicDegreeEq T n) → MvPolynomial (Fin n) R →ₐ[R] T)
      (p.map (algebraMap S T)) :
    MvPolynomial (Fin n) R →ₐ[R] T)
Tactic: rw [← mapEquivMonic_symm_map, IsScalarTower.coe_toAlgHom]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn_1 hn : n = m + k
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                    (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                  Algebra.TensorProduct.includeLeft) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                    (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                  Algebra.TensorProduct.includeRight) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
        n =
      1 ∧
    ∀ i > n,
      (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                      (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                    Algebra.TensorProduct.includeLeft) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                      (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                    Algebra.TensorProduct.includeRight) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
          i =
        0
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn_1 hn : n = m + k
h : Nontrivial R
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                    (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                  Algebra.TensorProduct.includeLeft) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                    (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                  Algebra.TensorProduct.includeRight) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
        n =
      1 ∧
    ∀ i > n,
      (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                      (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                    Algebra.TensorProduct.includeLeft) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                      (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                    Algebra.TensorProduct.includeRight) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
          i =
        0
have a : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
Tactic: nontriviality MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                    (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                  Algebra.TensorProduct.includeLeft) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
            (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                    (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                      MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                  Algebra.TensorProduct.includeRight) :
              (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
        n =
      1 ∧
    ∀ i > n,
      (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                      (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
                    Algebra.TensorProduct.includeLeft) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
              (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                      (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                        MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                    Algebra.TensorProduct.includeRight) :
                (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).coeff
          i =
        0
have refine_1 : (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
    (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
            (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
              MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
          Algebra.TensorProduct.includeLeft) :
      (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
    (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
            (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
              MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
          Algebra.TensorProduct.includeRight) :
      (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).Monic
Tactic: refine (MonicDegreeEq.mk _ ?_ ?_).2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
        (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                  MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
              Algebra.TensorProduct.includeLeft) :
          (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
        (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                  MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
              Algebra.TensorProduct.includeRight) :
          (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])).natDegree =
    n
have refine_2 : (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (Polynomial.map
        (↑Algebra.TensorProduct.includeLeft :
          MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R m))
      (Polynomial.map
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R k))).natDegree =
  n
Tactic: dsimp [mapEquivMonic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
        (Polynomial.map
          (↑Algebra.TensorProduct.includeLeft :
            MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R m))
        (Polynomial.map
          (↑Algebra.TensorProduct.includeRight :
            MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R k))).natDegree =
    n
have refine_2 : natDegree
      (Polynomial.map
        (↑Algebra.TensorProduct.includeLeft :
          MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R m)) +
    natDegree
      (Polynomial.map
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R k)) =
  n
Tactic: rw [((monic_freeMonic R m).map _).natDegree_mul ((monic_freeMonic R k).map _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ natDegree
        (Polynomial.map
          (↑Algebra.TensorProduct.includeLeft :
            MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R m)) +
      natDegree
        (Polynomial.map
          (↑Algebra.TensorProduct.includeRight :
            MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R k)) =
    n
have refine_2 : natDegree (R := MvPolynomial (Fin m) R) (freeMonic R m) + natDegree (R := MvPolynomial (Fin k) R) (freeMonic R k) = n
Tactic: simp_rw [(monic_freeMonic R _).natDegree_map, natDegree_freeMonic, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn_1 hn : n = m + k
h : Nontrivial R
h_1 : Nontrivial.{u_1} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
refine_2 :
  natDegree (R := MvPolynomial (Fin m) R) (freeMonic R m) + natDegree (R := MvPolynomial (Fin k) R) (freeMonic R k) = n
⊢ natDegree
        (Polynomial.map
          (↑Algebra.TensorProduct.includeLeft :
            MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R m)) +
      natDegree
        (Polynomial.map
          (↑Algebra.TensorProduct.includeRight :
            MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R k)) =
    n
have refine_2₁ : m + k = n
Tactic: simp_rw [(monic_freeMonic R _).natDegree_map, natDegree_freeMonic, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
⊢ Polynomial.map
      (↑(universalFactorizationMap R n m k hn) :
        MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (freeMonic R n) =
    HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
      (Polynomial.map (R := MvPolynomial (Fin m) R)
        (algebraMap (MvPolynomial (Fin m) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (freeMonic R m))
      (Polynomial.map
        (↑Algebra.TensorProduct.includeRight :
          MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
        (freeMonic R k))
have change : (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) n :
          (a : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
            MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) n)
        (universalFactorizationMap R n m k hn)) :
    (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X]) =
  HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
    (Polynomial.map (R := MvPolynomial (Fin m) R)
      (algebraMap (MvPolynomial (Fin m) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) (freeMonic R m))
    (Polynomial.map
      (↑Algebra.TensorProduct.includeRight :
        MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (freeMonic R k))
Tactic: change (mapEquivMonic _ _ _ (universalFactorizationMap R n m k hn)).1 = _