awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
      ((g : (a : R[X]) → S) ((C : (a : R) → R[X]) a : R[X]) : S)
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
f' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = f.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : RingHom.{u, u_1} (AddMonoidAlgebra R ℕ) S := g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = g.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
C' : g = g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ)
rw : f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ) = g
rw₁ :
  Eq (α := RingHom.{u, u_1} R[X] S) (f'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
    (g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
rw₂ rw₃ :
  Eq (α := RingHom.{u, u_1} R[X] S) (g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
    (g'.comp (↑(toFinsuppIso R) : R[X] →+* AddMonoidAlgebra R ℕ))
⊢ f = g

Tactic:
rw [B, C', A]
-- Module: Mathlib.Algebra.Polynomial.Monomial
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : Semiring S
f g : RingHom.{u, u_1} R[X] S
h₁ : f.comp C = g.comp C
h₂ : Eq.{u_1 + 1} (α := S) ((f : (a : R[X]) → S) X : S) ((g : (a : R[X]) → S) X : S)
⊢ f = g

Tactic:
ringHom_ext (RingHom.congr_fun h₁) h₂

Premises used: RingHom.congr_fun, Polynomial.ringHom_ext
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := Fin n → R) ((toFn n : (a : R[X]) → Fin n → R) 0 : Fin n → R) (0 : Fin n → R)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x y : Fin n → R
a :
  ∀ (i : ℕ),
    coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
      (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
            { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
        i
⊢ { toFinsupp := (List.ofFn (x + y)).toFinsupp } =
    HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
      { toFinsupp := (List.ofFn y).toFinsupp : R[X] }

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
pos :
  ∀ (h : i < n),
    coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
      (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
            { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
        i
neg :
  ∀ (h : ¬i < n),
    coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
      (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
            { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
        i
⊢ coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
    (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
          { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
      i

Tactic:
by_cases h : i < n
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : i < n
⊢ coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
    (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
          { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
      i

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : ¬i < n
⊢ coeff { toFinsupp := (List.ofFn (x + y)).toFinsupp : R[X] } i =
    (HAdd.hAdd (α := R[X]) { toFinsupp := (List.ofFn x).toFinsupp : R[X] }
          { toFinsupp := (List.ofFn y).toFinsupp : R[X] }).coeff
      i

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x : R
p : Fin n → R
a :
  ∀ (i : ℕ),
    coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
      (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
            { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
        i
⊢ { toFinsupp := (List.ofFn (x • p)).toFinsupp } =
    HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
      { toFinsupp := (List.ofFn p).toFinsupp : R[X] }

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
pos :
  ∀ (h : i < n),
    coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
      (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
            { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
        i
neg :
  ∀ (h : ¬i < n),
    coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
      (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
            { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
        i
⊢ coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
          { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
      i

Tactic:
by_cases h : i < n
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : i < n
⊢ coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
          { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
      i

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : ¬i < n
⊢ coeff { toFinsupp := (List.ofFn (x • p)).toFinsupp : R[X] } i =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) x : R)
          { toFinsupp := (List.ofFn p).toFinsupp : R[X] }).coeff
      i

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
v : Fin 0 → R
⊢ Eq (α := R[X]) ((ofFn 0 : (a : Fin 0 → R) → R[X]) v : R[X]) (0 : R[X])

Tactic:
rfl

Premises used: List.toFinsupp, Option.getD, List.getD, Multiset.zero, Finset.empty, Multiset.ofList, List.filter, Finset.filter, rfl, Multiset.filter
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : Ne (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
contrapose : ∀ (h : n = 0), Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
⊢ n ≠ 0

Tactic:
contrapose h
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : n = 0
subst : ∀ {v : Fin 0 → R}, Eq (α := R[X]) ((ofFn 0 : (a : Fin 0 → R) → R[X]) v : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])

Tactic:
subst h
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
v : Fin 0 → R
⊢ Eq (α := R[X]) ((ofFn 0 : (a : Fin 0 → R) → R[X]) v : R[X]) (0 : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n i : ℕ
v : Fin n → R
hi : i < n
⊢ coeff ((ofFn n : (a : Fin n → R) → R[X]) v) i = v (⟨i, hi⟩ : Fin n)

Tactic:
simp [ofFn, hi]

Premises used: Polynomial.ofFn
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n i : ℕ
v : Fin n → R
hi : n ≤ i
⊢ Eq.{u_1 + 1} (α := R) (coeff ((ofFn n : (a : Fin n → R) → R[X]) v) i) 0

Tactic:
simp [ofFn, Nat.not_lt_of_ge hi]

Premises used: Nat.not_lt_of_ge, Polynomial.ofFn
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
rw : ∀ (N : ℕ), n - 1 < N → Eq.{u_1 + 1} (α := R) (coeff ((ofFn n : (a : Fin n → R) → R[X]) v) N) 0
⊢ natDegree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < n

Tactic:
rw [Nat.lt_iff_le_pred h, natDegree_le_iff_coeff_eq_zero]

Premises used: Polynomial.natDegree_le_iff_coeff_eq_zero, Nat.lt_iff_le_pred
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ∀ (N : ℕ), n - 1 < N → Eq.{u_1 + 1} (α := R) (coeff ((ofFn n : (a : Fin n → R) → R[X]) v) N) 0

Tactic:
fun _ h ↦ ofFn_coeff_eq_zero_of_ge _ <| Nat.le_of_pred_lt h

Premises used: Nat.le_of_pred_lt, Polynomial.ofFn_coeff_eq_zero_of_ge
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ∀ (N : ℕ), n - 1 < N → Eq.{u_1 + 1} (α := R) (coeff ((ofFn n : (a : Fin n → R) → R[X]) v) N) 0

Tactic:
exact fun _ h ↦ ofFn_coeff_eq_zero_of_ge _ <| Nat.le_of_pred_lt h

Premises used: Nat.le_of_pred_lt, Polynomial.ofFn_coeff_eq_zero_of_ge
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
pos :
  ∀ (h : Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])),
    degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)
neg :
  ∀ (h : ¬Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])),
    degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)
⊢ degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)

Tactic:
by_cases h : ofFn n v = 0

Premises used: DFunLike.coe, Polynomial.ofFn
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
pos : LT.lt (α := WithBot ℕ) ⊥ (↑n : WithBot ℕ)
⊢ degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)

Tactic:
simp only [h, degree_zero]

Premises used: Polynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
⊢ LT.lt (α := WithBot ℕ) ⊥ (↑n : WithBot ℕ)

Tactic:
Batteries.compareOfLessAndEq_eq_lt.mp rfl

Premises used: Batteries.compareOfLessAndEq_eq_lt, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
⊢ LT.lt (α := WithBot ℕ) ⊥ (↑n : WithBot ℕ)

Tactic:
exact Batteries.compareOfLessAndEq_eq_lt.mp rfl

Premises used: Batteries.compareOfLessAndEq_eq_lt, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
⊢ degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)

Tactic:
(natDegree_lt_iff_degree_lt h).mp
      <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr <| ne_zero_of_ofFn_ne_zero h) _

Premises used: Iff.mpr, Polynomial.natDegree_lt_iff_degree_lt, Polynomial.ne_zero_of_ofFn_ne_zero, Iff.mp, Nat.one_le_iff_ne_zero, Polynomial.ofFn_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) (0 : R[X])
⊢ degree.{u_1} (R := R) ((ofFn n : (a : Fin n → R) → R[X]) v) < (↑n : WithBot ℕ)

Tactic:
exact (natDegree_lt_iff_degree_lt h).mp
      <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr <| ne_zero_of_ofFn_ne_zero h) _

Premises used: Iff.mpr, Polynomial.natDegree_lt_iff_degree_lt, Polynomial.ne_zero_of_ofFn_ne_zero, Iff.mp, Nat.one_le_iff_ne_zero, Polynomial.ofFn_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
pos :
  ∀ (h : n = 0),
    Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
      (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
neg :
  ∀ (h : ¬n = 0),
    Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
      (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
⊢ Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])

Tactic:
by_cases h : n = 0
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : n = 0
pos :
  ∀ (v : Fin 0 → R),
    Eq (α := R[X]) ((ofFn 0 : (a : Fin 0 → R) → R[X]) v : R[X])
      (∑ i : Fin 0, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])
⊢ Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])

Tactic:
subst h
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
v : Fin 0 → R
⊢ Eq (α := R[X]) ((ofFn 0 : (a : Fin 0 → R) → R[X]) v : R[X])
    (∑ i : Fin 0, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])

Tactic:
simp [ofFn]

Premises used: Polynomial.ofFn
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬n = 0
neg :
  Eq.{u_1 + 1} (α := R[X])
    (∑ i ∈ Finset.range n, (monomial i : (a : R) → R[X]) (coeff ((ofFn n : (a : Fin n → R) → R[X]) v) i))
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i))
⊢ Eq (α := R[X]) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X])
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i) : R[X])

