awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin m
rw :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.equiv (basis R (m + n)) (basisProd R m n) (Equiv.refl (Fin (m + n))) :
          (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.castAdd n i) : ↥R[X]_(m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
rw₁ :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((Equiv.refl (Fin (m + n)) : (a : Fin (m + n)) → Fin (m + n)) (Fin.castAdd n i) : Fin (m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
rw₂ :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n) (Fin.castAdd n i) : ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.castAdd n i) : ↥R[X]_(m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
have rw₃ : Eq (α := ↥R[X]_m × ↥R[X]_n) (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
  (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
Tactic: rw [addLinearEquiv, Basis.equiv_apply, Equiv.refl_apply, basisProd_castAdd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin n
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.natAdd m i) : ↥R[X]_(m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
have rw : Eq (α := ↥R[X]_m × ↥R[X]_n)
  ((Basis.equiv (basis R (m + n)) (basisProd R m n) (Equiv.refl (Fin (m + n))) :
        (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
      ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.natAdd m i) : ↥R[X]_(m + n)) :
    ↥R[X]_m × ↥R[X]_n)
  ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
Tactic: rw [addLinearEquiv, Basis.equiv_apply, Equiv.refl_apply, basisProd_natAdd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin n
rw :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.equiv (basis R (m + n)) (basisProd R m n) (Equiv.refl (Fin (m + n))) :
          (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.natAdd m i) : ↥R[X]_(m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.natAdd m i) : ↥R[X]_(m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
have rw₁ : Eq (α := ↥R[X]_m × ↥R[X]_n)
  ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n)
      ((Equiv.refl (Fin (m + n)) : (a : Fin (m + n)) → Fin (m + n)) (Fin.natAdd m i) : Fin (m + n)) :
    ↥R[X]_m × ↥R[X]_n)
  ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
Tactic: rw [addLinearEquiv, Basis.equiv_apply, Equiv.refl_apply, basisProd_natAdd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin n
rw :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.equiv (basis R (m + n)) (basisProd R m n) (Equiv.refl (Fin (m + n))) :
          (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.natAdd m i) : ↥R[X]_(m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
rw₁ :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((Equiv.refl (Fin (m + n)) : (a : Fin (m + n)) → Fin (m + n)) (Fin.natAdd m i) : Fin (m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.natAdd m i) : ↥R[X]_(m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
have rw₂ : Eq (α := ↥R[X]_m × ↥R[X]_n)
  ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n) (Fin.natAdd m i) : ↥R[X]_m × ↥R[X]_n)
  ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
Tactic: rw [addLinearEquiv, Basis.equiv_apply, Equiv.refl_apply, basisProd_natAdd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin n
rw :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.equiv (basis R (m + n)) (basisProd R m n) (Equiv.refl (Fin (m + n))) :
          (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.natAdd m i) : ↥R[X]_(m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
rw₁ :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((Equiv.refl (Fin (m + n)) : (a : Fin (m + n)) → Fin (m + n)) (Fin.natAdd m i) : Fin (m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
rw₂ :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n) (Fin.natAdd m i) : ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
        ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.natAdd m i) : ↥R[X]_(m + n)) :
      ↥R[X]_m × ↥R[X]_n)
    ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
have rw₃ : Eq (α := ↥R[X]_m × ↥R[X]_n) ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
  ((0, (basis R n : (a : Fin n) → ↥R[X]_n) i) : ↥R[X]_m × ↥R[X]_n)
Tactic: rw [addLinearEquiv, Basis.equiv_apply, Equiv.refl_apply, basisProd_natAdd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
P : ↥R[X]_m
⊢ (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) P)) :
      R[X]) =
    (↑P : R[X])
have rw : Eq.{u_1 + 1} (α := R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
        ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n)
          (∑ i : Fin m,
            HSMul.hSMul (α := R) (β := ↥R[X]_m)
              ((((Basis.repr (basis R m) : (a : ↥R[X]_m) → Fin m →₀ R) P : Fin m →₀ R) : (a : Fin m) → R) i : R)
              ((basis R m : (a : Fin m) → ↥R[X]_m) i : ↥R[X]_m)))) :
    R[X])
  (↑(∑ i : Fin m,
        HSMul.hSMul (α := R) (β := ↥R[X]_m)
          ((((Basis.repr (basis R m) : (a : ↥R[X]_m) → Fin m →₀ R) P : Fin m →₀ R) : (a : Fin m) → R) i : R)
          ((basis R m : (a : Fin m) → ↥R[X]_m) i : ↥R[X]_m)) :
    R[X])
Tactic: rw [← (basis ..).sum_repr P]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
Q : ↥R[X]_n
⊢ (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) Q)) :
      R[X]) =
    (↑Q : R[X]) * HPow.hPow (α := R[X]) X m
