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
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
hj : (↑j : ℕ∞) < ψ.order
pos : HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) (0 : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have pos₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_of_lt_order j hj, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have hij₁ : (i, j).1 + (i, j).2 = n
Tactic: rw [mem_antidiagonal] at hij
Cleared hypotheses: hij, hi, hj
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
⊢ False
have neg : (↑n : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑i : ℕ∞) (↑j : ℕ∞)
Tactic: apply ne_of_lt (lt_of_lt_of_le hn <| add_le_add hi hj)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
⊢ (↑n : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑i : ℕ∞) (↑j : ℕ∞)
have neg : Eq (α := ℕ∞) (↑n : ℕ∞) (↑(i + j) : ℕ∞)
Tactic: rw [← Nat.cast_add, hij]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ (↑i : ℕ∞)
hj : ψ.order ≤ (↑j : ℕ∞)
neg : Eq (α := ℕ∞) (↑n : ℕ∞) (↑(i + j) : ℕ∞)
⊢ (↑n : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑i : ℕ∞) (↑j : ℕ∞)
have neg₁ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
Tactic: rw [← Nat.cast_add, hij]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
⊢ (n + 1) • φ.order ≤ (φ ^ (n + 1)).order
have succ : n • φ.order + HSMul.hSMul (α := ℕ) 1 φ.order ≤ (φ ^ (n + 1)).order
Tactic: grw [add_smul, one_smul, pow_succ, ih, le_order_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
succ : n • φ.order + HSMul.hSMul (α := ℕ) 1 φ.order ≤ (φ ^ (n + 1)).order
⊢ (n + 1) • φ.order ≤ (φ ^ (n + 1)).order
have succ₁ : n • φ.order + φ.order ≤ (φ ^ (n + 1)).order
Tactic: grw [add_smul, one_smul, pow_succ, ih, le_order_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
succ : n • φ.order + HSMul.hSMul (α := ℕ) 1 φ.order ≤ (φ ^ (n + 1)).order
succ₁ : n • φ.order + φ.order ≤ (φ ^ (n + 1)).order
⊢ (n + 1) • φ.order ≤ (φ ^ (n + 1)).order
have succ₂ : n • φ.order + φ.order ≤ (φ ^ n * φ).order
Tactic: grw [add_smul, one_smul, pow_succ, ih, le_order_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
succ : n • φ.order + HSMul.hSMul (α := ℕ) 1 φ.order ≤ (φ ^ (n + 1)).order
succ₁ : n • φ.order + φ.order ≤ (φ ^ (n + 1)).order
succ₂ : n • φ.order + φ.order ≤ (φ ^ n * φ).order
⊢ (n + 1) • φ.order ≤ (φ ^ (n + 1)).order
have succ₃ : (φ ^ n).order + φ.order ≤ (φ ^ n * φ).order
Tactic: grw [add_smul, one_smul, pow_succ, ih, le_order_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
succ : n • φ.order + HSMul.hSMul (α := ℕ) 1 φ.order ≤ (φ ^ (n + 1)).order
succ₁ : n • φ.order + φ.order ≤ (φ ^ (n + 1)).order
succ₂ : n • φ.order + φ.order ≤ (φ ^ n * φ).order
succ₃ : (φ ^ n).order + φ.order ≤ (φ ^ n * φ).order
⊢ (n + 1) • φ.order ≤ (φ ^ (n + 1)).order
have succ₄ : (φ ^ n * φ).order ≤ (φ ^ n * φ).order
Tactic: grw [add_smul, one_smul, pow_succ, ih, le_order_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ n • φ.order ≤ (φ ^ n).order
have zero : HSMul.hSMul (α := ℕ) 0 φ.order ≤ (HPow.hPow (β := ℕ) φ 0).order
Tactic: induction n with
  | zero => simp
  | succ n ih => grw [add_smul, one_smul, pow_succ, ih, le_order_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
zero : HSMul.hSMul (α := ℕ) 0 φ.order ≤ (HPow.hPow (β := ℕ) φ 0).order
⊢ n • φ.order ≤ (φ ^ n).order
have succ : ∀ (n : ℕ) (ih : n • φ.order ≤ (φ ^ n).order), (n + 1) • φ.order ≤ (φ ^ (n + 1)).order
Tactic: induction n with
  | zero => simp
  | succ n ih => grw [add_smul, one_smul, pow_succ, ih, le_order_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)
⊢ ∑ i ∈ Finset.cons a s ha, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
have cons : (φ a).order + ∑ x ∈ s, (φ x).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
Tactic: grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_order_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)
cons : (φ a).order + ∑ x ∈ s, (φ x).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
⊢ ∑ i ∈ Finset.cons a s ha, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
have cons₁ : (φ a).order + ∑ x ∈ s, (φ x).order ≤ (φ a * ∏ x ∈ s, φ x).order
Tactic: grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_order_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)
cons : (φ a).order + ∑ x ∈ s, (φ x).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
cons₁ : (φ a).order + ∑ x ∈ s, (φ x).order ≤ (φ a * ∏ x ∈ s, φ x).order
⊢ ∑ i ∈ Finset.cons a s ha, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
have cons₂ : (φ a).order + order.{u_2} (R := R) (∏ i ∈ s, φ i) ≤ (φ a * ∏ x ∈ s, φ x).order
Tactic: grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_order_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)
cons : (φ a).order + ∑ x ∈ s, (φ x).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
cons₁ : (φ a).order + ∑ x ∈ s, (φ x).order ≤ (φ a * ∏ x ∈ s, φ x).order
cons₂ : (φ a).order + order.{u_2} (R := R) (∏ i ∈ s, φ i) ≤ (φ a * ∏ x ∈ s, φ x).order
⊢ ∑ i ∈ Finset.cons a s ha, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ i)
have cons₃ : (φ a * ∏ i ∈ s, φ i).order ≤ (φ a * ∏ i ∈ s, φ i).order
Tactic: grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_order_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
s : Finset ι
⊢ ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)
have empty : ∑ i ∈ ∅, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ ∅, φ 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_order_mul]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
s : Finset ι
empty : ∑ i ∈ ∅, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ ∅, φ i)
⊢ ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)
have cons : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (ih : ∑ i ∈ s, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ s, φ i)),
  ∑ i ∈ Finset.cons a s ha, (φ i).order ≤ order.{u_2} (R := R) (∏ i ∈ Finset.cons a s ha, φ 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_order_mul]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ 1 ≤ φ.order ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
