awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min
      (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) *
        HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hr' : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
γ : Γ₀ˣ := Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) ⋯
hbc : (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
    HMul.hMul (β := Γ₀) (↑γ : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min
      (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) *
        HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hr' : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
γ : Γ₀ˣ := Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) ⋯
⊢ (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)

Tactic:
Valuation.inversion_estimate v y_ne h

Premises used: Valuation.inversion_estimate
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min
      (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) *
        HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hr' : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
γ : Γ₀ˣ := Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) ⋯
⊢ (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)

Tactic:
exact Valuation.inversion_estimate v y_ne h

Premises used: Valuation.inversion_estimate
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min
      (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) *
        HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hr' : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
γ : Γ₀ˣ := Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) ⋯
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) (0 : Γ₀)

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min
      (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) *
        HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hr' : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
γ : Γ₀ˣ := Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) ⋯
v₁ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
    HMul.hMul (β := Γ₀) (↑γ : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) < (v : (a : K) → Γ₀) s

Tactic:
calc
    v (x⁻¹ - y⁻¹) * v r < γ * v r := by gcongr; exact Valuation.inversion_estimate v y_ne h
    _ = v s := div_mul_cancel₀ _ (by simpa)

Premises used: div_mul_cancel₀, HSub.hSub, Inv.inv, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
⊢ IsTopologicalRing K

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
s_in : s ∈ 𝓝 x⁻¹
obtain :
  ∀ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ)
    (hs :
      {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s),
    s ∈ map Inv.inv (𝓝 x)
⊢ s ∈ map Inv.inv (𝓝 x)

Tactic:
obtain ⟨γ, hs⟩ := Valued.mem_nhds.mp s_in

Premises used: Valued.mem_nhds, Iff.mp
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s
rw :
  ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)} ⊆
      Inv.inv ⁻¹' s
⊢ s ∈ map Inv.inv (𝓝 x)

Tactic:
rw [mem_map, Valued.mem_nhds]

Premises used: Valued.mem_nhds, Filter.mem_map
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
h :
  {y : K |
      (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * (γ' * γ')) γ') : ValueGroup₀ v)} ⊆
    Inv.inv ⁻¹' s
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)} ⊆
      Inv.inv ⁻¹' s

Tactic:
use min (γ * (γ' * γ')) γ'

Premises used: HMul.hMul, Min.min
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
y : K
y_in :
  Membership.mem (γ := Set K)
    {y : K |
      (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * (γ' * γ')) γ') : ValueGroup₀ v)}
    y
h :
  Membership.mem (γ := Set K)
    {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} y⁻¹
⊢ y ∈ Inv.inv ⁻¹' s

Tactic:
apply hs
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
y : K
y_in :
  Membership.mem (γ := Set K)
    {y : K |
      (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * (γ' * γ')) γ') : ValueGroup₀ v)}
    y
⊢ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    min ((↑γ : ValueGroup₀ v) * ((↑γ' : ValueGroup₀ v) * (↑γ' : ValueGroup₀ v))) (↑γ' : ValueGroup₀ v)

Tactic:
simp only [mem_setOf_eq, Units.min_val, Units.val_mul] at y_in

Premises used: Units.min_val, Set.mem_setOf_eq, Units.val_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
y : K
y_in :
  (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    min ((↑γ : ValueGroup₀ v) * ((↑γ' : ValueGroup₀ v) * (↑γ' : ValueGroup₀ v))) (↑γ' : ValueGroup₀ v)
⊢ Membership.mem (γ := Set K)
    {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} y⁻¹

Tactic:
Valuation.inversion_estimate _ x_ne y_in

Premises used: Set.Mem, setOf, Valuation.inversion_estimate
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
this : T2Space K
⊢ T0Space K

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
suffices : T2Space K
⊢ T0Space K

Tactic:
suffices T2Space K by infer_instance
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
H : ∀ (x : K), x ≠ 0 → ∃ (U : Set K), Membership.mem (γ := Filter K) (𝓝 0) U ∧ x ∉ U
⊢ T2Space K

Tactic:
apply IsTopologicalAddGroup.t2Space_of_zero_sep

Premises used: IsTopologicalAddGroup.t2Space_of_zero_sep
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
⊢ ∃ (U : Set K), Membership.mem (γ := Filter K) (𝓝 0) U ∧ x ∉ U

Tactic:
⟨{ k | v k < v x }, ?_, fun h => lt_irrefl _ h⟩

Premises used: lt_irrefl, Valued.v, setOf, And.intro, LT.lt, Exists.intro, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
H :
  Membership.mem (γ := Filter K) (𝓝 0)
    {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)}
⊢ ∃ (U : Set K), Membership.mem (γ := Filter K) (𝓝 0) U ∧ x ∉ U

Tactic:
refine ⟨{ k | v k < v x }, ?_, fun h => lt_irrefl _ h⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
H :
  ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    Subset.{u_1} (α := Set K)
      {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - 0) < (↑γ : ValueGroup₀ v)}
      {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)}
⊢ Membership.mem (γ := Filter K) (𝓝 0)
    {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)}

Tactic:
rw [Valued.mem_nhds]

Premises used: Valued.mem_nhds
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
⊢ let γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
    Units.mk0
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        x)
      ⋯;
  γ' =
    Units.mk0
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        x)
      ⋯

