awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ φ.order = (↑n : ℕ∞) ↔
    (∀ (i : ℕ), Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)) ∧
      ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
simp [order_eq_nat]

Premises used: PowerSeries.order_eq_nat
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ∞
top :
  φ.order = ⊤ ↔
    (∀ (i : ℕ), Eq (α := ℕ∞) (↑i : ℕ∞) ⊤ → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)) ∧
      ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) ⊤ → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
coe :
  ∀ (n : ℕ),
    φ.order = (↑n : ℕ∞) ↔
      (∀ (i : ℕ), Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)) ∧
        ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ φ.order = n ↔
    (∀ (i : ℕ), (↑i : ℕ∞) = n → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)) ∧
      ∀ (i : ℕ), (↑i : ℕ∞) < n → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
cases n with
  | top => simp
  | coe n => simp [order_eq_nat]

Premises used: PowerSeries.order_eq_nat
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ φ.order = MvPowerSeries.order φ

Tactic:
eq_of_le_of_ge ?_ ?_

Premises used: eq_of_le_of_ge
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
refine_1 : φ.order ≤ MvPowerSeries.order φ
refine_2 : MvPowerSeries.order φ ≤ φ.order
⊢ φ.order = MvPowerSeries.order φ

Tactic:
refine eq_of_le_of_ge ?_ ?_

Premises used: eq_of_le_of_ge
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : ℕ∞) < φ.order
⊢ Eq (α := R) ((coeff ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
have : coeff ↑(Finsupp.degree d) φ = 0 := coeff_of_lt_order _ hd
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : ℕ∞) < φ.order
this : Eq (α := R) ((coeff ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ ∀ b ∈ d.support, b ≠ () → Eq (α := ℕ) ((d : (a : Unit) → ℕ) b : ℕ) (0 : ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : ℕ∞) < φ.order
this : Eq (α := R) ((coeff ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ () ∉ d.support → Eq (α := ℕ) ((d : (a : Unit) → ℕ) () : ℕ) (0 : ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : ℕ∞) < φ.order
this : Eq (α := R) ((coeff ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Eq (α := ℕ) ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d : ℕ) ((d : (a : Unit) → ℕ) () : ℕ)

Tactic:
have eq_aux : d.degree = d () := Finset.sum_eq_single _ (by simp) (by simp)
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : ℕ∞) < φ.order
this : Eq (α := R) ((coeff ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : (a : R⟦X⟧) → R) φ : R) (0 : R)
eq_aux : Eq (α := ℕ) ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d : ℕ) ((d : (a : Unit) → ℕ) () : ℕ)
⊢ Eq (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)

Tactic:
(PowerSeries.coeff_def rfl (R := R)) ▸ (eq_aux ▸ this)

Premises used: Eq.rec, PowerSeries.coeff_def, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : ℕ∞) < φ.order
this : Eq (α := R) ((coeff ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : (a : R⟦X⟧) → R) φ : R) (0 : R)
eq_aux : Eq (α := ℕ) ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d : ℕ) ((d : (a : Unit) → ℕ) () : ℕ)
⊢ Eq (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)

Tactic:
exact (PowerSeries.coeff_def rfl (R := R)) ▸ (eq_aux ▸ this)
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ φ.order ≤ MvPowerSeries.order φ

Tactic:
refine MvPowerSeries.le_order fun d hd => by
      have : coeff ↑(Finsupp.degree d) φ = 0 := coeff_of_lt_order _ hd
      have eq_aux : d.degree = d () := Finset.sum_eq_single _ (by simp) (by simp)
      exact (PowerSeries.coeff_def rfl (R := R)) ▸ (eq_aux ▸ this)

Premises used: MvPowerSeries.le_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
i : ℕ
hi : (↑i : ℕ∞) < MvPowerSeries.order φ
⊢ (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) (single () i)) : ℕ∞) < MvPowerSeries.order φ

Tactic:
rw [← Finsupp.degree_single () i] at hi

Premises used: Unit.unit, Finsupp.degree_single
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
i : ℕ
hi : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) (single () i)) : ℕ∞) < MvPowerSeries.order φ
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
MvPowerSeries.coeff_of_lt_order hi

Premises used: MvPowerSeries.coeff_of_lt_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
i : ℕ
hi : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) (single () i)) : ℕ∞) < MvPowerSeries.order φ
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
exact MvPowerSeries.coeff_of_lt_order hi

