-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_eq_of_equiv_aux {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

Proof state:
case intro
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))
⊢ False

Tactic:
let i := max N (max (stationaryPoint hf) (stationaryPoint hg))

Result:
case intro
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 : ℕ := N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)
⊢ False

Proof state:
case intro
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 (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
h :
  padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) ≠
    padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)
hi : N ≤ i
hN' :
  padicNorm p (↑(f - g) i) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) -
      padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ False

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'

Result:
case intro
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 (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
h :
  padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) ≠
    padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)
hi : N ≤ i
hN' :
  padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) -
      padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ False

Proof state:
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 (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
h :
  padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) ≠
    padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)
hi : N ≤ i
hN' :
  padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) -
      padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) -
      padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) ≤
    padicNorm p (↑f i)

Tactic:
apply sub_le_self

Result:
case a
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 (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
h :
  padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) ≠
    padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)
hi : N ≤ i
hN' :
  padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) -
      padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ 0 ≤ padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))

Proof state:
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

Tactic:
obtain ⟨N, hN⟩ := hfg _ hpn

Result:
case intro
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))
⊢ False

Proof state:
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 (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
h :
  padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) ≠
    padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)
hi : N ≤ i
hN' :
  padicNorm p (↑(f - g) i) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) -
      padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
⊢ padicNorm p (↑f i) ≠ padicNorm p (-↑g i)

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

Result:
no goals