awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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.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)
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
have neg : HMul.hMul (α := R) (β := R) (0 : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: rw [coeff_of_lt_order_toNat ij.1 h', zero_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⟧
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
⊢ HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0
have neg₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_of_lt_order_toNat ij.1 h', zero_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⟧
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
⊢ HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) ((coeff ij.2 : (a : R⟦X⟧) → R) ψ : R) = 0
have neg : HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) (0 : R) = 0
Tactic: rw [coeff_of_lt_order_toNat ij.2 h', mul_zero]
-- 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)
h' : ij.2 < ψ.order.toNat
neg : HMul.hMul (α := R) (β := R) ((coeff ij.1 : (a : R⟦X⟧) → R) φ : R) (0 : 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₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_of_lt_order_toNat ij.2 h', mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
have pos : ∀ (h : f = 0 ∨ g = 0), (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
Tactic: by_cases! h : f = 0 ∨ g = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
have neg : ∀ (h : f ≠ 0 ∧ g ≠ 0), (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
Tactic: by_cases! h : f = 0 ∨ g = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f = 0 ∨ g = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
have pos : ∀ (h : f = 0), (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
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
f g : R⟦X⟧
h : f = 0 ∨ g = 0
pos : ∀ (h : f = 0), (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
have pos₁ : ∀ (h : g = 0), (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
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
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
have 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)
Tactic: apply X_pow_mul_cancel (k := f.order.toNat + g.order.toNat)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder
have 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
Tactic: rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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
⊢ 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
have 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
Tactic: rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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.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)
have 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)
Tactic: rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ 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)
have 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)
Tactic: rw [X_pow_mul, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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)
⊢ 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)
have 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)
Tactic: rw [X_pow_mul, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)
have _ : 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: calc
    _ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by
        rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
    _ = f * g := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) := by
        rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
    _ = X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder) := by
        rw [X_pow_mul, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f * 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.divXPowOrder * g.divXPowOrder)
have _₁ : HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder = f * g
Tactic: calc
    _ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by
        rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
    _ = f * g := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) := by
        rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
    _ = X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder) := by
        rw [X_pow_mul, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder
_₁ : HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder = f * g
⊢ 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)
have _₂ : f * g =
  HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * g.divXPowOrder)
Tactic: calc
    _ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by
        rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
    _ = f * g := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) := by
        rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
    _ = X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder) := by
        rw [X_pow_mul, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder
_₁ : HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder = f * g
_₂ :
  f * g =
    HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * 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.divXPowOrder * g.divXPowOrder)
have _₃ : 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: calc
    _ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by
        rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
    _ = f * g := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) := by
        rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
    _ = X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder) := by
        rw [X_pow_mul, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
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.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder
_₁ : HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder = f * g
_₂ :
  f * g =
    HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * g.divXPowOrder)
_₃ :
  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)
⊢ 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)
have _₄ : 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: calc
    _ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by
        rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
    _ = f * g := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) := by
        rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
    _ = X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder) := by
        rw [X_pow_mul, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
⊢ (p.toSubring T hp).order = p.order
have refine_1 : (p.toSubring T hp).order ≤ p.order
Tactic: refine eq_of_le_of_ge ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
refine_1 : (p.toSubring T hp).order ≤ p.order
⊢ (p.toSubring T hp).order = p.order
have refine_2 : p.order ≤ (p.toSubring T hp).order
Tactic: refine eq_of_le_of_ge ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
⊢ Tendsto f u (𝓝 g) ↔
    ∀ (d : ℕ),
      Tendsto (β := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) u
        (𝓝 ((coeff d : (a : R⟦X⟧) → R) g) : Filter R)
have rw : (∀ (d : Unit →₀ ℕ),
    Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R)) ↔
  ∀ (d : ℕ),
    Tendsto (β := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) u
      (𝓝 ((coeff d : (a : R⟦X⟧) → R) g) : Filter R)
Tactic: rw [MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto]