-- Mathlib/RingTheory/LaurentSeries.lean
theorem Cauchy.eventually_mem_nhds {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ)
    {U : Set K⸨X⸩} (hU : U ∈ 𝓝 (Cauchy.limit hℱ)) : ∀ᶠ f in ℱ, f ∈ U

Proof state:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < ↑γ}

Tactic:
have hD : ((Multiplicative.ofAdd (-D) : Multiplicative ℤ) : ℤₘ₀) < γ := by
  rw [← WithZero.coe_unzero γ.ne_zero, WithZero.coe_lt_coe, hD₀, neg_neg, ofAdd_sub,
    ofAdd_toAdd, div_lt_comm, div_self', ← ofAdd_zero, Multiplicative.ofAdd_lt]
  exact zero_lt_one

Result:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < ↑γ}

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
this : ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < ↑γ}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
apply this.mono fun _ hf ↦ hU₁ hf

Result:
no goals

Proof state:
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

Tactic:
obtain ⟨γ, hU₁⟩ := Valued.mem_nhds.mp hU

Result:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
n : ℤ
hn : n < D
⊢ (x✝ - limit hℱ).coeff n = 0

Tactic:
rw [HahnSeries.coeff_sub, sub_eq_zero, hf n hn |>.symm]

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
n : ℤ
hn : n < D
⊢ coeff hℱ n = (limit hℱ).coeff n

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
⊢ ↑(ofAdd (-D)) < ↑γ

Tactic:
rw [← WithZero.coe_unzero γ.ne_zero, WithZero.coe_lt_coe, hD₀, neg_neg, ofAdd_sub,
  ofAdd_toAdd, div_lt_comm, div_self', ← ofAdd_zero, Multiplicative.ofAdd_lt]

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
⊢ 0 < 1

Proof state:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < ↑γ}

Tactic:
apply coeff_eventually_equal (D := D) hℱ |>.mono

Result:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
⊢ ∀ (x : K⸨X⸩), (∀ d < D, coeff hℱ d = x.coeff d) → x ∈ {y | Valued.v (y - limit hℱ) < ↑γ}

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
⊢ ∀ n < D, (x✝ - limit hℱ).coeff n = 0

Tactic:
intro n hn

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
n : ℤ
hn : n < D
⊢ (x✝ - limit hℱ).coeff n = 0

Proof state:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < ↑γ}

Tactic:
set D := -((WithZero.unzero γ.ne_zero).toAdd - 1) with hD₀

Result:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < ↑γ}

Proof state:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
⊢ ∀ (x : K⸨X⸩), (∀ d < D, coeff hℱ d = x.coeff d) → x ∈ {y | Valued.v (y - limit hℱ) < ↑γ}

Tactic:
intro _ hf

Result:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
⊢ x✝ ∈ {y | Valued.v (y - limit hℱ) < ↑γ}

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
⊢ 0 < 1

Tactic:
exact zero_lt_one

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
n : ℤ
hn : n < D
⊢ coeff hℱ n = (limit hℱ).coeff n

Tactic:
rfl

Result:
no goals

Proof state:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
suffices ∀ᶠ f in ℱ, f ∈ {y : K⸨X⸩ | Valued.v (y - limit hℱ) < ↑γ} by
  apply this.mono fun _ hf ↦ hU₁ hf

Result:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < ↑γ}