awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
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 :
  ∀ (x : K⟮X⟯)
    (hx :
      ((restrict₀ Valued.v :
              K⟮X⟯ →*₀ MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v) :
            (a : K⟮X⟯) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
          x =
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)),
    ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
      {y : K⸨X⸩ |
          LT.lt (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) y :
              WithZero (Multiplicative ℤ))
            ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
              WithZero (Multiplicative ℤ))} ⊆
        X
⊢ ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
    {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) y :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))} ⊆
      X

Tactic:
obtain ⟨x, hx⟩ := restrict₀_surjective _ d.1

Premises used: Units.val, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))}
x : K⟮X⟯
hx :
  ((restrict₀ Valued.v :
          K⟮X⟯ →*₀ MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v) :
        (a : K⟮X⟯) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
      x =
    (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)
⊢ ¬Eq (α := MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v)
      (((restrict₀ Valued.v :
              K⟮X⟯ →*₀ MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v) :
            (a : K⟮X⟯) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
          x :
        MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v)
      (0 : MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))}
x : K⟮X⟯
hx :
  ((restrict₀ Valued.v :
          K⟮X⟯ →*₀ MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v) :
        (a : K⟮X⟯) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
      x =
    (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)
⊢ ∀ (a : K⸨X⸩),
    LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a :
          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) :
          WithZero (Multiplicative ℤ)) →
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a :
          WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))

Tactic:
simp [v_def, valuation_coe_ratFunc]

Premises used: RatFunc.v_def, LaurentSeries.valuation_coe_ratFunc
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))}
⊢ 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:
subset_trans (fun _ _ ↦ ?_) pre_T

Premises used: subset_trans
-- Module: Mathlib.RingTheory.LaurentSeries
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 :
  ∀ (x : K⟮X⟯ × K⟮X⟯),
    Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯))
        (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))
        x →
      Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯)) ((fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w) x
⊢ 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 subset_trans (fun _ _ ↦ ?_) pre_T

Premises used: subset_trans
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))}
x : K⟮X⟯ × K⟮X⟯
h_1 :
  Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯))
    (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))
    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) x)
⊢ Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯)) ((fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w) x

Tactic:
apply hd
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))}
x : K⟮X⟯ × K⟮X⟯
h :
  Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯))
    (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))
    x
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
          (a : 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⸩)) :
      WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))

Tactic:
assumption
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
⊢ UniformContinuous (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (β := K⟮X⟯)
    (⇑(WithVal.equiv (polynomialValuationX K)) : (a : WithVal (polynomialValuationX K)) → K⟮X⟯)

Tactic:
(Valuation.IsEquiv.refl).uniformContinuous_equiv rfl

Premises used: Valuation.IsEquiv.uniformContinuous_equiv, rfl, Valuation.IsEquiv.refl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
⊢ Continuous.{u_2, u_2} (X := K⟮X⟯) (Y := K⸨X⸩) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩)

Tactic:
(isUniformInducing_iff'.1 (inducing_coe)).1.continuous

Premises used: LaurentSeries.inducing_coe, UniformContinuous.continuous, And.left, isUniformInducing_iff', Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
⊢ Continuous (X := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (Y := K⸨X⸩)
    (Function.comp (β := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩)
      (⇑(WithVal.equiv (polynomialValuationX K)) : (a : WithVal (polynomialValuationX K)) → K⟮X⟯))

Tactic:
continuous_coe.comp uniformContinuous_withVal_equiv.continuous

Premises used: LaurentSeries.continuous_coe, Continuous.comp, UniformContinuous.continuous, LaurentSeries.uniformContinuous_withVal_equiv
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K⟮X⟯
⊢ Eq (α := space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (LaurentSeriesPkg K))
    (AbstractCompletion.coe (LaurentSeriesPkg K) (WithVal.toVal (polynomialValuationX K) x))
    ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x)

Tactic:
rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
⊢ Eq (α := K⸨X⸩) ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) x : K⸨X⸩)
    ((extensionAsRingHom K ⋯ : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) x : K⸨X⸩)

