awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp3 : p % 4 = 3
hq3 : q % 4 = 3
hpq : p ≠ q
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)
have rw : legendreSym p (↑q : ℤ) = 1 ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)
Tactic: rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q,
    quadratic_reciprocity_three_mod_four hp3 hq3, neg_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp3 : p % 4 = 3
hq3 : q % 4 = 3
hpq : p ≠ q
rw : legendreSym p (↑q : ℤ) = 1 ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)
have rw₁ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym q (↑p : ℤ) = -1
Tactic: rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q,
    quadratic_reciprocity_three_mod_four hp3 hq3, neg_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp3 : p % 4 = 3
hq3 : q % 4 = 3
hpq : p ≠ q
rw : legendreSym p (↑q : ℤ) = 1 ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)
rw₁ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym q (↑p : ℤ) = -1
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)
have rw₂ : legendreSym p (↑q : ℤ) = 1 ↔ -legendreSym p (↑q : ℤ) = -1
Tactic: rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q,
    quadratic_reciprocity_three_mod_four hp3 hq3, neg_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (goal)
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp3 : p % 4 = 3
hq3 : q % 4 = 3
hpq : p ≠ q
rw : legendreSym p (↑q : ℤ) = 1 ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)
rw₁ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym q (↑p : ℤ) = -1
rw₂ : legendreSym p (↑q : ℤ) = 1 ↔ -legendreSym p (↑q : ℤ) = -1
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)
have rw₃ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym p (↑q : ℤ) = 1
Tactic: rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q,
    quadratic_reciprocity_three_mod_four hp3 hq3, neg_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℤ
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ)
have rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % (↑4 : ℤ)) : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ)
Tactic: rw [← ZMod.intCast_mod n 4, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℤ
rw :
  Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % (↑4 : ℤ)) : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ)
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ)
have rw₁ : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ)
Tactic: rw [← ZMod.intCast_mod n 4, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (hypothesis)
Goal:
n : ℤ
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 : ℤ)
have help : ∀ (m : ℤ),
  0 ≤ m →
    m < 4 →
      Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (if m % 2 = 0 then 0 else if m = 1 then 1 else -1 : ℤ)
Tactic: have help : ∀ m : ℤ, 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 := by
    decide
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 4 →
        Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (if m % 2 = 0 then 0 else if m = 1 then 1 else -1 : ℤ)
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 : ℤ)
have rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % (↑4 : ℤ)) : ZMod 4) : ℤ)
  (if n % 4 % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 : ℤ)
Tactic: rw [← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 4), ← ZMod.intCast_mod n 4]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℕ
hn : n % 2 = 1
⊢ (χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) = HPow.hPow (α := ℤ) (-1) (n / 2)
have rw : (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n / 2)
Tactic: rw [χ₄_nat_eq_if_mod_four]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n / 2)
have simp : (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n / 2)
Tactic: simp only [hn, Nat.one_ne_zero, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n / 2)
have nth_rewrite : (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) ((4 * (n / 4) + n % 4) / 2)
Tactic: nth_rewrite 3 [← Nat.div_add_mod n 4]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) ((HMul.hMul (α := ℕ) 2 2 * (n / 4) + n % 4) / 2)
have rw : (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n % 4 / 2)
Tactic: rw [mul_assoc, add_comm, Nat.add_mul_div_left _ _ zero_lt_two, pow_add, pow_mul,
    neg_one_sq, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (hypothesis)
Goal:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n % 4 / 2)
have help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (m / 2)
Tactic: have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → ite (m = 1) (1 : ℤ) (-1) = (-1) ^ (m / 2) := by decide
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℕ
hn : n % 4 = 1
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (1 : ℤ)
have rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑1 : ZMod 4) : ℤ) (1 : ℤ)
Tactic: rw [χ₄_nat_mod_four, hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℕ
hn : n % 4 = 3
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (-1 : ℤ)
have rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑3 : ZMod 4) : ℤ) (-1 : ℤ)
Tactic: rw [χ₄_nat_mod_four, hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℤ
hn : n % 4 = 1
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (1 : ℤ)
have rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑1 : ZMod 4) : ℤ) (1 : ℤ)
Tactic: rw [χ₄_int_mod_four, hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℤ
hn : n % 4 = 3
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (-1 : ℤ)
have rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑3 : ZMod 4) : ℤ) (-1 : ℤ)
Tactic: rw [χ₄_int_mod_four, hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
have rw : Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
Tactic: rw [← ZMod.natCast_mod n 8]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℤ
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
have rw : Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % (↑8 : ℤ)) : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
Tactic: rw [← ZMod.intCast_mod n 8, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℤ
rw :
  Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % (↑8 : ℤ)) : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
