-- 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 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

Tactic:
rw [eq_coeff_of_valuation_sub_lt K hg (d := 0)]

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
⊢ f.coeff n = 0

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
⊢ 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
x✝ : K⸨X⸩
hg : Valued.v (x✝ - f) ≤ ↑(ofAdd 0)
n : ℤ
hn : n < ⋯.min ⋯ ⊓ 0 - 1
⊢ n < 0

Tactic:
exact lt_of_lt_of_le hn <| le_of_lt (Int.sub_one_lt_of_le <| min_le_right _ _)

Result:
no goals

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) ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
⊢ ∃ N, ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0

Tactic:
by_cases hf : f = 0

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
⊢ ∃ N, ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ ↑(ofAdd 0) → ∀ n < N, g.coeff n = 0

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

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
x : K⸨X⸩
hg : Valued.v (x - f) ≤ ↑(ofAdd 0)
⊢ ∀ n < 0, x.coeff n = 0

Tactic:
rw [hf, sub_zero] at 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 ≤ ↑(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
x✝ : K⸨X⸩
hg : Valued.v (x✝ - f) ≤ ↑(ofAdd 0)
n : ℤ
hn : n < ⋯.min ⋯ ⊓ 0 - 1
⊢ f.coeff n = 0

Tactic:
exact Function.nmem_support.mp fun h ↦
f.2.isWF.not_lt_min (HahnSeries.support_nonempty_iff.mpr hf) h
<| lt_trans hn <| Int.sub_one_lt_iff.mpr <| min_le_left _ _

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
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
apply mem_of_superset (inter_mem hS hT)

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
⊢ S ∩ T ⊆ {x | (fun f => ∀ n < N, f.coeff n = 0) x}

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
x : K⸨X⸩
hg : Valued.v x ≤ ↑(ofAdd 0)
⊢ ∀ n < 0, x.coeff n = 0

Tactic:
exact (valuation_le_iff_coeff_lt_eq_zero K).mp hg

Result:
no goals