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_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 :
  ∃ 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
val :
  ∀ (j : K) (hj : j ∈ t)
    (hj' :
      Membership.mem (γ := Set K)
        (if (v : (a : K) → Γ₀) j ≤ (↑(↑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) → Γ₀) j : Γ₀)})
        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
⊢ ∃ 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 ⟨j, hj, hj'⟩ := hj
-- 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
j : K
hj : j ∈ t
hj' :
  Membership.mem (γ := Set K)
    (if (v : (a : K) → Γ₀) j ≤ (↑(↑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) → Γ₀) j : Γ₀)})
    c
right :
  (if hi' : (v : (a : K) → Γ₀) j ≤ (↑(↑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) → Γ₀) j) ⋯)
        ⋯) =
    i
⊢ ∃ 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:
use j, hj
-- 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
j : K
hj : j ∈ t
hj' :
  Membership.mem (γ := Set K)
    (if (v : (a : K) → Γ₀) j ≤ (↑(↑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) → Γ₀) j : Γ₀)})
    c
pos :
  ∀ (hcj : (v : (a : K) → Γ₀) j ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀))
    (hj' : Membership.mem (γ := Set K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)} c),
    (if hi' : (v : (a : K) → Γ₀) j ≤ (↑(↑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) → Γ₀) j) ⋯)
          ⋯) =
      i
neg :
  ∀ (hcj : ¬(v : (a : K) → Γ₀) j ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀))
    (hj' :
      Membership.mem (γ := Set K)
        {w : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w : Γ₀) ((v : (a : K) → Γ₀) j : Γ₀)} c),
    (if hi' : (v : (a : K) → Γ₀) j ≤ (↑(↑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) → Γ₀) j) ⋯)
          ⋯) =
      i
⊢ (if hi' : (v : (a : K) → Γ₀) j ≤ (↑(↑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) → Γ₀) j) ⋯)
        ⋯) =
    i

Tactic:
split_ifs at hj' with hcj
-- 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
j : K
hj : j ∈ t
hcj : (v : (a : K) → Γ₀) j ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hj' : Membership.mem (γ := Set K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)} c
⊢ i ≤ z

Tactic:
simp only [Set.mem_setOf_eq, hc, Subtype.coe_le_coe, Units.val_le_val] at hj'

Premises used: Subtype.coe_le_coe, Units.val_le_val, Set.mem_setOf_eq
-- 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
j : K
hj : j ∈ t
hcj : (v : (a : K) → Γ₀) j ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hj' : i ≤ z
⊢ (if hi' : (v : (a : K) → Γ₀) j ≤ (↑(↑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) → Γ₀) j) ⋯)
        ⋯) =
    i

Tactic:
simp [hcj, le_antisymm hj' hzi]

Premises used: le_antisymm
-- 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
j : K
hj : j ∈ t
hcj : ¬(v : (a : K) → Γ₀) j ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hj' : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) c : Γ₀) ((v : (a : K) → Γ₀) j : Γ₀)
neg :
  Units.mk0
      (Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x)
        ((v : (a : K) → Γ₀) j) ⋯)
      ⋯ =
    i
⊢ (if hi' : (v : (a : K) → Γ₀) j ≤ (↑(↑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) → Γ₀) j) ⋯)
        ⋯) =
    i

Tactic:
rw [dif_neg hcj]

Premises used: dif_neg
-- 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
j : K
hj : j ∈ t
hcj : ¬(v : (a : K) → Γ₀) j ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
hj' : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) c : Γ₀) ((v : (a : K) → Γ₀) j : Γ₀)
⊢ Units.mk0
      (Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x)
        ((v : (a : K) → Γ₀) j) ⋯)
      ⋯ =
    i

Tactic:
simp [← hj', hc]
-- 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₁ 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:
classical
  refine (t.finite_toSet.dependent_image ?_).subset ?_
  · refine fun i hi ↦ if hi' : v i ≤ z then z else Units.mk0 ⟨(v i), by simp⟩ ?_
    push Not at hi'
    exact Subtype.coe_injective.ne_iff.mp (hi'.trans' z0).ne'
  · intro i
    simp only [Set.mem_Icc, Finset.mem_coe, exists_prop, Set.mem_setOf_eq, and_imp]
    -- we get the `c` from the cover that covers our arbitrary `i` with its set
    obtain ⟨c, hc⟩ := i.val.prop
    intro hzi hi1
    have hj := ht (hc.trans_le hi1)
    simp only [Set.mem_iUnion, exists_prop, U] at hj
    obtain ⟨j, hj, hj'⟩ := hj
    use j, hj
    -- and this `c` is either less than or greater than (or equal to) the threshold element
    split_ifs at hj' with hcj
    · simp only [Set.mem_setOf_eq, hc, Subtype.coe_le_coe, Units.val_le_val] at hj'
      simp [hcj, le_antisymm hj' hzi]
    · simp only [Set.mem_setOf_eq] at hj'
      rw [dif_neg hcj]
      simp [← hj', hc]

Premises used: and_imp, Valued.v, Set.mem_iUnion, Subtype.coe_le_coe, Units.val_le_val, Set.Finite.subset, Set.mem_setOf_eq, Set.Finite.dependent_image, LE.le, exists_prop, dite, Subtype.mk, Units.mk0, Set.mem_Icc, Finset.finite_toSet, DFunLike.coe, Finset.mem_coe, 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)
rw : MulArchimedean.{u_2} (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ MulArchimedean.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)

Tactic:
rw [← Units.mulArchimedean_iff]

Premises used: Units.mulArchimedean_iff
-- 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)
obtain :
  ∀ (val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ),
    MulArchimedean.{u_2} (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ MulArchimedean.{u_2} (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ

Tactic:
obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc

Premises used: Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer
-- 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)
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ MulArchimedean.{u_2} (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ

Tactic:
MulArchimedean.of_locallyFiniteOrder

Premises used: MulArchimedean.of_locallyFiniteOrder
-- 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)
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ MulArchimedean.{u_2} (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ

Tactic:
exact MulArchimedean.of_locallyFiniteOrder

Premises used: MulArchimedean.of_locallyFiniteOrder
-- 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 : CompactSpace.{u_1} ↥𝒪[K]
⊢ Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]

Tactic:
have hi : Valuation.Integers (R := K) Valued.v 𝒪[K] := Valuation.integer.integers 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 : CompactSpace.{u_1} ↥𝒪[K]
hi : Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]
⊢ IsCompact (↑𝒪[K] : Set K)

Tactic:
have hc : IsCompact (X := K) 𝒪[K] := isCompact_iff_compactSpace.mpr hc
-- 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 : CompactSpace.{u_1} ↥𝒪[K]
hi : Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]
hc : IsCompact (↑𝒪[K] : Set K)
obtain : ∀ (val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), IsPrincipalIdealRing.{u_1} ↥𝒪[K]
⊢ IsPrincipalIdealRing.{u_1} ↥𝒪[K]

Tactic:
obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc

Premises used: Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer
-- 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 : CompactSpace.{u_1} ↥𝒪[K]
hi : Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]
hc : IsCompact (↑𝒪[K] : Set K)
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ MulArchimedean.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)

Tactic:
have hm := mulArchimedean_mrange_of_isCompact_integer hc
-- 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 : CompactSpace.{u_1} ↥𝒪[K]
hi : Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]
hc : IsCompact (↑𝒪[K] : Set K)
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hm : MulArchimedean.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)
⊢ IsPrincipalIdealRing.{u_1} ↥𝒪[K]

Tactic:
hi.isPrincipalIdealRing_iff_not_denselyOrdered_mrange.mpr fun _ ↦ ?_

Premises used: Iff.mpr, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange
-- 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 : CompactSpace.{u_1} ↥𝒪[K]
hi : Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]
hc : IsCompact (↑𝒪[K] : Set K)
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hm : MulArchimedean.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)
refine : DenselyOrdered.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v) → False
⊢ IsPrincipalIdealRing.{u_1} ↥𝒪[K]

