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 Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ Eq (α := IsLocalRing.ResidueField ↥𝒪[K])
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) y :
      IsLocalRing.ResidueField ↥𝒪[K])
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → ↥𝒪[K] ⧸ IsLocalRing.maximalIdeal ↥𝒪[K]) x :
      HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) (IsLocalRing.maximalIdeal ↥𝒪[K]))
have mp : Membership.mem (γ := Ideal ↥𝒪[K]) 𝓂[K] (y - x)
Tactic: convert!
      (Ideal.Quotient.mk_eq_mk_iff_sub_mem (I := 𝓂[K]) y x).mpr
        _
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ Membership.mem (γ := Ideal ↥𝒪[K]) 𝓂[K] (y - x)
have mp : Membership.mem (γ := Set ↥𝒪[K])
  {y : ↥(Valuation.integer v) |
    LE.le.{u_2} (α := Γ₀)
      ((v : (a : K) → Γ₀) ((algebraMap (↥(Valuation.integer v)) K : (a : ↥v.integer) → K) y : K) : Γ₀)
      ((v : (a : K) → Γ₀) ((algebraMap (↥(Valuation.integer v)) K : (a : ↥v.integer) → K) p : K) : Γ₀)}
  (y - x)
Tactic: rw [Valued.maximalIdeal, hp.maximalIdeal_eq, ← SetLike.mem_coe,
      (Valuation.integer.integers _).coe_span_singleton_eq_setOf_le_v_algebraMap]
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ Membership.mem (γ := Set ↥𝒪[K])
    {y : ↥(Valuation.integer v) |
      LE.le.{u_2} (α := Γ₀)
        ((v : (a : K) → Γ₀) ((algebraMap (↥(Valuation.integer v)) K : (a : ↥v.integer) → K) y : K) : Γ₀)
        ((v : (a : K) → Γ₀) ((algebraMap (↥(Valuation.integer v)) K : (a : ↥v.integer) → K) p : K) : Γ₀)}
    (y - x)
