awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
s : Finset ι
φ : R⟦X⟧
f : ι → R⟦X⟧
⊢ (∀ 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)
have 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)
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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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)
⊢ (∀ 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)
have 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 a s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ insert a 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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
s : Finset ι
φ : R⟦X⟧
f : ι → R⟦X⟧
⊢ (∀ 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)
have 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)
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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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)
⊢ (∀ 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)
have 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 a s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ insert a 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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Ring R
φ : R⟦X⟧
⊢ (-φ).order = φ.order
have by_contra! : ∀ (h : (-φ).order ≠ φ.order), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_2
inst : Ring R
φ : R⟦X⟧
h : (-φ).order ≠ φ.order
⊢ False
have this : φ = 0
Tactic: have : φ = 0 := by simpa using (order_add_of_order_ne _ _ h).symm
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (divXPowOrder 0) 0
have h : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (divXPowOrder 0) : R) ((coeff n : (a : R⟦X⟧) → R) 0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) (0 : R) ↔ f = 0
have pos : ∀ (h : f = 0), Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) (0 : R) ↔ f = 0
Tactic: by_cases h : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) (0 : R) ↔ f = 0
have neg : ∀ (h : ¬f = 0), Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f.divXPowOrder : R) (0 : R) ↔ f = 0
Tactic: by_cases h : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
⊢ HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder = f
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
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)
have 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)
Tactic: rw [coeff_X_pow_mul']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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)
⊢ 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)
have neg : ∀ (h : ¬f.order.toNat ≤ n), Eq (α := R) (0 : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
h : ¬f.order.toNat ≤ n
⊢ Eq (α := R) (0 : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
have h₁ : n < f.order.toNat
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
h : n < f.order.toNat
⊢ Eq (α := R) (0 : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
have neg : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_of_lt_order_toNat _ h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
⊢ φ.order = emultiplicity X φ
have inl : order.{u_2} (R := R) 0 = emultiplicity.{u_2} (α := R⟦X⟧) X 0
Tactic: rcases eq_or_ne φ 0 with (rfl | hφ)
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
inl : order.{u_2} (R := R) 0 = emultiplicity.{u_2} (α := R⟦X⟧) X 0
⊢ φ.order = emultiplicity X φ
have inr : ∀ (hφ : φ ≠ 0), φ.order = emultiplicity X φ
Tactic: rcases eq_or_ne φ 0 with (rfl | hφ)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
⊢ (↑n : ℕ∞) = emultiplicity X φ
have hn : φ.order.toNat = n
Tactic: have hn : φ.order.toNat = n := by simp [ho]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
⊢ (↑n : ℕ∞) = emultiplicity X φ
have inr : emultiplicity X φ = (↑φ.order.toNat : ℕ∞)
Tactic: rw [← hn, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
⊢ emultiplicity X φ = (↑φ.order.toNat : ℕ∞)
have inr : (↑φ.order.toNat : ℕ∞) ≤ emultiplicity X φ
Tactic: apply le_antisymm _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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 φ
⊢ emultiplicity X φ = (↑φ.order.toNat : ℕ∞)
have apply : emultiplicity X φ ≤ (↑φ.order.toNat : ℕ∞)
Tactic: apply le_antisymm _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
⊢ (↑φ.order.toNat : ℕ∞) ≤ emultiplicity X φ
have inr : HPow.hPow (α := R⟦X⟧) X φ.order.toNat ∣ φ
Tactic: apply le_emultiplicity_of_pow_dvd
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
⊢ emultiplicity X φ ≤ (↑φ.order.toNat : ℕ∞)
have h : emultiplicity X φ < HAdd.hAdd (α := ℕ∞) (↑φ.order.toNat : ℕ∞) 1
Tactic: apply Order.le_of_lt_add_one
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = (↑n : ℕ∞)
hn : φ.order.toNat = n
⊢ emultiplicity X φ < HAdd.hAdd (α := ℕ∞) (↑φ.order.toNat : ℕ∞) 1
have h : ¬HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1) ∣ φ
Tactic: rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
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) * ψ
⊢ False
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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) * ψ
this :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
    ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1) * ψ) : R)
⊢ False
have h : ∀ (this : Eq (α := R) ((coeff φ.order.toNat : (a : R⟦X⟧) → R) φ : R) (0 : R)), False
Tactic: rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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) * ψ
this :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
    ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1) * ψ) : R)
h : ∀ (this : Eq (α := R) ((coeff φ.order.toNat : (a : R⟦X⟧) → R) φ : R) (0 : R)), False
⊢ False
have h₁ : ∀
  (this :
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
      ((coeff n : (a : R⟦X⟧) → R) (ψ * HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1)) : R)),
  (↑n : ℕ∞) < (HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1)).order
