awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet (↑s : Set (σ →₀ ℕ))
k : ℕ
hk : 1 ≤ k
p : MvPowerSeries σ R
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) k) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ k) : MvPolynomial σ R)
have base : Eq (α := MvPolynomial σ R)
  ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
      (HPow.hPow (α := MvPowerSeries σ R) (β := ℕ)
        (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) 1) :
    MvPolynomial σ R)
  ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (HPow.hPow (β := ℕ) p 1) : MvPolynomial σ R)
Tactic: induction k, hk using Nat.le_induction with
  | base => simp [truncFinset_truncFinset]
  | succ n hmn ih =>
    ext x; by_cases hx : x ∈ s
    · rw [coeff_truncFinset_of_mem _ hx, coeff_truncFinset_of_mem _ hx, pow_succ,
        ← coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx, ih, truncFinset_truncFinset
        (by rfl), pow_succ, coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx]
    simp [coeff_truncFinset_eq_zero _ hx]
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet (↑s : Set (σ →₀ ℕ))
k : ℕ
hk : 1 ≤ k
p : MvPowerSeries σ R
base :
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R) (β := ℕ)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) 1) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (HPow.hPow (β := ℕ) p 1) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) k) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ k) : MvPolynomial σ R)
have succ : ∀ (n : ℕ) (hmn : 1 ≤ n)
  (ih :
    Eq (α := MvPolynomial σ R)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (HPow.hPow (α := MvPowerSeries σ R)
            (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
        MvPolynomial σ R)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)),
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1)) : MvPolynomial σ R)
Tactic: induction k, hk using Nat.le_induction with
  | base => simp [truncFinset_truncFinset]
  | succ n hmn ih =>
    ext x; by_cases hx : x ∈ s
    · rw [coeff_truncFinset_of_mem _ hx, coeff_truncFinset_of_mem _ hx, pow_succ,
        ← coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx, ih, truncFinset_truncFinset
        (by rfl), pow_succ, coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx]
    simp [coeff_truncFinset_eq_zero _ hx]
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPowerSeries σ R
a : σ →₀ ℕ
⊢ Membership.mem (γ := Finset (σ →₀ ℕ))
      (MvPolynomial.support.{u_2, u_1} (R := R) ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)) a →
    a ∈ s
