awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))))
⊢ 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
-- 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))))
hpne : padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)
⊢ 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'

Premises used: sub_eq_add_neg, CauSeq.sub_apply, padicNorm.add_eq_max_of_ne, padicNorm.neg, max_eq_left_of_lt
-- 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))))
hpne : padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) 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))))
⊢ padicNorm p ((↑f : ℕ → ℚ) i) ≠ padicNorm p (-(↑g : ℕ → ℚ) i)

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'

Premises used: sub_eq_add_neg, CauSeq.sub_apply, padicNorm.add_eq_max_of_ne, padicNorm.neg, max_eq_left_of_lt
-- 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 : ℕ → ℚ) (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)
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)
⊢ padicNorm p ((↑f : ℕ → ℚ) i) < padicNorm p ((↑f : ℕ → ℚ) i)

Tactic:
apply lt_of_lt_of_le hN'

Premises used: lt_of_lt_of_le
-- 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 : ℕ → ℚ) (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)
a : 0 ≤ padicNorm p ((↑g : ℕ → ℚ) (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)))) ≤
    padicNorm p ((↑f : ℕ → ℚ) i)

Tactic:
apply sub_le_self

Premises used: sub_le_self
-- 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 : ℕ → ℚ) (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)
⊢ 0 ≤ padicNorm p ((↑g : ℕ → ℚ) (max N (max (stationaryPoint hf) (stationaryPoint hg))))

Tactic:
apply padicNorm.nonneg

Premises used: padicNorm.nonneg
-- 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 : ℕ → ℚ) (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)

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
-- 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 : ℕ → ℚ) (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)
this : padicNorm p ((↑f : ℕ → ℚ) i) < padicNorm p ((↑f : ℕ → ℚ) i)
⊢ False

Tactic:
lt_irrefl _ this

Premises used: lt_irrefl
-- 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 : ℕ → ℚ) (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)
this : padicNorm p ((↑f : ℕ → ℚ) i) < padicNorm p ((↑f : ℕ → ℚ) i)
⊢ False

Tactic:
exact lt_irrefl _ this

Premises used: lt_irrefl
-- 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
by_contra :
  ∀ (h : ¬padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))), False
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))

Tactic:
by_contra h
-- 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))
⊢ False

Tactic:
norm_eq_of_equiv_aux hf hg hfg h hlt

Premises used: _private.0.PadicSeq.norm_eq_of_equiv_aux
-- 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))
⊢ False

Tactic:
exact norm_eq_of_equiv_aux hf hg hfg h hlt

Premises used: _private.0.PadicSeq.norm_eq_of_equiv_aux
-- 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))
hle : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≤ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
inr : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) < padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
⊢ False

Tactic:
apply norm_eq_of_equiv_aux hg hf (Setoid.symm hfg) (Ne.symm h)

Premises used: Ne.symm, _private.0.PadicSeq.norm_eq_of_equiv_aux, Setoid.symm
-- 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))
hle : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≤ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) < padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))

Tactic:
lt_of_le_of_ne hle h

Premises used: lt_of_le_of_ne
-- 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))
hle : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) ≤ padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) < padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))

Tactic:
exact lt_of_le_of_ne hle h

Premises used: lt_of_le_of_ne
-- 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))
⊢ 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

Premises used: PadicSeq.stationaryPoint, Ne.symm, _private.0.PadicSeq.norm_eq_of_equiv_aux, Setoid.symm, lt_or_ge, padicNorm, Subtype.val
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
⊢ g ≈ 0

Tactic:
have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ f.norm = g.norm

Tactic:
simp [norm, hf, hg]

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

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

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))

Tactic:
norm_eq_of_equiv hf hg hfg

Premises used: _private.0.PadicSeq.norm_eq_of_equiv
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg))

Tactic:
exact norm_eq_of_equiv hf hg hfg

Premises used: _private.0.PadicSeq.norm_eq_of_equiv
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
⊢ f.norm = g.norm

Tactic:
exact if hf : f ≈ 0 then by
    have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
    simp [norm, hf, hg]
  else by
    have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg
    unfold norm; split_ifs; exact norm_eq_of_equiv hf hg hfg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
⊢ f.norm = g.norm

Tactic:
classical
  exact if hf : f ≈ 0 then by
    have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
    simp [norm, hf, hg]
  else by
    have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg
    unfold norm; split_ifs; exact norm_eq_of_equiv hf hg hfg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
split_ifs :
  padicNorm p ((↑(f + g) : ℕ → ℚ) (stationaryPoint hfg)) ≤
    max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))
⊢ 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))))

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
rw :
  padicNorm p ((↑(f + g) : ℕ → ℚ) (max (stationaryPoint hfg) (max (stationaryPoint hf) (stationaryPoint hg)))) ≤
    max (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 hfg)) ≤
    max (padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) (padicNorm p ((↑g : ℕ → ℚ) (stationaryPoint hg)))

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
hfg : f + g ≈ 0
⊢ 0 ≤ max f.norm g.norm

Tactic:
have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
this : 0 ≤ max f.norm g.norm
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
simpa only [hfg, norm]

Premises used: PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ (f - 0).LimZero

Tactic:
change LimZero (f - 0) at hf

Premises used: HSub.hSub, OfNat.ofNat, CauSeq.LimZero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : (f - 0).LimZero
⊢ LimZero (f + g - g)

Tactic:
simpa only [sub_zero, add_sub_cancel_right] using hf

Premises used: sub_zero, add_sub_cancel_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ f + g ≈ g

Tactic:
have hfg' : f + g ≈ g := by
        change LimZero (f - 0) at hf
        change LimZero (f + g - g); · simpa only [sub_zero, add_sub_cancel_right] using hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
⊢ (f + g).norm = g.norm

Tactic:
have hcfg : (f + g).norm = g.norm := norm_equiv hfg'
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
⊢ f.norm = 0

Tactic:
have hcl : f.norm = 0 := (norm_zero_iff f).2 hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
rw : max 0 g.norm = g.norm
⊢ max f.norm g.norm = g.norm

Tactic:
rw [hcl]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ max 0 g.norm = g.norm

Tactic:
max_eq_right (norm_nonneg _)

Premises used: PadicSeq.norm_nonneg, max_eq_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ max 0 g.norm = g.norm

Tactic:
exact max_eq_right (norm_nonneg _)

Premises used: PadicSeq.norm_nonneg, max_eq_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ max f.norm g.norm = g.norm

Tactic:
have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
this : max f.norm g.norm = g.norm
rw : (f + g).norm ≤ g.norm
rw₁ rw₂ : g.norm ≤ g.norm
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
rw [this, hcfg]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ (g - 0).LimZero

Tactic:
change LimZero (g - 0) at hg

Premises used: HSub.hSub, OfNat.ofNat, CauSeq.LimZero