awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
rw : subst (HAdd.hAdd (α := A⟦X⟧) 1 X - 1) (log A) = log A
rw₁ : subst X (log A) = log A
rw₂ rw₃ : log A = log A
⊢ (HAdd.hAdd (α := A⟦X⟧) 1 X).logOf = log A

Tactic:
rw [logOf_eq, add_sub_cancel_left, X_subst]

Premises used: PowerSeries.logOf_eq, add_sub_cancel_left, PowerSeries.X_subst
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
simp_rw : ∀ (h : φ.order + ψ.order = ⊤), φ.order = ⊤ ∨ ψ.order = ⊤
⊢ φ = 0 ∨ ψ = 0

Tactic:
simp_rw [← order_eq_top, order_mul] at h ⊢

Premises used: PowerSeries.order_eq_top, PowerSeries.order_mul
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ.order + ψ.order = ⊤
⊢ φ.order = ⊤ ∨ ψ.order = ⊤

Tactic:
WithTop.add_eq_top.mp h

Premises used: WithTop.add_eq_top, ENat, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ.order + ψ.order = ⊤
⊢ φ.order = ⊤ ∨ ψ.order = ⊤

Tactic:
exact WithTop.add_eq_top.mp h

Premises used: WithTop.add_eq_top, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
⊢ IsDomain.{u_1} R⟦X⟧

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
this : Eq (α := Ideal R⟦X⟧) (Ideal.span {X}) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)
rw : Ideal.IsPrime (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)
⊢ Ideal.IsPrime (α := R⟦X⟧) (Ideal.span {X})

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
this : Eq (α := Ideal R⟦X⟧) (Ideal.span {X}) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)
⊢ Ideal.IsPrime (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)

Tactic:
RingHom.ker_isPrime _

Premises used: RingHom.ker_isPrime
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
this : Eq (α := Ideal R⟦X⟧) (Ideal.span {X}) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)
⊢ Ideal.IsPrime (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)

Tactic:
exact RingHom.ker_isPrime _

Premises used: RingHom.ker_isPrime
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
suffices : Eq (α := Ideal R⟦X⟧) (Ideal.span {X}) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)
⊢ Ideal.IsPrime (α := R⟦X⟧) (Ideal.span {X})

Tactic:
suffices Ideal.span ({X} : Set R⟦X⟧) = RingHom.ker constantCoeff by
    rw [this]
    exact RingHom.ker_isPrime _
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h :
  ∀ (x : R⟦X⟧),
    Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) x ↔
      Membership.mem (γ := Ideal R⟦X⟧) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff) x
⊢ Eq (α := Ideal R⟦X⟧) (Ideal.span {X}) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)

Tactic:
apply Ideal.ext

Premises used: Ideal.ext
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
φ : R⟦X⟧
h : Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) φ ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
h₁ : X ∣ φ ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
h₂ h₃ :
  Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R) ↔
    Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) φ ↔
    Membership.mem (γ := Ideal R⟦X⟧) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff) φ

Tactic:
rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]

Premises used: RingHom.mem_ker, Ideal.mem_span_singleton, PowerSeries.X_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
rw : Ideal.IsPrime (α := R⟦X⟧) (Ideal.span {X})
rw₁ : Ne.{u_1 + 1} (α := R⟦X⟧) X 0
⊢ Prime.{u_1} (M := R⟦X⟧) X

Tactic:
rw [← Ideal.span_singleton_prime]

Premises used: Ideal.span_singleton_prime
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ Ideal.IsPrime (α := R⟦X⟧) (Ideal.span {X})

Tactic:
span_X_isPrime

Premises used: PowerSeries.span_X_isPrime
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ Ideal.IsPrime (α := R⟦X⟧) (Ideal.span {X})

Tactic:
exact span_X_isPrime

Premises used: PowerSeries.span_X_isPrime
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : Eq.{u_1 + 1} (α := R⟦X⟧) X 0
⊢ False

Tactic:
simpa [map_zero (coeff 1)] using congr_arg (coeff 1) h

Premises used: map_zero, PowerSeries.coeff, congr_arg, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ Irreducible.{u_1} (M := R⟦X⟧) X

Tactic:
X_prime.irreducible

Premises used: Prime.irreducible, PowerSeries.X_prime
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : Eq (α := R⟦X⟧) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧)
rw :
  ∀
    (h :
      ∀ (n : ℕ),
        Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
          ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R))
    (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
⊢ p = q

Tactic:
rw [PowerSeries.ext_iff] at *

Premises used: PowerSeries.ext_iff
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
      ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R)
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R)

Tactic:
specialize h n
-- Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R)
rwa :
  ∀
    (h :
      HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) p : R) =
        (coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧)),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
rwa₁ :
  ∀
    (h :
      HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) p : R) =
        HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) q : R)),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (h : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)

