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 : LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) (1 : Γ₀)
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
⊢ ∃ (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:
use if v w ≤ z then a else w

Premises used: Valued.v, DFunLike.coe
-- 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 : 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
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
⊢ 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:
split_ifs
-- 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 : LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) (1 : Γ₀)
h : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
h_1 : (v : (a : K) → Γ₀) a ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
⊢ Membership.mem (γ := Set K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)} w

Tactic:
simp_all
-- 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 : LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) (1 : Γ₀)
h : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
h_1 : ¬(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:
simp_all
-- 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 : LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) (1 : Γ₀)
h : ¬(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:
simp_all
-- 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 : ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
val : ∀ (t : Finset K) (ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i), (Set.Icc z 1).Finite
⊢ (Set.Icc z 1).Finite

Tactic:
obtain ⟨t, ht⟩ := this
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
⊢ (Set.Icc z 1).Finite

Tactic:
(t.finite_toSet.dependent_image ?_).subset ?_

Premises used: Set.Finite.subset, Set.Finite.dependent_image, Finset.finite_toSet
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
val : (i : K) → i ∈ (↑t : Set K) → (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
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)
                ⋯)
              ⋯) =
          y}
⊢ (Set.Icc z 1).Finite

Tactic:
refine (t.finite_toSet.dependent_image ?_).subset ?_

Premises used: Set.Finite.subset, Set.Finite.dependent_image, Finset.finite_toSet
-- 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 : Γ₀)}
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)) : Γ₀)
⊢ Membership.mem (α := Γ₀) (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) ((v : (a : K) → Γ₀) i : Γ₀)

Tactic:
simp
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
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) ⋯ :
        ↥(MonoidHom.mrange (F := Valuation K Γ₀) v))
      (0 : ↥(MonoidHom.mrange (F := Valuation K Γ₀) v))
⊢ (i : K) → i ∈ (↑t : Set K) → (↥(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⟩ ?_

Premises used: Valued.v, LE.le, dite, Subtype.mk, Units.mk0, DFunLike.coe
-- 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 : Γ₀)}
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)) : Γ₀)
⊢ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) i

Tactic:
push Not at hi'

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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
i : K
hi : i ∈ (↑t : Set K)
hi' : (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) i
⊢ 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))

Tactic:
Subtype.coe_injective.ne_iff.mp (hi'.trans' z0).ne'

Premises used: Function.Injective.ne_iff, Subtype.coe_injective, LT.lt.trans', LT.lt.ne', Iff.mp
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
i : K
hi : i ∈ (↑t : Set K)
hi' : (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) < (v : (a : K) → Γ₀) i
⊢ 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))

Tactic:
exact Subtype.coe_injective.ne_iff.mp (hi'.trans' z0).ne'

Premises used: Function.Injective.ne_iff, Subtype.coe_injective, Iff.mp
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
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)
                ⋯)
              ⋯) =
          i
⊢ 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

Tactic:
simp only [Set.mem_Icc, Finset.mem_coe, exists_prop, Set.mem_setOf_eq, and_imp]

Premises used: and_imp, Set.mem_setOf_eq, exists_prop, Set.mem_Icc, Finset.mem_coe
-- 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 : Γ₀)}
t : Finset K
ht : (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
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) ⋯)
                ⋯) =
            i
⊢ 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

Tactic:
obtain ⟨c, hc⟩ := i.val.prop

Premises used: Units.val, Subtype.prop
-- 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_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
⊢ Membership.mem (γ := Set K) (⋃ i ∈ t, U i) c

Tactic:
have hj := ht (hc.trans_le hi1)
-- 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_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
⊢ ∃ 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

Premises used: Set.mem_iUnion, exists_prop