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

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}
⊢ X ∈ nhds 0

Tactic:
simp only [Valued.mem_nhds, sub_zero]

Result:
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

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)
⊢ (fun x => x.2 - x.1) x✝¹ ∈ {y | Valued.v (y - 0) < ↑d}

Tactic:
erw [Set.mem_setOf_eq, sub_zero, valuation_eq_LaurentSeries_valuation,
  RatFunc.coe_sub]

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)
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) (↑x✝¹.2 - ↑x✝¹.1) < ↑d

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}
⊢ X ∈ nhds 0 ∧ (fun x => x.2 - x.1) ⁻¹' X ⊆ (fun x => x.2 - x.1) ⁻¹' X

Tactic:
refine ⟨?_, Set.Subset.refl _⟩

Result:
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}
⊢ X ∈ nhds 0

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
⊢ {P | Valued.v P < ↑d} ∈ nhds 0 ∧ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d} ⊆ S

Tactic:
simp only [Valued.mem_nhds, sub_zero]

Result:
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
⊢ (∃ γ, {y | Valued.v y < ↑γ} ⊆ {P | Valued.v P < ↑d}) ∧ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d} ⊆ S

Proof state:
case h.mp.intro.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
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
⊢ ∃ t ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t ⊆ S

Tactic:
use {P : RatFunc K | Valued.v P < ↑d}

Result:
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
⊢ {P | Valued.v P < ↑d} ∈ nhds 0 ∧ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d} ⊆ S

Proof state:
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

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

Result:
case h.mp.intro.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
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
⊢ ∃ t ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t ⊆ S

Proof state:
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)

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

Result:
case h
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

Proof state:
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

Tactic:
let X := {f : K⸨X⸩ | Valued.v f < ↑d}

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✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
⊢ ∃ 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
⊢ (∃ γ, {y | Valued.v y < ↑γ} ⊆ {P | Valued.v P < ↑d}) ∧ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d} ⊆ S

Tactic:
refine ⟨⟨d, by rfl⟩, subset_trans (fun _ _ ↦ pre_R ?_) pre_T⟩

Result:
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

Proof state:
case h
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:
constructor

Result:
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

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