Premises used: MvPowerSeries.coeff_of_lt_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ MvPowerSeries.order φ ≤ φ.order

Tactic:
refine le_order φ (MvPowerSeries.order φ) fun i hi => by
      rw [← Finsupp.degree_single () i] at hi
      exact MvPowerSeries.coeff_of_lt_order hi

Premises used: PowerSeries.le_order, MvPowerSeries.order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
⊢ min φ.order ψ.order ≤ (φ + ψ).order

Tactic:
le_order _ _ ?_

Premises used: PowerSeries.le_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
refine : ∀ (i : ℕ), (↑i : ℕ∞) < min φ.order ψ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
⊢ min φ.order ψ.order ≤ (φ + ψ).order

Tactic:
refine le_order _ _ ?_

Premises used: PowerSeries.le_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
⊢ ∀ (i : ℕ), (↑i : ℕ∞) < min φ.order ψ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)

Tactic:
simp +contextual [coeff_of_lt_order]

Premises used: PowerSeries.coeff_of_lt_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
rw : φ.order ≤ φ.order ∧ φ.order ≤ ψ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
rw [le_inf_iff, this]

Premises used: le_inf_iff
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ φ.order ≤ φ.order ∧ φ.order ≤ ψ.order

Tactic:
⟨le_rfl, le_of_lt H⟩

Premises used: le_rfl, le_of_lt, And.intro
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ φ.order ≤ φ.order ∧ φ.order ≤ ψ.order

Tactic:
exact ⟨le_rfl, le_of_lt H⟩
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
suffices : (φ + ψ).order = φ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
suffices order (φ + ψ) = order φ by
    rw [le_inf_iff, this]
    exact ⟨le_rfl, le_of_lt H⟩
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
rw :
  (∀ (i : ℕ), (↑i : ℕ∞) = φ.order → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)) ∧
    ∀ (i : ℕ), (↑i : ℕ∞) < φ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
⊢ (φ + ψ).order = φ.order

Tactic:
rw [order_eq]

Premises used: PowerSeries.order_eq
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
left : ∀ (i : ℕ), (↑i : ℕ∞) = φ.order → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
right : ∀ (i : ℕ), (↑i : ℕ∞) < φ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
⊢ (∀ (i : ℕ), (↑i : ℕ∞) = φ.order → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)) ∧
    ∀ (i : ℕ), (↑i : ℕ∞) < φ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : (↑i : ℕ∞) = φ.order
⊢ (↑i : ℕ∞) < ψ.order

Tactic:
rw [← hi] at H
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : (↑i : ℕ∞) = φ.order
H₁ : (↑i : ℕ∞) < ψ.order
⊢ (↑i : ℕ∞) = φ.order

Tactic:
rw [← hi] at H
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : (↑i : ℕ∞) < ψ.order
hi : (↑i : ℕ∞) = φ.order
left : Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)

Tactic:
rw [(coeff _).map_add, coeff_of_lt_order i H, add_zero]

Premises used: LinearMap.map_add, PowerSeries.coeff_of_lt_order, PowerSeries.coeff, add_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : (↑i : ℕ∞) < ψ.order
hi : (↑i : ℕ∞) = φ.order
⊢ Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
(order_eq_nat.1 hi.symm).1

Premises used: And.left, Iff.mp, Eq.symm, PowerSeries.order_eq_nat
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : (↑i : ℕ∞) < ψ.order
hi : (↑i : ℕ∞) = φ.order
⊢ Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
exact (order_eq_nat.1 hi.symm).1

Premises used: And.left, Iff.mp, Eq.symm, PowerSeries.order_eq_nat
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : (↑i : ℕ∞) < φ.order
right : HAdd.hAdd (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) ((coeff i : (a : R⟦X⟧) → R) ψ : R) = 0
right₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff i : (a : R⟦X⟧) → R) ψ : R) = 0
right₂ : HAdd.hAdd (α := R) 0 0 = 0
right₃ right₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)

