awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
pos :
  ∀
    (hx :
      Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))
        (0 : WithZero (Multiplicative ℤ))),
    ∃ (f : K⟮X⟯),
      Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))
neg :
  ∀
    (hx :
      ¬Eq (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
            WithZero (Multiplicative ℤ))
          (0 : WithZero (Multiplicative ℤ))),
    ∃ (f : K⟮X⟯),
      Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))
⊢ ∃ (f : K⟮X⟯),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))

Tactic:
by_cases hx : Valued.v x = 0

Premises used: Valued.v, DFunLike.coe
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
hx :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) 0 :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
⊢ ∃ (f : K⟮X⟯),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))

Tactic:
use 0
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
hx :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) 0 :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
hx :
  ¬Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := K⟮X⟯) (β := ℤ) RatFunc.X
          (-log
              (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
                x))) :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
⊢ ∃ (f : K⟮X⟯),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))

Tactic:
use RatFunc.X ^ (-log (Valued.v x))

Premises used: RatFunc.X, Valued.v, WithZero.log, DFunLike.coe, Neg.neg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
hx :
  ¬Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
h :
  exp
      (-HSMul.hSMul (α := ℤ) (β := ℤ)
          (log
            (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x))
          (-1)) =
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := K⟮X⟯) (β := ℤ) RatFunc.X
          (-log
              (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
                x))) :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))

Tactic:
rw [zpow_neg, map_inv₀, map_zpow₀, v_def, valuation_X_eq_neg_one, ← exp_zsmul, ← exp_neg]

Premises used: map_inv₀, RatFunc.v_def, zpow_neg, WithZero.exp_zsmul, map_zpow₀, WithZero.exp_neg, Polynomial.valuation_X_eq_neg_one
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
hx :
  ¬Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ exp
      (-HSMul.hSMul (α := ℤ) (β := ℤ)
          (log
            (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x))
          (-1)) =
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x

Tactic:
simp [exp_log, hx]