Tactic:
rwa [coeff_rescale, coeff_rescale, mul_right_inj' <| pow_ne_zero _ ha] at h

Premises used: PowerSeries.coeff_rescale, pow_ne_zero, mul_right_inj'
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
contrapose! : (∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔ φ = 0
⊢ (∃ (n : ℕ), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔ φ ≠ 0

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ (∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔ φ = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
⊢ order.{u_1} (R := R) 0 = ⊤

Tactic:
dif_pos rfl

Premises used: dif_pos, PowerSeries.order, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
pos : ∀ (h : φ = 0), LT.lt (α := ℕ∞) ⊤ ⊤ ↔ φ ≠ 0
neg :
  ∀ (h : ¬φ = 0),
    LT.lt (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞) ⊤ ↔
      φ ≠ 0
⊢ LT.lt (α := ℕ∞)
      (if h : φ = 0 then ⊤
      else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
      ⊤ ↔
    φ ≠ 0

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : φ = 0
⊢ LT.lt (α := ℕ∞) ⊤ ⊤ ↔ φ ≠ 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : ¬φ = 0
⊢ LT.lt (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞) ⊤ ↔
    φ ≠ 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ φ.order = ⊤ ↔ φ = 0

Tactic:
simpa using order_finite_iff_ne_zero.not_left

Premises used: PowerSeries.order_finite_iff_ne_zero, Iff.not_left
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
hf : φ ≠ 0
rw rw₁ : φ.order = φ.order
⊢ (↑φ.order.toNat : ℕ∞) = φ.order

Tactic:
rw [ENat.coe_toNat_eq_self.mpr (order_eq_top.not.mpr hf)]

Premises used: Iff.mpr, Iff.not, ENat.coe_toNat_eq_self, PowerSeries.order_eq_top
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
simp :
  Ne (α := R)
    ((coeff
            (ENat.toNat
              (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)) :
          (a : R⟦X⟧) → R)
        φ :
      R)
    (0 : R)
⊢ Ne (α := R) ((coeff φ.order.toNat : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
simp only [order, h, not_false_iff, dif_neg]

Premises used: dif_neg, PowerSeries.order, not_false_iff
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
generalize_proofs :
  ∀ (h : ∃ (n : ℕ), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)),
    Ne (α := R)
      ((coeff
              (ENat.toNat
                (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) h) : ℕ∞)) :
            (a : R⟦X⟧) → R)
          φ :
        R)
      (0 : R)
⊢ Ne (α := R)
    ((coeff
            (ENat.toNat
              (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)) :
          (a : R⟦X⟧) → R)
        φ :
      R)
    (0 : R)

Tactic:
generalize_proofs h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h_1 : φ ≠ 0
h : ∃ (n : ℕ), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Ne (α := R)
    ((coeff
            (ENat.toNat
              (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) h) : ℕ∞)) :
          (a : R⟦X⟧) → R)
        φ :
      R)
    (0 : R)

Tactic:
Nat.find_spec h

Premises used: Nat.find, ENat.toNat, WithTop.untopD, WithTop.recTopCoe, Nat.find_spec
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h_1 : φ ≠ 0
h : ∃ (n : ℕ), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Ne (α := R)
    ((coeff
            (ENat.toNat
              (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) h) : ℕ∞)) :
          (a : R⟦X⟧) → R)
        φ :
      R)
    (0 : R)

Tactic:
exact Nat.find_spec h

Premises used: Nat.find_spec
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
simp :
  Ne (α := R)
    ((coeff
            (ENat.toNat
              (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)) :
          (a : R⟦X⟧) → R)
        φ :
      R)
    (0 : R)
simp₁ :
  ∀ (h : ∃ (n : ℕ), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)),
    Ne (α := R)
      ((coeff
              (ENat.toNat
                (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) h) : ℕ∞)) :
            (a : R⟦X⟧) → R)
          φ :
        R)
      (0 : R)
⊢ Ne (α := R) ((coeff φ.order.toNat : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
classical
  simp only [order, h, not_false_iff, dif_neg]
  generalize_proofs h
  exact Nat.find_spec h

Premises used: dif_neg, PowerSeries.order, not_false_iff
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
rw :
  LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)
    (↑n : ℕ∞)
hnc : ¬φ = 0
⊢ φ.order ≤ (↑n : ℕ∞)

Tactic:
rw [order, dif_neg]

Premises used: dif_neg, PowerSeries.order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)
    (↑n : ℕ∞)

Tactic:
simpa using ⟨n, le_rfl, h⟩
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ ¬φ = 0

Tactic:
exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩

Premises used: PowerSeries.exists_coeff_ne_zero_iff_ne_zero, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ ¬φ = 0

Tactic:
exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩

Premises used: PowerSeries.exists_coeff_ne_zero_iff_ne_zero, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
rw :
  LE.le (α := ℕ∞)
    (if h : φ = 0 then ⊤
    else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
    (↑n : ℕ∞)
rw₁ :
  LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)
    (↑n : ℕ∞)
hnc : ¬φ = 0
rw₂ :
  LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)
    (↑n : ℕ∞)