Tactic:
rw [(coeff _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
      zero_add]

Premises used: LinearMap.map_add, PowerSeries.coeff_of_lt_order, lt_trans, PowerSeries.coeff, zero_add
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
⊢ (φ + ψ).order = min φ.order ψ.order

Tactic:
le_antisymm ?_ (min_order_le_order_add _ _)

Premises used: PowerSeries.min_order_le_order_add, le_antisymm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
refine : (φ + ψ).order ≤ min φ.order ψ.order
⊢ (φ + ψ).order = min φ.order ψ.order

Tactic:
refine le_antisymm ?_ (min_order_le_order_add _ _)

Premises used: PowerSeries.min_order_le_order_add, le_antisymm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
inl : ∀ (φ_lt_ψ : φ.order < ψ.order), (φ + ψ).order ≤ min φ.order ψ.order
inr : ∀ (ψ_lt_φ : ψ.order < φ.order), (φ + ψ).order ≤ min φ.order ψ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
rcases h.lt_or_gt with (φ_lt_ψ | ψ_lt_φ)

Premises used: Ne.lt_or_gt
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
φ_lt_ψ : φ.order < ψ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
apply order_add_of_order_ne.aux _ _ φ_lt_ψ

Premises used: _private.0.PowerSeries.order_add_of_order_ne.aux
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
ψ_lt_φ : ψ.order < φ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
simpa only [add_comm, inf_comm] using order_add_of_order_ne.aux _ _ ψ_lt_φ

Premises used: _private.0.PowerSeries.order_add_of_order_ne.aux, inf_comm, add_comm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
S : Type u_2
inst_1 : Semiring S
f : R →+* S
i : ℕ
hi : (↑i : ℕ∞) < φ.order
⊢ Eq.{u_2 + 1} (α := S) ((coeff i : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) φ : S⟦X⟧) : S) (0 : S)

Tactic:
simp [coeff_of_lt_order i hi]

Premises used: PowerSeries.coeff_of_lt_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
a : R
i : ℕ
hi : (↑i : ℕ∞) < φ.order
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (a • φ) : R) (0 : R)

Tactic:
simp [coeff_of_lt_order i hi]

Premises used: PowerSeries.coeff_of_lt_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : ∀ (i : ℕ), (↑i : ℕ∞) < φ.order + ψ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
⊢ φ.order + ψ.order ≤ (φ * ψ).order

Tactic:
apply le_order

Premises used: PowerSeries.le_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
h :
  ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R) ((coeff x.2 : (a : R⟦X⟧) → R) ψ : R) = 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)

