awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := ⋯
s : Set K
hs : Membership.mem (γ := Filter K) (nhds 0) s
hs' : IsCompact s
r : ValueGroupWithZero K
hr_1 : r ≠ 0
hrs : {x : K | (valuation K : (a : K) → ValueGroupWithZero K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
hr1 : 1 ≤ r
x : K
hx :
  LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
⊢ (valuation K : (a : K) → ValueGroupWithZero K) x < r

Tactic:
hx.trans_lt (hr.trans_le hr1)

Premises used: LT.lt.trans_le, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := ⋯
s : Set K
hs : Membership.mem (γ := Filter K) (nhds 0) s
hs' : IsCompact s
r : ValueGroupWithZero K
hr_1 : r ≠ 0
hrs : {x : K | (valuation K : (a : K) → ValueGroupWithZero K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
hr1 : 1 ≤ r
x : K
hx :
  LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
⊢ (valuation K : (a : K) → ValueGroupWithZero K) x < r

Tactic:
exact hx.trans_lt (hr.trans_le hr1)

Premises used: LT.lt.trans_le, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := ⋯
s : Set K
hs : Membership.mem (γ := Filter K) (nhds 0) s
hs' : IsCompact s
neg :
  ∀ (r : K) (hr : r ≠ 0)
    (hr1 :
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
        (1 : ValueGroupWithZero K))
    (H :
      {x : K |
          LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
            ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
        s),
    IsCompact.{u_1} (X := K)
      {x : K |
        LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
          ((valuation K : (a : K) → ValueGroupWithZero K) γ : ValueGroupWithZero K)}
⊢ IsCompact.{u_1} (X := K)
    {x : K |
      LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) γ : ValueGroupWithZero K)}

Tactic:
obtain ⟨r, hr, hr1, H⟩ :
      ∃ r', r' ≠ 0 ∧ valuation K r' < 1 ∧ { x | valuation K x ≤ valuation K r' } ⊆ s := by
    obtain ⟨r, hr, hrs⟩ := (IsValuativeTopology.hasBasis_nhds_zero' K).mem_iff.mp hs
    obtain ⟨r', hr', hr⟩ := Valuation.IsNontrivial.exists_lt_one (v := valuation K)
    simp only [ne_eq] at hr'
    obtain hr1 | hr1 := lt_or_ge r 1
    · obtain ⟨r, rfl⟩ := ValuativeRel.valuation_surjective r
      simp only [ne_eq, map_eq_zero] at hr
      refine ⟨r ^ 2, by simpa using hr, by simpa [pow_two], fun x hx ↦ hrs ?_⟩
      simp only [map_pow, Set.mem_setOf_eq] at hx ⊢
      exact hx.trans_lt (by simpa [pow_two, hr])
    · refine ⟨r', hr', hr, .trans ?_ hrs⟩
      intro x hx
      dsimp at hx ⊢
      exact hx.trans_lt (hr.trans_le hr1)
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := ⋯
s : Set K
hs : Membership.mem (γ := Filter K) (nhds 0) s
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
H :
  {x : K |
      LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
    s
neg :
  ∀
    (H :
      {x : K |
          LE.le (α :=
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
              (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            ((Valuation.restrict (valuation K) :
                  (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
                x :
              MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
                (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            ((Valuation.restrict (valuation K) :
                  (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
                r :
              MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
                (↑(valuation K) : K →*₀ ValueGroupWithZero K))} ⊆
        s),
    IsCompact.{u_1} (X := K)
      {x : K |
        LE.le (α :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
          ((Valuation.restrict (valuation K) :
                (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
              x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
              (↑(valuation K) : K →*₀ ValueGroupWithZero K))
          ((Valuation.restrict (valuation K) :
                (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
              γ :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
              (↑(valuation K) : K →*₀ ValueGroupWithZero K))}
⊢ IsCompact.{u_1} (X := K)
    {x : K |
      LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) γ : ValueGroupWithZero K)}

Tactic:
simp_rw [← (valuation K).restrict_le_iff] at H ⊢

Premises used: Valuation.restrict_le_iff, ValuativeRel.valuation
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := ⋯
s : Set K
hs : Membership.mem (γ := Filter K) (nhds 0) s
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
H :
  {x : K |
      LE.le (α :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            r :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
            (↑(valuation K) : K →*₀ ValueGroupWithZero K))} ⊆
    s
⊢ γ / r ≠ 0

Tactic:
simp [hr, div_eq_zero_iff, hγ]

Premises used: div_eq_zero_iff
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := ⋯
s : Set K
hs : Membership.mem (γ := Filter K) (nhds 0) s
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
H :
  {x : K |
      LE.le (α :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            r :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
            (↑(valuation K) : K →*₀ ValueGroupWithZero K))} ⊆
    s
⊢ Eq (α := Set K)
    {x : K |
      LE.le (α :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            γ :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
            (↑(valuation K) : K →*₀ ValueGroupWithZero K))}
    (Set.image (α := K) (⇑(Homeomorph.mulLeft₀ (γ / r) ⋯) : (a : K) → K)
      {x : K |
        LE.le (α :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
          ((Valuation.restrict Valued.v :
                (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K →*₀ ValueGroupWithZero K))
              x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
          ((Valuation.restrict (valuation K) :
                (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
              r :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
              (↑(valuation K) : K →*₀ ValueGroupWithZero K))})

Tactic:
.trans ?_ (Equiv.image_eq_preimage_symm _ _).symm

Premises used: Equiv.image_eq_preimage_symm, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := ⋯
s : Set K
hs : Membership.mem (γ := Filter K) (nhds 0) s
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
H :
  {x : K |
      LE.le (α :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            r :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
            (↑(valuation K) : K →*₀ ValueGroupWithZero K))} ⊆
    s
x : K
⊢ LT.lt (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
    (0 : MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))
    ((Valuation.restrict Valued.v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K →*₀ ValueGroupWithZero K))
        γ :
      MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑Valued.v : K →*₀ ValueGroupWithZero K))

Tactic:
simp [hγ]
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := ⋯
s : Set K
hs : Membership.mem (γ := Filter K) (nhds 0) s
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
H :
  {x : K |
      LE.le (α :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K) (↑(valuation K) : K →*₀ ValueGroupWithZero K))
        ((Valuation.restrict (valuation K) :
              (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑(valuation K) : K →*₀ ValueGroupWithZero K))
            r :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ ValueGroupWithZero K)
            (↑(valuation K) : K →*₀ ValueGroupWithZero K))} ⊆
    s
x : K
⊢ LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
      ((valuation K : (a : K) → ValueGroupWithZero K) γ : ValueGroupWithZero K) ↔
    LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) (r * x) : ValueGroupWithZero K)
      ((valuation K : (a : K) → ValueGroupWithZero K) (r * γ) : ValueGroupWithZero K)

Tactic:
simp [hr]
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
⊢ CompactSpace.{u_1} ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))

Tactic:
isCompact_iff_compactSpace.mp (isCompact_closedBall K 1)

Premises used: isCompact_iff_compactSpace, IsNonarchimedeanLocalField.isCompact_closedBall, Iff.mp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K_1 : Type u_1
inst : Field K_1
inst_1 : ValuativeRel K_1
inst_2 : TopologicalSpace K_1
inst_3 : IsNonarchimedeanLocalField K_1
K : Type u_2
inst_4 : Field K
inst_5 : ValuativeRel K
inst_6 : UniformSpace K
inst_7 : IsUniformAddGroup K
inst_8 : IsValuativeTopology K
⊢ Valuation.Compatible (R := K) Valued.v

Tactic:
inferInstanceAs (valuation K).Compatible

Premises used: _private.0.IsNonarchimedeanLocalField.instCompatibleValueGroupWithZeroV._proof_1
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
⊢ IsDiscreteValuationRing.{u_1} ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))

Tactic:
letI := IsTopologicalAddGroup.rightUniformSpace K
  haveI := isUniformAddGroup_of_addCommGroup (G := K)
  haveI : CompactSpace (Valued.integer K) := inferInstanceAs (CompactSpace 𝒪[K])
  Valued.integer.isDiscreteValuationRing_of_compactSpace

Premises used: Set.Mem, setOf, Valued.integer.isDiscreteValuationRing_of_compactSpace
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
h : Nonempty.{u_1 + 1} (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))
⊢ ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ)

Tactic:
apply Nonempty.some

Premises used: Nonempty.some
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K
h :
  ∀ (val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) Valued.v))ˣ),
    Nonempty.{u_1 + 1} (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))
⊢ Nonempty.{u_1 + 1} (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨_⟩ := Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer
    (isCompact_iff_compactSpace.mpr (inferInstance : CompactSpace 𝒪[K]))

Premises used: Iff.mpr, isCompact_iff_compactSpace, inferInstance, Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) Valued.v))ˣ
e : ↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)) ≃*o ValueGroupWithZero K :=
  {
    toMulEquiv :=
      MulEquiv.ofBijective (F :=
        ↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)) →* ValueGroupWithZero K)
        (Submonoid.subtype (MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K))) ⋯,
    map_le_map_iff' := ⋯ }
