awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU :
  ∀ x ∉ U,
    ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a - x)}
refine :
  ∀ (h : 0 ∉ U),
    ∃ (γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)),
      ¬γ = 0 ∧ U ⊆ (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) ⁻¹' Ici γ
⊢ 0 ∈ U ∨
    ∃ (γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)),
      ¬γ = 0 ∧ U ⊆ (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) ⁻¹' Ici γ

Tactic:
refine (em _).imp_right fun h ↦ ?_

Premises used: em, Or.imp_right
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU :
  ∀ x ∉ U,
    ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a - x)}
h_1 : 0 ∉ U
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
h : U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a - 0)}
⊢ U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a}

Tactic:
simp only [sub_zero] at h

Premises used: sub_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU :
  ∀ x ∉ U,
    ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a - x)}
h_1 : 0 ∉ U
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
h : U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a}
⊢ ∃ (γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)),
    ¬γ = 0 ∧ U ⊆ (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) ⁻¹' Ici γ

Tactic:
⟨γ.1, γ.ne_zero, h.trans ?_⟩

Premises used: Units.val, HasSubset.Subset.trans, Units.ne_zero, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU :
  ∀ x ∉ U,
    ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a - x)}
h_1 : 0 ∉ U
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
h : U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a}
refine :
  Subset.{u_1} (α := Set K)
    {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a}
    ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) ⁻¹' Ici (↑γ : ValueGroup₀ v))
⊢ ∃ (γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)),
    ¬γ = 0 ∧ U ⊆ (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) ⁻¹' Ici γ

Tactic:
refine ⟨γ.1, γ.ne_zero, h.trans ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU :
  ∀ x ∉ U,
    ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a - x)}
h_1 : 0 ∉ U
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
h : U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a}
a : K
⊢ Membership.mem (γ := Set K)
      {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a} a →
    Membership.mem (γ := Set K)
      ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) ⁻¹' Ici (↑γ : ValueGroup₀ v)) a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Continuous.{u_1, u_2} (X := hat K) extension

Tactic:
Completion.isDenseInducing_coe.continuous_extend ?_