Tactic:
rw [coeff_mul, Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero, PowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
pos :
  ∀ (hi : (↑i : ℕ∞) < φ.order),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
neg :
  ∀ (hi : φ.order ≤ (↑i : ℕ∞)),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0

Tactic:
by_cases! hi : ↑i < order φ

Premises used: PowerSeries.order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : (↑i : ℕ∞) < φ.order
pos : HMul.hMul (α := R) (β := R) (0 : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
pos₁ pos₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0

Tactic:
rw [coeff_of_lt_order i hi, zero_mul]

Premises used: PowerSeries.coeff_of_lt_order, MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
pos :
  ∀ (hj : (↑j : ℕ∞) < ψ.order),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
neg :
  ∀ (hj : ψ.order ≤ (↑j : ℕ∞)),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0

Tactic:
by_cases! hj : ↑j < order ψ

Premises used: PowerSeries.order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
hj : (↑j : ℕ∞) < ψ.order
pos : HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) (0 : R) = 0
pos₁ pos₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0

Tactic:
rw [coeff_of_lt_order j hj, mul_zero]

Premises used: PowerSeries.coeff_of_lt_order, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
⊢ (i, j).1 + (i, j).2 = n

Tactic:
rw [mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
hij₁ : (i, j).1 + (i, j).2 = n
⊢ φ.order ≤ (↑i : ℕ∞)

Tactic:
rw [mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
hij₁ : (i, j).1 + (i, j).2 = n
hi₁ : φ.order ≤ (↑i : ℕ∞)
⊢ ψ.order ≤ (↑j : ℕ∞)

Tactic:
rw [mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
neg : False
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0

Tactic:
exfalso
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
neg : (↑n : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑i : ℕ∞) (↑j : ℕ∞)
⊢ False

Tactic:
apply ne_of_lt (lt_of_lt_of_le hn <| add_le_add hi hj)

Premises used: add_le_add, ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
neg : Eq (α := ℕ∞) (↑n : ℕ∞) (↑(i + j) : ℕ∞)
neg₁ neg₂ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ (↑n : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑i : ℕ∞) (↑j : ℕ∞)

Tactic:
rw [← Nat.cast_add, hij]

Premises used: Nat.cast_add
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ HSMul.hSMul (α := ℕ) 0 φ.order ≤ (HPow.hPow (β := ℕ) φ 0).order

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
succ : n • φ.order + HSMul.hSMul (α := ℕ) 1 φ.order ≤ (φ ^ (n + 1)).order
succ₁ : n • φ.order + φ.order ≤ (φ ^ (n + 1)).order
succ₂ : n • φ.order + φ.order ≤ (φ ^ n * φ).order
succ₃ : (φ ^ n).order + φ.order ≤ (φ ^ n * φ).order
succ₄ succ₅ : (φ ^ n * φ).order ≤ (φ ^ n * φ).order
⊢ (n + 1) • φ.order ≤ (φ ^ (n + 1)).order

Tactic:
grw [add_smul, one_smul, pow_succ, ih, le_order_mul]

Premises used: pow_succ, PowerSeries.le_order_mul, one_smul, add_smul
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
zero : HSMul.hSMul (α := ℕ) 0 φ.order ≤ (HPow.hPow (β := ℕ) φ 0).order
succ : ∀ (n : ℕ) (ih : n • φ.order ≤ (φ ^ n).order), (n + 1) • φ.order ≤ (φ ^ (n + 1)).order
⊢ n • φ.order ≤ (φ ^ n).order

Tactic:
induction n with
  | zero => simp
  | succ n ih => grw [add_smul, one_smul, pow_succ, ih, le_order_mul]

Premises used: pow_succ, PowerSeries.le_order_mul, one_smul, add_smul
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
⊢ ∑ i ∈ ∅, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ ∅, φ i)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)
cons : (φ a).order + ∑ x ∈ s, (φ x).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
cons₁ : (φ a).order + ∑ x ∈ s, (φ x).order ≤ (φ a * ∏ x ∈ s, φ x).order
cons₂ : (φ a).order + order.{u_2} (R := R) (∏ i ∈ s, φ i) ≤ (φ a * ∏ x ∈ s, φ x).order
cons₃ cons₄ : (φ a * ∏ i ∈ s, φ i).order ≤ (φ a * ∏ i ∈ s, φ i).order
⊢ ∑ i ∈ Finset.cons a s ha, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)

Tactic:
grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_order_mul]

Premises used: Finset.sum_cons, PowerSeries.le_order_mul, Finset.prod_cons
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
s : Finset ι
empty : ∑ i ∈ ∅, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ ∅, φ i)
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (ih : ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)),
    ∑ i ∈ Finset.cons a s ha, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
⊢ ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih => grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_order_mul]

Premises used: PowerSeries.le_order_mul
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
mp : 1 ≤ φ.order → Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
mpr : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R) → 1 ≤ φ.order
⊢ 1 ≤ φ.order ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : 1 ≤ φ.order
mp : Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
rw [← coeff_zero_eq_constantCoeff]

Premises used: PowerSeries.coeff_zero_eq_constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : 1 ≤ φ.order
mp : (↑0 : ℕ∞) < φ.order
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
apply coeff_of_lt_order

Premises used: PowerSeries.coeff_of_lt_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : 1 ≤ φ.order
⊢ (↑0 : ℕ∞) < φ.order

Tactic:
simpa using Order.one_le_iff_pos.mp h

Premises used: Iff.mp, Order.one_le_iff_pos
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ 1 ≤ φ.order

Tactic:
le_order _ _ fun d hd ↦ ?_

Premises used: PowerSeries.le_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
mpr : ∀ (d : ℕ) (hd : LT.lt (α := ℕ∞) (↑d : ℕ∞) 1), Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ 1 ≤ φ.order

Tactic:
refine le_order _ _ fun d hd ↦ ?_

Premises used: PowerSeries.le_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
d : ℕ
hd : LT.lt (α := ℕ∞) (↑d : ℕ∞) 1
⊢ d = 0

Tactic:
rw [Nat.cast_lt_one] at hd

Premises used: Nat.cast_lt_one
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
d : ℕ
hd : d = 0
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
simp [hd, h]