awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.valuation = g.valuation ↔ f.norm = g.norm
have ha₀ : LT.lt (α := ℚ) 0 (↑p : ℚ)
Tactic: rw [norm_eq_zpow_neg_valuation hf, norm_eq_zpow_neg_valuation hg, ← neg_inj, zpow_right_inj₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
ha₀ : LT.lt (α := ℚ) 0 (↑p : ℚ)
⊢ f.valuation = g.valuation ↔ f.norm = g.norm
have ha₁ : Ne (α := ℚ) (↑p : ℚ) 1
Tactic: rw [norm_eq_zpow_neg_valuation hf, norm_eq_zpow_neg_valuation hg, ← neg_inj, zpow_right_inj₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
⊢ (f * g).norm = f.norm * g.norm
have hg : f * g ≈ 0
Tactic: have hg : f * g ≈ 0 := mul_equiv_zero' _ hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ (f * g).norm = f.norm * g.norm
have hf₁ : f * g ≈ 0
Tactic: have hf : f * g ≈ 0 := mul_equiv_zero _ hg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f * g ≈ 0 then 0 else padicNorm p ((↑(f * g) : ℕ → ℚ) (stationaryPoint hf))) =
    HMul.hMul (α := ℚ) (if hf : f ≈ 0 then 0 else padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)))
      (if hf : g ≈ 0 then 0 else padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hf)))
have hfg : ¬f * g ≈ 0
Tactic: have hfg := mul_not_equiv_zero hf hg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ (if hf : f * g ≈ 0 then 0 else padicNorm p ((↑(f * g) : ℕ → ℚ) (stationaryPoint hf))) =
    HMul.hMul (α := ℚ) (if hf : f ≈ 0 then 0 else padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)))
      (if hf : g ≈ 0 then 0 else padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hf)))
have simp : padicNorm p ((↑(f * g) : ℕ → ℚ) (stationaryPoint sorry)) =
  padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint sorry)) * padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint sorry))
Tactic: simp only [hfg, hf, hg, dite_false]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p ((↑(f * g) : ℕ → ℚ) (stationaryPoint ⋯)) =
    padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) * padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
have rw : padicNorm p ((↑(f * g) : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) =
  padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) *
    padicNorm p ((↑g : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg))))
Tactic: rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ norm (const (padicNorm p) q) = padicNorm p q
have inl : norm (const (padicNorm p) 0) = padicNorm p 0
Tactic: obtain rfl | hq := eq_or_ne q 0
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
inl : norm (const (padicNorm p) 0) = padicNorm p 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
have inr : ∀ (hq : q ≠ 0), norm (const (padicNorm p) q) = padicNorm p q
Tactic: obtain rfl | hq := eq_or_ne q 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
⊢ ∃ (z : ℤ), a.norm = HPow.hPow (α := ℚ) (↑p : ℚ) (-z)
have let : ∀ (k : ℚ) (hk : a.norm = padicNorm p k) (hk' : k ≠ 0), ∃ (z : ℤ), a.norm = HPow.hPow (α := ℚ) (↑p : ℚ) (-z)
Tactic: let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (p := p) 1 = 1
have h1 : ¬HasEquiv.Equiv (α := PadicSeq p) 1 0
Tactic: have h1 : ¬(1 : PadicSeq p) ≈ 0 := one_not_equiv_zero _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hlt : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))
⊢ False
have hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
Tactic: have hpn : 0 < padicNorm p (f (stationaryPoint hf)) - padicNorm p (g (stationaryPoint hg)) :=
    sub_pos_of_lt hlt
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hlt : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
⊢ False
have obtain : ∀ (N : ℕ)
  (hN :
    ∀ j ≥ N,
      padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
        padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))),
  False
Tactic: obtain ⟨N, hN⟩ := hfg _ hpn
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hlt : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
⊢ False
have hi : N ≤ i
Tactic: have hi : N ≤ i := le_max_left _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hlt : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
⊢ False
have hN' : padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
  padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
Tactic: have hN' := hN _ hi
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hlt : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
    padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