have mp : 1 ≤ φ.order → Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
mp : 1 ≤ φ.order → Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ 1 ≤ φ.order ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
have mpr : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R) → 1 ≤ φ.order
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : 1 ≤ φ.order
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
have mp : Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: rw [← coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : 1 ≤ φ.order
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)
have mp : (↑0 : ℕ∞) < φ.order
Tactic: apply coeff_of_lt_order
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ 1 ≤ φ.order
have mpr : ∀ (d : ℕ) (hd : LT.lt (α := ℕ∞) (↑d : ℕ∞) 1), Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: refine le_order _ _ fun d hd ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
d : ℕ
hd : LT.lt (α := ℕ∞) (↑d : ℕ∞) 1
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) φ : R) (0 : R)
have hd₁ : d = 0
Tactic: rw [Nat.cast_lt_one] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ φ.order ≠ 0 ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
have rw : 1 ≤ φ.order ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: rw [← ENat.one_le_iff_ne_zero, one_le_order_iff_constCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
rw : 1 ≤ φ.order ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ φ.order ≠ 0 ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
have rw₁ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R) ↔
  Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: rw [← ENat.one_le_iff_ne_zero, one_le_order_iff_constCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ (↑n : ℕ∞) ≤ (φ ^ n).order
have refine : (↑n : ℕ∞) ≤ n • φ.order
Tactic: refine .trans ?_ (le_order_pow _ n)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = if a = 0 then ⊤ else (↑n : ℕ∞)
have pos : ∀ (h : a = 0), order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = ⊤
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
pos : ∀ (h : a = 0), order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = ⊤
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = if a = 0 then ⊤ else (↑n : ℕ∞)
have neg : ∀ (h : ¬a = 0), order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : a = 0
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = ⊤
have pos : order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) 0) = ⊤
Tactic: rw [h, order_eq_top, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : a = 0
pos : order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) 0) = ⊤
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = ⊤
have pos₁ : Eq.{u_1 + 1} (α := R⟦X⟧) ((monomial n : (a : R) → R⟦X⟧) 0 : R⟦X⟧) (0 : R⟦X⟧)
Tactic: rw [h, order_eq_top, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : a = 0
pos : order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) 0) = ⊤
pos₁ : Eq.{u_1 + 1} (α := R⟦X⟧) ((monomial n : (a : R) → R⟦X⟧) 0 : R⟦X⟧) (0 : R⟦X⟧)
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = ⊤
have pos₂ : Eq.{u_1 + 1} (α := R⟦X⟧) 0 0
Tactic: rw [h, order_eq_top, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)
have neg : (∀ (i : ℕ),
    Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
      Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)) ∧
  ∀ (i : ℕ),
    LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
      Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
