-- Mathlib/RingTheory/LaurentSeries.lean
theorem Cauchy.coeff_eventually_equal {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) {D : ℤ} :
    ∀ᶠ f : K⸨X⸩ in ℱ, ∀ d, d < D → coeff hℱ d = f.coeff d

Proof state:
case pos
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : (∀ i < ℓ, x ∈ φ i) ∧ ∀ (i : ℤ), ℓ ≤ i → i ≤ N → x ∈ φ i
H : i < ℓ
⊢ x ∈ φ i

case neg
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : (∀ i < ℓ, x ∈ φ i) ∧ ∀ (i : ℤ), ℓ ≤ i → i ≤ N → x ∈ φ i
H : ¬i < ℓ
⊢ x ∈ φ i

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

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
⊢ ∀ i < D, (⋂ n, ⋂ (_ : n < ℓ), φ n) ∩ ⋂ n, ⋂ (_ : ℓ ≤ n ∧ n ≤ N), φ n ⊆ φ i

Tactic:
intro i hi x hx

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : x ∈ (⋂ n, ⋂ (_ : n < ℓ), φ n) ∩ ⋂ n, ⋂ (_ : ℓ ≤ n ∧ n ≤ N), φ n
⊢ x ∈ φ i

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d

Tactic:
let φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : x ∈ (⋂ n, ⋂ (_ : n < ℓ), φ n) ∩ ⋂ n, ⋂ (_ : ℓ ≤ n ∧ n ≤ N), φ n
⊢ x ∈ φ i

Tactic:
simp only [Set.mem_inter_iff, Set.mem_iInter, and_imp] at hx

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : (∀ i < ℓ, x ∈ φ i) ∧ ∀ (i : ℤ), ℓ ≤ i → i ≤ N → x ∈ φ i
⊢ x ∈ φ i

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
intersec₂ : ⋂ 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

Tactic:
suffices (⋂ n ∈ Set.Iio ℓ, φ n) ∩ (⋂ n ∈ Set.Icc ℓ N, φ n) ∈ ℱ by
  exact ℱ.sets_of_superset this <| intersec₂.trans intersec₁

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n, ⋂ (_ : n < ℓ), φ n ∈ ℱ ∧ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Tactic:
constructor

Result:
case left
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n, ⋂ (_ : n < ℓ), φ n ∈ ℱ

case right
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Proof state:
case h.e'_5.h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
this : {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d} ∈ ℱ
x✝ : K⸨X⸩
⊢ x✝ ∈ ⋂ n, ⋂ (_ : n < ℓ), φ n ↔ x✝ ∈ {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d}

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq]

Result:
case h.e'_5.h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
this : {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d} ∈ ℱ
x✝ : K⸨X⸩
⊢ (∀ i < ℓ, x✝ ∈ φ i) ↔ ∀ d < ⋯.choose, coeff hℱ d = x✝.coeff d

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : (∀ i < ℓ, x ∈ φ i) ∧ ∀ (i : ℤ), ℓ ≤ i → i ≤ N → x ∈ φ i
⊢ x ∈ φ i

Tactic:
by_cases H : i < ℓ

Result:
case pos
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : (∀ i < ℓ, x ∈ φ i) ∧ ∀ (i : ℤ), ℓ ≤ i → i ≤ N → x ∈ φ i
H : i < ℓ
⊢ x ∈ φ i

case neg
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := ℓ ⊔ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : (∀ i < ℓ, x ∈ φ i) ∧ ∀ (i : ℤ), ℓ ≤ i → i ≤ N → x ∈ φ i
H : ¬i < ℓ
⊢ x ∈ φ i

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
a✝ : K⸨X⸩
hf : a✝ ∈ ⋂ n ∈ Set.Iio D, φ n
⊢ a✝ ∈ {x | ∀ d < D, coeff hℱ d = x.coeff d}

Tactic:
simpa only [Set.mem_iInter] using hf

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.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

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d => {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d