have rw : (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
        ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n)
          (∑ i : Fin n,
            HSMul.hSMul (α := R) (β := ↥R[X]_n)
              ((((Basis.repr (basis R n) : (a : ↥R[X]_n) → Fin n →₀ R) Q : Fin n →₀ R) : (a : Fin n) → R) i : R)
              ((basis R n : (a : Fin n) → ↥R[X]_n) i : ↥R[X]_n)))) :
    R[X]) =
  (↑(∑ i : Fin n,
          HSMul.hSMul (α := R) (β := ↥R[X]_n)
            ((((Basis.repr (basis R n) : (a : ↥R[X]_n) → Fin n →₀ R) Q : Fin n →₀ R) : (a : Fin n) → R) i : R)
            ((basis R n : (a : Fin n) → ↥R[X]_n) i : ↥R[X]_n)) :
      R[X]) *
    HPow.hPow (α := R[X]) X m
Tactic: rw [← (basis ..).sum_repr Q]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1 : ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X])
have rw : Eq.{u_1 + 1} (α := R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
        (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n) (PQ.1, 0)
          ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
    R[X])
Tactic: rw [LinearMap.inl_apply, LinearMap.inr_apply, Prod.add_def, add_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
rw :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n) (PQ.1, 0)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X])
⊢ Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1 : ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X])
have rw₁ : Eq.{u_1 + 1} (α := R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) ((PQ.1, 0) + (0, PQ.2))) :
    R[X])
Tactic: rw [LinearMap.inl_apply, LinearMap.inr_apply, Prod.add_def, add_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
rw :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n) (PQ.1, 0)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X])
rw₁ :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) ((PQ.1, 0) + (0, PQ.2))) :
      R[X])
⊢ Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1 : ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X])
have rw₂ : Eq.{u_1 + 1} (α := R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
        ((PQ.1, 0).1 + (0, PQ.2).1, (PQ.1, 0).2 + (0, PQ.2).2)) :
    R[X])
Tactic: rw [LinearMap.inl_apply, LinearMap.inr_apply, Prod.add_def, add_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
rw :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n) (PQ.1, 0)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X])
rw₁ :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) ((PQ.1, 0) + (0, PQ.2))) :
      R[X])
rw₂ :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((PQ.1, 0).1 + (0, PQ.2).1, (PQ.1, 0).2 + (0, PQ.2).2)) :
      R[X])
⊢ Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1 : ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X])
have rw₃ : Eq.{u_1 + 1} (α := R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
        ((PQ.1, 0).1, (PQ.1, 0).2 + (0, PQ.2).2)) :
    R[X])
Tactic: rw [LinearMap.inl_apply, LinearMap.inr_apply, Prod.add_def, add_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
rw :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n) (PQ.1, 0)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X])
rw₁ :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) ((PQ.1, 0) + (0, PQ.2))) :
      R[X])
rw₂ :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((PQ.1, 0).1 + (0, PQ.2).1, (PQ.1, 0).2 + (0, PQ.2).2)) :
      R[X])
rw₃ :
  Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((PQ.1, 0).1, (PQ.1, 0).2 + (0, PQ.2).2)) :
      R[X])
⊢ Eq.{u_1 + 1} (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1 : ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X])
have rw₄ : Eq.{u_1 + 1} (α := R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X])
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) ((PQ.1, 0).1, (0, PQ.2).2)) :
    R[X])
Tactic: rw [LinearMap.inl_apply, LinearMap.inr_apply, Prod.add_def, add_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1 : ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
have rw : (↑(HAdd.hAdd (α := ↥R[X]_(m + n)) (β := ↥R[X]_(m + n))
        ((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1) :
          ↥R[X]_(m + n))
        ((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2) :
          ↥R[X]_(m + n))) :
    R[X]) =
  (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
Tactic: rw [map_add, Submodule.coe_add, addLinearEquiv_symm_apply_inl, addLinearEquiv_symm_apply_inr]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
rw :
  (↑(HAdd.hAdd (α := ↥R[X]_(m + n)) (β := ↥R[X]_(m + n))
          ((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
              ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1) :
            ↥R[X]_(m + n))
          ((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
              ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2) :
            ↥R[X]_(m + n))) :
      R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
⊢ (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1 : ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
have rw₁ : HAdd.hAdd (α := R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1)) :
      R[X])
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2)) :
      R[X]) =
  (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
Tactic: rw [map_add, Submodule.coe_add, addLinearEquiv_symm_apply_inl, addLinearEquiv_symm_apply_inr]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
rw :
  (↑(HAdd.hAdd (α := ↥R[X]_(m + n)) (β := ↥R[X]_(m + n))
          ((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
              ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1) :
            ↥R[X]_(m + n))
          ((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
              ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2) :
            ↥R[X]_(m + n))) :
      R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
rw₁ :
  HAdd.hAdd (α := R[X])
      (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1)) :
        R[X])
      (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2)) :
        R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
⊢ (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1 : ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
have rw₂ : (↑PQ.1 : R[X]) +
    (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2)) :
      R[X]) =
  (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
Tactic: rw [map_add, Submodule.coe_add, addLinearEquiv_symm_apply_inl, addLinearEquiv_symm_apply_inr]