Tactic: rw [order_eq]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
⊢ (∀ (i : ℕ),
      Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
        Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)) ∧
    ∀ (i : ℕ),
      LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
        Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
have neg : ∀ (i : ℕ),
  Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
    Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
neg :
  ∀ (i : ℕ),
    Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
      Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
⊢ (∀ (i : ℕ),
      Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
        Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)) ∧
    ∀ (i : ℕ),
      LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
        Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
have neg₁ : ∀ (i : ℕ),
  LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) →
    Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞)
⊢ Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
have hi₁ : i = n
Tactic: simp only [Nat.cast_inj] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i = n
⊢ Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
have neg : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
Tactic: rwa [hi, coeff_monomial_same]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i = n
neg : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
⊢ Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
have neg₁ : a ≠ 0
Tactic: rwa [hi, coeff_monomial_same]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞)
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
have hi₁ : i < n
Tactic: simp only [Nat.cast_lt] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
have neg : ¬i = n
Tactic: rw [coeff_monomial, if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)
have rw : Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑n : ℕ∞)) (↑n : ℕ∞)
Tactic: rw [order_monomial, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
h : a ≠ 0
rw : Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑n : ℕ∞)) (↑n : ℕ∞)
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
Tactic: rw [order_monomial, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)
have rw : Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑n : ℕ∞)) (↑n : ℕ∞)
Tactic: classical
  rw [order_monomial, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
h : a ≠ 0
rw : Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑n : ℕ∞)) (↑n : ℕ∞)
⊢ order.{u_1} (R := R) ((monomial n : (a : R) → R⟦X⟧) a) = (↑n : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
Tactic: classical
  rw [order_monomial, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
this : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0 : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
have rw : Eq.{u_1 + 1} (α := R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0) 0
Tactic: rw [this, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
this : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0 : R)
rw : Eq.{u_1 + 1} (α := R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0) 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [this, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
have suffices : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0 : R)
Tactic: suffices coeff n (φ * ψ) = ∑ p ∈ antidiagonal n, 0 by rw [this, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0 : R)
have rw : Eq.{u_1 + 1} (α := R)
  (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) φ : R) ((coeff p.2 : (a : R⟦X⟧) → R) ψ : R))
  (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0)
Tactic: rw [coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
⊢ Eq.{u_1 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) φ : R) ((coeff p.2 : (a : R⟦X⟧) → R) ψ : R))
    (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n, 0)
have apply : ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R) ((coeff x.2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R) ((coeff x.2 : (a : R⟦X⟧) → R) ψ : R) = 0
have refine : LE.le (α := ℕ∞) (↑x.2 : ℕ∞) (↑n : ℕ∞)
Tactic: refine mul_eq_zero_of_right (coeff x.fst φ) (coeff_of_lt_order x.snd (lt_of_le_of_lt ?_ h))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ LE.le (α := ℕ∞) (↑x.2 : ℕ∞) (↑n : ℕ∞)
have hx₁ : x.1 + x.2 = n
Tactic: rw [mem_antidiagonal] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < ψ.order
x : ℕ × ℕ
hx : x.1 + x.2 = n
⊢ LE.le (α := ℕ∞) (↑x.2 : ℕ∞) (↑n : ℕ∞)
have norm_cast : x.2 ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
t : ∀ i ∈ insert a s, (↑k : ℕ∞) < (f i).order
⊢ Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ insert a s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
have t₁ : (↑k : ℕ∞) < (f a).order ∧ ∀ a ∈ s, (↑k : ℕ∞) < (f a).order
Tactic: simp only [Finset.mem_insert, forall_eq_or_imp] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, (↑k : ℕ∞) < (f i).order) →
    Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
t : (↑k : ℕ∞) < (f a).order ∧ ∀ a ∈ s, (↑k : ℕ∞) < (f a).order
⊢ Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ i ∈ insert a s, (1 - f i)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
have insert : Eq (α := R) ((coeff k : (a : R⟦X⟧) → R) (φ * ∏ x ∈ s, (1 - f x)) : R) ((coeff k : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1]