awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
⊢ (f, g) ∈ S ×ˢ T

Tactic:
simp [hf.1, hg.2]

Premises used: And.right, And.left
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
⊢ (f, g) ∈ S ×ˢ T

Tactic:
have h_prod : (f, g) ∈ S ×ˢ T := by simp [hf.1, hg.2]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
h_prod : (f, g) ∈ S ×ˢ T
⊢ Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N, f.coeff n = 0) x} g

Tactic:
hN g (le_of_lt ?_)

Premises used: Set.Mem, setOf, le_of_lt
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
h_prod : (f, g) ∈ S ×ˢ T
h :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (g - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N, f.coeff n = 0) x} g

Tactic:
refine hN g (le_of_lt ?_)

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
h_prod : (f, g) ∈ S ×ˢ T
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (g - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simpa [Valuation.restrict_def, ← Valuation.restrict_lt_one_iff] using H h_prod

Premises used: Valuation.restrict_lt_one_iff, Valuation.restrict_def
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x : UniformSpace K := ⊥
obtain : ∀ (N : ℤ) (hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0), ∃ (N : ℤ), ∀ n < N, coeff hℱ n = 0
⊢ ∃ (N : ℤ), ∀ n < N, coeff hℱ n = 0

Tactic:
obtain ⟨N, hN⟩ := exists_lb_eventual_support hℱ

Premises used: LaurentSeries.Cauchy.exists_lb_eventual_support
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
⊢ ∃ (N : ℤ), ∀ n < N, coeff hℱ n = 0

Tactic:
⟨N, fun n hn ↦ Ultrafilter.eq_of_le_pure (hℱ.map (uniformContinuous_coeff n)).1
      ((principal_singleton _).symm ▸ coeff_tendsto _ _) ?_⟩

Premises used: LaurentSeries.Cauchy.coeff, LaurentSeries.Cauchy.coeff_tendsto, Cauchy.map, Eq.rec, And.left, Filter.principal_singleton, Exists.intro, Ultrafilter.eq_of_le_pure, LaurentSeries.uniformContinuous_coeff, Eq.symm
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
refine : ∀ (n : ℤ) (hn : n < N), LE.le (α := Filter K) (Filter.map (fun (f : K⸨X⸩) ↦ f.coeff n) ℱ) (pure 0)
⊢ ∃ (N : ℤ), ∀ n < N, coeff hℱ n = 0

Tactic:
refine ⟨N, fun n hn ↦ Ultrafilter.eq_of_le_pure (hℱ.map (uniformContinuous_coeff n)).1
      ((principal_singleton _).symm ▸ coeff_tendsto _ _) ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
n : ℤ
hn : n < N
simp : Membership.mem (γ := Filter K) (Filter.map (fun (f : K⸨X⸩) ↦ f.coeff n) ℱ) 0
⊢ LE.le (α := Filter K) (Filter.map (fun (f : K⸨X⸩) ↦ f.coeff n) ℱ) (pure 0)

Tactic:
simp only [pure_zero, nonpos_iff]

Premises used: Filter.pure_zero, Filter.nonpos_iff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
n : ℤ
hn : n < N
⊢ Membership.mem (γ := Filter K) (Filter.map (fun (f : K⸨X⸩) ↦ f.coeff n) ℱ) 0

Tactic:
apply Filter.mem_of_superset hN (fun _ ha ↦ ha _ hn)

Premises used: Filter.mem_of_superset
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
⊢ BddBelow (Function.support (coeff hℱ))

Tactic:
⟨(exists_lb_support hℱ).choose, fun d hd ↦ ?_⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro, Exists.choose, LaurentSeries.Cauchy.exists_lb_support
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
refine : ∀ (d : ℤ) (hd : d ∈ Function.support (coeff hℱ)), ⋯.choose (p := fun (N : ℤ) ↦ ∀ n < N, coeff hℱ n = 0) ≤ d
⊢ BddBelow (Function.support (coeff hℱ))

Tactic:
refine ⟨(exists_lb_support hℱ).choose, fun d hd ↦ ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
d : ℤ
hd : d ∈ Function.support (coeff hℱ)
by_contra : ∀ (hNd : ¬⋯.choose (p := fun (N : ℤ) ↦ ∀ n < N, coeff hℱ n = 0) ≤ d), False
⊢ ⋯.choose (p := fun (N : ℤ) ↦ ∀ n < N, coeff hℱ n = 0) ≤ d

Tactic:
by_contra hNd
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
d : ℤ
hd : d ∈ Function.support (coeff hℱ)
hNd : ¬⋯.choose (p := fun (N : ℤ) ↦ ∀ n < N, coeff hℱ n = 0) ≤ d
⊢ False

Tactic:
hd ((exists_lb_support hℱ).choose_spec d (not_le.mp hNd))

Premises used: not_le, Exists.choose_spec, Iff.mp, LaurentSeries.Cauchy.exists_lb_support
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
d : ℤ
hd : d ∈ Function.support (coeff hℱ)
hNd : ¬⋯.choose (p := fun (N : ℤ) ↦ ∀ n < N, coeff hℱ n = 0) ≤ d
⊢ False

Tactic:
exact hd ((exists_lb_support hℱ).choose_spec d (not_le.mp hNd))

Premises used: not_le, Exists.choose_spec, Iff.mp, LaurentSeries.Cauchy.exists_lb_support
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
obtain :
  ∀ (N₁ : ℤ) (hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0) (N₂ : ℤ) (hN₂ : ∀ n < N₂, coeff hℱ n = 0),
    ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d

Tactic:
obtain ⟨⟨N₁, hN₁⟩, ⟨N₂, hN₂⟩⟩ := exists_lb_eventual_support hℱ, exists_lb_support hℱ

Premises used: LaurentSeries.Cauchy.exists_lb_eventual_support, LaurentSeries.Cauchy.exists_lb_support
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d

Tactic:
⟨min N₁ N₂, ℱ.3 hN₁ fun _ hf d hd ↦ ?_⟩

Premises used: Filter.sets_of_superset, Exists.intro, Min.min
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
refine :
  ∀ (x : K⸨X⸩) (hf : Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N₁, f.coeff n = 0) x} x) (d : ℤ)
    (hd : d < min N₁ N₂), coeff hℱ d = x.coeff d
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d