have hy'₁ : dist y x < ‖p‖
Tactic: rw [dist_comm] at hy'
Cleared hypotheses: hy'
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
⊢ TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
have mpr : ∀ ε > 0, ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
Tactic: rw [Metric.totallyBounded_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 Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
have mpr : ∀ (p : ↥𝒪[K]) (hp : Irreducible p),
  ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
Tactic: obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
have hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
Tactic: have hp' := Valuation.integer.v_irreducible_lt_one hp
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
have mpr : ∀ (n : ℕ) (hn : ‖(↑p : K)‖ ^ n < ε),
  ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖(p : K)‖ ^ n < ε := exists_pow_lt_of_lt_one εpos
      (toNormedField.norm_lt_one_iff.mpr hp')
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
have hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
Tactic: have hF := finite_quotient_maximalIdeal_pow_of_finite_residueField H n
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
have mpr : Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ
  (⋃ (y : ↥𝒪[K]),
    ⋃ (_ :
      Membership.mem (γ := Set ↥𝒪[K])
        (Set.image (α := Quotient (Submodule.quotientRel (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))) Quotient.out Set.univ)
        y),
      Metric.ball y ε)
Tactic: refine ⟨Quotient.out '' (Set.univ (α := 𝒪[K] ⧸ (𝓂[K] ^ n))), Set.toFinite _, ?_⟩
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
⊢ Eq.{u_1 + 1} (α := Set ↥𝒪[K])
    {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n}
    (Metric.closedBall 0 (‖p‖ ^ n))
have h : ∀ (x : ↥𝒪[K]),
  Membership.mem (γ := Set ↥𝒪[K])
      {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n} x ↔
    Membership.mem (γ := Set ↥𝒪[K]) (Metric.closedBall 0 (‖p‖ ^ n)) x
Tactic: ext
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
⊢ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ
    (⋃ (y : ↥𝒪[K]),
      ⋃ (_ :
        Membership.mem (γ := Set ↥𝒪[K])
          (Set.image (α := Quotient (Submodule.quotientRel (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))) Quotient.out
            Set.univ)
          y),
        Metric.ball y ε)
have this : Eq.{u_1 + 1} (α := Set ↥𝒪[K])
  {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n}
  (Metric.closedBall 0 (‖p‖ ^ n))
Tactic: have : {y : 𝒪[K] | v (y : K) ≤ v (p : K) ^ n} = Metric.closedBall 0 (‖p‖ ^ n) := by
      ext
      simp [← norm_pow]
-- 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
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
this :
  Eq.{u_1 + 1} (α := Set ↥𝒪[K])
    {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n}
    (Metric.closedBall 0 (‖p‖ ^ n))
⊢ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ
    (⋃ (y : ↥𝒪[K]),
      ⋃ (_ :
        Membership.mem (γ := Set ↥𝒪[K])
          (Set.image (α := Quotient (Submodule.quotientRel (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))) Quotient.out
            Set.univ)
          y),
        Metric.ball y ε)
have mpr : ∀ (i : ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n),
  Metric.closedBall (Quotient.out i) (‖(↑p : K)‖ ^ n) ⊆
    ⋃ (y : Quotient (Submodule.quotientRel (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))), Metric.ball y.out ε
Tactic: simp only [Ideal.univ_eq_iUnion_image_add (𝓂[K] ^ n), hp.maximalIdeal_pow_eq_setOf_le_v_coe_pow,
      this, AddSubgroupClass.coe_norm, Set.image_univ, Set.mem_range, Set.iUnion_exists,
      Set.iUnion_iUnion_eq', Set.iUnion_subset_iff, Metric.vadd_closedBall, vadd_eq_add, add_zero]
-- 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)
⊢ Nonempty.{u_2 + 1} (LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ)
have val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
Tactic: constructor
-- 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)
⊢ LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
have val : ∀ (a b : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc a b).Finite
Tactic: refine LocallyFiniteOrder.ofFiniteIcc ?_
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ (Set.Icc x y).Finite
have inl : ∀ (hxy : y < x), (Set.Icc x y).Finite
Tactic: rcases lt_trichotomy y x with hxy | rfl | hxy
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
inl : ∀ (hxy : y < x), (Set.Icc x y).Finite
⊢ (Set.Icc x y).Finite
have inr : (Set.Icc y y).Finite
Tactic: rcases lt_trichotomy y x with hxy | rfl | hxy
Cleared hypotheses: x
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
inl : ∀ (hxy : y < x), (Set.Icc x y).Finite
inr : (Set.Icc y y).Finite
⊢ (Set.Icc x y).Finite
have inr₁ : ∀ (hxy : x < y), (Set.Icc x y).Finite
Tactic: rcases lt_trichotomy y x with hxy | rfl | hxy
-- 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)
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.Icc x y).Finite
have inl : Set.Finite.{u_2} (α := (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) ∅
Tactic: rw [Set.Icc_eq_empty_of_lt]
-- 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)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : x < y
⊢ (Set.Icc x y).Finite
have 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
Tactic: wlog! h : x ≤ 1 generalizing x y
-- 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)
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
⊢ (Set.Icc x y).Finite
have wlog! : ∀ (x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) (hxy : x < y) (h : x ≤ 1), (Set.Icc x y).Finite
Tactic: wlog! h : x ≤ 1 generalizing x y
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
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 x y).Finite
have this₁ : (Set.Icc y⁻¹ x⁻¹).Finite
Tactic: specialize this y⁻¹ x⁻¹ (inv_lt_inv' hxy) (inv_le_one_of_one_le (h.trans hxy).le)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
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
have inr : Set.Icc x y ⊆ (Set.Icc y⁻¹ x⁻¹)⁻¹
Tactic: refine (this.inv).subset ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
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 ⊆ (Set.Icc y⁻¹ x⁻¹)⁻¹
have inr : Set.Icc x y ⊆ Set.Icc x⁻¹⁻¹ y⁻¹⁻¹
Tactic: rw [Set.inv_Icc]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
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
⊢ (Set.Icc x y).Finite
have pf : MonoidHomClass (Valuation K Γ₀) K Γ₀
Tactic: generalize_proofs _ _ _ _ hxu hyu
-- 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)
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 Γ₀
⊢ (Set.Icc x y).Finite
have inl : ∀ (hy : y ≤ 1), (Set.Icc x y).Finite
Tactic: rcases le_total y 1 with hy | hy
-- 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)
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
⊢ (Set.Icc x y).Finite
have inr : ∀ (hy : 1 ≤ y), (Set.Icc x y).Finite
Tactic: rcases le_total y 1 with hy | hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
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 x y).Finite
have H : (Set.Icc y⁻¹ 1).Finite
Tactic: have H : (Set.Icc y⁻¹ 1).Finite := this _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
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
have inr : Set.Icc x y = Set.Icc x 1 ∪ (Set.Icc y⁻¹ 1)⁻¹
Tactic: refine ((this x).union H.inv).subset (le_of_eq ?_)
-- 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)
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 1 ∪ (Set.Icc y⁻¹ 1)⁻¹
have inr : Set.Icc x y = Set.Icc x y⁻¹⁻¹
Tactic: rw [Set.inv_Icc, inv_one, Set.Icc_union_Icc_eq_Icc]
-- 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)
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
⊢ Set.Icc x y = Set.Icc x 1 ∪ (Set.Icc y⁻¹ 1)⁻¹
have inr₂ : 1 ≤ y⁻¹⁻¹
Tactic: rw [Set.inv_Icc, inv_one, Set.Icc_union_Icc_eq_Icc]
-- 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)
⊢ ∀ (a b : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc a b).Finite
have val : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).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]
-- 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))ˣ
⊢ (Set.Icc z 1).Finite
have val : ∀ (a : K) (ha : (v : (a : K) → Γ₀) a = (↑(↑z : ↥(MonoidHom.mrange v)) : Γ₀)), (Set.Icc z 1).Finite
Tactic: obtain ⟨a, ha⟩ := z.val.prop
-- 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)) : Γ₀)
⊢ (Set.Icc z 1).Finite
have val : ∀ (hz1 : 1 < z), (Set.Icc z 1).Finite
Tactic: rcases lt_or_ge 1 z with hz1 | hz1
-- 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)) : Γ₀)
val : ∀ (hz1 : 1 < z), (Set.Icc z 1).Finite
⊢ (Set.Icc z 1).Finite
have val₁ : ∀ (hz1 : z ≤ 1), (Set.Icc z 1).Finite
Tactic: rcases lt_or_ge 1 z with hz1 | hz1
-- 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 : 1 < z
⊢ (Set.Icc z 1).Finite
have val : Set.Finite.{u_2} (α := (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) ∅
Tactic: rw [Set.Icc_eq_empty_of_lt]