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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : y < x
⊢ Set.Finite.{u_2} (α := (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) ∅

Tactic:
exact Set.finite_empty

Premises used: Set.finite_empty
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : y < x
⊢ y < x

Tactic:
simp [hxy]
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ (Set.Icc y y).Finite

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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
inr :
  ∀ (this : ∀ (x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) (hxy : x < y) (h : x ≤ 1), (Set.Icc x y).Finite)
    (h : 1 < x), (Set.Icc x y).Finite
wlog! : ∀ (x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) (hxy : x < y) (h : x ≤ 1), (Set.Icc x y).Finite
⊢ (Set.Icc x y).Finite

Tactic:
wlog! h : x ≤ 1 generalizing x y
-- 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)
this_1 : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
this : ∀ (x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) (hxy : x < y) (h : x ≤ 1), (Set.Icc x y).Finite
h : 1 < x
⊢ (Set.Icc y⁻¹ x⁻¹).Finite

Tactic:
specialize this y⁻¹ x⁻¹ (inv_lt_inv' hxy) (inv_le_one_of_one_le (h.trans hxy).le)

Premises used: LT.lt.le, inv_le_one_of_one_le, inv_lt_inv', Inv.inv, LT.lt.trans
-- 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)
this_1 : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : 1 < x
this : (Set.Icc y⁻¹ x⁻¹).Finite
⊢ (Set.Icc x y).Finite

Tactic:
(this.inv).subset ?_

Premises used: Set.Finite.subset, Set.Finite.inv
-- 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)
this_1 : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : 1 < x
this : (Set.Icc y⁻¹ x⁻¹).Finite
inr : Set.Icc x y ⊆ (Set.Icc y⁻¹ x⁻¹)⁻¹
⊢ (Set.Icc x y).Finite

Tactic:
refine (this.inv).subset ?_

Premises used: Set.Finite.subset, Set.Finite.inv
-- 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)
this_1 : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : 1 < x
this : (Set.Icc y⁻¹ x⁻¹).Finite
inr : Set.Icc x y ⊆ Set.Icc x⁻¹⁻¹ y⁻¹⁻¹
⊢ Set.Icc x y ⊆ (Set.Icc y⁻¹ x⁻¹)⁻¹

Tactic:
rw [Set.inv_Icc]

Premises used: Set.inv_Icc
-- 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)
this_1 : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : 1 < x
this : (Set.Icc y⁻¹ x⁻¹).Finite
a : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ a ∈ Set.Icc x y → a ∈ Set.Icc x⁻¹⁻¹ y⁻¹⁻¹

Tactic:
simp +contextual
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
⊢ MonoidHomClass (Valuation K Γ₀) K Γ₀

Tactic:
generalize_proofs _ _ _ _ hxu hyu
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
⊢ MonoidHomClass (Valuation K Γ₀) K Γ₀

Tactic:
generalize_proofs _ _ _ _ hxu hyu
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
inl : ∀ (hy : y ≤ 1), (Set.Icc x y).Finite
inr : ∀ (hy : 1 ≤ y), (Set.Icc x y).Finite
⊢ (Set.Icc x y).Finite

Tactic:
rcases le_total y 1 with hy | hy

Premises used: le_total, OfNat.ofNat
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
hy : y ≤ 1
⊢ (Set.Icc x y).Finite

Tactic:
(this x).subset (Set.Icc_subset_Icc_right hy)

Premises used: Set.Mem, Set.Icc_subset_Icc_right, Set.Finite.subset
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
hy : y ≤ 1
⊢ (Set.Icc x y).Finite

Tactic:
exact (this x).subset (Set.Icc_subset_Icc_right hy)

Premises used: Set.Icc_subset_Icc_right, Set.Finite.subset
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
hy : 1 ≤ y
⊢ (Set.Icc y⁻¹ 1).Finite

Tactic:
have H : (Set.Icc y⁻¹ 1).Finite := 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ (Set.Icc x y).Finite

Tactic:
((this x).union H.inv).subset (le_of_eq ?_)

Premises used: Set.Finite.union, Set.Mem, Set.Finite.subset, Set.Finite.inv, le_of_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 : IsCompact (↑𝒪[K] : Set K)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
inr : Set.Icc x y = Set.Icc x 1 ∪ (Set.Icc y⁻¹ 1)⁻¹
⊢ (Set.Icc x y).Finite

Tactic:
refine ((this x).union H.inv).subset (le_of_eq ?_)

Premises used: Set.Finite.union, Set.Finite.subset, Set.Finite.inv, le_of_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 : IsCompact (↑𝒪[K] : Set K)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
inr : Set.Icc x y = Set.Icc x y⁻¹⁻¹
inr₁ : x ≤ 1
inr₂ : 1 ≤ y⁻¹⁻¹
⊢ Set.Icc x y = Set.Icc x 1 ∪ (Set.Icc y⁻¹ 1)⁻¹

Tactic:
rw [Set.inv_Icc, inv_one, Set.Icc_union_Icc_eq_Icc]

Premises used: Set.Icc_union_Icc_eq_Icc, inv_one, Set.inv_Icc
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ Set.Icc x y = Set.Icc x y⁻¹⁻¹

Tactic:
simp [h, hy]
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ x ≤ 1

