awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
have obtain : ∀ (N : ℕ)
  (hN :
    ∀ i ≥ N,
      (padicNormE : (a : ℚ_[p]) → ℚ)
          ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                    (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                ℕ → ℚ_[p])
              i -
            q) <
        ε'),
  ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
Tactic: obtain ⟨N, hN⟩ := hq ε' hε'.1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
have exists : ∀ j ≥ N, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
Tactic: exists N
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
⊢ ‖(↑(f - const norm q) : ℕ → ℚ_[p]) i‖ < ε
have h : (padicNormE : (a : ℚ_[p]) → ℚ)
    ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
              cau_seq_norm_e) :
          ℕ → ℚ_[p])
        i -
      q) <
  ε'
Tactic: have h := hN i hi
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'
⊢ ‖(↑(f - const norm q) : ℕ → ℚ_[p]) i‖ < ε
have change : ‖(↑f : ℕ → ℚ_[p]) i - q‖ < ε
Tactic: change norm (f i - q) < ε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'
⊢ ‖(↑f : ℕ → ℚ_[p]) i - q‖ < ε
have refine : ‖(↑f : ℕ → ℚ_[p]) i - q‖ < (↑ε' : ℝ)
Tactic: refine lt_trans ?_ hε'.2
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'
⊢ ‖(↑f : ℕ → ℚ_[p]) i - q‖ < (↑ε' : ℝ)
have dsimp : LT.lt (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q)) : ℝ) (↑ε' : ℝ)
Tactic: dsimp [norm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖(↑f : ℕ → ℚ_[p]) i‖ ≤ a
⊢ ‖f.lim‖ ≤ a
have obtain : ∀ (N : ℕ) (hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → ℚ_[p]) j‖ < a), ‖f.lim‖ ≤ a
Tactic: obtain ⟨N, hN⟩ := Setoid.symm (CauSeq.equiv_lim f) _ ha
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖(↑f : ℕ → ℚ_[p]) i‖ ≤ a
N : ℕ
hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → ℚ_[p]) j‖ < a
⊢ ‖f.lim‖ ≤ a
have f₁ : ‖f.lim‖ = ‖f.lim - (↑f : ℕ → ℚ_[p]) N + (↑f : ℕ → ℚ_[p]) N‖
Tactic: calc
    ‖f.lim‖ = ‖f.lim - f N + f N‖ := by simp
    _ ≤ max ‖f.lim - f N‖ ‖f N‖ := nonarchimedean _ _
    _ ≤ a := max_le (le_of_lt (hN _ le_rfl)) (hf _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ CompleteSpace ℚ_[p]
have a : ∀ (u : ℕ → ℚ_[p]), CauchySeq u → ∃ (a : ℚ_[p]), Tendsto u atTop (nhds a)
Tactic: apply complete_of_cauchySeq_tendsto
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
⊢ ∃ (a : ℚ_[p]), Tendsto u atTop (nhds a)
have a : ∀ (s : Set ℚ_[p]) (h : s ∈ nhds c.lim), s ∈ Filter.map u atTop
Tactic: refine ⟨c.lim, fun s h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
s : Set ℚ_[p]
h : s ∈ nhds c.lim
⊢ s ∈ Filter.map u atTop
have a : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball c.lim ε ⊆ s), s ∈ Filter.map u atTop
Tactic: rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
s : Set ℚ_[p]
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
⊢ s ∈ Filter.map u atTop
have this : ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(c - const norm c.lim) : ℕ → ℚ_[p]) j‖ < ε
Tactic: have := c.equiv_lim ε ε0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
s : Set ℚ_[p]
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(c - const norm c.lim) : ℕ → ℚ_[p]) j‖ < ε
⊢ s ∈ Filter.map u atTop
have a : ∃ (a : ℕ), ∀ b ≥ a, b ∈ u ⁻¹' s
Tactic: simp only [mem_map, mem_atTop_sets]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
⊢ PadicSeq.valuation f = PadicSeq.valuation g
have pos : ∀ (hf : f ≈ 0), PadicSeq.valuation f = PadicSeq.valuation g
Tactic: by_cases hf : f ≈ 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
pos : ∀ (hf : f ≈ 0), PadicSeq.valuation f = PadicSeq.valuation g
⊢ PadicSeq.valuation f = PadicSeq.valuation g
have neg : ∀ (hf : ¬f ≈ 0), PadicSeq.valuation f = PadicSeq.valuation g
Tactic: by_cases hf : f ≈ 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : f ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g
have hg : g ≈ 0
Tactic: have hg : g ≈ 0 := Setoid.trans (Setoid.symm h) hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g
have hg : ¬g ≈ 0
Tactic: have hg : ¬g ≈ 0 := fun hg ↦ hf (Setoid.trans h hg)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g
have neg : PadicSeq.norm f = PadicSeq.norm g
Tactic: rw [PadicSeq.val_eq_iff_norm_eq hf hg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x ≠ 0 → ‖x‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation)
have h : ∀ (f : CauSeq ℚ (padicNorm p)),
  Ne (α := ℚ_[p]) ⟦f⟧ 0 → norm (E := ℚ_[p]) ⟦f⟧ = HPow.hPow (α := ℝ) (↑p : ℝ) (-valuation ⟦f⟧)