Premises used: WithZero.exp_log
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
rw :
  Eq.{u_2 + 1} (α := Filter (K⟮X⟯ × K⟮X⟯))
    {
      sets :=
        {s : Set (K⟮X⟯ × K⟮X⟯) |
          ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
            Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) t ∧
              (fun (x : K⟮X⟯ × K⟮X⟯) ↦
                    ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1,
                      (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
                  t ⊆
                s},
      univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
    (uniformity K⟮X⟯)
⊢ IsUniformInducing.{u_2, u_2} (α := K⟮X⟯) (β := K⸨X⸩) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩)

Tactic:
rw [isUniformInducing_iff, Filter.comap]

Premises used: isUniformInducing_iff, Filter.comap
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
h :
  ∀ (S : Set (K⟮X⟯ × K⟮X⟯)),
    Membership.mem (γ := Filter (K⟮X⟯ × K⟮X⟯))
        {
          sets :=
            {s : Set (K⟮X⟯ × K⟮X⟯) |
              ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
                Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) t ∧
                  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
                        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1,
                          (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
                      t ⊆
                    s},
          univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
        S ↔
      Membership.mem (γ := Filter (K⟮X⟯ × K⟮X⟯)) (uniformity K⟮X⟯) S
⊢ Eq.{u_2 + 1} (α := Filter (K⟮X⟯ × K⟮X⟯))
    {
      sets :=
        {s : Set (K⟮X⟯ × K⟮X⟯) |
          ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
            Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) t ∧
              (fun (x : K⟮X⟯ × K⟮X⟯) ↦
                    ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1,
                      (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
                  t ⊆
                s},
      univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
    (uniformity K⟮X⟯)

Tactic:
ext S
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
h :
  (∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
      (∃ (t_1 : Set K⸨X⸩),
          Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun (x : K⟮X⟯ × K⟮X⟯) ↦
              ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
            t ⊆
          S) ↔
    ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
⊢ Membership.mem (γ := Filter (K⟮X⟯ × K⟮X⟯))
      {
        sets :=
          {s : Set (K⟮X⟯ × K⟮X⟯) |
            ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
              Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) t ∧
                (fun (x : K⟮X⟯ × K⟮X⟯) ↦
                      ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1,
                        (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
                    t ⊆
                  s},
        univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
      S ↔
    Membership.mem (γ := Filter (K⟮X⟯ × K⟮X⟯)) (uniformity K⟮X⟯) S

Tactic:
simp only [Filter.mem_mk, Set.mem_setOf_eq, uniformity_eq_comap_nhds_zero,
    Filter.mem_comap]

Premises used: Filter.mem_mk, Set.mem_setOf_eq, uniformity_eq_comap_nhds_zero, Filter.mem_comap
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
h :
  (∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
      (∃ (t_1 : Set K⸨X⸩),
          Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun (x : K⟮X⟯ × K⟮X⟯) ↦
              ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
            t ⊆
          S) →
    ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
h₁ :
  (∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S) →
    ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
      (∃ (t_1 : Set K⸨X⸩),
          Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun (x : K⟮X⟯ × K⟮X⟯) ↦
              ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
            t ⊆
          S
⊢ (∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
      (∃ (t_1 : Set K⸨X⸩),
          Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun (x : K⟮X⟯ × K⟮X⟯) ↦
              ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
            t ⊆
          S) ↔
    ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S

Tactic:
constructor
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T :
  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
      T ⊆
    S
R : Set K⸨X⸩
hR : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) R
pre_R : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R ⊆ T
h :
  ∀ (d : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ)
    (hd :
      {y : 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 ℤ)))
              (y - 0) <
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
        R),
    ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
⊢ ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S

Tactic:
obtain ⟨d, hd⟩ := Valued.mem_nhds.mp hR

Premises used: Valued.mem_nhds, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T :
  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
      T ⊆
    S
R : Set K⸨X⸩
hR : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) R
pre_R : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hd :
  {y : 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 ℤ)))
          (y - 0) <
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    R
h :
  Membership.mem (γ := Filter K⟮X⟯) (nhds 0)
      {P : K⟮X⟯ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))} ∧
    Set.preimage (β := K⟮X⟯) (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1)
        {P : K⟮X⟯ |
          LT.lt (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
              WithZero (Multiplicative ℤ))
            ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
              WithZero (Multiplicative ℤ))} ⊆
      S
⊢ ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S

Tactic:
use {P : K⟮X⟯ | Valued.v P < embedding d.1}

Premises used: Units.val, MonoidWithZeroHom.ValueGroup₀.embedding, DFunLike.coe
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T :
  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
      T ⊆
    S
R : Set K⸨X⸩
hR : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) R
pre_R : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hd :
  {y : 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 ℤ)))
          (y - 0) <
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    R
⊢ (∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
      Subset.{u_2} (α := Set K⟮X⟯)
        {y : 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 ℤ)))
              y <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
        {P : K⟮X⟯ |
          LT.lt (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
              WithZero (Multiplicative ℤ))
            ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
              WithZero (Multiplicative ℤ))}) ∧
    Set.preimage (β := K⟮X⟯) (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1)
        {P : K⟮X⟯ |
          LT.lt (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
              WithZero (Multiplicative ℤ))
            ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
              WithZero (Multiplicative ℤ))} ⊆
      S

Tactic:
⟨?_, subset_trans (fun _ _ ↦ pre_R ?_) pre_T⟩

Premises used: subset_trans, And.intro
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T :
  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
      T ⊆
    S
R : Set K⸨X⸩
hR : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) R
pre_R : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hd :
  {y : 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 ℤ)))
          (y - 0) <
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    R
x : K⟮X⟯
hx :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))
rw :
  ¬Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ Ne (α := MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v)
    (((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₀ (F := K⟮X⟯ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⟮X⟯ →*₀ WithZero (Multiplicative ℤ)))
    (0 : MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v)

Tactic:
rw [Valuation.restrict_def, ne_eq, restrict₀_eq_zero_iff]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff, ne_eq, Valuation.restrict_def
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T :
  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
      T ⊆
    S
R : Set K⸨X⸩
hR : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) R
pre_R : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hd :
  {y : 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 ℤ)))
          (y - 0) <
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    R
x : K⟮X⟯
hx :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))
⊢ ¬Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T :
  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
      T ⊆
    S
R : Set K⸨X⸩
hR : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) R
pre_R : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hd :
  {y : 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 ℤ)))
          (y - 0) <
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    R
x : K⟮X⟯ × K⟮X⟯
h_1 :
  Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯))
    (Set.preimage (β := K⟮X⟯) (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1)
      {P : K⟮X⟯ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))})
    x
h :
  Membership.mem (γ := Set K⸨X⸩)
    {y : 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 ℤ)))
          (y - 0) <
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
    ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1)
      ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2))
⊢ Membership.mem (α := K⸨X⸩ × K⸨X⸩) (γ := Set (K⸨X⸩ × K⸨X⸩)) ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R)
    (((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2) : K⸨X⸩ × K⸨X⸩)

Tactic:
apply hd