awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
a : stationaryPoint hf ≤ max v2 (stationaryPoint hf)
a₁ : max v2 (stationaryPoint hf) ≤ max v1 (max v2 (stationaryPoint hf))
a₂ : ℕ
⊢ stationaryPoint hf ≤ max v1 (max v2 (stationaryPoint hf))

Tactic:
apply le_trans

Premises used: le_trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ max v2 (stationaryPoint hf)

Tactic:
apply le_max_right v2

Premises used: le_max_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ max v2 (stationaryPoint hf) ≤ max v1 (max v2 (stationaryPoint hf))

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
hnc : ¬(↑f : ℕ → ℚ) (stationaryPoint hf) = 0
⊢ f.norm = HPow.hPow (α := ℚ) (↑p : ℚ) (-f.valuation)

Tactic:
rw [norm, valuation, dif_neg hf, dif_neg hf, padicNorm, if_neg]

Premises used: PadicSeq.valuation, dif_neg, padicNorm, if_neg, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : (↑f : ℕ → ℚ) (stationaryPoint hf) = 0
hnc : LimZero f
⊢ False

Tactic:
apply CauSeq.not_limZero_of_not_congr_zero hf

Premises used: CauSeq.not_limZero_of_not_congr_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : (↑f : ℕ → ℚ) (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
h : ∀ j ≥ stationaryPoint hf, padicNorm p ((↑f : ℕ → ℚ) j) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p ((↑f : ℕ → ℚ) j) < ε

Tactic:
use stationaryPoint hf

Premises used: PadicSeq.stationaryPoint
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : (↑f : ℕ → ℚ) (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) < ε
⊢ padicNorm p ((↑f : ℕ → ℚ) n) < ε

Tactic:
rw [stationaryPoint_spec hf le_rfl hn]

Premises used: le_rfl, PadicSeq.stationaryPoint_spec
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : (↑f : ℕ → ℚ) (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) < ε

Tactic:
simpa [H] using hε
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
ha₀ : LT.lt (α := ℚ) 0 (↑p : ℚ)
ha₁ : Ne (α := ℚ) (↑p : ℚ) 1
⊢ f.valuation = g.valuation ↔ f.norm = g.norm

Tactic:
rw [norm_eq_zpow_neg_valuation hf, norm_eq_zpow_neg_valuation hg, ← neg_inj, zpow_right_inj₀]

Premises used: zpow_right_inj₀, PadicSeq.norm_eq_zpow_neg_valuation, neg_inj
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ LT.lt (α := ℚ) 0 (↑p : ℚ)

Tactic:
mod_cast (Fact.out : p.Prime).pos

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.Prime.pos, Nat.cast, LT.lt, congrFun', Nat.cast_zero, Eq.symm, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ LT.lt (α := ℚ) 0 (↑p : ℚ)

Tactic:
exact mod_cast (Fact.out : p.Prime).pos

Premises used: Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ Ne (α := ℚ) (↑p : ℚ) 1

Tactic:
mod_cast (Fact.out : p.Prime).ne_one

Premises used: congrArg, cast, Ne, Nat.cast, Nat.Prime.ne_one, Nat.cast_inj._simp_1, Eq.symm, Nat.cast_one, Not, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ Ne (α := ℚ) (↑p : ℚ) 1

Tactic:
exact mod_cast (Fact.out : p.Prime).ne_one

Premises used: Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
⊢ f * g ≈ 0

Tactic:
have hg : f * g ≈ 0 := mul_equiv_zero' _ hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
hg : f * g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
simp only [hf, hg, norm, dif_pos, zero_mul]

Premises used: MulZeroClass.zero_mul, dif_pos, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ f * g ≈ 0

Tactic:
have hf : f * g ≈ 0 := mul_equiv_zero _ hg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf_1 : ¬f ≈ 0
hg : g ≈ 0
hf : f * g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
simp only [hf, hg, norm, dif_pos, mul_zero]

Premises used: dif_pos, MulZeroClass.mul_zero, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ¬f * g ≈ 0

Tactic:
have hfg := mul_not_equiv_zero hf hg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
simp :
  padicNorm p ((↑(f * g) : ℕ → ℚ) (stationaryPoint ⋯)) =
    padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) * padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))
⊢ (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)))

Tactic:
simp only [hfg, hf, hg, dite_false]

Premises used: dite_false
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
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))))
v1 v2 v1₁ v3 v2₁ v3₁ : ℕ
⊢ padicNorm p ((↑(f * g) : ℕ → ℚ) (stationaryPoint ⋯)) =
    padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint ⋯)) * padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint ⋯))

Tactic:
rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]

Premises used: PadicSeq.lift_index_left_left, PadicSeq.lift_index_right, PadicSeq.lift_index_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ (f * g).norm = f.norm * g.norm

Tactic:
exact if hf : f ≈ 0 then by
    have hg : f * g ≈ 0 := mul_equiv_zero' _ hf
    simp only [hf, hg, norm, dif_pos, zero_mul]
  else
    if hg : g ≈ 0 then by
      have hf : f * g ≈ 0 := mul_equiv_zero _ hg
      simp only [hf, hg, norm, dif_pos, mul_zero]
    else by
      unfold norm
      have hfg := mul_not_equiv_zero hf hg
      simp only [hfg, hf, hg, dite_false]
      -- Porting note: originally `padic_index_simp [hfg, hf, hg]`
      rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
      apply padicNorm.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ (f * g).norm = f.norm * g.norm