Tactic:
simp [h, hy]
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
h : x ≤ 1
pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
pf_1 : MonoidHomClass (Valuation K Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ 1 ≤ y⁻¹⁻¹

Tactic:
simp [h, hy]
-- 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 : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
⊢ ∀ (a b : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc a b).Finite

Tactic:
suffices ∀ z : (MonoidHom.mrange (Valued.v : Valuation K Γ₀))ˣ, (Set.Icc z 1).Finite by
    rintro x y
    rcases lt_trichotomy y x with hxy | rfl | hxy
    · rw [Set.Icc_eq_empty_of_lt]
      · exact Set.finite_empty
      · simp [hxy]
    · simp
    wlog! h : x ≤ 1 generalizing x y
    · specialize this y⁻¹ x⁻¹ (inv_lt_inv' hxy) (inv_le_one_of_one_le (h.trans hxy).le)
      refine (this.inv).subset ?_
      rw [Set.inv_Icc]
      intro
      simp +contextual
    generalize_proofs _ _ _ _ hxu hyu
    rcases le_total y 1 with hy | hy
    · exact (this x).subset (Set.Icc_subset_Icc_right hy)
    · have H : (Set.Icc y⁻¹ 1).Finite := this _
      refine ((this x).union H.inv).subset (le_of_eq ?_)
      rw [Set.inv_Icc, inv_one, Set.Icc_union_Icc_eq_Icc] <;>
      simp [h, hy]
-- 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))ˣ
val : ∀ (a : K) (ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)), (Set.Icc z 1).Finite
⊢ (Set.Icc z 1).Finite

Tactic:
obtain ⟨a, ha⟩ := z.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 : IsCompact (↑𝒪[K] : Set K)
z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
a : K
ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
val : ∀ (hz1 : 1 < z), (Set.Icc z 1).Finite
val₁ : ∀ (hz1 : z ≤ 1), (Set.Icc z 1).Finite
⊢ (Set.Icc z 1).Finite

Tactic:
rcases lt_or_ge 1 z with hz1 | hz1

Premises used: lt_or_ge, OfNat.ofNat
-- 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 : 1 < z
val : Set.Finite.{u_2} (α := (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) ∅
val₁ : 1 < z
⊢ (Set.Icc z 1).Finite

Tactic:
rw [Set.Icc_eq_empty_of_lt]

Premises used: Set.Icc_eq_empty_of_lt
-- 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 : 1 < z
⊢ Set.Finite.{u_2} (α := (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) ∅

Tactic:
Set.finite_empty

Premises used: Set.finite_empty
-- 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 : 1 < z
⊢ Set.Finite.{u_2} (α := (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) ∅

Tactic:
exact Set.finite_empty

Premises used: Set.finite_empty
-- 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 : 1 < z
⊢ 1 < z

Tactic:
simp [hz1]
-- 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
⊢ 0 < (↑z : ↥(MonoidHom.mrange v))

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
⊢ 0 < (↑z : ↥(MonoidHom.mrange v))

Tactic:
have z0' : 0 < (z : MonoidHom.mrange (Valued.v : Valuation K Γ₀)) := by 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))
⊢ 0 < (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)

Tactic:
have z0 : 0 < ((z : MonoidHom.mrange (Valued.v : Valuation K Γ₀)) : Γ₀) :=
    Subtype.coe_lt_coe.mpr z0'
-- 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)) : Γ₀)
⊢ LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)

Tactic:
simp [ha, z0]
-- 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)) : Γ₀)
⊢ LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) a : Γ₀)

Tactic:
have a0 : 0 < v a := by simp [ha, z0]
-- 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 : Γ₀)}
⊢ ∀ (hUo : ∀ (i : K), IsOpen (U i)) (hsU : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i),
    ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i

Tactic:
have := hc.elim_finite_subcover U
-- 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
val : ∀ (i : K), IsOpen (U i)
val₁ : (↑𝒪[K] : Set K) ⊆ ⋃ (i : K), U i
val₂ : ∀ (this : ∃ (t : Finset K), (↑𝒪[K] : Set K) ⊆ ⋃ i ∈ t, U i), (Set.Icc z 1).Finite
⊢ (Set.Icc z 1).Finite

Tactic:
specialize 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 : Γ₀)}
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
val :
  IsOpen.{u_1} (X := K)
    (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w_1 : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w_1 : Γ₀) ((v : (a : K) → Γ₀) w : Γ₀)})
⊢ IsOpen (U w)

Tactic:
simp only [U]
-- 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
pos :
  ∀ (hw : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)),
    IsOpen.{u_1} (X := K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
neg :
  ∀ (hw : ¬(v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)),
    IsOpen.{u_1} (X := K) {w_1 : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w_1 : Γ₀) ((v : (a : K) → Γ₀) w : Γ₀)}
⊢ IsOpen.{u_1} (X := K)
    (if (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀) then
      {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
    else {w_1 : K | Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) w_1 : Γ₀) ((v : (a : K) → Γ₀) w : Γ₀)})

Tactic:
split_ifs with hw
-- 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 : (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)
pos :
  ∀ (b : K) (hb : (v : (a : K) → Γ₀) b = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)),
    IsOpen.{u_1} (X := K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}
⊢ IsOpen.{u_1} (X := K) {w : K | (v : (a : K) → Γ₀) w ≤ (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)}

Tactic:
obtain ⟨b, hb⟩ := MonoidHom.mem_mrange.mp z.1.2

Premises used: Units.val, Iff.mp, Subtype.property, MonoidHom.mem_mrange