Tactic:
rfl

Premises used: Set.Mem, UniformSpace.Completion.extension, AbstractCompletion.compare, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
x y : RatFuncAdicCompl K
rw :
  HMul.hMul (α := K⸨X⸩) (β := K⸨X⸩)
      ((extensionAsRingHom K ⋯ : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) x : K⸨X⸩)
      ((extensionAsRingHom K ⋯ : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) y : K⸨X⸩) =
    HMul.hMul (α := K⸨X⸩) (β := K⸨X⸩) ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) x : K⸨X⸩)
      ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) y : K⸨X⸩)
⊢ Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) (x * y) =
    Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) x * Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) y

Tactic:
rw [Equiv.toFun_as_coe, UniformEquiv.coe_toEquiv, comparePkg_eq_extension,
        (extensionAsRingHom K (continuous_coe' _)).map_mul]

Premises used: LaurentSeries.extensionAsRingHom, UniformEquiv.coe_toEquiv, Equiv.toFun_as_coe, LaurentSeries.continuous_coe', LaurentSeries.comparePkg_eq_extension, RingHom.map_mul
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
x y : RatFuncAdicCompl K
⊢ HMul.hMul (α := K⸨X⸩) (β := K⸨X⸩)
      ((extensionAsRingHom K ⋯ : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) x : K⸨X⸩)
      ((extensionAsRingHom K ⋯ : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) y : K⸨X⸩) =
    HMul.hMul (α := K⸨X⸩) (β := K⸨X⸩) ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) x : K⸨X⸩)
      ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) y : K⸨X⸩)

Tactic:
simp [← comparePkg_eq_extension]

Premises used: LaurentSeries.comparePkg_eq_extension
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
x y : RatFuncAdicCompl K
rw :
  HAdd.hAdd (α := K⸨X⸩) (β := K⸨X⸩)
      ((extensionAsRingHom K ⋯ : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) x : K⸨X⸩)
      ((extensionAsRingHom K ⋯ : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) y : K⸨X⸩) =
    HAdd.hAdd (α := K⸨X⸩) (β := K⸨X⸩) ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) x : K⸨X⸩)
      ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) y : K⸨X⸩)
⊢ Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) (x + y) =
    Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) x + Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) y

Tactic:
rw [Equiv.toFun_as_coe, UniformEquiv.coe_toEquiv, comparePkg_eq_extension,
        (extensionAsRingHom K (continuous_coe' _)).map_add]

Premises used: LaurentSeries.extensionAsRingHom, UniformEquiv.coe_toEquiv, Equiv.toFun_as_coe, LaurentSeries.continuous_coe', LaurentSeries.comparePkg_eq_extension, RingHom.map_add
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
x y : RatFuncAdicCompl K
⊢ HAdd.hAdd (α := K⸨X⸩) (β := K⸨X⸩)
      ((extensionAsRingHom K ⋯ : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) x : K⸨X⸩)
      ((extensionAsRingHom K ⋯ : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) y : K⸨X⸩) =
    HAdd.hAdd (α := K⸨X⸩) (β := K⸨X⸩) ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) x : K⸨X⸩)
      ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) y : K⸨X⸩)

Tactic:
simp [← comparePkg_eq_extension]

Premises used: LaurentSeries.comparePkg_eq_extension
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⟦X⟧
⊢ Eq (α := RatFuncAdicCompl K)
    ((LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      RatFuncAdicCompl K)
    (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg)

Tactic:
rfl

Premises used: Set.Mem, setOf, AbstractCompletion.compare, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
⊢ Eq (α := K⸨X⸩) ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x : K⸨X⸩)
    (AbstractCompletion.compare ratfuncAdicComplPkg (LaurentSeriesPkg K) x :
      space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (LaurentSeriesPkg K))

Tactic:
rfl

Premises used: Set.Mem, setOf, AbstractCompletion.compare, AbstractCompletion.extend, rfl, ite