-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem divided_by_X_pow_orderMul {f g : R⟦X⟧} (hf : f ≠ 0) (hg : g ≠ 0) :
    divided_by_X_pow_order hf * divided_by_X_pow_order hg =
      divided_by_X_pow_order (mul_ne_zero hf hg)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R⟦X⟧
hf : f ≠ 0
hg : g ≠ 0
df : ℕ := f.order.lift ⋯
dg : ℕ := g.order.lift ⋯
dfg : ℕ := (f * g).order.lift ⋯
H_add_d : df + dg = dfg
H : X ^ (f * g).order.lift ⋯ * divided_by_X_pow_order ⋯ = f * g
⊢ X ^ (df + dg) * divided_by_X_pow_order hf * divided_by_X_pow_order hg =
    X ^ dfg * divided_by_X_pow_order hf * divided_by_X_pow_order hg

Tactic:
rw [H_add_d]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R⟦X⟧
hf : f ≠ 0
hg : g ≠ 0
df : ℕ := f.order.lift ⋯
dg : ℕ := g.order.lift ⋯
dfg : ℕ := (f * g).order.lift ⋯
H_add_d : df + dg = dfg
H : X ^ (f * g).order.lift ⋯ * divided_by_X_pow_order ⋯ = f * g
⊢ f * g = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)

Tactic:
calc
  f * g = X ^ df * divided_by_X_pow_order hf * (X ^ dg * divided_by_X_pow_order hg) := by
    rw [self_eq_X_pow_order_mul_divided_by_X_pow_order,
      self_eq_X_pow_order_mul_divided_by_X_pow_order]
  _ = X ^ df * X ^ dg * divided_by_X_pow_order hf * divided_by_X_pow_order hg := by ring
  _ = X ^ (df + dg) * divided_by_X_pow_order hf * divided_by_X_pow_order hg := by rw [pow_add]
  _ = X ^ dfg * divided_by_X_pow_order hf * divided_by_X_pow_order hg := by rw [H_add_d]
  _ = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg) := by rw [mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R⟦X⟧
hf : f ≠ 0
hg : g ≠ 0
df : ℕ := f.order.lift ⋯
dg : ℕ := g.order.lift ⋯
dfg : ℕ := (f * g).order.lift ⋯
H_add_d : df + dg = dfg
H : X ^ (f * g).order.lift ⋯ * divided_by_X_pow_order ⋯ = f * g
⊢ X ^ df * divided_by_X_pow_order hf * (X ^ dg * divided_by_X_pow_order hg) =
    X ^ df * X ^ dg * divided_by_X_pow_order hf * divided_by_X_pow_order hg

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R⟦X⟧
hf : f ≠ 0
hg : g ≠ 0
df : ℕ := f.order.lift ⋯
dg : ℕ := g.order.lift ⋯
⊢ divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯

Tactic:
set dfg := (f * g).order.lift (order_finite_iff_ne_zero.mpr (mul_ne_zero hf hg))

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R⟦X⟧
hf : f ≠ 0
hg : g ≠ 0
df : ℕ := f.order.lift ⋯
dg : ℕ := g.order.lift ⋯
dfg : ℕ := (f * g).order.lift ⋯
⊢ divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R⟦X⟧
hf : f ≠ 0
hg : g ≠ 0
df : ℕ := f.order.lift ⋯
dg : ℕ := g.order.lift ⋯
dfg : ℕ := (f * g).order.lift ⋯
H_add_d : df + dg = dfg
this : f * g = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)
H :
  X ^ (X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)).order.lift ⋯ * divided_by_X_pow_order ⋯ =
    X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)
⊢ X ^ dfg * divided_by_X_pow_order ⋯ = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)

Tactic:
convert H

Result:
no goals