have rw₁ : Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
Tactic: rw [← ZMod.intCast_mod n 8, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (hypothesis)
Goal:
n : ℤ
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ)
    (if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 : ℤ)
have help : ∀ (m : ℤ),
  0 ≤ m →
    m < 8 →
      Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
        (if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 : ℤ)
Tactic: have help :
    ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈ m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 := by
    decide
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 : ℤ)
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ)
    (if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 : ℤ)
have rw : Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % (↑8 : ℤ)) : ZMod 8) : ℤ)
  (if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 : ℤ)
Tactic: rw [← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (hypothesis)
Goal:
n : ℤ
⊢ Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ)
    (if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 : ℤ)
have help : ∀ (m : ℤ),
  0 ≤ m →
    m < 8 →
      Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
        (if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 : ℤ)
Tactic: have help :
    ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈' m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 := by
    decide
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 : ℤ)
⊢ Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ)
    (if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 : ℤ)
have rw : Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(n % (↑8 : ℤ)) : ZMod 8) : ℤ)
  (if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 : ℤ)
Tactic: rw [← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.ZModChar (goal)
Goal:
a : ℤ
⊢ (χ₈' : (a : ZMod 8) → ℤ) (↑a : ZMod 8) =
    HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑a : ZMod 4) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑a : ZMod 8) : ℤ)
have rw : (χ₈' : (a : ZMod 8) → ℤ) (↑a : ZMod 8) =
  HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (cast (n := 8) (↑a : ZMod 8)) : ℤ)
    ((χ₈ : (a : ZMod 8) → ℤ) (↑a : ZMod 8) : ℤ)
Tactic: rw [← @cast_intCast 8 (ZMod 4) _ 4 _ (by lia) a]
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (hypothesis)
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
⊢ IsTopologicalDivisionRing K
have this₁ : IsUniformAddGroup K
Tactic: haveI := isUniformAddGroup_of_addCommGroup (G := K)
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : ValueGroupWithZero K
⊢ IsCompact.{u_1} (X := K) {x : K | (valuation K : (a : K) → ValueGroupWithZero K) x ≤ γ}
have 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)}
Tactic: obtain ⟨γ, rfl⟩ := ValuativeRel.valuation_surjective γ
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : TopologicalSpace K
inst_3 : IsNonarchimedeanLocalField K
γ : 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)}
have 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)}
Tactic: by_cases hγ : γ = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
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)}
⊢ 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)}
have 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)}
Tactic: by_cases hγ : γ = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
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 := ⋯
⊢ 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)}
have 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)}
Tactic: obtain ⟨s, hs, -, hs'⟩ := LocallyCompactSpace.local_compact_nhds (0 : K) .univ Filter.univ_mem
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
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),
    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
have 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
Tactic: obtain ⟨r, hr, hrs⟩ := (IsValuativeTopology.hasBasis_nhds_zero' K).mem_iff.mp hs
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨r', hr', hr⟩ := Valuation.IsNontrivial.exists_lt_one (v := valuation K)
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
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)
⊢ ∃ (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
have 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
Tactic: obtain hr1 | hr1 := lt_or_ge r 1
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain hr1 | hr1 := lt_or_ge r 1
-- Lean 4 proof step from Mathlib.NumberTheory.LocalField.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨r, rfl⟩ := ValuativeRel.valuation_surjective r
Cleared hypotheses: r, hr_1, hrs, hr1