-- 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:
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 i) < padicNorm p (↑f i)

Tactic:
apply lt_of_lt_of_le hN'

Result:
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)

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))
i : ℕ := N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)
hi : N ≤ i
⊢ False

Tactic:
have hN' := hN _ hi

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)
hi : N ≤ i
hN' : padicNorm p (↑(f - g) i) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (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 (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

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

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)
this : padicNorm p (↑f i) < padicNorm p (↑f i)
⊢ 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))
i : ℕ := N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)
hi : N ≤ i
hN' : padicNorm p (↑(f - g) i) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
⊢ False

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

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 - g) i) <
    padicNorm p (↑f (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg))) -
      padicNorm p (↑g (N ⊔ (stationaryPoint hf ⊔ stationaryPoint hg)))
⊢ False