Tactic: rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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) * ψ
this :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
    ((coeff n : (a : R⟦X⟧) → R) (ψ * HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1)) : R)
⊢ (↑n : ℕ∞) < (HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1)).order
have h : LT.lt (α := ℕ∞) (↑n : ℕ∞) (if Eq.{u_2 + 1} (α := R) 1 0 then ⊤ else (↑(φ.order.toNat + 1) : ℕ∞))
Tactic: rw [X_pow_eq, order_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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) * ψ
this :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
    ((coeff n : (a : R⟦X⟧) → R) (ψ * HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1)) : R)
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (if Eq.{u_2 + 1} (α := R) 1 0 then ⊤ else (↑(φ.order.toNat + 1) : ℕ∞))
have pos : Eq.{u_2 + 1} (α := R) 1 0 → LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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) * ψ
this :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
    ((coeff n : (a : R⟦X⟧) → R) (ψ * HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1)) : R)
pos : Eq.{u_2 + 1} (α := R) 1 0 → LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (if Eq.{u_2 + 1} (α := R) 1 0 then ⊤ else (↑(φ.order.toNat + 1) : ℕ∞))
have neg : ¬Eq.{u_2 + 1} (α := R) 1 0 → LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(φ.order.toNat + 1) : ℕ∞)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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) * ψ
this :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
    ((coeff n : (a : R⟦X⟧) → R) (ψ * HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1)) : R)