have contrapose : a ∉ s → a ∉ MvPolynomial.support.{u_2, u_1} (R := R) ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)
Tactic: contrapose
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
⊢ (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p ↔ p.support ⊆ s
have refine_1 : ∀ (h : (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p), p.support ⊆ s
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ MvPolynomial.ext _ _ fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
refine_1 :
  ∀ (h : (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p), p.support ⊆ s
⊢ (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p ↔ p.support ⊆ s
have refine_2 : ∀ (h : p.support ⊆ s) (x : σ →₀ ℕ),
  MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
    MvPolynomial.coeff x p
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ MvPolynomial.ext _ _ fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p
⊢ p.support ⊆ s
have refine_1 : MvPolynomial.support.{u_2, u_1} (R := R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) ⊆
  s
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : p.support ⊆ s
x : σ →₀ ℕ
⊢ MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
    MvPolynomial.coeff x p
have pos : x ∈ s →
  MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
    MvPolynomial.coeff x p
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : p.support ⊆ s
x : σ →₀ ℕ
pos :
  x ∈ s →
    MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
      MvPolynomial.coeff x p
⊢ MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
    MvPolynomial.coeff x p
have neg : x ∉ s →
  MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
    MvPolynomial.coeff x p
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
⊢ (trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
have a₁ : ∀ (m : σ →₀ ℕ),
  MvPolynomial.coeff m
      ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p)) =
    MvPolynomial.coeff m
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
⊢ (trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
have a₁ : ∀ (m : σ →₀ ℕ),
  MvPolynomial.coeff m
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p)) =
    MvPolynomial.coeff m
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
⊢ f = g ↔
    ∀ (n : σ →₀ ℕ),
      Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
have refine : ∀
  (h :
    ∀ (n : σ →₀ ℕ),
      Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)),
  f = g
Tactic: refine ⟨fun h => by simp [h], fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
⊢ f = g
have h₁ : ∀ (n : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
have h₁ : Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
  ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
Tactic: specialize h n
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
f' : MvPowerSeries σ R
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)
have rw : Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
  (if n ≤ n then (coeff n : (a : MvPowerSeries σ R) → R) f' else 0 : R)
Tactic: rw [coeff_trunc', if_pos le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
f' : MvPowerSeries σ R
rw :
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (if n ≤ n then (coeff n : (a : MvPowerSeries σ R) → R) f' else 0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)
have rw₁ : Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
Tactic: rw [coeff_trunc', if_pos le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
have this : ∀ {f' : MvPowerSeries σ R},
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)
Tactic: have {f' : MvPowerSeries σ R} : f'.coeff n = (trunc' R n f').coeff n := by
    rw [coeff_trunc', if_pos le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
this :
  ∀ {f' : MvPowerSeries σ R},
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
      (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
have h₁ : Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))
  (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g))
Tactic: simp_rw [this, h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
⊢ f = g ↔
    ∃ᶠ (m : σ →₀ ℕ) in atTop,
      Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
        ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
have refine : ∀
  (h :
    ∃ᶠ (m : σ →₀ ℕ) in atTop,
      Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
        ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)),
  f = g
Tactic: refine ⟨fun h => by simp [h, atTop_neBot], fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
⊢ f = g
have h₁ : ∀ (n : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
have h₁ : ∀ (m : σ →₀ ℕ) (hm₁ : n ≤ m)
  (hm₂ :
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)),
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
Tactic: obtain ⟨m, hm₁, hm₂⟩ := h.forall_exists_of_atTop n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ :
  Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
f' : MvPowerSeries σ R
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (MvPolynomial.coeff n ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)
have rw : Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
  (if n ≤ m then (coeff n : (a : MvPowerSeries σ R) → R) f' else 0 : R)
Tactic: rw [coeff_trunc', if_pos hm₁]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ :
  Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
f' : MvPowerSeries σ R
rw :
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (if n ≤ m then (coeff n : (a : MvPowerSeries σ R) → R) f' else 0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (MvPolynomial.coeff n ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)
have rw₁ : Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
Tactic: rw [coeff_trunc', if_pos hm₁]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ :
  Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
have this : ∀ {f' : MvPowerSeries σ R},
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (MvPolynomial.coeff n ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)
Tactic: have {f' : MvPowerSeries σ R} : f'.coeff n = (trunc' R m f').coeff n := by
    rw [coeff_trunc', if_pos hm₁]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
h : n ≠ 0
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯)
    0
have revert : ∀ (h : n ≠ 0),
  Membership.mem (γ := Finset (σ →₀ ℕ)) (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) sorry)
    0
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
⊢ ∀ (h : n ≠ 0),
    Membership.mem (γ := Finset (σ →₀ ℕ))
      (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯) 0
have contrapose : 0 ∉ Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) sorry → n = 0
Tactic: contrapose
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
x : σ →₀ ℕ
p q : MvPowerSeries σ R
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < n
x_1 x_2 : σ →₀ ℕ
h : x_2 ≤ x_1
⊢ x_1 ∈ (↑(Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯) : Set (σ →₀ ℕ)) →
    x_2 ∈ (↑(Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯) : Set (σ →₀ ℕ))
have simp : (degree : (a : σ →₀ ℕ) → ℕ) x_1 < n → (degree : (a : σ →₀ ℕ) → ℕ) x_2 < n
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
p : MvPowerSeries σ R
h : n ≠ 0
⊢ MvPolynomial.totalDegree.{u_2, u_1} (R := R) (σ := σ)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) <
    n
have apply : sup.{0, u_1} (β := σ →₀ ℕ) (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) sorry)
    (⇑degree : (a : σ →₀ ℕ) → ℕ) <
  n
Tactic: apply (totalDegree_truncFinset p).trans_lt
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
p : MvPolynomial σ R
h : n ≠ 0
⊢ (truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p ↔ p.totalDegree < n
have rw : (∀ x ∈ (↑p.support : Set (σ →₀ ℕ)),
    Membership.mem (γ := Set (σ →₀ ℕ)) {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n} x) ↔
  ∀ b ∈ p.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) < n
Tactic: rw [truncTotal, truncFinset_coe_eq_self_iff, Set.Finite.subset_toFinset,
    MvPolynomial.totalDegree, Finset.sup_lt_iff (bot_lt_iff_ne_bot.mpr h), Set.subset_def]
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
⊢ N = J • N
have refine : N ≤ J • N
Tactic: refine le_antisymm ?_ (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
⊢ n ∈ J • N
have obtain : ∀ (r : R) (hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0), n ∈ J • N
Tactic: obtain ⟨r, hr⟩ := Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hN hIN
-- Lean 4 proof step from Mathlib.RingTheory.Nakayama (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
⊢ n ∈ J • N
have obtain : ∀ (s : R) (hs : s * r - 1 ∈ J), n ∈ J • N
Tactic: obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r (hIjac hr.1)