awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin m
rw :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.reindex (Basis.prod (basis R m) (basis R n)) finSumFinEquiv : (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)
rw₁ :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.prod (basis R m) (basis R n) : (a : Fin m ⊕ Fin n) → ↥R[X]_m × ↥R[X]_n)
        ((Equiv.symm finSumFinEquiv : (a : Fin (m + n)) → Fin m ⊕ Fin n) (Fin.castAdd n i) : Fin m ⊕ Fin 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)
    ((Basis.prod (basis R m) (basis R n) : (a : Fin m ⊕ Fin n) → ↥R[X]_m × ↥R[X]_n) (Sum.inl i) : ↥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)
    (Sum.elim (β := Fin n)
        (Function.comp (β := ↥R[X]_m) (⇑(LinearMap.inl R (↥R[X]_m) ↥R[X]_n) : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n)
          (⇑(basis R m) : (a : Fin m) → ↥R[X]_m))
        (Function.comp (β := ↥R[X]_n) (⇑(LinearMap.inr R (↥R[X]_m) ↥R[X]_n) : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n)
          (⇑(basis R n) : (a : Fin n) → ↥R[X]_n))
        (Sum.inl i) :
      ↥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)
    (Function.comp (β := ↥R[X]_m) (⇑(LinearMap.inl R (↥R[X]_m) ↥R[X]_n) : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n)
        (⇑(basis R m) : (a : Fin m) → ↥R[X]_m) i :
      ↥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)
    (((fun (x : ↥R[X]_m) ↦ (x, 0)) ∘ (⇑(basis R m) : (a : Fin m) → ↥R[X]_m)) i : ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
rw₆ 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)
⊢ 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)

Tactic:
rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply,
    Sum.elim_inl, LinearMap.coe_inl, Function.comp_apply]

Premises used: Module.Basis.prod_apply, finSumFinEquiv_symm_apply_castAdd, Polynomial.degreeLT.basisProd, LinearMap.coe_inl, Sum.elim_inl, Function.comp_apply, Module.Basis.reindex_apply
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin n
rw :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.reindex (Basis.prod (basis R m) (basis R n)) finSumFinEquiv : (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)
rw₁ :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.prod (basis R m) (basis R n) : (a : Fin m ⊕ Fin n) → ↥R[X]_m × ↥R[X]_n)
        ((Equiv.symm finSumFinEquiv : (a : Fin (m + n)) → Fin m ⊕ Fin n) (Fin.natAdd m i) : Fin m ⊕ Fin 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)
    ((Basis.prod (basis R m) (basis R n) : (a : Fin m ⊕ Fin n) → ↥R[X]_m × ↥R[X]_n) (Sum.inr i) : ↥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)
    (Sum.elim (α := Fin m)
        (Function.comp (β := ↥R[X]_m) (⇑(LinearMap.inl R (↥R[X]_m) ↥R[X]_n) : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n)
          (⇑(basis R m) : (a : Fin m) → ↥R[X]_m))
        (Function.comp (β := ↥R[X]_n) (⇑(LinearMap.inr R (↥R[X]_m) ↥R[X]_n) : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n)
          (⇑(basis R n) : (a : Fin n) → ↥R[X]_n))
        (Sum.inr i) :
      ↥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)
    (Function.comp (β := ↥R[X]_n) (⇑(LinearMap.inr R (↥R[X]_m) ↥R[X]_n) : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n)
        (⇑(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)
rw₅ :
  Eq (α := ↥R[X]_m × ↥R[X]_n) ((Prod.mk 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)
rw₆ 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)
⊢ 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 [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]

Premises used: LinearMap.coe_inr, Module.Basis.prod_apply, Polynomial.degreeLT.basisProd, finSumFinEquiv_symm_apply_natAdd, Sum.elim_inr, Function.comp_apply, Module.Basis.reindex_apply
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [addLinearEquiv, Basis.equiv_apply, Equiv.refl_apply, basisProd_castAdd]

Premises used: Equiv.refl_apply, Module.Basis.equiv_apply, Polynomial.degreeLT.addLinearEquiv, Polynomial.degreeLT.basisProd_castAdd
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [addLinearEquiv, Basis.equiv_apply, Equiv.refl_apply, basisProd_natAdd]

Premises used: Equiv.refl_apply, Module.Basis.equiv_apply, Polynomial.degreeLT.addLinearEquiv, Polynomial.degreeLT.basisProd_natAdd
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin m
⊢ Eq (α := ↥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)
          ((basis R m : (a : Fin m) → ↥R[X]_m) i : ↥R[X]_m)) :
      ↥R[X]_(m + n))
    ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.castAdd n i) : ↥R[X]_(m + n))

Tactic:
(LinearEquiv.symm_apply_eq _).2 (addLinearEquiv_castAdd i).symm

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, Polynomial.degreeLT.addLinearEquiv_castAdd, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
j : Fin n
⊢ Eq (α := ↥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)
          ((basis R n : (a : Fin n) → ↥R[X]_n) j : ↥R[X]_n)) :
      ↥R[X]_(m + n))
    ((basis R (m + n) : (a : Fin (m + n)) → ↥R[X]_(m + n)) (Fin.natAdd m j) : ↥R[X]_(m + n))

