awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
rw : 1 ≤ φ.order ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
rw₁ rw₂ :
  Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R) ↔
    Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ φ.order ≠ 0 ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
rw [← ENat.one_le_iff_ne_zero, one_le_order_iff_constCoeff_eq_zero]

Premises used: PowerSeries.one_le_order_iff_constCoeff_eq_zero, ENat.one_le_iff_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ (↑n : ℕ∞) ≤ (φ ^ n).order

Tactic:
.trans ?_ (le_order_pow _ n)

Premises used: PowerSeries.le_order_pow, LE.le.trans
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
refine : (↑n : ℕ∞) ≤ n • φ.order
⊢ (↑n : ℕ∞) ≤ (φ ^ n).order

Tactic:
refine .trans ?_ (le_order_pow _ n)
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ (↑n : ℕ∞) ≤ n • φ.order

Tactic:
simpa using le_mul_of_one_le_right' (one_le_order_iff_constCoeff_eq_zero.mpr hf)

Premises used: Iff.mpr, PowerSeries.one_le_order_iff_constCoeff_eq_zero, le_mul_of_one_le_right'
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
pos : ∀ (h : a = 0), order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = ⊤
neg : ∀ (h : ¬a = 0), order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = if a = 0 then ⊤ else (↑n : ℕ∞)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : a = 0
pos : order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) 0) = ⊤
pos₁ : Eq.{u_1 + 1} (α := R⟦X⟧) ((monomial n : (a : R) → R⟦X⟧) 0 : R⟦X⟧) (0 : R⟦X⟧)
pos₂ pos₃ : Eq.{u_1 + 1} (α := R⟦X⟧) 0 0
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = ⊤

Tactic:
rw [h, order_eq_top, map_zero]

Premises used: map_zero, PowerSeries.order_eq_top
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
neg :
  (∀ (i : ℕ),
      Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
        Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)) ∧
    ∀ (i : ℕ),
      LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
        Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)

Tactic:
rw [order_eq]

Premises used: PowerSeries.order_eq
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
neg :
  ∀ (i : ℕ),
    Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
      Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
neg₁ :
  ∀ (i : ℕ),
    LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
      Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
⊢ (∀ (i : ℕ),
      Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
        Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)) ∧
    ∀ (i : ℕ),
      LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
        Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞)
⊢ i = n

Tactic:
simp only [Nat.cast_inj] at hi

Premises used: Nat.cast_inj
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i = n
neg : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
neg₁ neg₂ neg₃ neg₄ : a ≠ 0
⊢ Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)

Tactic:
rwa [hi, coeff_monomial_same]

Premises used: PowerSeries.coeff_monomial_same
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞)
⊢ i < n

Tactic:
simp only [Nat.cast_lt] at hi

Premises used: Nat.cast_lt
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
neg : ¬i = n
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)

Tactic:
rw [coeff_monomial, if_neg]

Premises used: PowerSeries.coeff_monomial, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ ¬i = n

Tactic:
ne_of_lt hi

Premises used: ne_of_lt
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ ¬i = n

Tactic:
exact ne_of_lt hi

Premises used: ne_of_lt
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
h : a ≠ 0
rw : Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑n : ℕ∞)) (↑n : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)

Tactic:
rw [order_monomial, if_neg h]

Premises used: PowerSeries.order_monomial, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
h : a ≠ 0
rw : Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑n : ℕ∞)) (↑n : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)

Tactic:
classical
  rw [order_monomial, if_neg h]

Premises used: PowerSeries.order_monomial, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
this : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0 : R)
rw : Eq.{u_1 + 1} (α := R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)

Tactic:
rw [this, Finset.sum_const_zero]

Premises used: Finset.sum_const_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
suffices : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0 : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)

Tactic:
suffices coeff n (φ * ψ) = ∑ p ∈ antidiagonal n, 0 by rw [this, Finset.sum_const_zero]
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) φ : R) ((coeff p.2 : (a : R⟦X⟧) → R) ψ : R))
    (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0 : R)

Tactic:
rw [coeff_mul]

Premises used: PowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
apply :
  ∀ 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.{u_1 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) φ : R) ((coeff p.2 : (a : R⟦X⟧) → R) ψ : R))
    (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0)

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
x : ℕ × ℕ
hx : 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

Tactic:
mul_eq_zero_of_right (coeff x.fst φ) (coeff_of_lt_order x.snd (lt_of_le_of_lt ?_ h))

Premises used: lt_of_le_of_lt, PowerSeries.coeff_of_lt_order, mul_eq_zero_of_right, PowerSeries.coeff, Prod.fst, Prod.snd, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
refine : LE.le (α := ℕ∞) (↑x.2 : ℕ∞) (↑n : ℕ∞)
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R) ((coeff x.2 : (a : R⟦X⟧) → R) ψ : R) = 0

Tactic:
refine mul_eq_zero_of_right (coeff x.fst φ) (coeff_of_lt_order x.snd (lt_of_le_of_lt ?_ h))

