awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
b : K
hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
pos :
  ∀ (z0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀))
    (hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)),
    IsOpen.{u_1} (X := K) {w : K | LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀)}
⊢ IsOpen.{u_1} (X := K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}

Tactic:
rw [← hb] at z0 ⊢
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
b : K
z0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀)
hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
pos :
  IsOpen.{u_1} (X := K)
    {w : K |
      LE.le.{u_2} (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) b :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))}
⊢ IsOpen.{u_1} (X := K) {w : K | LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀)}

Tactic:
simp_rw [← v.restrict_le_iff]

Premises used: Valuation.restrict_le_iff, Valued.v
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
b : K
z0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀)
hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
⊢ IsOpen.{u_1} (X := K)
    {w : K |
      LE.le.{u_2} (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) b :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))}

Tactic:
Valued.isOpen_closedBall _ ?_

Premises used: setOf, Valued.isOpen_closedBall
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
b : K
z0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀)
hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
pos :
  Ne.{u_2 + 1} (α := MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)
    ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) b :
      MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)
⊢ IsOpen.{u_1} (X := K)
    {w : K |
      LE.le.{u_2} (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) b :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))}

Tactic:
refine Valued.isOpen_closedBall _ ?_

Premises used: Valued.isOpen_closedBall
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
b : K
z0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀)
hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
pos : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) b : Γ₀) (0 : Γ₀)
⊢ Ne.{u_2 + 1} (α := MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)
    ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) b :
      MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)

Tactic:
rw [ne_eq, ← map_zero v.restrict, v.restrict_inj, map_zero]

Premises used: Valued.v, map_zero, Valuation.restrict_inj, ne_eq, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
b : K
z0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀)
hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
⊢ ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) b : Γ₀) (0 : Γ₀)

Tactic:
z0.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
b : K
z0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀)
hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
⊢ ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) b : Γ₀) (0 : Γ₀)

Tactic:
exact z0.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : ¬(v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
neg :
  IsOpen.{u_1} (X := K)
    {w_1 : K |
      Eq.{u_2 + 1} (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w_1 :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))}
⊢ IsOpen.{u_1} (X := K) {w_1 : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w_1 : Γ₀) ((v : (a : K) → Γ₀) w : Γ₀)}

Tactic:
simp_rw [← v.restrict_inj]

Premises used: Valued.v, Valuation.restrict_inj
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : ¬(v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
⊢ IsOpen.{u_1} (X := K)
    {w_1 : K |
      Eq.{u_2 + 1} (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w_1 :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))}

Tactic:
Valued.isOpen_sphere _ ?_

Premises used: setOf, Valued.isOpen_sphere
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : ¬(v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
neg :
  Ne.{u_2 + 1} (α := MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)
    ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w :
      MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)
⊢ IsOpen.{u_1} (X := K)
    {w_1 : K |
      Eq.{u_2 + 1} (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w_1 :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))}

Tactic:
refine Valued.isOpen_sphere _ ?_

Premises used: Valued.isOpen_sphere
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : ¬(v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
⊢ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) w

Tactic:
push Not at hw

Premises used: Not
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) w
neg : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) 0 : Γ₀)
⊢ Ne.{u_2 + 1} (α := MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)
    ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) w :
      MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)

Tactic:
rw [← map_zero v.restrict, ne_eq, v.restrict_inj]

Premises used: Valued.v, map_zero, Valuation.restrict_inj, ne_eq, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) w
⊢ ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) 0 : Γ₀)

Tactic:
(hw.trans' ?_).ne'

Premises used: LT.lt.trans', LT.lt.ne'
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) w
neg : (v : (a : K) → Γ₀) 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
⊢ ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) 0 : Γ₀)

Tactic:
refine (hw.trans' ?_).ne'

Premises used: LT.lt.trans', LT.lt.ne'
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
hw : (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) w
⊢ (v : (a : K) → Γ₀) 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)

Tactic:
simp [z0]
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hz1 : z ≤ 1
z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
U : K → Set K :=
  fun (y : K) ↦
    if (v : (a : K) → Γ₀) y ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)}
this :
  ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
w : K
val :
  LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) (1 : Γ₀) →
    ∃ (i : K),
      Membership.mem (γ := Set K)
        (if (v : (a : K) → Γ₀) i ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
          {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
        else {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) i : Γ₀)})
        w
⊢ w ∈ (↑𝒪[K] : Set K) → Membership.mem (γ := Set K) (⋃ (i : K), U i) w

Tactic:
simp only [integer, SetLike.mem_coe, Valuation.mem_integer_iff, Set.mem_iUnion, U]

Premises used: Valued.integer, Set.mem_iUnion, SetLike.mem_coe, Valuation.mem_integer_iff