Tactic:
(LinearEquiv.symm_apply_eq _).2 (addLinearEquiv_natAdd j).symm

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, Polynomial.degreeLT.addLinearEquiv_natAdd, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
P : ↥R[X]_m
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])
⊢ (↑((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])

Tactic:
rw [← (basis ..).sum_repr P]

Premises used: Polynomial.degreeLT.basis, Module.Basis.sum_repr
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
P : ↥R[X]_m
⊢ 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:
simp [-LinearMap.coe_inl, addLinearEquiv_symm_apply_inl_basis]

Premises used: LinearMap.coe_inl, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
Q : ↥R[X]_n
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
⊢ (↑((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

Tactic:
rw [← (basis ..).sum_repr Q]

Premises used: Polynomial.degreeLT.basis, Module.Basis.sum_repr
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
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)
            (∑ 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:
simp [-LinearMap.coe_inr, Finset.sum_mul, addLinearEquiv_symm_apply_inr_basis,
    smul_eq_C_mul, mul_assoc, ← pow_add, add_comm]

Premises used: LinearMap.coe_inr, Polynomial.smul_eq_C_mul, mul_assoc, pow_add, add_comm, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis, Finset.sum_mul
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
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])
rw₄ 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])
⊢ 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])

Tactic:
rw [LinearMap.inl_apply, LinearMap.inr_apply, Prod.add_def, add_zero, zero_add]

Premises used: LinearMap.inr_apply, Prod.add_def, zero_add, LinearMap.inl_apply, add_zero
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
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
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
rw₃ rw₄ :
  (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m =
    (↑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

Tactic:
rw [map_add, Submodule.coe_add, addLinearEquiv_symm_apply_inl, addLinearEquiv_symm_apply_inr]

Premises used: Polynomial.degreeLT.addLinearEquiv_symm_apply_inr, Submodule.coe_add, map_add, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
rw :
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
rw₁ rw₂ :
  (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m =
    (↑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)) PQ) : R[X]) =
    (↑PQ.1 : R[X]) + HPow.hPow (α := R[X]) X m * (↑PQ.2 : R[X])

Tactic:
rw [X_pow_mul, addLinearEquiv_symm_apply]

Premises used: Polynomial.degreeLT.addLinearEquiv_symm_apply, Polynomial.X_pow_mul
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
rw :
  (↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m =
      (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) ∧
    (↑f : R[X]) %ₘ HPow.hPow (α := R[X]) X m =
      (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])
⊢ (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) =
      (↑f : R[X]) %ₘ HPow.hPow (α := R[X]) X m ∧
    (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) =
      (↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m

Tactic:
rw [and_comm, eq_comm, eq_comm (b := _ %ₘ _)]

Premises used: and_comm, eq_comm
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
⊢ (↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m =
      (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) ∧
    (↑f : R[X]) %ₘ HPow.hPow (α := R[X]) X m =
      (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])

Tactic:
div_modByMonic_unique _ _ (monic_X_pow _) ⟨?_, ?_⟩

Premises used: Polynomial.monic_X_pow, Polynomial.div_modByMonic_unique, And.intro
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
refine_1 :
  (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) +
      HPow.hPow (α := R[X]) X m * (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) =
    (↑f : R[X])
refine_2 :
  degree.{u_2} (R := R) (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) <
    (HPow.hPow (α := R[X]) X m).degree
⊢ (↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m =
      (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) ∧
    (↑f : R[X]) %ₘ HPow.hPow (α := R[X]) X m =
      (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])

Tactic:
refine div_modByMonic_unique _ _ (monic_X_pow _) ⟨?_, ?_⟩

Premises used: Polynomial.monic_X_pow, Polynomial.div_modByMonic_unique, And.intro
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
refine_1 :
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f)) :
      R[X]) =
    (↑f : R[X])
refine_1₁ refine_1₂ : (↑f : R[X]) = (↑f : R[X])
⊢ (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) +
      HPow.hPow (α := R[X]) X m * (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) =
    (↑f : R[X])

Tactic:
rw [← addLinearEquiv_symm_apply', LinearEquiv.symm_apply_apply]

Premises used: LinearEquiv.symm_apply_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply'
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
refine_2 :
  Membership.mem (γ := Submodule R R[X]) (R[X]_m)
    (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])
⊢ degree.{u_2} (R := R) (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) <
    (HPow.hPow (α := R[X]) X m).degree

Tactic:
rw [degree_X_pow, ← mem_degreeLT]

Premises used: Polynomial.degree_X_pow, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
⊢ Membership.mem (γ := Submodule R R[X]) (R[X]_m)
    (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])

Tactic:
Subtype.prop _

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
⊢ Membership.mem (γ := Submodule R R[X]) (R[X]_m)
    (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])

Tactic:
exact Subtype.prop _

Premises used: Subtype.prop