-- 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 ⋯
⊢ divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯

Tactic:
set dg := g.order.lift (order_finite_iff_ne_zero.mpr 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 ⋯
⊢ 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
H : X ^ (f * g).order.lift ⋯ * divided_by_X_pow_order ⋯ = f * g
⊢ divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯

Tactic:
have : f * g = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg) := by
  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:
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
this : f * g = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)
⊢ 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
H : X ^ (f * g).order.lift ⋯ * divided_by_X_pow_order ⋯ = f * g
⊢ f * g = X ^ df * divided_by_X_pow_order hf * (X ^ dg * divided_by_X_pow_order hg)

Tactic:
rw [self_eq_X_pow_order_mul_divided_by_X_pow_order,
  self_eq_X_pow_order_mul_divided_by_X_pow_order]

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 ⋯
⊢ divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯

Tactic:
have H_add_d : df + dg = dfg := by
  simp_all [df, dg, dfg, order_mul f g]

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 ⋯
H_add_d : df + dg = dfg
⊢ 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
H : X ^ (f * g).order.lift ⋯ * divided_by_X_pow_order ⋯ = f * g
this : f * g = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)
⊢ divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯

Tactic:
refine (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero (pow_ne_zero dfg X_ne_zero) ?_).symm

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 ⋯
H_add_d : df + dg = dfg
H : X ^ (f * g).order.lift ⋯ * divided_by_X_pow_order ⋯ = f * g
this : f * g = 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)

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
this : f * g = 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:
simp only [this] at H

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 ⋯
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)

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 ^ dfg * 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 [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 * X ^ dg * divided_by_X_pow_order hf * divided_by_X_pow_order hg =
    X ^ (df + dg) * divided_by_X_pow_order hf * divided_by_X_pow_order hg

Tactic:
rw [pow_add]

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
⊢ divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯

Tactic:
have H := self_eq_X_pow_order_mul_divided_by_X_pow_order (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 ⋯
H_add_d : df + dg = dfg
H : X ^ (f * g).order.lift ⋯ * divided_by_X_pow_order ⋯ = f * g
⊢ 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
⊢ divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯

Tactic:
set df := f.order.lift (order_finite_iff_ne_zero.mpr hf)

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 ⋯
⊢ 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 ⋯
⊢ df + dg = dfg

Tactic:
simp_all [df, dg, dfg, order_mul f g]

Result:
no goals