awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
a : ℤ
⊢ (χ₈' : (a : ZMod 8) → ℤ) (↑a : ZMod 8) =
    HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (cast (n := 8) (↑a : ZMod 8)) : ℤ)
      ((χ₈ : (a : ZMod 8) → ℤ) (↑a : ZMod 8) : ℤ)

Tactic:
exact χ₈'_eq_χ₄_mul_χ₈ a

Premises used: Int.cast, ZMod.χ₈'_eq_χ₄_mul_χ₈
-- 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 : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
⊢ IsUniformAddGroup K

Tactic:
haveI := isUniformAddGroup_of_addCommGroup (G := K)
-- 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
⊢ IsTopologicalDivisionRing K

Tactic:
infer_instance
-- 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
γ : ValueGroupWithZero K
obtain :
  ∀ (γ : 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)}
⊢ IsCompact.{u_1} (X := K) {x : K | (valuation K : (a : K) → ValueGroupWithZero K) x ≤ γ}

Tactic:
obtain ⟨γ, rfl⟩ := ValuativeRel.valuation_surjective γ

Premises used: ValuativeRel.valuation_surjective, rfl
-- 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
pos :
  ∀ (hγ : γ = 0),
    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)}
neg :
  ∀ (hγ : ¬γ = 0),
    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:
by_cases hγ : γ = 0
-- 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
⊢ 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 [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 := ⋯
neg :
  ∀ (s : Set K) (hs : Membership.mem (γ := Filter K) (nhds 0) s) (hs' : IsCompact 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 ⟨s, hs, -, hs'⟩ := LocallyCompactSpace.local_compact_nhds (0 : K) .univ Filter.univ_mem

Premises used: Set.univ, LocallyCompactSpace.local_compact_nhds, Filter.univ_mem, OfNat.ofNat
-- 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
obtain :
  ∀ (r : ValueGroupWithZero K) (hr : r ≠ 0) (hrs : {x : K | (valuation K : (a : K) → ValueGroupWithZero K) x < r} ⊆ s),
    ∃ (r' : K),
      r' ≠ 0 ∧
        LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
            (1 : ValueGroupWithZero K) ∧
          {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
⊢ ∃ (r' : K),
    r' ≠ 0 ∧
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
          (1 : ValueGroupWithZero K) ∧
        {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

Tactic:
obtain ⟨r, hr, hrs⟩ := (IsValuativeTopology.hasBasis_nhds_zero' K).mem_iff.mp hs

Premises used: Filter.HasBasis.mem_iff, IsValuativeTopology.hasBasis_nhds_zero', Iff.mp
-- 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 : r ≠ 0
hrs : {x : K | (valuation K : (a : K) → ValueGroupWithZero K) x < r} ⊆ s
obtain :
  ∀ (r' : K) (hr' : r' ≠ 0)
    (hr :
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
        (1 : ValueGroupWithZero K)),
    ∃ (r' : K),
      r' ≠ 0 ∧
        LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
            (1 : ValueGroupWithZero K) ∧
          {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
⊢ ∃ (r' : K),
    r' ≠ 0 ∧
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
          (1 : ValueGroupWithZero K) ∧
        {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

Tactic:
obtain ⟨r', hr', hr⟩ := Valuation.IsNontrivial.exists_lt_one (v := valuation K)

Premises used: Valuation.IsNontrivial.exists_lt_one
-- 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)
inl :
  ∀ (hr1 : r < 1),
    ∃ (r' : K),
      r' ≠ 0 ∧
        LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
            (1 : ValueGroupWithZero K) ∧
          {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
inr :
  ∀ (hr1 : 1 ≤ r),
    ∃ (r' : K),
      r' ≠ 0 ∧
        LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
            (1 : ValueGroupWithZero K) ∧
          {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
⊢ ∃ (r' : K),
    r' ≠ 0 ∧
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
          (1 : ValueGroupWithZero K) ∧
        {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

Tactic:
obtain hr1 | hr1 := lt_or_ge r 1

Premises used: lt_or_ge, OfNat.ofNat
-- 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 : r < 1
inl :
  ∀ (r : K)
    (hr :
      Ne (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
        (0 : ValueGroupWithZero K))
    (hrs :
      {x : K |
          LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
            ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
        s)
    (hr1 :
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
        (1 : ValueGroupWithZero K)),
    ∃ (r' : K),
      r' ≠ 0 ∧
        LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
            (1 : ValueGroupWithZero K) ∧
          {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
⊢ ∃ (r' : K),
    r' ≠ 0 ∧
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
          (1 : ValueGroupWithZero K) ∧
        {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

Tactic:
obtain ⟨r, rfl⟩ := ValuativeRel.valuation_surjective r

Premises used: ValuativeRel.valuation_surjective, rfl
-- 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
hr_1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
r : K
hr :
  Ne (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (0 : ValueGroupWithZero K)
hrs :
  {x : K |
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
    s
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
⊢ ¬r = 0

Tactic:
simp only [ne_eq, map_eq_zero] at hr

Premises used: map_eq_zero, ne_eq
-- 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
hr_1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
r : K
hrs :
  {x : K |
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
    s
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
hr : ¬r = 0
⊢ HPow.hPow (β := ℕ) r 2 ≠ 0

Tactic:
simpa using 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
γ : 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
hr_1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
r : K
hrs :
  {x : K |
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
    s
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
hr : ¬r = 0
⊢ LT.lt (α := ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) (HPow.hPow (β := ℕ) r 2) : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)

Tactic:
simpa [pow_two]

Premises used: pow_two
-- 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
hr_1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
r : K
hrs :
  {x : K |
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
    s
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
hr : ¬r = 0
inl :
  ∀ (x : K)
    (hx :
      Membership.mem (γ := Set K)
        {x : K |
          LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
            ((valuation K : (a : K) → ValueGroupWithZero K) (HPow.hPow (β := ℕ) r 2) : ValueGroupWithZero K)}
        x),
    Membership.mem (γ := Set K)
      {x : K |
        LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
          ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)}
      x
⊢ ∃ (r' : K),
    r' ≠ 0 ∧
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
          (1 : ValueGroupWithZero K) ∧
        {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

Tactic:
refine ⟨r ^ 2, by simpa using hr, by simpa [pow_two], fun x hx ↦ hrs ?_⟩
-- 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
hr_1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
r : K
hrs :
  {x : K |
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
    s
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
hr : ¬r = 0
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K |
      LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) (HPow.hPow (β := ℕ) r 2) : ValueGroupWithZero K)}
    x
⊢ (valuation K : (a : K) → ValueGroupWithZero K) x ≤
    HPow.hPow (α := ValueGroupWithZero K) (β := ℕ)
      ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K) 2

Tactic:
simp only [map_pow, Set.mem_setOf_eq] at hx ⊢

Premises used: Set.mem_setOf_eq, map_pow
-- 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
hr_1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
r : K
hrs :
  {x : K |
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
    s
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
hr : ¬r = 0
x : K
hx :
  (valuation K : (a : K) → ValueGroupWithZero K) x ≤
    HPow.hPow (α := ValueGroupWithZero K) (β := ℕ)
      ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K) 2
⊢ HPow.hPow (α := ValueGroupWithZero K) (β := ℕ)
      ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K) 2 <
    (valuation K : (a : K) → ValueGroupWithZero K) r

Tactic:
simpa [pow_two, hr]

Premises used: pow_two
-- 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
hr_1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
r : K
hrs :
  {x : K |
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)} ⊆
    s
hr1 :
  LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)
    (1 : ValueGroupWithZero K)
hr : ¬r = 0
x : K
hx :
  (valuation K : (a : K) → ValueGroupWithZero K) x ≤
    HPow.hPow (α := ValueGroupWithZero K) (β := ℕ)
      ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K) 2
⊢ LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
    ((valuation K : (a : K) → ValueGroupWithZero K) r : ValueGroupWithZero K)

Tactic:
exact hx.trans_lt (by simpa [pow_two, hr])

Premises used: 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
⊢ ∃ (r' : K),
    r' ≠ 0 ∧
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
          (1 : ValueGroupWithZero K) ∧
        {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

Tactic:
⟨r', hr', hr, .trans ?_ hrs⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- 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
inr :
  Subset.{u_1} (α := Set K)
    {x : K |
      LE.le (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) x : ValueGroupWithZero K)
        ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)}
    {x : K | (valuation K : (a : K) → ValueGroupWithZero K) x < r}
⊢ ∃ (r' : K),
    r' ≠ 0 ∧
      LT.lt (α := ValueGroupWithZero K) ((valuation K : (a : K) → ValueGroupWithZero K) r' : ValueGroupWithZero K)
          (1 : ValueGroupWithZero K) ∧
        {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

Tactic:
refine ⟨r', hr', hr, .trans ?_ hrs⟩