Tactic:
rw [as_sum_range' (ofFn n v) n <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr h) v]

Premises used: Iff.mpr, Polynomial.as_sum_range', Nat.one_le_iff_ne_zero, DFunLike.coe, Polynomial.ofFn_natDegree_lt, Polynomial.ofFn
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬n = 0
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ i ∈ Finset.range n, (monomial i : (a : R) → R[X]) (coeff ((ofFn n : (a : Fin n → R) → R[X]) v) i))
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (v i))

Tactic:
simp [Finset.sum_range]

Premises used: Finset.sum_range
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
v : Fin n → R
⊢ (toFn n : (a : R[X]) → Fin n → R) ((ofFn n : (a : Fin n → R) → R[X]) v : R[X]) = v

Tactic:
simp [toFn, ofFn, LinearMap.pi]

Premises used: Polynomial.toFn, LinearMap.pi, Polynomial.ofFn
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := Fin n → R) (β := R[X]) (⇑(ofFn n) : (a : Fin n → R) → R[X])

Tactic:
Function.LeftInverse.injective <| toFn_comp_ofFn_eq_id n

Premises used: Function.LeftInverse.injective, Polynomial.toFn_comp_ofFn_eq_id
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := R[X]) (β := Fin n → R) (⇑(toFn n) : (a : R[X]) → Fin n → R)

