-- Mathlib/RingTheory/LaurentSeries.lean
lemma Cauchy.exists_lb_eventual_support {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) :
    ∃ N, ∀ᶠ f : K⸨X⸩ in ℱ, ∀ n < N, f.coeff n = (0 : K)

Proof state:
case intro.intro.intro.intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
obtain ⟨f, hf⟩ := forall_mem_nonempty_iff_neBot.mpr hℱ.1 (S ∩ T) (inter_mem_iff.mpr ⟨hS, hT⟩)

Result:
case intro.intro.intro.intro.intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

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

Tactic:
let entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    Valued.v (P.snd - P.fst) < ((Multiplicative.ofAdd 0 : Multiplicative ℤ) : ℤₘ₀)}

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ := mem_prod_iff.mp <| Filter.le_def.mp hℱ.2 entourage
  <| (Valued.hasBasis_uniformity K⸨X⸩ ℤₘ₀).mem_of_mem (i := ζ) (by tauto)

Result:
case intro.intro.intro.intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
⊢ True

Tactic:
tauto

Result:
no goals

Proof state:
case pos
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : f = 0
⊢ ∃ N, ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0

Tactic:
refine ⟨0, fun x hg ↦ ?_⟩

Result:
case pos
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : f = 0
x : K⸨X⸩
hg : Valued.v (x - f) ≤ ↑(ofAdd 0)
⊢ ∀ n < 0, x.coeff n = 0

Proof state:
case neg
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : ¬f = 0
⊢ ∃ N, ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0

Tactic:
refine ⟨min (f.2.isWF.min (HahnSeries.support_nonempty_iff.mpr hf)) 0 - 1, fun _ hg n hn ↦ ?_⟩

Result:
case neg
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : ¬f = 0
x✝ : K⸨X⸩
hg : Valued.v (x✝ - f) ≤ ↑(ofAdd 0)
n : ℤ
hn : n < ⋯.min ⋯ ⊓ 0 - 1
⊢ x✝.coeff n = 0

Proof state:
case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
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⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
h_prod : (f, g) ∈ entourage
⊢ g ∈ {x | (fun f => ∀ n < N, f.coeff n = 0) x}

Tactic:
exact hN g (le_of_lt h_prod)

Result:
no goals

Proof state:
case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
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⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
⊢ g ∈ {x | (fun f => ∀ n < N, f.coeff n = 0) x}

Tactic:
have h_prod : (f, g) ∈ entourage := Set.prod_mono (Set.inter_subset_left (t := T))
  (Set.inter_subset_right (s := S)) |>.trans H <| Set.mem_prod.mpr ⟨hf, hg⟩

Result:
case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
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⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
h_prod : (f, g) ∈ entourage
⊢ g ∈ {x | (fun f => ∀ n < N, f.coeff n = 0) x}

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
let ζ := Units.mk0 (G₀ := ℤₘ₀) _ (WithZero.coe_ne_zero (a := (Multiplicative.ofAdd 0)))

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Proof state:
case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
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⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0
⊢ S ∩ T ⊆ {x | (fun f => ∀ n < N, f.coeff n = 0) x}

Tactic:
intro g hg

Result:
case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
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⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
⊢ g ∈ {x | (fun f => ∀ n < N, f.coeff n = 0) x}

Proof state:
case intro.intro.intro.intro.intro.intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
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⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
use N

Result:
case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v (P.2 - P.1) < ↑(ofAdd 0)}
ζ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd 0) ⋯
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⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0