awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 ℤ))
⊢ 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)
have rw : ¬Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
Tactic: rw [Valuation.restrict_def, ne_eq, restrict₀_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 :
  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
⊢ 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⸩)
have 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))
Tactic: apply hd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 :
  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
⊢ 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))
have h : ((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 ℤ)))
    (HSub.hSub (α := K⸨X⸩) (β := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2 : K⸨X⸩)
      ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1 : K⸨X⸩)) <
  (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)
Tactic: simp only [sub_zero, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 :
  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
⊢ ((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 ℤ)))
      (HSub.hSub (α := K⸨X⸩) (β := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2 : K⸨X⸩)
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1 : K⸨X⸩)) <
    (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have h : LT.lt (α := WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (x.2 - x.1)) :
    WithZero (Multiplicative ℤ))
  ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
    WithZero (Multiplicative ℤ))
Tactic: rw [← map_sub, Valuation.restrict_lt_iff_lt_embedding]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 :
  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
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
          (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (x.2 - x.1)) :
      WithZero (Multiplicative ℤ))
    ((embedding :
          (a : MonoidWithZeroHom.ValueGroup₀ (valuation K⸨X⸩ (PowerSeries.idealX K))) → WithZero (Multiplicative ℤ))
        (↑d : MonoidWithZeroHom.ValueGroup₀ (valuation K⸨X⸩ (PowerSeries.idealX K))) :
      WithZero (Multiplicative ℤ))
have h : LT.lt (α := WithZero (Multiplicative ℤ))
  (((polynomialValuationX K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
      (x.2 - x.1) :
    WithZero (Multiplicative ℤ))
  ((embedding :
        (a : MonoidWithZeroHom.ValueGroup₀ (valuation K⸨X⸩ (PowerSeries.idealX K))) → WithZero (Multiplicative ℤ))
      (↑d : MonoidWithZeroHom.ValueGroup₀ (valuation K⸨X⸩ (PowerSeries.idealX K))) :
    WithZero (Multiplicative ℤ))
Tactic: rwa [← valuation_eq_LaurentSeries_valuation]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ 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
have 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)} ⊆
      w),
  ∃ (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
Tactic: obtain ⟨d, hd⟩ := Valued.mem_nhds.mp hT
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
⊢ ∃ (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
have X_def : let X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))};
X =
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
Tactic: set X := {f : K⸨X⸩ | Valued.v f < embedding d.1} with X_def
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
X_def :
  X =
    {f : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
⊢ ∃ (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
have h : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) X ∧
  Subset (α := Set (K⸨X⸩ × K⸨X⸩)) ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X)
    ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X)
Tactic: refine ⟨(fun x : K⸨X⸩ × K⸨X⸩ ↦ x.snd - x.fst) ⁻¹' X, ⟨X, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
X_def :
  X =
    {f : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
h :
  Membership.mem (γ := Filter K⸨X⸩) (nhds 0) X ∧
    Subset (α := Set (K⸨X⸩ × K⸨X⸩)) ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X)
      ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X)
⊢ ∃ (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
have h₁ : Set.preimage (β := K⸨X⸩ × K⸨X⸩)
    (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))
    ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X) ⊆
  S
Tactic: refine ⟨(fun x : K⸨X⸩ × K⸨X⸩ ↦ x.snd - x.fst) ⁻¹' X, ⟨X, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
X_def :
  X =
    {f : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
⊢ Membership.mem (γ := Filter K⸨X⸩) (nhds 0) X ∧
    Subset (α := Set (K⸨X⸩ × K⸨X⸩)) ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X)
      ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X)
have h : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) X
Tactic: refine ⟨?_, Set.Subset.refl _⟩