awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
s : ℕ
F_mul :
  HMul.hMul (α := K⟦ℤ⟧) (β := K⟦ℤ⟧)
      ((((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s))⁻¹ : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) =
    f
hs : HahnSeries.order f = -(↑s : ℤ)
this : Eq.{u_2 + 1} (α := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1) 1
h h₁ h₂ h₃ :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
⊢ ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑η : WithZero (Multiplicative ℤ)) * (↑γ : WithZero (Multiplicative ℤ))

Tactic:
rwa [← Units.val_mul]

Premises used: Units.val_mul
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
s : ℕ
F_mul :
  ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F =
    HMul.hMul (α := K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s) : K⟦ℤ⟧) f
hs : HahnSeries.order f = -(↑s : ℤ)
⊢ Ne (α := K⟦ℤ⟧)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s) : K⟦ℤ⟧)
    (0 : K⟦ℤ⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
neg :
  ∀ (s : ℕ) (hs : -HahnSeries.order f = -(↑s : ℤ)),
    ∃ (Q : K⟮X⟯),
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
        (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (Q : K⟮X⟯),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
      (↑γ : WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg ord_nonpos)

Premises used: Int.neg_nonpos_of_nonneg, Int.exists_eq_neg_ofNat
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
neg :
  ∀ (P : K[X])
    (hP :
      ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * F - (↑P : K⟦X⟧)) <
        (↑γ : WithZero (Multiplicative ℤ))),
    ∃ (Q : K⟮X⟯),
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
        (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (Q : K⟮X⟯),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
      (↑γ : WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt (PowerSeries.X ^ s * F) γ

Premises used: HMul.hMul, LaurentSeries.exists_Polynomial_intValuation_lt, PowerSeries.X, HPow.hPow
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * F - (↑P : K⟦X⟧)) <
    (↑γ : WithZero (Multiplicative ℤ))
h :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (↑P : K⟮X⟯) : K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (Q : K⟮X⟯),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
      (↑γ : WithZero (Multiplicative ℤ))

Tactic:
use P
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * F - (↑P : K⟦X⟧)) <
    (↑γ : WithZero (Multiplicative ℤ))
h :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * f.powerSeriesPart - (↑P : K⟦X⟧)) <
    (↑γ : WithZero (Multiplicative ℤ))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (↑P : K⟮X⟯) : K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))

Tactic:
rw [← X_order_mul_powerSeriesPart (neg_inj.1 hs).symm, ← RatFunc.coe_coe,
      ← PowerSeries.coe_sub, ← coe_algebraMap, adicValued_apply, valuation_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, LaurentSeries.coe_algebraMap, RatFunc.coe_coe, PowerSeries.coe_sub, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, neg_inj, Iff.mp, Eq.symm, LaurentSeries.X_order_mul_powerSeriesPart
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * F - (↑P : K⟦X⟧)) <
    (↑γ : WithZero (Multiplicative ℤ))
⊢ ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * f.powerSeriesPart - (↑P : K⟦X⟧)) <
    (↑γ : WithZero (Multiplicative ℤ))

Tactic:
hP
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * F - (↑P : K⟦X⟧)) <
    (↑γ : WithZero (Multiplicative ℤ))
⊢ ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * f.powerSeriesPart - (↑P : K⟦X⟧)) <
    (↑γ : WithZero (Multiplicative ℤ))

Tactic:
exact hP
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
rw :
  Eq.{u_2 + 1} (α := Set K⸨X⸩) (closure (Set.range (ι := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩))) Set.univ
⊢ DenseRange.{u_2, u_2} (X := K⸨X⸩) (α := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩)

Tactic:
rw [denseRange_iff_closure_range]

Premises used: denseRange_iff_closure_range
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
h :
  ∀ (f : K⸨X⸩),
    Membership.mem (γ := Set K⸨X⸩) (closure (Set.range (ι := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩))) f ↔
      Membership.mem (γ := Set K⸨X⸩) Set.univ f
⊢ Eq.{u_2 + 1} (α := Set K⸨X⸩) (closure (Set.range (ι := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩))) Set.univ

Tactic:
ext f
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h :
  ∀ {V : Set (K⸨X⸩ × K⸨X⸩)},
    Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) V →
      SetRel.IsSymm V →
        ∃ (a : K⟮X⟯),
          Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
⊢ Membership.mem (γ := Set K⸨X⸩) (closure (Set.range (ι := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩))) f ↔
    Membership.mem (γ := Set K⸨X⸩) Set.univ f

Tactic:
simp only [UniformSpace.mem_closure_iff_symm_ball, Set.mem_univ, iff_true, Set.Nonempty,
    Set.mem_inter_iff, Set.mem_range, exists_exists_eq_and]

Premises used: Set.mem_range, Set.mem_inter_iff, iff_true, Set.Nonempty, exists_exists_eq_and, Set.mem_univ, UniformSpace.mem_closure_iff_symm_ball
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) V
h_symm : SetRel.IsSymm V
⊢ Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (Filter.comap (β := K⸨X⸩) (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) (nhds 0)) V

