awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) * ψ
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
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
⊢ False

Tactic:
rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this

Premises used: PowerSeries.coeff_mul_of_lt_order, PowerSeries.X_pow_mul
-- 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) * ψ
this : Eq (α := R) ((coeff φ.order.toNat : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ False

Tactic:
coeff_order hφ this

Premises used: PowerSeries.coeff_order
-- 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) * ψ
this : Eq (α := R) ((coeff φ.order.toNat : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ False

Tactic:
exact coeff_order hφ this

Premises used: PowerSeries.coeff_order
-- 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) * ψ
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 : LT.lt (α := ℕ∞) (↑n : ℕ∞) (if Eq.{u_2 + 1} (α := R) 1 0 then ⊤ else (↑(φ.order.toNat + 1) : ℕ∞))
⊢ (↑n : ℕ∞) < (HPow.hPow (α := R⟦X⟧) X (φ.order.toNat + 1)).order

Tactic:
rw [X_pow_eq, order_monomial]

Premises used: PowerSeries.order_monomial, PowerSeries.X_pow_eq
-- 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) * ψ
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 : ℕ∞) ⊤
neg : ¬Eq.{u_2 + 1} (α := R) 1 0 → LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(φ.order.toNat + 1) : ℕ∞)
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (if Eq.{u_2 + 1} (α := R) 1 0 then ⊤ else (↑(φ.order.toNat + 1) : ℕ∞))

Tactic:
split_ifs
-- 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) * ψ
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 : ℕ∞) ⊤

Tactic:
simp
-- 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) * ψ
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
neg : φ.order.toNat < φ.order.toNat + 1
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(φ.order.toNat + 1) : ℕ∞)

Tactic:
rw [← hn, ENat.coe_lt_coe]

Premises used: ENat.coe_lt_coe
-- 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) * ψ
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
⊢ φ.order.toNat < φ.order.toNat + 1

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
inr : ∀ (x : ℕ∞) (ho : φ.order = x), x = emultiplicity X φ
⊢ φ.order = 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

Premises used: not_le, PowerSeries.coeff_mul_of_lt_order, PowerSeries.order_monomial, PowerSeries.X_pow_mul, le_emultiplicity_of_pow_dvd, eq_comm, pow_dvd_iff_le_emultiplicity, Nat.cast_add, le_antisymm, Order.le_of_lt_add_one, ENat.coe_lt_coe, PowerSeries.order, PowerSeries.X_pow_eq, PowerSeries.X_pow_order_dvd, Nat.cast_one
-- 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 inr₁ : ∀ (hφ : φ ≠ 0), φ.order = emultiplicity X φ
⊢ φ.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

Premises used: not_le, PowerSeries.coeff_mul_of_lt_order, PowerSeries.order_monomial, PowerSeries.X_pow_mul, le_emultiplicity_of_pow_dvd, eq_comm, pow_dvd_iff_le_emultiplicity, Nat.cast_add, le_antisymm, Order.le_of_lt_add_one, ENat.coe_lt_coe, PowerSeries.order, PowerSeries.X_pow_eq, PowerSeries.X_pow_order_dvd, eq_or_ne, OfNat.ofNat, Nat.cast_one, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
⊢ order.{u_1} (R := R) 1 = 0

Tactic:
simpa using order_monomial_of_ne_zero 0 (1 : R) one_ne_zero

Premises used: one_ne_zero, OfNat.ofNat, PowerSeries.order_monomial_of_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
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
b : Prop
⊢ f.order = 0

Tactic:
apply And.left

Premises used: And.left
-- Module: Mathlib.RingTheory.PowerSeries.Order
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
⊢ (↑{ val := u, inv := v, val_inv := hu, inv_val := hv : R⟦X⟧ˣ } : R⟦X⟧).order + v.order ≤ (u * v).order

Tactic:
order_mul_ge _ _

Premises used: PowerSeries.order_mul_ge
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
⊢ order.{u_1} (R := R) X = 1

Tactic:
simpa only [Nat.cast_one] using order_monomial_of_ne_zero 1 (1 : R) one_ne_zero

Premises used: one_ne_zero, OfNat.ofNat, Nat.cast_one, PowerSeries.order_monomial_of_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
h : Ne.{u_1 + 1} (α := R) 1 0
⊢ (HPow.hPow (α := R⟦X⟧) X n).order = (↑n : ℕ∞)

Tactic:
rw [X_pow_eq, order_monomial_of_ne_zero]

Premises used: PowerSeries.X_pow_eq, PowerSeries.order_monomial_of_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
⊢ Ne.{u_1 + 1} (α := R) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
⊢ Ne.{u_1 + 1} (α := R) 1 0

Tactic:
exact one_ne_zero

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

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

Tactic:
simp [coeff_X]

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

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

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
apply : (φ * ψ).order ≤ φ.order + ψ.order
⊢ (φ * ψ).order = φ.order + ψ.order

Tactic:
apply le_antisymm _ (le_order_mul _ _)

Premises used: PowerSeries.le_order_mul, le_antisymm
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
pos : ∀ (h : φ = 0 ∨ ψ = 0), (φ * ψ).order ≤ φ.order + ψ.order
neg : ∀ (h : φ ≠ 0 ∧ ψ ≠ 0), (φ * ψ).order ≤ φ.order + ψ.order
⊢ (φ * ψ).order ≤ φ.order + ψ.order

Tactic:
by_cases! h : φ = 0 ∨ ψ = 0
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0 ∨ ψ = 0
pos : ∀ (h : φ = 0), (φ * ψ).order ≤ φ.order + ψ.order
pos₁ : ∀ (h : ψ = 0), (φ * ψ).order ≤ φ.order + ψ.order
⊢ (φ * ψ).order ≤ φ.order + ψ.order