hnc₁ : ¬φ = 0
rw₃ :
  LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)
    (↑n : ℕ∞)
hnc₂ hnc₃ : ¬φ = 0
⊢ φ.order ≤ (↑n : ℕ∞)

Tactic:
classical
  rw [order, dif_neg]
  · simpa using ⟨n, le_rfl, h⟩
  · exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩

Premises used: PowerSeries.exists_coeff_ne_zero_iff_ne_zero, dif_neg, PowerSeries.order, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < φ.order
contrapose! : ∀ (h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)), φ.order ≤ (↑n : ℕ∞)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ φ.order ≤ (↑n : ℕ∞)

Tactic:
order_le _ h

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

Tactic:
exact order_le _ h

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

Tactic:
by_cases h' : φ = 0
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : φ = 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
simp [h']
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
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⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
neg : (↑n : ℕ∞) < φ.order
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
refine 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⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
neg : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑φ.order.toNat : ℕ∞)
neg₁ neg₂ neg₃ neg₄ : n < φ.order.toNat
⊢ (↑n : ℕ∞) < φ.order

Tactic:
rwa [← coe_toNat_order h', ENat.coe_lt_coe]

Premises used: PowerSeries.coe_toNat_order, ENat.coe_lt_coe
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
pos : φ = 0 → LE.le (α := ℕ∞) (↑n : ℕ∞) ⊤
neg :
  ∀ (h : ¬φ = 0),
    LE.le (α := ℕ∞) (↑n : ℕ∞)
      (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞)
    (if h : φ = 0 then ⊤
    else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
h_1 : φ = 0
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
h_1 : ¬φ = 0
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞)
    (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)

Tactic:
simpa [Nat.le_find_iff]

Premises used: Nat.le_find_iff
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
simp :
  LE.le (α := ℕ∞) (↑n : ℕ∞)
    (if h : φ = 0 then ⊤
    else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
pos : φ = 0 → LE.le (α := ℕ∞) (↑n : ℕ∞) ⊤
neg neg₁ :
  ∀ (h : ¬φ = 0),
    LE.le (α := ℕ∞) (↑n : ℕ∞)
      (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)
⊢ (↑n : ℕ∞) ≤ φ.order

Tactic:
classical
  simp only [order]
  split_ifs
  · simp
  · simpa [Nat.le_find_iff]

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

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) ⊤ → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ ⊤ ≤ φ.order

Tactic:
simpa using ext (by simpa using h)

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

Tactic:
nat_le_order φ n _

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

Tactic:
convert! nat_le_order φ n _

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

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ∞
h : ∀ (i : ℕ), (↑i : ℕ∞) < n → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
top :
  ∀ (h : ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) ⊤ → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)), ⊤ ≤ φ.order
coe :
  ∀ (n : ℕ)
    (h : ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)),
    (↑n : ℕ∞) ≤ φ.order
⊢ n ≤ φ.order

Tactic:
cases n with
  | top => simpa using ext (by simpa using h)
  | coe n =>
    convert! nat_le_order φ n _
    simpa using h

Premises used: PowerSeries.ext
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
inl :
  order.{u_1} (R := R) 0 = (↑n : ℕ∞) ↔
    Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) 0 : R) (0 : R) ∧
      ∀ i < n, Eq.{u_1 + 1} (α := R) ((coeff i : (a : R⟦X⟧) → R) 0 : R) (0 : R)
inr :
  ∀ (hφ : φ ≠ 0),
    φ.order = (↑n : ℕ∞) ↔
      Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
        ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ φ.order = (↑n : ℕ∞) ↔
    Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
      ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)

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_1
inst : Semiring R
n : ℕ
⊢ order.{u_1} (R := R) 0 = (↑n : ℕ∞) ↔
    Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) 0 : R) (0 : R) ∧
      ∀ i < n, Eq.{u_1 + 1} (α := R) ((coeff i : (a : R⟦X⟧) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
hφ : φ ≠ 0
⊢ φ.order = (↑n : ℕ∞) ↔
    Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
      ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
simp [order, dif_neg hφ, Nat.find_eq_iff]

Premises used: dif_neg, PowerSeries.order, Nat.find_eq_iff
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
inl :
  order.{u_1} (R := R) 0 = (↑n : ℕ∞) ↔
    Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) 0 : R) (0 : R) ∧
      ∀ i < n, Eq.{u_1 + 1} (α := R) ((coeff i : (a : R⟦X⟧) → R) 0 : R) (0 : R)
inr inr₁ :
  ∀ (hφ : φ ≠ 0),
    φ.order = (↑n : ℕ∞) ↔
      Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
        ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ φ.order = (↑n : ℕ∞) ↔
    Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
      ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
classical
  rcases eq_or_ne φ 0 with (rfl | hφ)
  · simp
  simp [order, dif_neg hφ, Nat.find_eq_iff]

Premises used: PowerSeries.order, eq_or_ne, OfNat.ofNat, Nat.find_eq_iff, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ φ.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)

Tactic:
simp