Premises used: lt_of_le_of_lt, PowerSeries.coeff_of_lt_order, mul_eq_zero_of_right, PowerSeries.coeff, Prod.fst, Prod.snd, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ x.1 + x.2 = n

Tactic:
rw [mem_antidiagonal] at hx

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
x : ℕ × ℕ
hx : x.1 + x.2 = n
norm_cast : x.2 ≤ n
⊢ LE.le (α := ℕ∞) (↑x.2 : ℕ∞) (↑n : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
x : ℕ × ℕ
hx : x.1 + x.2 = n
⊢ x.2 ≤ n

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Ring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * (1 - ψ)) : R) ((coeff n : (a : R⟦X⟧) → R) φ : R)

Tactic:
simp [coeff_mul_of_lt_order h, mul_sub]

Premises used: PowerSeries.coeff_mul_of_lt_order, mul_sub
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
⊢ (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ ∅, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
t : ∀ i ∈ insert a s, (↑k : ℕ∞) < (f i).order
⊢ (↑k : ℕ∞) < (f a).order ∧ ∀ a ∈ s, (↑k : ℕ∞) < (f a).order

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at t

Premises used: Finset.mem_insert, forall_eq_or_imp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
t : (↑k : ℕ∞) < (f a).order ∧ ∀ a ∈ s, (↑k : ℕ∞) < (f a).order
insert : Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ x ∈ s, (1 - f x)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ Insert.insert a s, (1 - f i)) : R)
    ((coeff k : (a : R⟦X⟧) → R) φ : R)

Tactic:
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1]

Premises used: PowerSeries.coeff_mul_one_sub_of_lt_order, Finset.prod_insert, mul_assoc, And.left, mul_right_comm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
t : (↑k : ℕ∞) < (f a).order ∧ ∀ a ∈ s, (↑k : ℕ∞) < (f a).order
⊢ Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ x ∈ s, (1 - f x)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)

Tactic:
ih t.2

Premises used: And.right
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
t : (↑k : ℕ∞) < (f a).order ∧ ∀ a ∈ s, (↑k : ℕ∞) < (f a).order
⊢ Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ x ∈ s, (1 - f x)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)

Tactic:
exact ih t.2

Premises used: And.right
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
s : Finset ι
φ : R⟦X⟧
f : ι → R⟦X⟧
empty :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ ∅, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
        Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)),
    (∀ i ∈ Insert.insert a s, (↑k : ℕ∞) < (f i).order) →
      Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ Insert.insert a s, (1 - f i)) : R)
        ((coeff k : (a : R⟦X⟧) → R) φ : R)
⊢ (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    intro t
    simp only [Finset.mem_insert, forall_eq_or_imp] at t
    rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1]
    exact ih t.2

Premises used: mul_assoc, Insert.insert, Finset.mem_insert, forall_eq_or_imp, mul_right_comm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
s : Finset ι
φ : R⟦X⟧
f : ι → R⟦X⟧
empty :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ ∅, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
        Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)),
    (∀ i ∈ Insert.insert a s, (↑k : ℕ∞) < (f i).order) →
      Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ Insert.insert a s, (1 - f i)) : R)
        ((coeff k : (a : R⟦X⟧) → R) φ : R)
⊢ (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    intro t
    simp only [Finset.mem_insert, forall_eq_or_imp] at t
    rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1]
    exact ih t.2

Premises used: mul_assoc, Insert.insert, Finset.mem_insert, forall_eq_or_imp, mul_right_comm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Ring R
φ : R⟦X⟧
by_contra! : ∀ (h : (-φ).order ≠ φ.order), False
⊢ (-φ).order = φ.order

Tactic:
by_contra! h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Ring R
φ : R⟦X⟧
h : (-φ).order ≠ φ.order
⊢ φ = 0

Tactic:
simpa using (order_add_of_order_ne _ _ h).symm

Premises used: PowerSeries.order_add_of_order_ne, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Ring R
φ : R⟦X⟧
h : (-φ).order ≠ φ.order
⊢ φ = 0

Tactic:
have : φ = 0 := by simpa using (order_add_of_order_ne _ _ h).symm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Ring R
φ : R⟦X⟧
h : (-φ).order ≠ φ.order
this : φ = 0
⊢ False

Tactic:
simp [this] at h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) f.divXPowOrder : R) ((coeff (n + f.order.toNat) : (a : R⟦X⟧) → R) f : R)

Tactic:
coeff_mk _ _

Premises used: PowerSeries.divXPowOrder, PowerSeries.coeff_mk
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
h :
  ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (divXPowOrder 0) : R) ((coeff n : (a : R⟦X⟧) → R) 0 : R)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (divXPowOrder 0) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (divXPowOrder 0) : R) ((coeff n : (a : R⟦X⟧) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) ((coeff f.order.toNat : (a : R⟦X⟧) → R) f : R)

Tactic:
simp [← coeff_zero_eq_constantCoeff]

Premises used: PowerSeries.coeff_zero_eq_constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
pos : ∀ (h : f = 0), Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) (0 : R) ↔ f = 0
neg : ∀ (h : ¬f = 0), Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) (0 : R) ↔ f = 0
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) (0 : R) ↔ f = 0