Tactic:
rw [uniformity_eq_comap_neg_add_nhds_zero_swapped] at hV

Premises used: uniformity_eq_comap_neg_add_nhds_zero_swapped
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) V
h_symm : SetRel.IsSymm V
hV₁ :
  Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (Filter.comap (β := K⸨X⸩) (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) (nhds 0)) V
⊢ SetRel.IsSymm V

Tactic:
rw [uniformity_eq_comap_neg_add_nhds_zero_swapped] at hV

Premises used: uniformity_eq_comap_neg_add_nhds_zero_swapped
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV :
  Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (Filter.comap (β := K⸨X⸩) (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) (nhds 0)) V
h_symm : SetRel.IsSymm V
h :
  ∀ (T : Set K⸨X⸩) (hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T)
    (hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V),
    ∃ (a : K⟮X⟯),
      Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)

Tactic:
obtain ⟨T, hT₀, hT₁⟩ := hV
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
h :
  ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ)
    (hγ :
      {x : K⸨X⸩ |
          ((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 ℤ)))
              x <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
        T),
    ∃ (a : K⟮X⟯),
      Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)

Tactic:
obtain ⟨γ, hγ⟩ := Valued.mem_nhds_zero.mp hT₀

Premises used: Valued.mem_nhds_zero, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((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 ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
h :
  ∀ (this : WithZero (Multiplicative ℤ)),
    ∃ (a : K⟮X⟯),
      Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)

Tactic:
have := (embedding γ.1)
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((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 ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
this : WithZero (Multiplicative ℤ)
h :
  ∀ (P : K⟮X⟯)
    (hP :
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)) :
          WithZero (Multiplicative ℤ))
        ((↑((Units.map (↑embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* WithZero (Multiplicative ℤ)) :
                  (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → (WithZero (Multiplicative ℤ))ˣ)
                γ) :
            WithZero (Multiplicative ℤ)) :
          WithZero (Multiplicative ℤ))),
    ∃ (a : K⟮X⟯),
      Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)

Tactic:
obtain ⟨P, hP⟩ := exists_ratFunc_val_lt f
    (Units.map (embedding (f := (valued K).v)).toMonoidHom γ)

Premises used: LaurentSeries.exists_ratFunc_val_lt, MonoidWithZeroHom.toMonoidHom, MonoidWithZeroHom.ValueGroup₀.embedding, DFunLike.coe, Units.map
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((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 ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)) :
      WithZero (Multiplicative ℤ))
    ((↑((Units.map (↑embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* WithZero (Multiplicative ℤ)) :
              (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → (WithZero (Multiplicative ℤ))ˣ)
            γ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
h : Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)

Tactic:
use P
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((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 ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)) :
      WithZero (Multiplicative ℤ))
    ((↑((Units.map (↑embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* WithZero (Multiplicative ℤ)) :
              (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → (WithZero (Multiplicative ℤ))ˣ)
            γ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
h :
  Membership.mem (α := K⸨X⸩ × K⸨X⸩) (γ := Set (K⸨X⸩ × K⸨X⸩)) ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T)
    ((f, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P) : K⸨X⸩ × K⸨X⸩)
⊢ Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)

Tactic:
apply hT₁
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((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 ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)) :
      WithZero (Multiplicative ℤ))
    ((↑((Units.map (↑embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* WithZero (Multiplicative ℤ)) :
              (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → (WithZero (Multiplicative ℤ))ˣ)
            γ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
h :
  Membership.mem (γ := Set K⸨X⸩)
    {x : K⸨X⸩ |
      ((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 ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
    ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) (f, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P))
⊢ Membership.mem (α := K⸨X⸩ × K⸨X⸩) (γ := Set (K⸨X⸩ × K⸨X⸩)) ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T)
    ((f, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P) : K⸨X⸩ × K⸨X⸩)

Tactic:
apply hγ
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((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 ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)) :
      WithZero (Multiplicative ℤ))
    ((↑((Units.map (↑embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* WithZero (Multiplicative ℤ)) :
              (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → (WithZero (Multiplicative ℤ))ˣ)
            γ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ Membership.mem (γ := Set K⸨X⸩)
    {x : K⸨X⸩ |
      ((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 ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
    ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) (f, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P))

Tactic:
simpa only [Units.coe_map, MonoidHom.coe_mk, ZeroHom.toFun_eq_coe, OneHom.coe_mk, add_comm,
    MonoidWithZeroHom.toZeroHom_coe, ← sub_eq_add_neg, Set.mem_setOf_eq,
    Valuation.restrict_lt_iff_lt_embedding]

Premises used: Units.coe_map, Valuation.restrict_lt_iff_lt_embedding, OneHom.coe_mk, sub_eq_add_neg, MonoidWithZeroHom.toZeroHom_coe, Set.mem_setOf_eq, add_comm, MonoidHom.coe_mk, ZeroHom.toFun_eq_coe