Tactic:
open Classical in
  Function.RightInverse.surjective <| toFn_comp_ofFn_eq_id n

Premises used: Polynomial.toFn_comp_ofFn_eq_id, Function.RightInverse.surjective
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
a : ∀ (i : ℕ), coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
⊢ (ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p) = p

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
pos : ∀ (h : i < n), coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
neg : ∀ (h : n ≤ i), coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i
⊢ coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i

Tactic:
by_cases! h : i < n
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : i < n
⊢ coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i

Tactic:
simp [h, toFn]

Premises used: Polynomial.toFn
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ p.natDegree < i

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ p.coeff i = 0

Tactic:
have : p.coeff i = 0 := coeff_eq_zero_of_natDegree_lt <| by lia
-- Module: Mathlib.Algebra.Polynomial.OfFn
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
this : p.coeff i = 0
⊢ coeff ((ofFn n : (a : Fin n → R) → R[X]) ((toFn n : (a : R[X]) → Fin n → R) p)) i = p.coeff i

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
⊢ ∃ (q : R[X]) (r : Fin 0 → R[X]),
    (∀ (i : Fin 0), (r i).degree < g.degree) ∧ f = q * HPow.hPow (β := ℕ) g 0 + ∑ i : Fin 0, r i * g ^ (↑i : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∃ (q : R[X]) (r : Fin n → R[X]),
    (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
succ :
  ∀ (q : R[X]) (r : Fin n → R[X]) (hr : ∀ (i : Fin n), (r i).degree < g.degree)
    (hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)),
    ∃ (q : R[X]) (r : Fin (n + 1) → R[X]),
      (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i : Fin (n + 1), r i * g ^ (↑i : ℕ)
⊢ ∃ (q : R[X]) (r : Fin (n + 1) → R[X]),
    (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i : Fin (n + 1), r i * g ^ (↑i : ℕ)

Tactic:
obtain ⟨q, r, hr, hf⟩ := ih
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
⊢ ∃ (q : R[X]) (r : Fin (n + 1) → R[X]),
    (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i : Fin (n + 1), r i * g ^ (↑i : ℕ)

Tactic:
⟨q /ₘ g, Fin.snoc r (q %ₘ g), fun i => ?_, hf.trans ?_⟩

Premises used: Fin.snoc, Polynomial.divByMonic, Polynomial.modByMonic, And.intro, Exists.intro, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
succ : ∀ (i : Fin (n + 1)), degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i) < g.degree
succ₁ :
  q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ) =
    q /ₘ g * g ^ (n + 1) +
      ∑ i : Fin (n + 1),
        HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i : R[X]) (g ^ (↑i : ℕ))
⊢ ∃ (q : R[X]) (r : Fin (n + 1) → R[X]),
    (∀ (i : Fin (n + 1)), (r i).degree < g.degree) ∧ f = q * g ^ (n + 1) + ∑ i : Fin (n + 1), r i * g ^ (↑i : ℕ)

Tactic:
refine ⟨q /ₘ g, Fin.snoc r (q %ₘ g), fun i => ?_, hf.trans ?_⟩
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
i : Fin n
⊢ degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i.castSucc) < g.degree

Tactic:
simpa using hr i
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
⊢ degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) (Fin.last n)) < g.degree

Tactic:
simpa using degree_modByMonic_lt q hg

Premises used: Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
i : Fin (n + 1)
succ :
  ∀ (i : Fin n), degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i.castSucc) < g.degree
succ₁ : degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) (Fin.last n)) < g.degree
⊢ degree.{u_1} (R := R) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i) < g.degree

Tactic:
cases i using Fin.lastCases with
      | cast i => simpa using hr i
      | last => simpa using degree_modByMonic_lt q hg

Premises used: cast, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
succ :
  q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ) =
    q * g ^ n +
      ∑ i : Fin n,
        HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i.castSucc : R[X])
          (g ^ (↑i.castSucc : ℕ))
⊢ q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ) =
    q /ₘ g * g ^ (n + 1) +
      ∑ i : Fin (n + 1),
        HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i : R[X]) (g ^ (↑i : ℕ))

Tactic:
rw [Fin.sum_univ_castSucc, ← add_rotate', Fin.snoc_last, Fin.val_last,
        ← add_assoc, pow_succ', ← mul_assoc, ← add_mul, mul_comm (q /ₘ g) g,
        modByMonic_add_div q]

Premises used: add_mul, Fin.sum_univ_castSucc, add_assoc, mul_assoc, Polynomial.divByMonic, add_rotate', Polynomial.modByMonic_add_div, mul_comm, pow_succ', Fin.val_last, Fin.snoc_last
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ)
⊢ q * g ^ n + ∑ i : Fin n, r i * g ^ (↑i : ℕ) =
    q * g ^ n +
      ∑ i : Fin n,
        HMul.hMul (α := R[X]) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ R[X]) r (q %ₘ g) i.castSucc : R[X])
          (g ^ (↑i.castSucc : ℕ))

Tactic:
simp