awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : Membership.mem (γ := Set K⸨X⸩) ((⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n) ∩ ⋂ (n : ℤ), ⋂ (_ : ℓ ≤ n ∧ n ≤ N), φ n) x
⊢ x ∈ φ i
have hx₁ : (∀ (i : ℤ) (i_1 : i < ℓ), x ∈ φ i) ∧ ∀ (i : ℤ), ℓ ≤ i → i ≤ N → x ∈ φ i
Tactic: simp only [Set.mem_inter_iff, Set.mem_iInter, and_imp] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : (∀ (i : ℤ) (i_1 : i < ℓ), x ∈ φ i) ∧ ∀ (i : ℤ), ℓ ≤ i → i ≤ N → x ∈ φ i
⊢ x ∈ φ i
have pos : ∀ (H : i < ℓ), x ∈ φ i
Tactic: by_cases! H : i < ℓ
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : (∀ (i : ℤ) (i_1 : i < ℓ), x ∈ φ i) ∧ ∀ (i : ℤ), ℓ ≤ i → i ≤ N → x ∈ φ i
pos : ∀ (H : i < ℓ), x ∈ φ i
⊢ x ∈ φ i
have neg : ∀ (H : ℓ ≤ i), x ∈ φ i
Tactic: by_cases! H : i < ℓ
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d
have intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
Tactic: have intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ (⋂ n ∈ Set.Icc ℓ N, φ n) := by
    simp only [Set.mem_Iio, Set.mem_Icc, Set.subset_iInter_iff]
    intro i hi x hx
    simp only [Set.mem_inter_iff, Set.mem_iInter, and_imp] at hx
    by_cases! H : i < ℓ
    exacts [hx.1 _ H, hx.2 _ H <| le_of_lt <| lt_max_of_lt_right hi]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d
have suffices : (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
Tactic: suffices (⋂ n ∈ Set.Iio ℓ, φ n) ∩ (⋂ n ∈ Set.Icc ℓ N, φ n) ∈ ℱ by
    exact ℱ.sets_of_superset this <| intersec₂.trans intersec₁
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
⊢ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
have simp : ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ ∧ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
Tactic: simp only [Set.mem_Iio, inter_mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
⊢ ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ ∧ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
have left : ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
left : ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ
⊢ ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ ∧ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
have right : ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
⊢ ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ
have this : ∀ᶠ (f : K⸨X⸩) in ℱ,
  ∀ d < sorry.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = f.coeff d
Tactic: have := (exists_lb_coeff_ne hℱ).choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  ∀ᶠ (f : K⸨X⸩) in ℱ,
    ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = f.coeff d
⊢ ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ
have this₁ : {x : K⸨X⸩ |
    ∀ d < sorry.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
  ℱ
Tactic: rw [Filter.eventually_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ
⊢ ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ
have h : Eq.{u_2 + 1} (α := Set K⸨X⸩) (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n)
  {x : K⸨X⸩ |
    ∀ d < sorry.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d}
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ
⊢ Eq.{u_2 + 1} (α := Set K⸨X⸩) (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n)
    {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d}
have h : ∀ (x : K⸨X⸩),
  Membership.mem (γ := Set K⸨X⸩) (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n) x ↔
    Membership.mem (γ := Set K⸨X⸩)
      {x : K⸨X⸩ |
        ∀ d < sorry.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d}
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ
x : K⸨X⸩
⊢ Membership.mem (γ := Set K⸨X⸩) (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n) x ↔
    Membership.mem (γ := Set K⸨X⸩)
      {x : K⸨X⸩ |
        ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d}
      x
have h : (∀ (i : ℤ) (i_1 : i < ℓ), x ∈ φ i) ↔
  ∀ d < sorry.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
⊢ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
have right : ∀ i ∈ Set.Icc ℓ N, φ i ∈ ℱ
Tactic: rw [biInter_mem (Set.finite_Icc ℓ N)]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
i : ℤ
h : i ∈ Set.Icc ℓ N
⊢ φ i ∈ ℱ
have right : ∀ᶠ (y : K) in 𝓟 {coeff hℱ i}, coeff hℱ i = y
Tactic: apply (coeff_tendsto hℱ _).eventually
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U
have obtain : ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ)
  (hU₁ :
    {y : K⸨X⸩ |
        ((Valuation.restrict Valued.v :
                Valuation K⸨X⸩
                  (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                    (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
              (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
            (y - limit hℱ) <
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
      U),
  ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U
Tactic: obtain ⟨γ, hU₁⟩ := Valued.mem_nhds.mp hU
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {y : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (y - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
this :
  ∀ᶠ (f : K⸨X⸩) in ℱ,
    Membership.mem (γ := Set K⸨X⸩)
      {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (y - limit hℱ) :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))}
      f
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U
have this₁ : ∀ᶠ (f : K⸨X⸩) in ℱ,
  Membership.mem (γ := Set K⸨X⸩)
    {y : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (y - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
    f
Tactic: simp_rw [← Valued.v.restrict_lt_iff_lt_embedding] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {y : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (y - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U
have suffices : ∀ᶠ (f : K⸨X⸩) in ℱ,
  Membership.mem (γ := Set K⸨X⸩)
    {y : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (y - limit hℱ) :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
    f
Tactic: suffices ∀ᶠ f in ℱ, f ∈ {y : K⸨X⸩ | Valued.v (y - limit hℱ) < embedding γ.1} by
    simp_rw [← Valued.v.restrict_lt_iff_lt_embedding] at this
    apply this.mono fun _ hf ↦ hU₁ hf
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {y : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (y - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ,
    Membership.mem (γ := Set K⸨X⸩)
      {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (y - limit hℱ) :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))}
      f
have hD₀ : let D :=
  -HSub.hSub (α := ℤ)
      (log
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
      1;
D =
  -HSub.hSub (α := ℤ)
      (log
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
      1
Tactic: set D := -(log (embedding γ.1) - 1) with hD₀
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {y : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (y - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
D : ℤ :=
  -HSub.hSub (α := ℤ)
      (log
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
      1
hD₀ :
  D =
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1
⊢ exp (-D) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have rw : -
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1 <
  log
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v))
Tactic: rw [← lt_log_iff_exp_lt (by simp), hD₀]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {y : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (y - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
D : ℤ :=
  -HSub.hSub (α := ℤ)
      (log
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
      1
hD₀ :
  D =
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ,
    Membership.mem (γ := Set K⸨X⸩)
      {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (y - limit hℱ) :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))}
      f
have hD : exp (-D) <
  (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
    (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
Tactic: have hD : exp (-D) < embedding γ.1 := by
    rw [← lt_log_iff_exp_lt (by simp), hD₀]
    simp
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {y : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (y - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
D : ℤ :=
  -HSub.hSub (α := ℤ)
      (log
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
      1
hD₀ :
  D =
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1
hD :
  exp (-D) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ,
    Membership.mem (γ := Set K⸨X⸩)
      {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (y - limit hℱ) :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))}
      f
have apply : ∀ (x : K⸨X⸩),
  (∀ d < D, coeff hℱ d = x.coeff d) →
    Membership.mem (γ := Set K⸨X⸩)
      {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (y - limit hℱ) :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))}
      x
Tactic: apply coeff_eventually_equal (D := D) hℱ |>.mono