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_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
⊢ ∃ 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 : ∀ (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) sorry)
          sorry) =
      i
Tactic: obtain ⟨j, hj, hj'⟩ := hj
Cleared hypotheses: hj
-- 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_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
⊢ ∃ 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 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) sorry)
      sorry) =
  i
Tactic: use j, hj
-- 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_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
⊢ (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
have 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) sorry)
        sorry) =
    i
Tactic: split_ifs at hj' with hcj
Cleared hypotheses: hj'
-- 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_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
⊢ (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
have 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) sorry)
        sorry) =
    i
Tactic: split_ifs at hj' with hcj
Cleared hypotheses: hj'
-- 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
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
⊢ (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
have hj'₁ : i ≤ z
Tactic: simp only [Set.mem_setOf_eq, hc, Subtype.coe_le_coe, Units.val_le_val] at hj'
Cleared hypotheses: hj'
-- 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_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 : Γ₀)
⊢ (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
have neg : Units.mk0
    (Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange (F := Valuation K Γ₀) v) x)
      ((v : (a : K) → Γ₀) j) sorry)
    sorry =
  i
Tactic: rw [dif_neg hcj]
-- 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: 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]
-- 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: 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]
-- 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)
⊢ MulArchimedean.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)
have rw : MulArchimedean.{u_2} (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
Tactic: rw [← Units.mulArchimedean_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)
⊢ MulArchimedean.{u_2} (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
have obtain : ∀ (val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ),
  MulArchimedean.{u_2} (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
Tactic: obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc
-- 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 : CompactSpace.{u_1} ↥𝒪[K]
⊢ IsPrincipalIdealRing.{u_1} ↥𝒪[K]
have hi : 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
-- 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 : CompactSpace.{u_1} ↥𝒪[K]
hi : Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]
⊢ IsPrincipalIdealRing.{u_1} ↥𝒪[K]
have hc₁ : IsCompact (↑𝒪[K] : Set K)
Tactic: have hc : IsCompact (X := K) 𝒪[K] := isCompact_iff_compactSpace.mpr hc
-- 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_1 : CompactSpace.{u_1} ↥𝒪[K]
hi : Valuation.Integers.{u_1, u_2, u_1} (R := K) v ↥𝒪[K]
hc : IsCompact (↑𝒪[K] : Set K)
⊢ IsPrincipalIdealRing.{u_1} ↥𝒪[K]
have obtain : ∀ (val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), IsPrincipalIdealRing.{u_1} ↥𝒪[K]
Tactic: obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc
-- 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 : 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))ˣ
⊢ IsPrincipalIdealRing.{u_1} ↥𝒪[K]
have hm : MulArchimedean.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v)
Tactic: have hm := mulArchimedean_mrange_of_isCompact_integer hc
-- 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_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]
have refine : DenselyOrdered.{u_2} ↥(MonoidHom.mrange (F := Valuation K Γ₀) v) → False
Tactic: refine hi.isPrincipalIdealRing_iff_not_denselyOrdered_mrange.mpr fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
Goal:
K : Type u_3
Γ : Type u_4
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.IsNontrivial ↔ Ne.{u_3 + 1} (α := Ideal ↥v.integer) (IsLocalRing.maximalIdeal ↥v.integer) ⊥
have 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
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]
-- 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 Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
⊢ CompactSpace.{u_1} ↥𝒪[K] ↔ CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
have refine_1 : ∀ (h : CompactSpace.{u_1} ↥𝒪[K]),
  CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
Tactic: refine ⟨fun h ↦ ?_, fun ⟨_, _, h⟩ ↦ ⟨?_⟩⟩
-- 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 Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
refine_1 :
  ∀ (h : CompactSpace.{u_1} ↥𝒪[K]),
    CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
⊢ CompactSpace.{u_1} ↥𝒪[K] ↔ CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
have refine_2 : CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K] →
  CompleteSpace.{u_1} ↥𝒪[K] →
    IsDiscreteValuationRing.{u_1} ↥𝒪[K] → ∀ (h : Finite.{u_1 + 1} 𝓀[K]), IsCompact.{u_1} (X := ↥𝒪[K]) Set.univ
Tactic: refine ⟨fun h ↦ ?_, fun ⟨_, _, h⟩ ↦ ⟨?_⟩⟩
-- 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 Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : CompactSpace.{u_1} ↥𝒪[K]
⊢ CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
have this : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
Tactic: have : IsDiscreteValuationRing 𝒪[K] := isDiscreteValuationRing_of_compactSpace
-- 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 Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : CompactSpace.{u_1} ↥𝒪[K]
this : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
⊢ CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
have refine_1 : Finite.{u_1 + 1} 𝓀[K]
Tactic: refine ⟨complete_of_compact, by assumption, ?_⟩
-- 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 Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h : CompactSpace.{u_1} ↥𝒪[K]
this : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
⊢ Finite.{u_1 + 1} 𝓀[K]
have h₁ : Finite.{u_1 + 1} 𝓀[K] ∧ IsComplete.{u_1} (α := ↥𝒪[K]) Set.univ
Tactic: rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete,
        totallyBounded_iff_finite_residueField] at h
Cleared hypotheses: h, this
-- 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 Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
h_1 : CompleteSpace.{u_1} ↥𝒪[K] ∧ IsDiscreteValuationRing.{u_1} ↥𝒪[K] ∧ Finite.{u_1 + 1} 𝓀[K]
left : CompleteSpace.{u_1} ↥𝒪[K]
left_1 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
⊢ IsCompact.{u_1} (X := ↥𝒪[K]) Set.univ
have h₁ : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
Tactic: rw [← totallyBounded_iff_finite_residueField] at h
Cleared hypotheses: h