Premises used: Set.Mem, setOf, IsDenseInducing.continuous_extend, Valued.extension, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
refine :
  ∀ (b : hat K),
    ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
      Tendsto (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (Filter.comap Completion.coe' (𝓝 b))
        (𝓝 c)
⊢ Continuous.{u_1, u_2} (X := hat K) extension

Tactic:
refine Completion.isDenseInducing_coe.continuous_extend ?_

Premises used: IsDenseInducing.continuous_extend, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
inl :
  ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
    Tendsto.{u_1, u_2} (α := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
      (Filter.comap (β := hat K) Completion.coe' (𝓝 0)) (𝓝 c)
inr :
  ∀ (h : x₀ ≠ 0),
    ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
      Tendsto (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (Filter.comap Completion.coe' (𝓝 x₀))
        (𝓝 c)
⊢ ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
    Tendsto (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (Filter.comap Completion.coe' (𝓝 x₀))
      (𝓝 c)

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 : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
    Tendsto.{u_1, u_2} (α := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
      (Filter.comap (β := hat K) Completion.coe' (𝓝 0)) (𝓝 c)

Tactic:
⟨0, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
inl :
  Tendsto.{u_1, u_2} (α := K) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (Filter.comap (β := hat K) Completion.coe' (𝓝 0))
    (𝓝 0)
⊢ ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
    Tendsto.{u_1, u_2} (α := K) (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
      (Filter.comap (β := hat K) Completion.coe' (𝓝 0)) (𝓝 c)

Tactic:
refine ⟨0, ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
inl :
  Tendsto.{u_1, u_2} (α := K) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (𝓝 0) (𝓝 0)
⊢ Tendsto.{u_1, u_2} (α := K) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (Filter.comap (β := hat K) Completion.coe' (𝓝 0))
    (𝓝 0)

Tactic:
rw [← Completion.coe_zero, ← Completion.isDenseInducing_coe.isInducing.nhds_eq_comap]

Premises used: Topology.IsInducing.nhds_eq_comap, IsDenseInducing.isInducing, UniformSpace.Completion.coe_zero, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Tendsto.{u_1, u_2} (α := K) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (𝓝 0) (𝓝 0)

Tactic:
Valued.continuous_valuation.tendsto' 0 0 (map_zero v.restrict)

Premises used: Set.Mem, MonoidWithZeroHomClass.toMonoidWithZeroHom, Valued.continuous_valuation, Valued.v, setOf, map_zero, Continuous.tendsto', OfNat.ofNat, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Tendsto.{u_1, u_2} (α := K) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (𝓝 0) (𝓝 0)

Tactic:
exact Valued.continuous_valuation.tendsto' 0 0 (map_zero v.restrict)

Premises used: Valued.continuous_valuation, Valued.v, map_zero, Continuous.tendsto', OfNat.ofNat, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
rw : Ne.{u_2 + 1} (α := Γ₀) 1 0
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀) (0 : Γ₀)

Tactic:
rw [Valuation.map_one]

Premises used: Valuation.map_one
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ Ne.{u_2 + 1} (α := Γ₀) 1 0

Tactic:
zero_ne_one.symm

Premises used: zero_ne_one, Ne.symm
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ Ne.{u_2 + 1} (α := Γ₀) 1 0

Tactic:
exact zero_ne_one.symm

Premises used: zero_ne_one, Ne.symm
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀) (0 : Γ₀)

Tactic:
have : (v (1 : K) : Γ₀) ≠ 0 := by
        rw [Valuation.map_one]
        exact zero_ne_one.symm
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀) (0 : Γ₀)
⊢ Membership.mem (γ := Filter K) (𝓝 1)
    {y : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)}

Tactic:
Valued.locally_const this

Premises used: Valued.locally_const
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀) (0 : Γ₀)
h₁ :
  Eq.{u_1 + 1} (α := Set K) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
    {y : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)}
⊢ Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})

Tactic:
convert! Valued.locally_const this

Premises used: Valued.locally_const
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀) (0 : Γ₀)
h₁ :
  ∀ (x : K),
    Membership.mem (γ := Set K) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1}) x ↔
      Membership.mem (γ := Set K)
        {y : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)} x
⊢ Eq.{u_1 + 1} (α := Set K) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
    {y : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)}

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
this : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀) (0 : Γ₀)
x : K
h₁ :
  Membership.mem (γ := Set K) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1}) x ↔
    Membership.mem (γ := Set K) {y : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) (1 : Γ₀)} x
h₂ :
  Membership.mem (α := Γ₀) (γ := Set Γ₀) {1} ((v : (a : K) → Γ₀) x : Γ₀) ↔
    Membership.mem (γ := Set K) {y : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) (1 : Γ₀)} x
h₃ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Membership.mem (γ := Set K) {y : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) (1 : Γ₀)} x
h₄ h₅ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Membership.mem (γ := Set K) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1}) x ↔
    Membership.mem (γ := Set K) {y : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀)}
      x

Tactic:
rw [Valuation.map_one, mem_preimage, mem_singleton_iff, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Valuation.map_one, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})

Tactic:
have preimage_one : v ⁻¹' {(1 : Γ₀)} ∈ 𝓝 (1 : K) := by
      have : (v (1 : K) : Γ₀) ≠ 0 := by
        rw [Valuation.map_one]
        exact zero_ne_one.symm
      convert! Valued.locally_const this
      ext x
      rw [Valuation.map_one, mem_preimage, mem_singleton_iff, mem_setOf_eq]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
rwa :
  ∀
    (preimage_one :
      Membership.mem (γ := Filter K) (Filter.comap (β := hat K) Completion.coe' (𝓝 (↑1 : hat K)))
        (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})),
    ∃ (V : Set (hat K)),
      Membership.mem (γ := Filter (hat K)) (𝓝 1) V ∧
        ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (preimage_one :
      ∃ (t : Set (hat K)),
        Membership.mem (γ := Filter (hat K)) (𝓝 (↑1 : hat K)) t ∧
          Completion.coe' ⁻¹' t ⊆ preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1}),
    ∃ (V : Set (hat K)),
      Membership.mem (γ := Filter (hat K)) (𝓝 1) V ∧
        ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (V : Set (hat K)),
    Membership.mem (γ := Filter (hat K)) (𝓝 1) V ∧
      ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rwa [Completion.isDenseInducing_coe.nhds_eq_comap, mem_comap] at preimage_one

