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.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)
⊢ 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)
have 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)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply,
    Sum.elim_inl, LinearMap.coe_inl, Function.comp_apply]
-- 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.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)
⊢ 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)
have 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)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply,
    Sum.elim_inl, LinearMap.coe_inl, Function.comp_apply]
-- 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.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)
⊢ 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)
have 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)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply,
    Sum.elim_inl, LinearMap.coe_inl, Function.comp_apply]
-- 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.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)
⊢ 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)
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 [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply,
    Sum.elim_inl, LinearMap.coe_inl, Function.comp_apply]
-- 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)
    ((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)
have 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)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]
-- 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.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)
⊢ 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)
have 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)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]
-- 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.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)
⊢ 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)
have 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)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]
-- 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.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)
⊢ 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)
have 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)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]
-- 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.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)
⊢ 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)
have 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)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]
-- 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.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)
⊢ 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)
have 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)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]
-- 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.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)
⊢ 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)
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 [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin m
⊢ 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.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)
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 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)
⊢ 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)
  ((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)
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 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)
⊢ 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)
  ((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 [addLinearEquiv, Basis.equiv_apply, Equiv.refl_apply, basisProd_castAdd]