⊢ Nontrivial.{u_1} (ValueGroupWithZero K)ˣ

Tactic:
have : Nontrivial (ValueGroupWithZero K)ˣ := isNontrivial_iff_nontrivial_units.mp inferInstance
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this_2 : IsUniformAddGroup K
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) Valued.v))ˣ
e : ↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)) ≃*o ValueGroupWithZero K :=
  {
    toMulEquiv :=
      MulEquiv.ofBijective (F :=
        ↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)) →* ValueGroupWithZero K)
        (Submonoid.subtype (MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K))) ⋯,
    map_le_map_iff' := ⋯ }
this : Nontrivial.{u_1} (ValueGroupWithZero K)ˣ
⊢ Nontrivial.{u_1} (↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)))ˣ

Tactic:
have : Nontrivial (↥(MonoidHom.mrange (valuation K)))ˣ :=
    (Units.map_injective (f := e.symm.toMonoidHom) e.symm.injective).nontrivial
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this_2 : IsUniformAddGroup K
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) Valued.v))ˣ
e : ↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)) ≃*o ValueGroupWithZero K :=
  {
    toMulEquiv :=
      MulEquiv.ofBijective (F :=
        ↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)) →* ValueGroupWithZero K)
        (Submonoid.subtype (MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K))) ⋯,
    map_le_map_iff' := ⋯ }
