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 Γ₀
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 (β := hat K) (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹)
    (SProd.sprod (α := Filter (hat K)) (β := Filter (hat K)) (𝓝 1) (𝓝 1)) (𝓝 1)

Tactic:
have : Tendsto (fun p : hat K × hat K => p.1 * p.2⁻¹) ((𝓝 1) ×ˢ (𝓝 1)) (𝓝 1) := by
        rw [← nhds_prod_eq]
        conv =>
          congr
          rfl
          rfl
          rw [← one_mul (1 : hat K)]
        refine
          Tendsto.mul continuous_fst.continuousAt (Tendsto.comp ?_ continuous_snd.continuousAt)
        convert! (continuousAt_inv₀ (zero_ne_one.symm : 1 ≠ (0 : hat K))).tendsto
        exact inv_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
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 (β := hat K) (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹)
    (SProd.sprod (α := Filter (hat K)) (β := Filter (hat K)) (𝓝 1) (𝓝 1)) (𝓝 1)
rcases :
  ∀ (U : Set (hat K)) (U_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) U)
    (hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').1 * (x, x').2⁻¹ ∈ V),
    ∃ (V' : Set (hat K)), Membership.mem (γ := Filter (hat K)) (𝓝 1) V' ∧ 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
⊢ ∃ (V' : Set (hat K)), Membership.mem (γ := Filter (hat K)) (𝓝 1) V' ∧ 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V

Tactic:
rcases tendsto_prod_self_iff.mp this V V_in with ⟨U, U_in, hU⟩

Premises used: Filter.tendsto_prod_self_iff, Iff.mp
-- 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 (β := hat K) (fun (p : hat K × hat K) ↦ p.1 * p.2⁻¹)
    (SProd.sprod (α := Filter (hat K)) (β := Filter (hat K)) (𝓝 1) (𝓝 1)) (𝓝 1)
U : Set (hat K)
U_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) U
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').1 * (x, x').2⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
⊢ Membership.mem (γ := Filter (hat K)) (𝓝 1) hatKstar

Tactic:
have : hatKstar ∈ 𝓝 (1 : hat K) := compl_singleton_mem_nhds 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
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_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)
U : Set (hat K)
U_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) U
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').1 * (x, x').2⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : Membership.mem (γ := Filter (hat K)) (𝓝 1) hatKstar
⊢ ∃ (V' : Set (hat K)), Membership.mem (γ := Filter (hat K)) (𝓝 1) V' ∧ 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V

Tactic:
⟨U ∩ hatKstar, Filter.inter_mem U_in this,
        ⟨fun ⟨_, h'⟩ ↦ h' rfl, fun x ⟨hx, _⟩ y ⟨hy, _⟩ ↦ hU _ _  hx hy⟩⟩

Premises used: False, HMul.hMul, Filter.inter_mem, Membership.mem, Inter.inter, Inv.inv, And.intro, Exists.intro, _private.0.Valued.continuous_extension.match_1, rfl, _private.0.Valued.continuous_extension.match_2
-- 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_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)
U : Set (hat K)
U_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) U
hU : ∀ (x x' : hat K), x ∈ U → x' ∈ U → (x, x').1 * (x, x').2⁻¹ ∈ V
hatKstar : Set (hat K) := {0}ᶜ
this : Membership.mem (γ := Filter (hat K)) (𝓝 1) hatKstar
⊢ ∃ (V' : Set (hat K)), Membership.mem (γ := Filter (hat K)) (𝓝 1) V' ∧ 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V

Tactic:
exact ⟨U ∩ hatKstar, Filter.inter_mem U_in this,
        ⟨fun ⟨_, h'⟩ ↦ h' rfl, fun x ⟨hx, _⟩ y ⟨hy, _⟩ ↦ hU _ _  hx hy⟩⟩
-- 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 : Γ₀)
⊢ ∃ (V' : Set (hat K)), Membership.mem (γ := Filter (hat K)) (𝓝 1) V' ∧ 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V

Tactic:
have : ∃ V' ∈ 𝓝 (1 : hat K), (0 : hat K) ∉ V' ∧ ∀ (x) (_ : x ∈ V') (y) (_ : y ∈ V'),
      x * y⁻¹ ∈ V := by
      have : Tendsto (fun p : hat K × hat K => p.1 * p.2⁻¹) ((𝓝 1) ×ˢ (𝓝 1)) (𝓝 1) := by
        rw [← nhds_prod_eq]
        conv =>
          congr
          rfl
          rfl
          rw [← one_mul (1 : hat K)]
        refine
          Tendsto.mul continuous_fst.continuousAt (Tendsto.comp ?_ continuous_snd.continuousAt)
        convert! (continuousAt_inv₀ (zero_ne_one.symm : 1 ≠ (0 : hat K))).tendsto
        exact inv_one.symm
      rcases tendsto_prod_self_iff.mp this V V_in with ⟨U, U_in, hU⟩
      let hatKstar := ({0}ᶜ : Set <| hat K)
      have : hatKstar ∈ 𝓝 (1 : hat K) := compl_singleton_mem_nhds zero_ne_one.symm
      exact ⟨U ∩ hatKstar, Filter.inter_mem U_in this,
        ⟨fun ⟨_, h'⟩ ↦ h' rfl, fun x ⟨hx, _⟩ y ⟨hy, _⟩ ↦ hU _ _  hx hy⟩⟩
-- 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 : ∃ (V' : Set (hat K)), Membership.mem (γ := Filter (hat K)) (𝓝 1) V' ∧ 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
inr :
  ∀ (V' : Set (hat K)) (V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V') (zeroV' : 0 ∉ V')
    (hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V),
    ∃ (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 this with ⟨V', V'_in, zeroV', hV'⟩
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
x : hat K
⊢ (fun (x : hat K) ↦ x * x₀⁻¹) ((fun (x : hat K) ↦ x * x₀) x) = x

Tactic:
simp only [mul_assoc, mul_inv_cancel₀ h, mul_one]

Premises used: mul_inv_cancel₀, mul_assoc, mul_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
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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
⊢ Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀

Tactic:
have l : Function.LeftInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
        intro x
        simp only [mul_assoc, mul_inv_cancel₀ h, mul_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
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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
x : hat K
⊢ (fun (x : hat K) ↦ x * x₀) ((fun (x : hat K) ↦ x * x₀⁻¹) x) = x

Tactic:
simp only [mul_assoc, inv_mul_cancel₀ h, mul_one]

Premises used: mul_assoc, mul_one, inv_mul_cancel₀
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
⊢ Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀

Tactic:
have r : Function.RightInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
        intro x
        simp only [mul_assoc, inv_mul_cancel₀ h, mul_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
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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
⊢ Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹

Tactic:
fun_prop
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
⊢ Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹

Tactic:
have c : Continuous fun x : hat K => x * x₀⁻¹ := by fun_prop
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
c : Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹
rw : (fun (x : hat K) ↦ x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀
⊢ (fun (x : hat K) ↦ x * x₀) '' V' ∈ 𝓝 x₀

Tactic:
rw [image_eq_preimage_of_inverse l r]

Premises used: Set.image_eq_preimage_of_inverse
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
c : Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹
⊢ V' ∈ 𝓝 (x₀ * x₀⁻¹)

Tactic:
rw [← mul_inv_cancel₀ h] at V'_in

Premises used: mul_inv_cancel₀
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
c : Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹
V'_in₁ : V' ∈ 𝓝 (x₀ * x₀⁻¹)
⊢ 0 ∉ V'

Tactic:
rw [← mul_inv_cancel₀ h] at V'_in

Premises used: mul_inv_cancel₀
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
c : Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹
V'_in₁ : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV'₁ : 0 ∉ V'
⊢ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V

Tactic:
rw [← mul_inv_cancel₀ h] at V'_in

Premises used: mul_inv_cancel₀
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
c : Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹
V'_in₁ : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV'₁ : 0 ∉ V'
hV'₁ : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
⊢ Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀

Tactic:
rw [← mul_inv_cancel₀ h] at V'_in

Premises used: mul_inv_cancel₀
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
c : Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹
V'_in₁ : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV'₁ : 0 ∉ V'
hV'₁ : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l₁ : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
⊢ Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀

Tactic:
rw [← mul_inv_cancel₀ h] at V'_in

Premises used: mul_inv_cancel₀
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
c : Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹
V'_in₁ : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV'₁ : 0 ∉ V'
hV'₁ : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l₁ : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r₁ : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
⊢ Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹

Tactic:
rw [← mul_inv_cancel₀ h] at V'_in

Premises used: mul_inv_cancel₀
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
c : Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹
⊢ (fun (x : hat K) ↦ x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀

Tactic:
c.continuousAt V'_in

Premises used: Set.Mem, setOf, Continuous.continuousAt, Set.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
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 : Γ₀)
V' : Set (hat K)
V'_in : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
r : Function.RightInverse (fun (x : hat K) ↦ x * x₀⁻¹) fun (x : hat K) ↦ x * x₀
c : Continuous (Y := hat K) fun (x : hat K) ↦ x * x₀⁻¹
⊢ (fun (x : hat K) ↦ x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀

Tactic:
exact c.continuousAt V'_in

Premises used: Continuous.continuousAt
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
⊢ (fun (x : hat K) ↦ x * x₀) '' V' ∈ 𝓝 x₀

Tactic:
have nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀ := by
      have l : Function.LeftInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
        intro x
        simp only [mul_assoc, mul_inv_cancel₀ h, mul_one]
      have r : Function.RightInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
        intro x
        simp only [mul_assoc, inv_mul_cancel₀ h, mul_one]
      have c : Continuous fun x : hat K => x * x₀⁻¹ := by fun_prop
      rw [image_eq_preimage_of_inverse l r]
      rw [← mul_inv_cancel₀ h] at V'_in
      exact c.continuousAt V'_in
-- 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 : Γ₀)
V' : Set (hat K)
V'_in : Membership.mem (γ := Filter (hat K)) (𝓝 1) V'
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun (x : hat K) ↦ x * x₀) '' V' ∈ 𝓝 x₀
rcases :
  ∀ (z₀ : K) (y₀ : hat K) (y₀_in : y₀ ∈ V') (H : y₀ * x₀ = (↑z₀ : hat K)),
    ∃ (z₀ : K), ∃ y₀ ∈ V', (↑z₀ : hat K) = y₀ * x₀ ∧ z₀ ≠ 0
⊢ ∃ (z₀ : K), ∃ y₀ ∈ V', (↑z₀ : hat K) = y₀ * x₀ ∧ z₀ ≠ 0

Tactic:
rcases Completion.denseRange_coe.mem_nhds nhds_right with ⟨z₀, y₀, y₀_in, H : y₀ * x₀ = z₀⟩

Premises used: UniformSpace.Completion.denseRange_coe, DenseRange.mem_nhds