-- Mathlib/RingTheory/LaurentSeries.lean
theorem inducing_coe : IsUniformInducing ((↑) : RatFunc K → K⸨X⸩)

Proof state:
case h.mpr.intro.intro
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
⊢ ∃ t, (∃ t_1 ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧ (fun x => (↑x.1, ↑x.2)) ⁻¹' t ⊆ S

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

Result:
case h.mpr.intro.intro.intro
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
⊢ ∃ t, (∃ t_1 ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧ (fun x => (↑x.1, ↑x.2)) ⁻¹' t ⊆ S

Proof state:
case h
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x => (↑x.1, ↑x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x => x.2 - x.1) ⁻¹' R ⊆ T
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d}
⊢ (↑x✝¹.1, ↑x✝¹.2) ∈ (fun x => x.2 - x.1) ⁻¹' R

Tactic:
apply hd

Result:
case h.a
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x => (↑x.1, ↑x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x => x.2 - x.1) ⁻¹' R ⊆ T
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d}
⊢ (fun x => x.2 - x.1) (↑x✝¹.1, ↑x✝¹.2) ∈ {y | Valued.v (y - 0) < ↑d}

Proof state:
case h.mpr.intro.intro.intro.refine_2.a
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => (↑x.1, ↑x.2)) ⁻¹' ((fun x => x.2 - x.1) ⁻¹' X)
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) (↑x✝¹.2 - ↑x✝¹.1) < ↑d

Tactic:
assumption

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro.refine_2
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => (↑x.1, ↑x.2)) ⁻¹' ((fun x => x.2 - x.1) ⁻¹' X)
⊢ x✝¹ ∈ (fun x => x.2 - x.1) ⁻¹' w✝

Tactic:
apply hd

Result:
case h.mpr.intro.intro.intro.refine_2.a
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => (↑x.1, ↑x.2)) ⁻¹' ((fun x => x.2 - x.1) ⁻¹' X)
⊢ (fun x => x.2 - x.1) x✝¹ ∈ {y | Valued.v (y - 0) < ↑d}

Proof state:
K : Type u_2
inst✝ : Field K
⊢ IsUniformInducing coeToLaurentSeries_fun

Tactic:
rw [isUniformInducing_iff, Filter.comap]

Result:
K : Type u_2
inst✝ : Field K
⊢ { sets := {s | ∃ t ∈ uniformity K⸨X⸩, (fun x => (↑x.1, ↑x.2)) ⁻¹' t ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯,
      inter_sets := ⋯ } =
    uniformity (RatFunc K)

Proof state:
case h.a
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x => (↑x.1, ↑x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x => x.2 - x.1) ⁻¹' R ⊆ T
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d}
⊢ (fun x => x.2 - x.1) (↑x✝¹.1, ↑x✝¹.2) ∈ {y | Valued.v (y - 0) < ↑d}

Tactic:
simp only [sub_zero, Set.mem_setOf_eq]

Result:
case h.a
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x => (↑x.1, ↑x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x => x.2 - x.1) ⁻¹' R ⊆ T
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d}
⊢ Valued.v (↑x✝¹.2 - ↑x✝¹.1) < ↑d

Proof state:
case h.mpr
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
⊢ (∃ t ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t ⊆ S) →
    ∃ t, (∃ t_1 ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧ (fun x => (↑x.1, ↑x.2)) ⁻¹' t ⊆ S

Tactic:
rintro ⟨_, ⟨hT, pre_T⟩⟩

Result:
case h.mpr.intro.intro
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
⊢ ∃ t, (∃ t_1 ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧ (fun x => (↑x.1, ↑x.2)) ⁻¹' t ⊆ S

Proof state:
case h.mpr.intro.intro.intro.refine_2
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
⊢ (fun x => (↑x.1, ↑x.2)) ⁻¹' ((fun x => x.2 - x.1) ⁻¹' X) ⊆ S

Tactic:
refine subset_trans (fun _ _ ↦ ?_) pre_T

Result:
case h.mpr.intro.intro.intro.refine_2
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => (↑x.1, ↑x.2)) ⁻¹' ((fun x => x.2 - x.1) ⁻¹' X)
⊢ x✝¹ ∈ (fun x => x.2 - x.1) ⁻¹' w✝

Proof state:
case h.mp
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
⊢ (∃ t, (∃ t_1 ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧ (fun x => (↑x.1, ↑x.2)) ⁻¹' t ⊆ S) →
    ∃ t ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t ⊆ S

Tactic:
rintro ⟨T, ⟨⟨R, ⟨hR, pre_R⟩⟩, pre_T⟩⟩

Result:
case h.mp.intro.intro.intro.intro
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x => (↑x.1, ↑x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x => x.2 - x.1) ⁻¹' R ⊆ T
⊢ ∃ t ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t ⊆ S

Proof state:
case h.mpr.intro.intro.intro.refine_1
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
⊢ ∃ γ, {y | Valued.v y < ↑γ} ⊆ X

Tactic:
use d

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x => (↑x.1, ↑x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x => x.2 - x.1) ⁻¹' R ⊆ T
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
⊢ {y | Valued.v y < ↑d} ⊆ {P | Valued.v P < ↑d}

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
⊢ { sets := {s | ∃ t ∈ uniformity K⸨X⸩, (fun x => (↑x.1, ↑x.2)) ⁻¹' t ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯,
      inter_sets := ⋯ } =
    uniformity (RatFunc K)

Tactic:
ext S

Result:
case h
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
⊢ S ∈
      { sets := {s | ∃ t ∈ uniformity K⸨X⸩, (fun x => (↑x.1, ↑x.2)) ⁻¹' t ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ } ↔
    S ∈ uniformity (RatFunc K)