Tactic:
classical
  exact if hf : f ≈ 0 then by
    have hg : f * g ≈ 0 := mul_equiv_zero' _ hf
    simp only [hf, hg, norm, dif_pos, zero_mul]
  else
    if hg : g ≈ 0 then by
      have hf : f * g ≈ 0 := mul_equiv_zero _ hg
      simp only [hf, hg, norm, dif_pos, mul_zero]
    else by
      unfold norm
      have hfg := mul_not_equiv_zero hf hg
      simp only [hfg, hf, hg, dite_false]
      -- Porting note: originally `padic_index_simp [hfg, hf, hg]`
      rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
      apply padicNorm.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : PadicSeq p
⊢ Eq (α := Completion.Cauchy (padicNorm p)) (mk f) 0 ↔ f ≈ 0

Tactic:
mk_eq

Premises used: CauSeq.Completion.ofRat, CauSeq.Completion.mk, CauSeq.Completion.mk_eq
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : PadicSeq p
⊢ Ne (α := Completion.Cauchy (padicNorm p)) (mk f) 0 ↔ ¬f ≈ 0

Tactic:
eq_zero_iff_equiv_zero _ |>.not

Premises used: Iff.not, PadicSeq.eq_zero_iff_equiv_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
inl : norm (const (padicNorm p) 0) = padicNorm p 0
inr : ∀ (hq : q ≠ 0), norm (const (padicNorm p) q) = padicNorm p q
⊢ norm (const (padicNorm p) q) = padicNorm p q

Tactic:
obtain rfl | hq := eq_or_ne q 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (const (padicNorm p) 0) = padicNorm p 0

Tactic:
simp [norm]

Premises used: PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q

Tactic:
simp [norm, not_equiv_zero_const_of_nonzero hq]

Premises used: PadicSeq.not_equiv_zero_const_of_nonzero, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
let : ∀ (k : ℚ) (hk : a.norm = padicNorm p k) (hk' : k ≠ 0), ∃ (z : ℤ), a.norm = HPow.hPow (α := ℚ) (↑p : ℚ) (-z)
⊢ ∃ (z : ℤ), a.norm = HPow.hPow (α := ℚ) (↑p : ℚ) (-z)

Tactic:
let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
k : ℚ
hk : a.norm = padicNorm p k
hk' : k ≠ 0
⊢ ∃ (z : ℤ), a.norm = HPow.hPow (α := ℚ) (↑p : ℚ) (-z)

Tactic:
simpa [hk] using padicNorm.values_discrete hk'

Premises used: padicNorm.values_discrete
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬HasEquiv.Equiv (α := PadicSeq p) 1 0

Tactic:
have h1 : ¬(1 : PadicSeq p) ≈ 0 := one_not_equiv_zero _
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h1 : ¬HasEquiv.Equiv (α := PadicSeq p) 1 0
⊢ norm (p := p) 1 = 1

Tactic:
simp [h1, norm]

Premises used: PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
⊢ 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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
obtain :
  ∀ (N : ℕ)
    (hN :
      ∀ j ≥ N,
        padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
          padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))),
    False
⊢ False

Tactic:
obtain ⟨N, hN⟩ := hfg _ hpn
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
⊢ N ≤ i

Tactic:
have hi : N ≤ i := le_max_left _ _
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ padicNorm p ((↑(f - g) : ℕ → ℚ) i) <
    padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))

Tactic:
have hN' := hN _ hi
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
⊢ 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

Premises used: PadicSeq.stationaryPoint, PadicSeq.lift_index_right, PadicSeq.lift_index_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))))
⊢ 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

Premises used: PadicSeq.stationaryPoint, PadicSeq.lift_index_right, PadicSeq.lift_index_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))))
⊢ ∀ j ≥ N,
    padicNorm p ((↑(f - g) : ℕ → ℚ) j) <
      padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) - padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))

Tactic:
rw [lift_index_left hf N (stationaryPoint hg), lift_index_right hg N (stationaryPoint hf)]
    at hN' h hlt

Premises used: PadicSeq.stationaryPoint, PadicSeq.lift_index_right, PadicSeq.lift_index_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
⊢ let i := max N (max (stationaryPoint hf) (stationaryPoint hg));
  N ≤ i

Tactic:
rw [lift_index_left hf N (stationaryPoint hg), lift_index_right hg N (stationaryPoint hf)]
    at hN' h hlt

Premises used: PadicSeq.stationaryPoint, PadicSeq.lift_index_right, PadicSeq.lift_index_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ 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

Premises used: PadicSeq.stationaryPoint, PadicSeq.lift_index_right, PadicSeq.lift_index_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))))
rwa rwa₁ rwa₂ 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)
⊢ padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)

Tactic:
rwa [← padicNorm.neg (g i)] at h

Premises used: padicNorm.neg, Subtype.val