Premises used: IsDenseInducing.nhds_eq_comap, Filter.mem_comap, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
inr :
  ∀ (V : Set (hat K)) (V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V)
    (hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)),
    ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
      Tendsto (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (Filter.comap Completion.coe' (𝓝 x₀))
        (𝓝 c)
⊢ ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
    Tendsto (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (Filter.comap Completion.coe' (𝓝 x₀))
      (𝓝 c)

Tactic:
obtain ⟨V, V_in, hV⟩ : ∃ V ∈ 𝓝 (1 : hat K), ∀ x : K, (x : hat K) ∈ V → (v x : Γ₀) = 1 := by
      rwa [Completion.isDenseInducing_coe.nhds_eq_comap, mem_comap] at preimage_one

Premises used: nhds, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
rw : Tendsto (β := hat K) (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)
⊢ Tendsto (β := hat K) (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹)
    (SProd.sprod (α := Filter (hat K)) (β := Filter (hat K)) (𝓝 1) (𝓝 1)) (𝓝 1)

Tactic:
rw [← nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
f : fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹
l₁ : 𝓝 (1, 1)
l₂ : 𝓝 1
| Tendsto (β := hat K) (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
| fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
| 𝓝 (1, 1)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
l₂ : 𝓝 (HMul.hMul (α := hat K) 1 1)
| 𝓝 1

Tactic:
rw [← one_mul (1 : hat K)]

Premises used: OfNat.ofNat, one_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
l₂ : 𝓝 (HMul.hMul (α := hat K) 1 1)
| Tendsto (β := hat K) (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)

Tactic:
congr
          rfl
          rfl
          rw [← one_mul (1 : hat K)]

Premises used: OfNat.ofNat, one_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
conv : Tendsto (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 (HMul.hMul (α := hat K) 1 1))
⊢ Tendsto (β := hat K) (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)

Tactic:
conv =>
          congr
          rfl
          rfl
          rw [← one_mul (1 : hat K)]

Premises used: OfNat.ofNat, one_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Tendsto (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 (HMul.hMul (α := hat K) 1 1))

Tactic:
Tendsto.mul continuous_fst.continuousAt (Tendsto.comp ?_ continuous_snd.continuousAt)

Premises used: continuous_snd, continuous_fst, Continuous.continuousAt, Filter.Tendsto.mul, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
this : Tendsto.{u_1, u_1} (α := hat K) Inv.inv (𝓝 (1, 1).2) (𝓝 1)
⊢ Tendsto (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 (HMul.hMul (α := hat K) 1 1))

Tactic:
refine
          Tendsto.mul continuous_fst.continuousAt (Tendsto.comp ?_ continuous_snd.continuousAt)

Premises used: continuous_snd, continuous_fst, Continuous.continuousAt, Filter.Tendsto.mul, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Tendsto.{u_1, u_1} (α := hat K) Inv.inv (𝓝 1) (𝓝 1⁻¹)

Tactic:
(continuousAt_inv₀ (zero_ne_one.symm : 1 ≠ (0 : hat K))).tendsto

Premises used: ContinuousInv₀.continuousAt_inv₀, zero_ne_one, Ne.symm, ContinuousAt.tendsto
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
h₁ : Eq.{u_1 + 1} (α := hat K) 1 1⁻¹
⊢ Tendsto.{u_1, u_1} (α := hat K) Inv.inv (𝓝 (1, 1).2) (𝓝 1)

Tactic:
convert! (continuousAt_inv₀ (zero_ne_one.symm : 1 ≠ (0 : hat K))).tendsto

Premises used: ContinuousInv₀.continuousAt_inv₀, zero_ne_one, Ne.symm, ContinuousAt.tendsto
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{u_1 + 1} (α := hat K) 1 1⁻¹

Tactic:
inv_one.symm

Premises used: inv_one, Eq.symm
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : Membership.mem (γ := Filter K) (𝓝 1) (preimage (β := Γ₀) (⇑v : (a : K) → Γ₀) {1})
V : Set (hat K)
V_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V
hV : ∀ (x : K), (↑x : hat K) ∈ V → Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{u_1 + 1} (α := hat K) 1 1⁻¹

Tactic:
exact inv_one.symm

Premises used: inv_one, Eq.symm