Tactic:
by_cases h : f = 0
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
h : f = 0
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) (0 : R) ↔ f = 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
h : ¬f = 0
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) (0 : R) ↔ f = 0

Tactic:
simp [constantCoeff_divXPowOrder, coeff_order h, h]

Premises used: PowerSeries.coeff_order, PowerSeries.constantCoeff_divXPowOrder
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder) : R)
      ((coeff n : (a : R⟦X⟧) → R) f : R)
⊢ HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder = f

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
h :
  Eq (α := R) (if f.order.toNat ≤ n then (coeff (n - f.order.toNat) : (a : R⟦X⟧) → R) f.divXPowOrder else 0 : R)
    ((coeff n : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder) : R)
    ((coeff n : (a : R⟦X⟧) → R) f : R)

Tactic:
rw [coeff_X_pow_mul']

Premises used: PowerSeries.coeff_X_pow_mul'
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
pos :
  ∀ (h : f.order.toNat ≤ n),
    Eq (α := R) ((coeff (n - f.order.toNat) : (a : R⟦X⟧) → R) f.divXPowOrder : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
neg : ∀ (h : ¬f.order.toNat ≤ n), Eq (α := R) (0 : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) (if f.order.toNat ≤ n then (coeff (n - f.order.toNat) : (a : R⟦X⟧) → R) f.divXPowOrder else 0 : R)
    ((coeff n : (a : R⟦X⟧) → R) f : R)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
h : f.order.toNat ≤ n
⊢ Eq (α := R) ((coeff (n - f.order.toNat) : (a : R⟦X⟧) → R) f.divXPowOrder : R) ((coeff n : (a : R⟦X⟧) → R) f : R)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
h : ¬f.order.toNat ≤ n
⊢ n < f.order.toNat

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
h : n < f.order.toNat
neg neg₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) (0 : R) ((coeff n : (a : R⟦X⟧) → R) f : R)

Tactic:
rw [coeff_of_lt_order_toNat _ h]

Premises used: PowerSeries.coeff_of_lt_order_toNat
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ HPow.hPow (α := R⟦X⟧) X φ.order.toNat ∣ φ

Tactic:
simpa only [X_pow_dvd_iff] using coeff_of_lt_order_toNat

Premises used: PowerSeries.coeff_of_lt_order_toNat, PowerSeries.X_pow_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
inl : order.{u_2} (R := R) 0 = emultiplicity.{u_2} (α := R⟦X⟧) X 0
inr : ∀ (hφ : φ ≠ 0), φ.order = emultiplicity X φ
⊢ φ.order = emultiplicity X φ

Tactic:
rcases eq_or_ne φ 0 with (rfl | hφ)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
⊢ order.{u_2} (R := R) 0 = emultiplicity.{u_2} (α := R⟦X⟧) X 0

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
ho : φ.order = ⊤
⊢ ⊤ = emultiplicity X φ

Tactic:
simp [hφ] at ho
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
⊢ φ.order.toNat = n

Tactic:
simp [ho]
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
⊢ φ.order.toNat = n

Tactic:
have hn : φ.order.toNat = n := by simp [ho]
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
inr : emultiplicity X φ = (↑φ.order.toNat : ℕ∞)
⊢ (↑n : ℕ∞) = emultiplicity X φ

Tactic:
rw [← hn, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
inr : (↑φ.order.toNat : ℕ∞) ≤ emultiplicity X φ
apply : emultiplicity X φ ≤ (↑φ.order.toNat : ℕ∞)
⊢ emultiplicity X φ = (↑φ.order.toNat : ℕ∞)

Tactic:
apply le_antisymm _

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
inr : HPow.hPow (α := R⟦X⟧) X φ.order.toNat ∣ φ
⊢ (↑φ.order.toNat : ℕ∞) ≤ emultiplicity X φ

Tactic:
apply le_emultiplicity_of_pow_dvd

Premises used: le_emultiplicity_of_pow_dvd
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
⊢ HPow.hPow (α := R⟦X⟧) X φ.order.toNat ∣ φ

Tactic:
apply X_pow_order_dvd

Premises used: PowerSeries.X_pow_order_dvd
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
h : emultiplicity X φ < HAdd.hAdd (α := ℕ∞) (↑φ.order.toNat : ℕ∞) 1
⊢ emultiplicity X φ ≤ (↑φ.order.toNat : ℕ∞)

Tactic:
apply Order.le_of_lt_add_one

Premises used: Order.le_of_lt_add_one
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
h : ¬HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1) ∣ φ
⊢ emultiplicity X φ < HAdd.hAdd (α := ℕ∞) (↑φ.order.toNat : ℕ∞) 1

Tactic:
rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]

Premises used: not_le, pow_dvd_iff_le_emultiplicity, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1) * ψ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
    ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1) * ψ) : R)

Tactic:
have := congr_arg (coeff n) H