-- 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
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

Tactic:
exact lt_irrefl _ this

Result:
no goals

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)
⊢ False

Tactic:
have hi : N ≤ i := le_max_left _ _

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
⊢ False

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))
⊢ False

Tactic:
have hpn : 0 < padicNorm p (f (stationaryPoint hf)) - padicNorm p (g (stationaryPoint hg)) :=
  sub_pos_of_lt hlt

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

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

Tactic:
apply padicNorm.nonneg

Result:
no goals

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)))
⊢ False

Tactic:
have hpne : padicNorm p (f i) ≠ padicNorm p (-g i) := by rwa [← padicNorm.neg (g i)] at h

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)))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ False