awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ w ∈ (↑𝒪[K] : Set K) → Membership.mem (γ := Set K) (⋃ (i : K), U i) w
have 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
Tactic: simp only [integer, SetLike.mem_coe, Valuation.mem_integer_iff, Set.mem_iUnion, 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
w : K
hw : 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
have h : Membership.mem (γ := Set K)
  (if
      (v : (a : K) → Γ₀) (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then a else 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) → Γ₀) (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then a else w) : Γ₀)})
  w
Tactic: use if v w ≤ z then a else w
-- 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 : LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) (1 : Γ₀)
⊢ Membership.mem (γ := Set K)
    (if
        (v : (a : K) → Γ₀) (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then a else 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) → Γ₀) (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then a else w) : Γ₀)})
    w
have pos : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
  (v : (a : K) → Γ₀) a ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
    Membership.mem (γ := Set K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)} w
Tactic: split_ifs
-- 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 : LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) (1 : Γ₀)
pos :
  (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
    (v : (a : K) → Γ₀) a ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
      Membership.mem (γ := Set K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)} w
⊢ Membership.mem (γ := Set K)
    (if
        (v : (a : K) → Γ₀) (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then a else 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) → Γ₀) (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then a else w) : Γ₀)})
    w
have neg : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
  ¬(v : (a : K) → Γ₀) a ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
    Membership.mem (γ := Set K) {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)}
      w
Tactic: split_ifs
-- 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 : LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) (1 : Γ₀)
pos :
  (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
    (v : (a : K) → Γ₀) a ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
      Membership.mem (γ := Set K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)} w
neg :
  (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
    ¬(v : (a : K) → Γ₀) a ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
      Membership.mem (γ := Set K)
        {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)} w
⊢ Membership.mem (γ := Set K)
    (if
        (v : (a : K) → Γ₀) (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then a else 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) → Γ₀) (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then a else w) : Γ₀)})
    w
have neg₁ : ¬(v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) →
  Membership.mem (γ := Set K)
    {w_1 : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w_1 : Γ₀) ((v : (a : K) → Γ₀) w : Γ₀)} w
Tactic: split_ifs
-- 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 : ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
⊢ (Set.Icc z 1).Finite
have val : ∀ (t : Finset K) (ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i), (Set.Icc z 1).Finite
Tactic: obtain ⟨t, ht⟩ := 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
⊢ (Set.Icc z 1).Finite
have val : (i : K) → i ∈ (↑t : Set K) → (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
Tactic: refine (t.finite_toSet.dependent_image ?_).subset ?_
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
val : (i : K) → i ∈ (↑t : Set K) → (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ (Set.Icc z 1).Finite
have val₁ : Set.Icc z 1 ⊆
  {y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ |
    ∃ (x : K) (_ : x ∈ (↑t : Set K)),
      (if hi' : (v : (a : K) → Γ₀) x ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then z
        else
          Units.mk0
            (Subtype.mk (p := fun (x : Γ₀) ↦
              Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x) ((v : (a : K) → Γ₀) x) sorry)
            sorry) =
        y}
Tactic: refine (t.finite_toSet.dependent_image ?_).subset ?_
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
⊢ (i : K) → i ∈ (↑t : Set K) → (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
have val : ∀ (i : K) (hi : i ∈ (↑t : Set K)) (hi' : ¬(v : (a : K) → Γ₀) i ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)),
  Ne.{u_2 + 1} (α := ↥(MonoidHom.mrange (F := Valuation K Γ₀) v))
    (Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x)
        ((v : (a : K) → Γ₀) i) sorry :
      ↥(MonoidHom.mrange (F := Valuation K Γ₀) v))
    (0 : ↥(MonoidHom.mrange (F := Valuation K Γ₀) v))
Tactic: refine fun i hi ↦ if hi' : v i ≤ z then z else Units.mk0 ⟨(v i), 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))
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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
i : K
hi : i ∈ (↑t : Set K)
hi' : ¬(v : (a : K) → Γ₀) i ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
⊢ Ne.{u_2 + 1} (α := ↥(MonoidHom.mrange (F := Valuation K Γ₀) v))
    (Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x)
        ((v : (a : K) → Γ₀) i) ⋯ :
      ↥(MonoidHom.mrange (F := Valuation K Γ₀) v))
    (0 : ↥(MonoidHom.mrange (F := Valuation K Γ₀) v))
have hi'₁ : (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) i
Tactic: push Not at hi'
Cleared hypotheses: hi'
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ i ∈ Set.Icc z 1 →
    Membership.mem (γ := Set (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ)
      {y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ |
        ∃ (x : K) (_ : x ∈ (↑t : Set K)),
          (if hi' : (v : (a : K) → Γ₀) x ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then z
            else
              Units.mk0
                (Subtype.mk (p := fun (x : Γ₀) ↦
                  Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x)
                  ((v : (a : K) → Γ₀) x) ⋯)
                ⋯) =
            y}
      i
have val : z ≤ i →
  i ≤ 1 →
    ∃ x ∈ t,
      (if hi' : (v : (a : K) → Γ₀) x ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then z
        else
          Units.mk0
            (Subtype.mk (p := fun (x : Γ₀) ↦
              Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x) ((v : (a : K) → Γ₀) x) sorry)
            sorry) =
        i
Tactic: simp only [Set.mem_Icc, Finset.mem_coe, exists_prop, Set.mem_setOf_eq, and_imp]
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ z ≤ i →
    i ≤ 1 →
      ∃ x ∈ t,
        (if hi' : (v : (a : K) → Γ₀) x ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then z
          else
            Units.mk0
              (Subtype.mk (p := fun (x : Γ₀) ↦
                Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x) ((v : (a : K) → Γ₀) x)
                ⋯)
              ⋯) =
          i
have val : ∀ (c : K) (hc : (v : (a : K) → Γ₀) c = (↑(↑i : ↥(MonoidHom.mrange v)) : Γ₀)),
  z ≤ i →
    i ≤ 1 →
      ∃ x ∈ t,
        (if hi' : (v : (a : K) → Γ₀) x ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then z
          else
            Units.mk0
              (Subtype.mk (p := fun (x : Γ₀) ↦
                Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x) ((v : (a : K) → Γ₀) x)
                sorry)
              sorry) =
          i
Tactic: obtain ⟨c, hc⟩ := i.val.prop
-- 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_1 : 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
c : K
hc : (v : (a : K) → Γ₀) c = (↑(↑i : ↥(MonoidHom.mrange v)) : Γ₀)
hzi : z ≤ i
hi1 : i ≤ 1
⊢ ∃ x ∈ t,
    (if hi' : (v : (a : K) → Γ₀) x ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then z
      else
        Units.mk0
          (Subtype.mk (p := fun (x : Γ₀) ↦
            Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x) ((v : (a : K) → Γ₀) x) ⋯)
          ⋯) =
      i
have hj : Membership.mem (γ := Set K) (⋃ i ∈ t, U i) c
Tactic: have hj := ht (hc.trans_le hi1)
-- 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_1 : 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
c : K
hc : (v : (a : K) → Γ₀) c = (↑(↑i : ↥(MonoidHom.mrange v)) : Γ₀)
hzi : z ≤ i
hi1 : i ≤ 1
hj : Membership.mem (γ := Set K) (⋃ i ∈ t, U i) c
⊢ ∃ x ∈ t,
    (if hi' : (v : (a : K) → Γ₀) x ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then z
      else
        Units.mk0
          (Subtype.mk (p := fun (x : Γ₀) ↦
            Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x) ((v : (a : K) → Γ₀) x) ⋯)
          ⋯) =
      i
have hj₁ : ∃ i ∈ t,
  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 : Γ₀)})
    c
Tactic: simp only [Set.mem_iUnion, exists_prop, U] at hj
Cleared hypotheses: hj