⊢ False
have hlt₁ : padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
Tactic: rw [lift_index_left hf N (stationaryPoint hg), lift_index_right hg N (stationaryPoint hf)]
    at hN' h hlt
Cleared hypotheses: h, hlt, hN, i, hi, hN'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hlt : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
    padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hlt₁ :
  padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ False
have h₁ : padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
  padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
Tactic: rw [lift_index_left hf N (stationaryPoint hg), lift_index_right hg N (stationaryPoint hf)]
    at hN' h hlt
Cleared hypotheses: h, hlt, hN, i, hi, hN'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≠ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hlt : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
    padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hlt₁ :
  padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h₁ :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN₁ :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hi₁ :
  let i := max N (max (stationaryPoint hf) (stationaryPoint hg));
  N ≤ i
⊢ False
have hN'₁ : let i := max N (max (stationaryPoint hf) (stationaryPoint hg));
padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
Tactic: rw [lift_index_left hf N (stationaryPoint hg), lift_index_right hg N (stationaryPoint hf)]
    at hN' h hlt
Cleared hypotheses: h, hlt, hN, i, hi, hN'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)
have rwa : ∀
  (h :
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠ padicNorm p (-(↑g : ℕ → ℚ) i))
  (hi : N ≤ i)
  (hN' :
    padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
      padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
        padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))),
  padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)
Tactic: rwa [← padicNorm.neg (g i)] at h
Cleared hypotheses: h, hi, hN'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ False
have hpne : padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)
Tactic: have hpne : padicNorm p (f i) ≠ padicNorm p (-g i) := by rwa [← padicNorm.neg (g i)] at h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)
⊢ False
have hN'₁ : padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
Tactic: rw [CauSeq.sub_apply, sub_eq_add_neg, add_eq_max_of_ne hpne, padicNorm.neg, max_eq_left_of_lt hlt]
    at hN'
Cleared hypotheses: hN', hpne
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)
⊢ padicNorm p ((↑f : ℕ → ℚ) i) < padicNorm p ((↑f : ℕ → ℚ) i)
have apply : padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≤
  padicNorm p ((↑f : ℕ → ℚ) i)
Tactic: apply lt_of_lt_of_le hN'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)
⊢ padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≤
    padicNorm p ((↑f : ℕ → ℚ) i)
have a : 0 ≤ padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
Tactic: apply sub_le_self
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p ((↑f : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)
⊢ False
have this : padicNorm p ((↑f : ℕ → ℚ) i) < padicNorm p ((↑f : ℕ → ℚ) i)
Tactic: have : padicNorm p (f i) < padicNorm p (f i) := by
    apply lt_of_lt_of_le hN'
    apply sub_le_self
    apply padicNorm.nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
have by_contra : ∀ (h : ¬padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
hle : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≤ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
⊢ False
have inr : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) < padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
Tactic: apply norm_eq_of_equiv_aux hg hf (Setoid.symm hfg) (Ne.symm h)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
⊢ False
have x : padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)) < padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ∨
  padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≤ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
Tactic: cases lt_or_ge (padicNorm p (g (stationaryPoint hg))) (padicNorm p (f (stationaryPoint hf))) with
  | inl hlt =>
    exact norm_eq_of_equiv_aux hf hg hfg h hlt
  | inr hle =>
    apply norm_eq_of_equiv_aux hg hf (Setoid.symm hfg) (Ne.symm h)
    exact lt_of_le_of_ne hle h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
⊢ f.norm = g.norm
have hg : g ≈ 0
Tactic: have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
⊢ f.norm = g.norm
have hg : ¬g ≈ 0
Tactic: have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ Eq (α := ℚ) (if hf : f ≈ 0 then 0 else padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)))
    (if hf : g ≈ 0 then 0 else padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hf)))
have split_ifs : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ LE.le (α := ℚ) (if hf : f + g ≈ 0 then 0 else padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hf)))
    (max (if hf : f ≈ 0 then 0 else padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)))
      (if hf : g ≈ 0 then 0 else padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hf))))
have split_ifs : padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) ≤
  max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
Tactic: split_ifs