Tactic: induction x using Quotient.inductionOn with | _ f
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
⊢ (↑(PadicSeq.norm f) : ℝ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
have h : (↑(HPow.hPow (α := ℚ) (↑p : ℚ) (-PadicSeq.valuation f)) : ℝ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
Tactic: rw [PadicSeq.norm_eq_zpow_neg_valuation]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
h : (↑(HPow.hPow (α := ℚ) (↑p : ℚ) (-PadicSeq.valuation f)) : ℝ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
⊢ (↑(PadicSeq.norm f) : ℝ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
have h₁ : ¬f ≈ 0
Tactic: rw [PadicSeq.norm_eq_zpow_neg_valuation]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
⊢ (↑(HPow.hPow (α := ℚ) (↑p : ℚ) (-PadicSeq.valuation f)) : ℝ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
have h : HPow.hPow (α := ℝ) (↑(↑p : ℚ) : ℝ) (-PadicSeq.valuation f) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
Tactic: rw [Rat.cast_zpow, Rat.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
h : HPow.hPow (α := ℝ) (↑(↑p : ℚ) : ℝ) (-PadicSeq.valuation f) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
⊢ (↑(HPow.hPow (α := ℚ) (↑p : ℚ) (-PadicSeq.valuation f)) : ℝ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
have h₁ : HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
Tactic: rw [Rat.cast_zpow, Rat.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
⊢ ¬f ≈ 0
have h : ¬f - 0 ≈ 0
Tactic: apply CauSeq.not_limZero_of_not_congr_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
⊢ ¬f - 0 ≈ 0
have h : ∀ (hf : f - 0 ≈ 0), Eq (α := ℚ_[p]) ⟦f⟧ 0
Tactic: contrapose hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : f - 0 ≈ 0
⊢ Eq (α := ℚ_[p]) ⟦f⟧ 0
have h : f ≈ const (padicNorm p) 0
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ valuation (p := p) (↑q : ℚ_[p]) = padicValRat p q
have inl : valuation (p := p) (↑0 : ℚ_[p]) = padicValRat p 0
Tactic: rcases eq_or_ne q 0 with rfl | hq
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
inl : valuation (p := p) (↑0 : ℚ_[p]) = padicValRat p 0
⊢ valuation (p := p) (↑q : ℚ_[p]) = padicValRat p q
have inr : ∀ (hq : q ≠ 0), valuation (p := p) (↑q : ℚ_[p]) = padicValRat p q
Tactic: rcases eq_or_ne q 0 with rfl | hq
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ valuation (p := p) (↑q : ℚ_[p]) = padicValRat p q
have inr : norm (E := ℚ_[p]) (↑q : ℚ_[p]) = HPow.hPow (α := ℝ) (↑p : ℝ) (-padicValRat p q)
Tactic: refine neg_injective ((zpow_right_strictMono₀ (mod_cast hp.out.one_lt)).injective
    <| (norm_eq_zpow_neg_valuation (mod_cast hq)).symm.trans ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ norm (E := ℚ_[p]) (↑q : ℚ_[p]) = HPow.hPow (α := ℝ) (↑p : ℝ) (-padicValRat p q)
have inr : padicNorm p q = HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)
Tactic: rw [eq_padicNorm, ← Rat.cast_natCast, ← Rat.cast_zpow, Rat.cast_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ valuation (p := p) (↑n : ℚ_[p]) = (↑(padicValInt p n) : ℤ)
have rw : valuation (p := p) (↑(↑n : ℚ) : ℚ_[p]) = (↑(padicValInt p n) : ℤ)
Tactic: rw [← Rat.cast_intCast, valuation_ratCast, padicValRat.of_int]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
rw : valuation (p := p) (↑(↑n : ℚ) : ℚ_[p]) = (↑(padicValInt p n) : ℤ)
⊢ valuation (p := p) (↑n : ℚ_[p]) = (↑(padicValInt p n) : ℤ)
have rw₁ : padicValRat p (↑n : ℚ) = (↑(padicValInt p n) : ℤ)
Tactic: rw [← Rat.cast_intCast, valuation_ratCast, padicValRat.of_int]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
rw : valuation (p := p) (↑(↑n : ℚ) : ℚ_[p]) = (↑(padicValInt p n) : ℤ)
rw₁ : padicValRat p (↑n : ℚ) = (↑(padicValInt p n) : ℤ)
⊢ valuation (p := p) (↑n : ℚ_[p]) = (↑(padicValInt p n) : ℤ)
have rw₂ : Eq (α := ℤ) (↑(padicValInt p n) : ℤ) (↑(padicValInt p n) : ℤ)
Tactic: rw [← Rat.cast_intCast, valuation_ratCast, padicValRat.of_int]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ valuation (p := p) (↑n : ℚ_[p]) = (↑(padicValNat p n) : ℤ)
have rw : valuation (p := p) (↑(↑n : ℚ) : ℚ_[p]) = (↑(padicValNat p n) : ℤ)
Tactic: rw [← Rat.cast_natCast, valuation_ratCast, padicValRat.of_nat]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : valuation (p := p) (↑(↑n : ℚ) : ℚ_[p]) = (↑(padicValNat p n) : ℤ)
⊢ valuation (p := p) (↑n : ℚ_[p]) = (↑(padicValNat p n) : ℤ)
have rw₁ : padicValRat p (↑n : ℚ) = (↑(padicValNat p n) : ℤ)
Tactic: rw [← Rat.cast_natCast, valuation_ratCast, padicValRat.of_nat]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : valuation (p := p) (↑(↑n : ℚ) : ℚ_[p]) = (↑(padicValNat p n) : ℤ)
rw₁ : padicValRat p (↑n : ℚ) = (↑(padicValNat p n) : ℤ)
⊢ valuation (p := p) (↑n : ℚ_[p]) = (↑(padicValNat p n) : ℤ)
have rw₂ : Eq (α := ℤ) (↑(padicValNat p n) : ℤ) (↑(padicValNat p n) : ℤ)
Tactic: rw [← Rat.cast_natCast, valuation_ratCast, padicValRat.of_nat]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation (p := p) 1 = 0
have rw : valuation (p := p) (↑1 : ℚ_[p]) = 0
Tactic: rw [← Nat.cast_one, valuation_natCast, padicValNat_one_right, cast_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : valuation (p := p) (↑1 : ℚ_[p]) = 0
⊢ valuation (p := p) 1 = 0
have rw₁ : Eq (α := ℤ) (↑(padicValNat p 1) : ℤ) 0
Tactic: rw [← Nat.cast_one, valuation_natCast, padicValNat_one_right, cast_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : valuation (p := p) (↑1 : ℚ_[p]) = 0
rw₁ : Eq (α := ℤ) (↑(padicValNat p 1) : ℤ) 0
⊢ valuation (p := p) 1 = 0
have rw₂ : Eq (α := ℤ) (↑0 : ℤ) 0
Tactic: rw [← Nat.cast_one, valuation_natCast, padicValNat_one_right, cast_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : valuation (p := p) (↑1 : ℚ_[p]) = 0
rw₁ : Eq (α := ℤ) (↑(padicValNat p 1) : ℤ) 0
rw₂ : Eq (α := ℤ) (↑0 : ℤ) 0
⊢ valuation (p := p) 1 = 0
have rw₃ : Eq (α := ℤ) 0 0
Tactic: rw [← Nat.cast_one, valuation_natCast, padicValNat_one_right, cast_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation (p := p) (↑p : ℚ_[p]) = 1
have rw : Eq (α := ℤ) (↑(padicValNat p p) : ℤ) 1
Tactic: rw [valuation_natCast, padicValNat_self, cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : Eq (α := ℤ) (↑(padicValNat p p) : ℤ) 1
⊢ valuation (p := p) (↑p : ℚ_[p]) = 1
have rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
Tactic: rw [valuation_natCast, padicValNat_self, cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : Eq (α := ℤ) (↑(padicValNat p p) : ℤ) 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
⊢ valuation (p := p) (↑p : ℚ_[p]) = 1
have rw₂ : Eq (α := ℤ) 1 1
Tactic: rw [valuation_natCast, padicValNat_self, cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation
have pos : ∀ (hx : x = 0), min x.valuation y.valuation ≤ (x + y).valuation
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
pos : ∀ (hx : x = 0), min x.valuation y.valuation ≤ (x + y).valuation
⊢ min x.valuation y.valuation ≤ (x + y).valuation
have neg : ∀ (hx : ¬x = 0), min x.valuation y.valuation ≤ (x + y).valuation
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation
have pos : ∀ (hy : y = 0), min x.valuation y.valuation ≤ (x + y).valuation
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
pos : ∀ (hy : y = 0), min x.valuation y.valuation ≤ (x + y).valuation
⊢ min x.valuation y.valuation ≤ (x + y).valuation
have neg : ∀ (hy : ¬y = 0), min x.valuation y.valuation ≤ (x + y).valuation
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation
have this : ‖x + y‖ ≤ max ‖x‖ ‖y‖
Tactic: have : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := nonarchimedean x y
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).valuation = x.valuation + y.valuation
have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
Tactic: have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ (x * y).valuation = x.valuation + y.valuation
have hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
Tactic: have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
⊢ (x * y).valuation = x.valuation + y.valuation
have hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
Tactic: have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
⊢ (x * y).valuation = x.valuation + y.valuation
have rwa : ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * ‖y‖) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
  (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
    norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
    zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos