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 : Γ₀)
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₀
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

Tactic:
⟨z₀, y₀, y₀_in, ⟨H.symm, ?_⟩⟩

Premises used: And.intro, Exists.intro, 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 : Γ₀)
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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = (↑z₀ : hat K)
refine : z₀ ≠ 0
⊢ ∃ (z₀ : K), ∃ y₀ ∈ V', (↑z₀ : hat K) = y₀ * x₀ ∧ z₀ ≠ 0

Tactic:
refine ⟨z₀, y₀, y₀_in, ⟨H.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 : Γ₀)
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₀
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = (↑0 : hat K)
⊢ False

Tactic:
mul_ne_zero (ne_of_mem_of_not_mem y₀_in zeroV') h H

Premises used: ne_of_mem_of_not_mem, mul_ne_zero
-- 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₀
y₀ : hat K
y₀_in : y₀ ∈ V'
H : y₀ * x₀ = (↑0 : hat K)
⊢ False

Tactic:
exact mul_ne_zero (ne_of_mem_of_not_mem y₀_in zeroV') h H

Premises used: ne_of_mem_of_not_mem, mul_ne_zero
-- 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₀
⊢ ∃ (z₀ : K), ∃ y₀ ∈ V', (↑z₀ : hat K) = y₀ * x₀ ∧ z₀ ≠ 0

Tactic:
have : ∃ z₀ : K, ∃ y₀ ∈ V', ↑z₀ = y₀ * x₀ ∧ z₀ ≠ 0 := by
      rcases Completion.denseRange_coe.mem_nhds nhds_right with ⟨z₀, y₀, y₀_in, H : y₀ * x₀ = z₀⟩
      refine ⟨z₀, y₀, y₀_in, ⟨H.symm, ?_⟩⟩
      rintro rfl
      exact mul_ne_zero (ne_of_mem_of_not_mem y₀_in zeroV') h H
-- 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₀
this : ∃ (z₀ : K), ∃ y₀ ∈ V', (↑z₀ : hat K) = y₀ * x₀ ∧ z₀ ≠ 0
inr :
  ∀ (z₀ : K) (y₀ : hat K) (y₀_in : y₀ ∈ V') (hz₀ : (↑z₀ : hat K) = y₀ * x₀) (z₀_ne : z₀ ≠ 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 this with ⟨z₀, y₀, y₀_in, hz₀, z₀_ne⟩
-- 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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
rwa rwa₁ rwa₂ rwa₃ : z₀ ≠ 0
⊢ Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
rwa [Valuation.ne_zero_iff]

Premises used: Valuation.ne_zero_iff
-- 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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
⊢ Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
have vz₀_ne : v.restrict z₀ ≠ 0 := by rwa [Valuation.ne_zero_iff]
-- 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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
    Tendsto (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (Filter.comap Completion.coe' (𝓝 x₀))
      (𝓝 c)

Tactic:
⟨v.restrict z₀, ?_⟩

Premises used: Valued.v, Exists.intro, DFunLike.coe, 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
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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
inr :
  Tendsto.{u_1, u_2} (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (Filter.comap Completion.coe' (𝓝 x₀))
    (𝓝 ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀) :
      Filter (ValueGroup₀ (F := Valuation K Γ₀) v))
⊢ ∃ (c : ValueGroup₀ (F := Valuation K Γ₀) v),
    Tendsto (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (Filter.comap Completion.coe' (𝓝 x₀))
      (𝓝 c)

Tactic:
refine ⟨v.restrict z₀, ?_⟩
-- 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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
inr :
  ∀ᶠ (b : hat K) in 𝓝 x₀,
    ∀ (a : K),
      (↑a : hat K) = b →
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a :
            ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ :
            ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ Tendsto.{u_1, u_2} (β := ValueGroup₀ (F := Valuation K Γ₀) v)
    ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      (a : K) → ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (Filter.comap Completion.coe' (𝓝 x₀))
    (𝓝 ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀) :
      Filter (ValueGroup₀ (F := Valuation K Γ₀) v))

Tactic:
rw [WithZeroTopology.tendsto_of_ne_zero vz₀_ne, eventually_comap]

Premises used: WithZeroTopology.tendsto_of_ne_zero, Filter.eventually_comap
-- 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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
h₁ :
  ∀ (x : hat K) (x_in : Membership.mem (γ := Set (hat K)) ((fun (x : hat K) ↦ x * x₀) '' V') x) (a : K)
    (ha : (↑a : hat K) = x),
    Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ ∀ᶠ (b : hat K) in 𝓝 x₀,
    ∀ (a : K),
      (↑a : hat K) = b →
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a :
            ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ :
            ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
filter_upwards [nhds_right] with x x_in a ha
-- 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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
x : hat K
x_in : Membership.mem (γ := Set (hat K)) ((fun (x : hat K) ↦ x * x₀) '' V') x
a : K
ha : (↑a : hat K) = x
h₁ :
  ∀ (y : hat K) (y_in : y ∈ V') (ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)),
    Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) a : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
rcases x_in with ⟨y, y_in, rfl⟩

Premises used: 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 : Γ₀)
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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
rw : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (a * z₀⁻¹) : Γ₀) (1 : Γ₀)
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
rw [v.restrict_def, ValueGroup₀.restrict₀_eq_one_iff]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_one_iff, Valued.v, Valuation.restrict_def
-- 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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
a₁ : (↑(a * z₀⁻¹) : hat K) ∈ V
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (a * z₀⁻¹) : Γ₀) (1 : Γ₀)

Tactic:
apply 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
nhds_right : (fun (x : hat K) ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
⊢ Eq (α := hat K) (↑z₀⁻¹ : hat K) (↑z₀ : hat K)⁻¹

Tactic:
have : (z₀⁻¹ : K) = (z₀ : hat K)⁻¹ := map_inv₀ (Completion.coeRingHom : K →+* hat K) z₀
-- 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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
this : Eq (α := hat K) (↑z₀⁻¹ : hat K) (↑z₀ : hat K)⁻¹
a₁ : y * y₀⁻¹ ∈ V
⊢ (↑(a * z₀⁻¹) : hat K) ∈ V

Tactic:
rw [Completion.coe_mul, this, ha, hz₀, mul_inv, mul_comm y₀⁻¹, ← mul_assoc, mul_assoc y,
        mul_inv_cancel₀ h, mul_one]

Premises used: mul_inv_cancel₀, mul_inv, mul_assoc, Inv.inv, UniformSpace.Completion.coe_mul, mul_comm, 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
nhds_right : (fun (x : hat K) ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
this : Eq (α := hat K) (↑z₀⁻¹ : hat K) (↑z₀ : hat K)⁻¹
⊢ y * y₀⁻¹ ∈ V

Tactic:
solve_by_elim
-- 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₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : (↑z₀ : hat K) = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) z₀ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
a : K
y : hat K
y_in : y ∈ V'
ha : Eq (α := hat K) (↑a : hat K) ((fun (x : hat K) ↦ x * x₀) y)
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a * z₀⁻¹) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
have : (v.restrict (a * z₀⁻¹)) = 1 := by
      rw [v.restrict_def, ValueGroup₀.restrict₀_eq_one_iff]
      apply hV
      have : (z₀⁻¹ : K) = (z₀ : hat K)⁻¹ := map_inv₀ (Completion.coeRingHom : K →+* hat K) z₀
      rw [Completion.coe_mul, this, ha, hz₀, mul_inv, mul_comm y₀⁻¹, ← mul_assoc, mul_assoc y,
        mul_inv_cancel₀ h, mul_one]
      solve_by_elim