awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ_1 : Type u_1
R_1 : Type u_2
inst : Semiring R_1
w_1 : σ_1 → ℕ
f_1 g_1 : MvPowerSeries σ_1 R_1
σ : Type u_1
R : Type u_2
inst_1 : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g

Tactic:
exact ⟨le_rfl, le_of_lt H₁⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
⊢ weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)

Tactic:
apply le_weightedOrder

Premises used: MvPowerSeries.le_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
h :
  ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)

Tactic:
rw [coeff_mul, Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
pos :
  ∀ (hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
neg :
  ∀ (hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0

Tactic:
by_cases! hi : weight w i < f.weightedOrder w

Premises used: Finsupp.weight, MvPowerSeries.weightedOrder, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f
pos : HMul.hMul (α := R) (β := R) (0 : R) ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) = 0
pos₁ pos₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0

Tactic:
rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]

Premises used: MulZeroClass.zero_mul, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
pos :
  ∀ (hj : (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞) < weightedOrder w g),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
neg :
  ∀ (hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0

Tactic:
by_cases! hj : weight w j < g.weightedOrder w

Premises used: Finsupp.weight, MvPowerSeries.weightedOrder, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞) < weightedOrder w g
pos : HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R) (0 : R) = 0
pos₁ pos₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0

Tactic:
rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]

Premises used: MulZeroClass.mul_zero, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
⊢ i + j = d

Tactic:
simp only [Finset.mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
hij : i + j = d
neg : False
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0

Tactic:
exfalso
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
hij : i + j = d
neg :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
⊢ False

Tactic:
apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)

Premises used: add_le_add, ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
hij : i + j = d
neg :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) (i + j)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
neg₁ :
  (↑(HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) i : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) j : ℕ)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
neg₂ neg₃ :
  HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)

Tactic:
rw [← hij, map_add, Nat.cast_add]

Premises used: map_add, Nat.cast_add
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h h₁ :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
h₂ :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g),
    ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
      HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
        0
h₃ :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g) (i j : σ →₀ ℕ)
    (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
pos :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g) (i j : σ →₀ ℕ)
    (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d)
    (hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
neg neg₁ :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g) (i j : σ →₀ ℕ)
    (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d)
    (hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
⊢ weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)

Tactic:
classical
  apply le_weightedOrder
  intro d hd
  rw [coeff_mul, Finset.sum_eq_zero]
  rintro ⟨i, j⟩ hij
  by_cases! hi : weight w i < f.weightedOrder w
  · rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
  · by_cases! hj : weight w j < g.weightedOrder w
    · rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]
    · simp only [Finset.mem_antidiagonal] at hij
      exfalso
      apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
      rw [← hij, map_add, Nat.cast_add]

Premises used: MulZeroClass.zero_mul, Finset.sum_eq_zero, map_add, MulZeroClass.mul_zero, Nat.cast_add, MvPowerSeries.weightedOrder, Finset.HasAntidiagonal.mem_antidiagonal, MvPowerSeries.le_weightedOrder, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ HSMul.hSMul (α := ℕ) 0 (weightedOrder w f) ≤ weightedOrder w (HPow.hPow (β := ℕ) f 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)
succ : n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
succ₁ : n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ n * f)
succ₂ : weightedOrder w (f ^ n) + weightedOrder w f ≤ weightedOrder w (f ^ n * f)
succ₃ succ₄ : weightedOrder w (f ^ n * f) ≤ weightedOrder w (f ^ n * f)
⊢ (n + 1) • weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))

Tactic:
grw [succ_nsmul, pow_succ, hn, le_weightedOrder_mul]

Premises used: MvPowerSeries.le_weightedOrder_mul, pow_succ, succ_nsmul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
zero : HSMul.hSMul (α := ℕ) 0 (weightedOrder w f) ≤ weightedOrder w (HPow.hPow (β := ℕ) f 0)
succ :
  ∀ (n : ℕ) (hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)),
    (n + 1) • weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
⊢ n • weightedOrder w f ≤ weightedOrder w (f ^ n)

Tactic:
induction n with
  | zero => simp
  | succ n hn => grw [succ_nsmul, pow_succ, hn, le_weightedOrder_mul]

Premises used: MvPowerSeries.le_weightedOrder_mul, pow_succ, WithTop.zero, succ_nsmul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
⊢ ∑ i ∈ ∅, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ ∅, f i)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)
cons :
  weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x) ≤
    weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