Tactic:
rcases h with h | h
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : ψ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
neg : (φ * ψ).order ≤ (↑(φ.order.toNat + ψ.order.toNat) : ℕ∞)
⊢ (φ * ψ).order ≤ φ.order + ψ.order

Tactic:
rw [← coe_toNat_order h.1, ← coe_toNat_order h.2, ← ENat.coe_add]

Premises used: PowerSeries.coe_toNat_order, And.right, And.left, ENat.coe_add
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
neg : Ne (α := R) ((coeff (φ.order.toNat + ψ.order.toNat) : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
⊢ (φ * ψ).order ≤ (↑(φ.order.toNat + ψ.order.toNat) : ℕ∞)

Tactic:
apply order_le

Premises used: PowerSeries.order_le
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ.order.toNat, ψ.order.toNat) ∈ @antidiagonal _ Nat.instAddMonoid _ (φ.order.toNat + ψ.order.toNat)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Order
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
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
⊢ Ne (α := R) ((coeff (φ.order.toNat + ψ.order.toNat) : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)

Tactic:
rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨φ.order.toNat, ψ.order.toNat⟩ (by simp)]

Premises used: Finset.sum_eq_single_of_mem, PowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ 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:
mul_ne_zero (coeff_order h.1) (coeff_order h.2)

Premises used: PowerSeries.coeff_order, And.right, And.left, mul_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ 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:
exact mul_ne_zero (coeff_order h.1) (coeff_order h.2)

Premises used: PowerSeries.coeff_order, And.right, And.left, mul_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Order
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
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
neg₂ :
  ∀ (h' : 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

Tactic:
rcases trichotomy_of_add_eq_add (mem_antidiagonal.mp hij) with h' | h' | h'

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, trichotomy_of_add_eq_add
-- Module: Mathlib.RingTheory.PowerSeries.Order
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)
h' : ij.1 = φ.order.toNat ∧ ij.2 = ψ.order.toNat
⊢ ij = (φ.order.toNat, ψ.order.toNat)

Tactic:
simp [Prod.ext_iff, h'.1, h'.2]

Premises used: Prod.ext_iff, And.right, And.left
-- Module: Mathlib.RingTheory.PowerSeries.Order
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)
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:
exact False.elim (h (by simp [Prod.ext_iff, h'.1, h'.2]))

Premises used: False.elim
-- Module: Mathlib.RingTheory.PowerSeries.Order
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)
h' : ij.1 < φ.order.toNat
neg : HMul.hMul (α := R) (β := R) (0 : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0
neg₁ neg₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0

Tactic:
rw [coeff_of_lt_order_toNat ij.1 h', zero_mul]

Premises used: PowerSeries.coeff_of_lt_order_toNat, MulZeroClass.zero_mul, Prod.fst
-- Module: Mathlib.RingTheory.PowerSeries.Order
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)
h' : ij.2 < ψ.order.toNat
neg : HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) (0 : R) = 0
neg₁ neg₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0

Tactic:
rw [coeff_of_lt_order_toNat ij.2 h', mul_zero]

Premises used: PowerSeries.coeff_of_lt_order_toNat, MulZeroClass.mul_zero, Prod.snd
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
pos : ∀ (h : f = 0 ∨ g = 0), (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
neg : ∀ (h : f ≠ 0 ∧ g ≠ 0), (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
by_cases! h : f = 0 ∨ g = 0
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f = 0 ∨ g = 0
pos : ∀ (h : f = 0), (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
pos₁ : ∀ (h : g = 0), (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
rcases h with (h | h)
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : g = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
neg :
  HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
apply X_pow_mul_cancel (k := f.order.toNat + g.order.toNat)

Premises used: PowerSeries.X_pow_mul_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
rw :
  HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f.order + g.order).toNat * (f * g).divXPowOrder
rw₁ rw₂ :
  HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder
⊢ HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder

Tactic:
rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]

Premises used: Iff.mpr, Iff.not, And.right, And.left, ENat.toNat_add, PowerSeries.order_eq_top, PowerSeries.order_mul
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder = f * g

Tactic:
simp [X_pow_order_mul_divXPowOrder]

Premises used: PowerSeries.X_pow_order_mul_divXPowOrder
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ f * g =
    HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * g.divXPowOrder)

Tactic:
simp [X_pow_order_mul_divXPowOrder]

Premises used: PowerSeries.X_pow_order_mul_divXPowOrder
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
rw :
  HPow.hPow (α := R⟦X⟧) X f.order.toNat * (f.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * g.divXPowOrder)) =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat)
rw₁ :
  f.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * g.divXPowOrder) * HPow.hPow (α := R⟦X⟧) X f.order.toNat =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat)
rw₂ :
  f.divXPowOrder * (g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X g.order.toNat) * HPow.hPow (α := R⟦X⟧) X f.order.toNat =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat)
rw₃ :
  f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X g.order.toNat * HPow.hPow (α := R⟦X⟧) X f.order.toNat =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat)
rw₄ :
  f.divXPowOrder * g.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * HPow.hPow (α := R⟦X⟧) X f.order.toNat) =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat)
rw₅ rw₆ :
  f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat) =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat)
⊢ HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * g.divXPowOrder) =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat)

Tactic:
rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]

Premises used: mul_assoc, pow_add, PowerSeries.X_pow_mul
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
rw :
  f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat) =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat)
rw₁ rw₂ :
  f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat)
⊢ f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat) =
    HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)

Tactic:
rw [X_pow_mul, add_comm]

Premises used: PowerSeries.X_pow_mul, add_comm