h : ¬Eq.{u_2 + 1} (α := R) 1 0
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(φ.order.toNat + 1) : ℕ∞)
have neg : φ.order.toNat < φ.order.toNat + 1
Tactic: rw [← hn, ENat.coe_lt_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
⊢ φ.order = emultiplicity X φ
have inr : ∀ (x : ℕ∞) (ho : φ.order = x), x = emultiplicity X φ
Tactic: cases ho : order φ with
  | top => simp [hφ] at ho
  | coe n =>
    have hn : φ.order.toNat = n := by simp [ho]
    rw [← hn, eq_comm]
    apply le_antisymm _
    · apply le_emultiplicity_of_pow_dvd
      apply X_pow_order_dvd
    · apply Order.le_of_lt_add_one
      rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]
      rintro ⟨ψ, H⟩
      have := congr_arg (coeff n) H
      rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this
      · exact coeff_order hφ this
      · rw [X_pow_eq, order_monomial]
        split_ifs
        · simp
        · rw [← hn, ENat.coe_lt_coe]
          simp
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
⊢ φ.order = emultiplicity X φ
have inl : order.{u_2} (R := R) 0 = emultiplicity.{u_2} (α := R⟦X⟧) X 0
Tactic: classical
  rcases eq_or_ne φ 0 with (rfl | hφ)
  · simp
  cases ho : order φ with
  | top => simp [hφ] at ho
  | coe n =>
    have hn : φ.order.toNat = n := by simp [ho]
    rw [← hn, eq_comm]
    apply le_antisymm _
    · apply le_emultiplicity_of_pow_dvd
      apply X_pow_order_dvd
    · apply Order.le_of_lt_add_one
      rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]
      rintro ⟨ψ, H⟩
      have := congr_arg (coeff n) H
      rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this
      · exact coeff_order hφ this
      · rw [X_pow_eq, order_monomial]
        split_ifs
        · simp
        · rw [← hn, ENat.coe_lt_coe]
          simp
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
inl : order.{u_2} (R := R) 0 = emultiplicity.{u_2} (α := R⟦X⟧) X 0
⊢ φ.order = emultiplicity X φ
have inr : ∀ (hφ : φ ≠ 0), φ.order = emultiplicity X φ
Tactic: classical
  rcases eq_or_ne φ 0 with (rfl | hφ)
  · simp
  cases ho : order φ with
  | top => simp [hφ] at ho
  | coe n =>
    have hn : φ.order.toNat = n := by simp [ho]
    rw [← hn, eq_comm]
    apply le_antisymm _
    · apply le_emultiplicity_of_pow_dvd
      apply X_pow_order_dvd
    · apply Order.le_of_lt_add_one
      rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]
      rintro ⟨ψ, H⟩
      have := congr_arg (coeff n) H
      rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this
      · exact coeff_order hφ this
      · rw [X_pow_eq, order_monomial]
        split_ifs
        · simp
        · rw [← hn, ENat.coe_lt_coe]
          simp
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : (↑{ val := u, inv := v, val_inv := hu, inv_val := hv : R⟦X⟧ˣ } : R⟦X⟧) = f
⊢ f.order = 0
have self : f.order = 0 ∧ v.order = 0
Tactic: apply And.left
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : (↑{ val := u, inv := v, val_inv := hu, inv_val := hv : R⟦X⟧ˣ } : R⟦X⟧) = f
self : f.order = 0 ∧ v.order = 0
⊢ f.order = 0
have b : Prop
Tactic: apply And.left
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
⊢ (HPow.hPow (α := R⟦X⟧) X n).order = (↑n : ℕ∞)
have h : Ne.{u_1 + 1} (α := R) 1 0
Tactic: rw [X_pow_eq, order_monomial_of_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (divXPowOrder X) 1
have h : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (divXPowOrder X) : R) ((coeff n : (a : R⟦X⟧) → R) 1 : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (divXPowOrder 1) 1
have h : ∀ (k : ℕ), Eq.{u_1 + 1} (α := R) ((coeff k : (a : R⟦X⟧) → R) (divXPowOrder 1) : R) ((coeff k : (a : R⟦X⟧) → R) 1 : R)
Tactic: ext k
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
⊢ (φ * ψ).order = φ.order + ψ.order
have apply : (φ * ψ).order ≤ φ.order + ψ.order
Tactic: apply le_antisymm _ (le_order_mul _ _)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
⊢ (φ * ψ).order ≤ φ.order + ψ.order
have pos : ∀ (h : φ = 0 ∨ ψ = 0), (φ * ψ).order ≤ φ.order + ψ.order
Tactic: by_cases! h : φ = 0 ∨ ψ = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
pos : ∀ (h : φ = 0 ∨ ψ = 0), (φ * ψ).order ≤ φ.order + ψ.order
⊢ (φ * ψ).order ≤ φ.order + ψ.order
have neg : ∀ (h : φ ≠ 0 ∧ ψ ≠ 0), (φ * ψ).order ≤ φ.order + ψ.order
Tactic: by_cases! h : φ = 0 ∨ ψ = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0 ∨ ψ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order
have pos : ∀ (h : φ = 0), (φ * ψ).order ≤ φ.order + ψ.order
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0 ∨ ψ = 0
pos : ∀ (h : φ = 0), (φ * ψ).order ≤ φ.order + ψ.order
⊢ (φ * ψ).order ≤ φ.order + ψ.order
have pos₁ : ∀ (h : ψ = 0), (φ * ψ).order ≤ φ.order + ψ.order
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order
have neg : (φ * ψ).order ≤ (↑(φ.order.toNat + ψ.order.toNat) : ℕ∞)
Tactic: rw [← coe_toNat_order h.1, ← coe_toNat_order h.2, ← ENat.coe_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ * ψ).order ≤ (↑(φ.order.toNat + ψ.order.toNat) : ℕ∞)
have neg : Ne (α := R) ((coeff (φ.order.toNat + ψ.order.toNat) : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
Tactic: apply order_le
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ Ne (α := R) ((coeff (φ.order.toNat + ψ.order.toNat) : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
have neg : HMul.hMul (α := R) (β := R) ((coeff (φ.order.toNat, ψ.order.toNat).1 : (a : R⟦X⟧) → R) φ : R)
    ((coeff (φ.order.toNat, ψ.order.toNat).2 : (a : R⟦X⟧) → R) ψ : R) ≠
  0
Tactic: rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨φ.order.toNat, ψ.order.toNat⟩ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
neg :
  HMul.hMul (α := R) (β := R) ((coeff (φ.order.toNat, ψ.order.toNat).1 : (a : R⟦X⟧) → R) φ : R)
      ((coeff (φ.order.toNat, ψ.order.toNat).2 : (a : R⟦X⟧) → R) ψ : R) ≠
    0
⊢ Ne (α := R) ((coeff (φ.order.toNat + ψ.order.toNat) : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
have neg₁ : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (φ.order.toNat + ψ.order.toNat),
  b ≠ (φ.order.toNat, ψ.order.toNat) →
    HMul.hMul (α := R) (β := R) ((coeff b.1 : (a : R⟦X⟧) → R) φ : R) ((coeff b.2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨φ.order.toNat, ψ.order.toNat⟩ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h_1 : φ ≠ 0 ∧ ψ ≠ 0
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ (φ.order.toNat + ψ.order.toNat)
h : ij ≠ (φ.order.toNat, ψ.order.toNat)
⊢ HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0
have neg : ∀ (h' : ij.1 = φ.order.toNat ∧ ij.2 = ψ.order.toNat),
  HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: rcases trichotomy_of_add_eq_add (mem_antidiagonal.mp hij) with h' | h' | h'
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h_1 : φ ≠ 0 ∧ ψ ≠ 0
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ (φ.order.toNat + ψ.order.toNat)
h : ij ≠ (φ.order.toNat, ψ.order.toNat)
neg :
  ∀ (h' : ij.1 = φ.order.toNat ∧ ij.2 = ψ.order.toNat),
    HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0
have neg₁ : ∀ (h' : ij.1 < φ.order.toNat),
  HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: rcases trichotomy_of_add_eq_add (mem_antidiagonal.mp hij) with h' | h' | h'