Tactic:
refine ⟨min N₁ N₂, ℱ.3 hN₁ fun _ hf d hd ↦ ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
x : K⸨X⸩
hf : Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N₁, f.coeff n = 0) x} x
d : ℤ
hd : d < min N₁ N₂
rw : coeff hℱ d = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := K) 0 0
⊢ coeff hℱ d = x.coeff d

Tactic:
rw [hf d (lt_of_lt_of_le hd (min_le_left _ _)), hN₂ d (lt_of_lt_of_le hd (min_le_right _ _))]

Premises used: min_le_left, min_le_right, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.LaurentSeries
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}
a : K⸨X⸩
hf : Membership.mem (γ := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) a
⊢ Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d} a

Tactic:
simpa only [Set.mem_iInter] using hf

Premises used: Set.mem_iInter
-- Module: Mathlib.RingTheory.LaurentSeries
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}
⊢ Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}

Tactic:
have intersec₁ :
    (⋂ n ∈ Set.Iio D, φ n) ⊆ {x : K⸨X⸩ | ∀ d : ℤ, d < D → coeff hℱ d = x.coeff d} := by
    intro _ hf
    simpa only [Set.mem_iInter] using hf
-- Module: Mathlib.RingTheory.LaurentSeries
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
simp : ∀ (i : ℤ) (i_1 : i < D), (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n) ∩ ⋂ (n : ℤ), ⋂ (_ : ℓ ≤ n ∧ n ≤ N), φ n ⊆ φ i
⊢ Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)

Tactic:
simp only [Set.mem_Iio, Set.mem_Icc, Set.subset_iInter_iff]

Premises used: Set.mem_Iio, Set.subset_iInter_iff, Set.mem_Icc
-- Module: Mathlib.RingTheory.LaurentSeries
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
⊢ (∀ (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

Premises used: and_imp, Set.mem_inter_iff, Set.mem_iInter
-- Module: Mathlib.RingTheory.LaurentSeries
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
neg : ∀ (H : ℓ ≤ i), x ∈ φ i
⊢ x ∈ φ i

Tactic:
by_cases! H : i < ℓ
-- Module: Mathlib.RingTheory.LaurentSeries
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
H : i < ℓ
⊢ x ∈ φ i

Tactic:
hx.1 _ H

Premises used: And.left
-- Module: Mathlib.RingTheory.LaurentSeries
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
H : ℓ ≤ i
⊢ x ∈ φ i

Tactic:
hx.2 _ H <| le_of_lt <| lt_max_of_lt_right hi

Premises used: le_of_lt, lt_max_of_lt_right, And.right
-- Module: Mathlib.RingTheory.LaurentSeries
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
H : i < ℓ
⊢ x ∈ φ i

Tactic:
exacts [hx.1 _ H, hx.2 _ H <| le_of_lt <| lt_max_of_lt_right hi]

Premises used: le_of_lt, lt_max_of_lt_right, And.right, And.left
-- Module: Mathlib.RingTheory.LaurentSeries
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
⊢ 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]
-- Module: Mathlib.RingTheory.LaurentSeries
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 : (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d

Tactic:
ℱ.sets_of_superset this <| intersec₂.trans intersec₁

Premises used: Filter.Eventually, HasSubset.Subset.trans, Filter.sets_of_superset
-- Module: Mathlib.RingTheory.LaurentSeries
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 : (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d

Tactic:
exact ℱ.sets_of_superset this <| intersec₂.trans intersec₁

Premises used: HasSubset.Subset.trans, Filter.sets_of_superset
-- Module: Mathlib.RingTheory.LaurentSeries
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)
suffices : (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d

Tactic:
suffices (⋂ n ∈ Set.Iio ℓ, φ n) ∩ (⋂ n ∈ Set.Icc ℓ N, φ n) ∈ ℱ by
    exact ℱ.sets_of_superset this <| intersec₂.trans intersec₁
-- Module: Mathlib.RingTheory.LaurentSeries
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)
simp : ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ ∧ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
⊢ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Tactic:
simp only [Set.mem_Iio, inter_mem_iff]

Premises used: Set.mem_Iio, Filter.inter_mem_iff
-- Module: Mathlib.RingTheory.LaurentSeries
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 ∈ ℱ
right : ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
⊢ ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ ∧ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Tactic:
constructor