cons₁ : weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x) ≤ weightedOrder w (f a * ∏ x ∈ s, f x)
cons₂ :
  weightedOrder w (f a) + weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i) ≤ weightedOrder w (f a * ∏ x ∈ s, f x)
cons₃ cons₄ : weightedOrder w (f a * ∏ i ∈ s, f i) ≤ weightedOrder w (f a * ∏ i ∈ s, f i)
⊢ ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)

Tactic:
grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]

Premises used: Finset.sum_cons, MvPowerSeries.le_weightedOrder_mul, Finset.prod_cons
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
s : Finset ι
empty : ∑ i ∈ ∅, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ ∅, f i)
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)),
    ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i) ≤
      weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
⊢ ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih => grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]

Premises used: MvPowerSeries.le_weightedOrder_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a : R
i : σ →₀ ℕ
hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f
⊢ Eq.{u_2 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) (a • f) : R) (0 : R)

Tactic:
simp [coeff_eq_zero_of_lt_weightedOrder _ hi]

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
S : Type u_3
inst_1 : Semiring S
φ : R →+* S
i : σ →₀ ℕ
hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f
⊢ Eq.{u_3 + 1} (α := S)
    ((coeff i : (a : MvPowerSeries σ S) → S)
        ((map φ : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f : MvPowerSeries σ S) :
      S)
    (0 : S)

Tactic:
simp [coeff_eq_zero_of_lt_weightedOrder _ hi]

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
simp : Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * (1 - g)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
simp only [mul_sub, mul_one, map_sub, sub_eq_self]

Premises used: map_sub, mul_sub, sub_eq_self, mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
apply : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f * g)
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)

Tactic:
apply coeff_eq_zero_of_lt_weightedOrder w

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f * g)

Tactic:
lt_of_lt_of_le (lt_of_lt_of_le h le_add_self) (le_weightedOrder_mul w)

Premises used: MvPowerSeries.le_weightedOrder_mul, le_add_self, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f * g)

Tactic:
exact lt_of_lt_of_le (lt_of_lt_of_le h le_add_self) (le_weightedOrder_mul w)

Premises used: MvPowerSeries.le_weightedOrder_mul, le_add_self, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
simp : Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (g * f) : R) (0 : R)
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) ((1 - g) * f) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
simp only [sub_mul, one_mul, map_sub, sub_eq_self]

Premises used: map_sub, sub_eq_self, sub_mul, one_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
apply : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g * f)
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (g * f) : R) (0 : R)

Tactic:
apply coeff_eq_zero_of_lt_weightedOrder w

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g * f)

Tactic:
apply lt_of_lt_of_le (lt_of_lt_of_le h le_self_add) (le_weightedOrder_mul w)

Premises used: MvPowerSeries.le_weightedOrder_mul, le_self_add, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ ∅, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
simp only [Finset.prod_empty, mul_one]

Premises used: Finset.prod_empty, mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
h : ∀ i ∈ insert a s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a) ∧
    ∀ a ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a)

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at h

Premises used: Finset.mem_insert, forall_eq_or_imp
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
h :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a) ∧
    ∀ a ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a)
insert :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ((1 - g a) * ∏ x ∈ s, (1 - g x))) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₁ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * (1 - g a) * ∏ x ∈ s, (1 - g x)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₂ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) ((f * ∏ x ∈ s, (1 - g x)) * (1 - g a)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₃ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ x ∈ s, (1 - g x)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₄ insert₅ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ Insert.insert a s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm,
      coeff_mul_left_one_sub_of_lt_weightedOrder w h.1, ih h.2]

Premises used: Finset.prod_insert, mul_assoc, MvPowerSeries.coeff_mul_left_one_sub_of_lt_weightedOrder, And.right, And.left, mul_right_comm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)
empty :
  ∀
    (h :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i → (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ ∅, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
        Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
          ((coeff d : (a : MvPowerSeries σ R) → R) f : R))
    (h : ∀ i ∈ Insert.insert a s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ Insert.insert a s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, mul_one]
  | insert a s ha ih =>
    simp only [Finset.mem_insert, forall_eq_or_imp] at h
    rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm,
      coeff_mul_left_one_sub_of_lt_weightedOrder w h.1, ih h.2]

Premises used: Finset.prod_empty, mul_assoc, Insert.insert, Finset.mem_insert, forall_eq_or_imp, mul_right_comm, mul_one