Tactic:
set γ' := Units.mk0 ((ValueGroup₀.restrict₀ _) x) (v.restrict.ne_zero_iff.mpr x_ne) with hdef

Premises used: Iff.mpr, Valued.v, Valuation.ne_zero_iff, Units.mk0, MonoidWithZeroHom.ValueGroup₀.restrict₀, DFunLike.coe, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
hdef :
  γ' =
    Units.mk0
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        x)
      ⋯
y : K
hy :
  Membership.mem (γ := Set K)
    {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - 0) < (↑γ' : ValueGroup₀ v)} y
⊢ LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
simp only [Valuation.restrict_lt_iff_lt_embedding, hdef, sub_zero, Units.val_mk0,
      mem_setOf_eq, embedding_restrict₀] at hy

Premises used: sub_zero, Valuation.restrict_lt_iff_lt_embedding, Set.mem_setOf_eq, MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀, Units.val_mk0
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
hdef :
  γ' =
    Units.mk0
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        x)
      ⋯
y : K
hy : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Membership.mem (γ := Set K) {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)} y

Tactic:
simpa using hy
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
hdef :
  γ' =
    Units.mk0
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        x)
      ⋯
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    Subset.{u_1} (α := Set K)
      {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - 0) < (↑γ : ValueGroup₀ v)}
      {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)}

Tactic:
exact ⟨γ', fun y hy => by
    simp only [Valuation.restrict_lt_iff_lt_embedding, hdef, sub_zero, Units.val_mk0,
      mem_setOf_eq, embedding_restrict₀] at hy
    simpa using hy⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
rw :
  ∀ (x : K),
    ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ Continuous[hv.toTopologicalSpace, topologicalSpace] (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
inl :
  ContinuousAt.{u_1, u_2} (X := K) (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 0
inr :
  ∀ (h : x ≠ 0),
    ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x

Tactic:
rcases eq_or_ne x 0 with (rfl | h)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
inl :
  ∀ (γ₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)),
    γ₀ ≠ 0 → ∀ᶠ (x : K) in 𝓝 0, (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < γ₀
⊢ ContinuousAt.{u_1, u_2} (X := K) (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 0

Tactic:
rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]

Premises used: ContinuousAt, map_zero, WithZeroTopology.tendsto_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)
hγ : γ ≠ 0
inl :
  ∃ (γ_1 : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    Subset.{u_1} (α := Set K)
      {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑γ_1 : ValueGroup₀ v)}
      {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < γ}
⊢ ∀ᶠ (x : K) in 𝓝 0, (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < γ

Tactic:
rw [Filter.Eventually, Valued.mem_nhds_zero]

Premises used: Filter.Eventually, Valued.mem_nhds_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)
hγ : γ ≠ 0
h :
  Subset.{u_1} (α := Set K)
    {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑(Units.mk0 γ hγ) : ValueGroup₀ v)}
    {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑(Units.mk0 γ hγ) : ValueGroup₀ v)}
⊢ ∃ (γ_1 : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    Subset.{u_1} (α := Set K)
      {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑γ_1 : ValueGroup₀ v)}
      {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < γ}

Tactic:
use Units.mk0 γ hγ

Premises used: Units.mk0
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)
hγ : γ ≠ 0
⊢ Subset.{u_1} (α := Set K)
    {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑(Units.mk0 γ hγ) : ValueGroup₀ v)}
    {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑(Units.mk0 γ hγ) : ValueGroup₀ v)}

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
⊢ Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
have v_ne : (v.restrict x : ValueGroup₀ hv.v) ≠ 0 := (Valuation.ne_zero_iff _).mpr h
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
inr :
  ∀ᶠ (x_1 : K) in 𝓝 x,
    Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x_1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ ContinuousAt.{u_1, u_2} (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x

Tactic:
rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero v_ne]

Premises used: WithZeroTopology.tendsto_of_ne_zero, ContinuousAt
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
inr : ∀ᶠ (x_1 : K) in 𝓝 x, Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ ∀ᶠ (x_1 : K) in 𝓝 x,
    Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x_1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
simp_rw [v.restrict_inj]

Premises used: Valued.v, Valuation.restrict_inj
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
simpa [restrict₀_apply] using v_ne

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ ∀ᶠ (x_1 : K) in 𝓝 x, Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
apply Valued.locally_const (by simpa [restrict₀_apply] using v_ne)

Premises used: Valued.locally_const
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
rw : ∀ (x : K), ContinuousAt.{u_1, u_2} (Y := Γ₀) (⇑v : (a : K) → Γ₀) x
⊢ Continuous[hv.toTopologicalSpace, topologicalSpace] (⇑v : (a : K) → Γ₀)

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt