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))
⊢ False
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
by_contra h
case inl
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

case inr
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ False
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))
⊢ False
cases'
  Decidable.em
    (padicNorm p (g (stationaryPoint hg)) < padicNorm p (f (stationaryPoint hf))) with
  hlt hnlt
no goals
case inl
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
exact norm_eq_of_equiv_aux hf hg hfg h hlt
case inr
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) < padicNorm p (↑g (stationaryPoint hg))
case inr
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ False
apply norm_eq_of_equiv_aux hg hf (Setoid.symm hfg) (Ne.symm h)
case inr.a
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) ≤ padicNorm p (↑g (stationaryPoint hg))

case inr.a
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
case inr
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) < padicNorm p (↑g (stationaryPoint hg))
apply lt_of_le_of_ne
case inr.a
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
case inr.a
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) ≤ padicNorm p (↑g (stationaryPoint hg))

case inr.a
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
apply le_of_not_gt hnlt
no goals
case inr.a
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))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
apply h