this_3 : Nontrivial.{u_1} (ValueGroupWithZero K)ˣ
this : Nontrivial.{u_1} (↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)))ˣ
⊢ Nonempty.{u_1 + 1} (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))

Tactic:
⟨e.symm.trans (LocallyFiniteOrder.orderMonoidWithZeroEquiv _)⟩

Premises used: LocallyFiniteOrder.orderMonoidWithZeroEquiv, Nonempty.intro, OrderMonoidIso.symm, OrderMonoidIso.trans
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
this_1 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this_2 : IsUniformAddGroup K
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) Valued.v))ˣ
e : ↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)) ≃*o ValueGroupWithZero K :=
  {
    toMulEquiv :=
      MulEquiv.ofBijective (F :=
        ↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)) →* ValueGroupWithZero K)
        (Submonoid.subtype (MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K))) ⋯,
    map_le_map_iff' := ⋯ }
this_3 : Nontrivial.{u_1} (ValueGroupWithZero K)ˣ
this : Nontrivial.{u_1} (↥(MonoidHom.mrange (F := Valuation K (ValueGroupWithZero K)) (valuation K)))ˣ
⊢ Nonempty.{u_1 + 1} (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))

Tactic:
exact ⟨e.symm.trans (LocallyFiniteOrder.orderMonoidWithZeroEquiv _)⟩
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
⊢ IsCyclic.{u_1} (ValueGroupWithZero K)ˣ

Tactic:
(Units.mapEquiv (valueGroupWithZeroIsoInt K).toMulEquiv).isCyclic.mpr inferInstance

Premises used: Iff.mpr, inferInstance, Units.mapEquiv, OrderMonoidIso.toMulEquiv, IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt, MulEquiv.isCyclic
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
⊢ ValuativeRel.IsDiscrete K

Tactic:
(ValuativeRel.nonempty_orderIso_withZeroMul_int_iff.mp ⟨valueGroupWithZeroIsoInt K⟩).1

Premises used: ValuativeRel.nonempty_orderIso_withZeroMul_int_iff, Nonempty.intro, And.left, Iff.mp, IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
⊢ IsRankLeOne K

Tactic:
ValuativeRel.isRankLeOne_iff_mulArchimedean.mpr
    (.comap (valueGroupWithZeroIsoInt K).toMonoidHom (valueGroupWithZeroIsoInt K).strictMono)

Premises used: Iff.mpr, ValuativeRel.isRankLeOne_iff_mulArchimedean, MulEquiv.toMonoidHom, MulArchimedean.comap, OrderMonoidIso.strictMono, OrderMonoidIso.toMulEquiv, IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
⊢ Finite.{u_1 + 1} (IsLocalRing.ResidueField ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))

Tactic:
letI := IsTopologicalAddGroup.rightUniformSpace K
  haveI := isUniformAddGroup_of_addCommGroup (G := K)
  letI : (Valued.v (R := K)).RankOne :=
  { hom' := IsRankLeOne.nonempty.some.emb (R := K).comp MonoidWithZeroHom.ValueGroup₀.embedding
    strictMono' := IsRankLeOne.nonempty.some.strictMono.comp
        MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
  (compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField.mp
    (inferInstanceAs (CompactSpace 𝒪[K]))).2.2

Premises used: Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, Set.Mem, Valuation.RankOne.mk, setOf, isUniformAddGroup_of_addCommGroup, And.right, Iff.mp, IsTopologicalAddGroup.rightUniformSpace