awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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
⊢ (Set.Icc z 1).Finite
have z0' : 0 < (↑z : ↥(MonoidHom.mrange v))
Tactic: have z0' : 0 < (z : MonoidHom.mrange (Valued.v : Valuation K Γ₀)) := by simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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))
⊢ (Set.Icc z 1).Finite
have z0 : 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
Tactic: have z0 : 0 < ((z : MonoidHom.mrange (Valued.v : Valuation K Γ₀)) : Γ₀) :=
    Subtype.coe_lt_coe.mpr z0'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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)) : Γ₀)
⊢ (Set.Icc z 1).Finite
have a0 : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)
Tactic: have a0 : 0 < v a := by simp [ha, z0]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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 : Γ₀)}
⊢ (Set.Icc z 1).Finite
have 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
Tactic: have := hc.elim_finite_subcover U
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
⊢ (Set.Icc z 1).Finite
have val : ∀ (i : K), IsOpen (U i)
Tactic: specialize this ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
val : ∀ (i : K), IsOpen (U i)
⊢ (Set.Icc z 1).Finite
have val₁ : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i
Tactic: specialize this ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
val : ∀ (i : K), IsOpen (U i)
val₁ : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i
⊢ (Set.Icc z 1).Finite
have val₂ : ∀ (this : ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i), (Set.Icc z 1).Finite
Tactic: specialize this ?_ ?_
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
⊢ IsOpen.{u_1} (X := K)
    (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w_1 : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w_1 : Γ₀) ((v : (a : K) → Γ₀) w : Γ₀)})
have pos : ∀ (hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)),
  IsOpen.{u_1} (X := K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
Tactic: split_ifs with hw
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
pos :
  ∀ (hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)),
    IsOpen.{u_1} (X := K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
⊢ IsOpen.{u_1} (X := K)
    (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w_1 : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w_1 : Γ₀) ((v : (a : K) → Γ₀) w : Γ₀)})
have neg : ∀ (hw : ¬(v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)),
  IsOpen.{u_1} (X := K) {w_1 : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w_1 : Γ₀) ((v : (a : K) → Γ₀) w : Γ₀)}
Tactic: split_ifs with hw
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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 : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
have pos : ∀ (b : K) (hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)),
  IsOpen.{u_1} (X := K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
Tactic: obtain ⟨b, hb⟩ := MonoidHom.mem_mrange.mp z.1.2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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)) : Γ₀)
⊢ IsOpen.{u_1} (X := K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
have 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 : Γ₀)}
Tactic: rw [← hb] at z0 ⊢
Cleared hypotheses: z0, hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) b : Γ₀)}
have 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 →*₀ Γ₀))}
Tactic: simp_rw [← v.restrict_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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 →*₀ Γ₀))}
have 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)
Tactic: refine Valued.isOpen_closedBall _ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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)) : Γ₀)
⊢ 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)
have pos : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) b : Γ₀) (0 : Γ₀)
Tactic: rw [ne_eq, ← map_zero v.restrict, v.restrict_inj, map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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} (α := Γ₀) ((v : (a : K) → Γ₀) w_1 : Γ₀) ((v : (a : K) → Γ₀) w : Γ₀)}
have 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 →*₀ Γ₀))}
Tactic: simp_rw [← v.restrict_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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 →*₀ Γ₀))}
have 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)
Tactic: refine Valued.isOpen_sphere _ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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)) : Γ₀)
⊢ 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)
have hw₁ : (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) w
Tactic: push Not at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
⊢ 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)
have neg : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) 0 : Γ₀)
Tactic: rw [← map_zero v.restrict, ne_eq, v.restrict_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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 : Γ₀)
have neg : (v : (a : K) → Γ₀) 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
Tactic: refine (hw.trans' ?_).ne'