Tactic:
refine hi.isPrincipalIdealRing_iff_not_denselyOrdered_mrange.mpr fun _ ↦ ?_

Premises used: Iff.mpr, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange
-- 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 : CompactSpace.{u_1} ↥𝒪[K]
hi : Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]
hc : IsCompact (↑𝒪[K] : Set K)
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hm : MulArchimedean.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)
h : DenselyOrdered.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)
⊢ False

Tactic:
not_subsingleton (MonoidHom.mrange (v : Valuation K Γ₀))ˣ
    (LocallyFiniteOrder.denselyOrdered_iff_subsingleton.mp inferInstance)

Premises used: Valued.v, Membership.mem, Units, inferInstance, Subtype, not_subsingleton, Iff.mp, MonoidHom.mrange, LocallyFiniteOrder.denselyOrdered_iff_subsingleton
-- 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 : CompactSpace.{u_1} ↥𝒪[K]
hi : Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]
hc : IsCompact (↑𝒪[K] : Set K)
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hm : MulArchimedean.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)
h : DenselyOrdered.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)
⊢ False

Tactic:
exact not_subsingleton (MonoidHom.mrange (v : Valuation K Γ₀))ˣ
    (LocallyFiniteOrder.denselyOrdered_iff_subsingleton.mp inferInstance)

Premises used: Valued.v, Membership.mem, Units, inferInstance, Subtype, not_subsingleton, Iff.mp, MonoidHom.mrange, LocallyFiniteOrder.denselyOrdered_iff_subsingleton
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_3
Γ : Type u_4
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
simp_rw :
  (∃ (x : K), x ≠ 0 ∧ LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)) ↔
    ∃ (x : ↥v.integer), LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) (↑x : K) : Γ) (1 : Γ) ∧ ¬x = 0
⊢ v.IsNontrivial ↔ Ne.{u_3 + 1} (α := Ideal ↥v.integer) (IsLocalRing.maximalIdeal ↥v.integer) ⊥

Tactic:
simp_rw [ne_eq, eq_bot_iff, v.isNontrivial_iff_exists_lt_one, SetLike.le_def, Ideal.mem_bot,
    not_forall, exists_prop, IsLocalRing.notMem_maximalIdeal.not_right,
    Valuation.Integer.not_isUnit_iff_valuation_lt_one]

Premises used: Ideal.mem_bot, Valuation.isNontrivial_iff_exists_lt_one, SetLike.le_def, exists_prop, ne_eq, Iff.not_right, Valuation.Integer.not_isUnit_iff_valuation_lt_one, IsLocalRing.notMem_maximalIdeal, eq_bot_iff, Classical.not_forall
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_3
Γ : Type u_4
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
h : ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)
x : K
hx0 : x ≠ 0
hx1 : LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)
⊢ LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) x ⋯) : K) : Γ) (1 : Γ) ∧
    ¬Eq (α := ↥v.integer) (Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) x ⋯) 0

Tactic:
simp [Subtype.ext_iff, *]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_3
Γ : Type u_4
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
h : ∃ (x : ↥v.integer), LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) (↑x : K) : Γ) (1 : Γ) ∧ ¬x = 0
x : ↥v.integer
hx1 : LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) (↑x : K) : Γ) (1 : Γ)
hx0 : ¬x = 0
⊢ (↑x : K) ≠ 0 ∧ LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) (↑x : K) : Γ) (1 : Γ)

Tactic:
simp [*]
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_3
Γ : Type u_4
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ (∃ (x : K), x ≠ 0 ∧ LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)) ↔
    ∃ (x : ↥v.integer), LT.lt.{u_4} (α := Γ) ((v : (a : K) → Γ) (↑x : K) : Γ) (1 : Γ) ∧ ¬x = 0

Tactic:
exact ⟨fun ⟨x, hx0, hx1⟩ ↦ ⟨⟨x, hx1.le⟩, by simp [Subtype.ext_iff, *]⟩,
  fun ⟨x, hx1, hx0⟩ ↦ ⟨x, by simp [*]⟩⟩