p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ norm f = norm g
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
⊢ norm f = norm g
have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
no goals
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ norm f = norm g
simp [norm, hf, hg]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ norm f = norm g
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
⊢ norm f = norm g
have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) =
    if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ norm f = norm g
unfold norm
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))
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) =
    if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))
split_ifs
no goals
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))
exact norm_eq_of_equiv hf hg hfg