p : ℕ
hp : Fact (Nat.Prime p)
⊢ (if h : const (padicNorm p) 1 ≈ 0 then (fun hf => 0) h
    else (fun hf => padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) h) =
    0
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation 1 = 0
change dite (CauSeq.const (padicNorm p) 1 ≈ _) _ _ = _
p : ℕ
hp : Fact (Nat.Prime p)
h : ¬const (padicNorm p) 1 ≈ 0
⊢ (if h : const (padicNorm p) 1 ≈ 0 then (fun hf => 0) h
    else (fun hf => padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) h) =
    0
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (if h : const (padicNorm p) 1 ≈ 0 then (fun hf => 0) h
    else (fun hf => padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) h) =
    0
have h : ¬CauSeq.const (padicNorm p) 1 ≈ 0 := by
  intro H
  erw [const_equiv p] at H
  exact one_ne_zero H
p : ℕ
hp : Fact (Nat.Prime p)
h : ¬const (padicNorm p) 1 ≈ 0
⊢ (fun hf => padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) h = 0
p : ℕ
hp : Fact (Nat.Prime p)
h : ¬const (padicNorm p) 1 ≈ 0
⊢ (if h : const (padicNorm p) 1 ≈ 0 then (fun hf => 0) h
    else (fun hf => padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) h) =
    0
rw [dif_neg h]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
h : ¬const (padicNorm p) 1 ≈ 0
⊢ (fun hf => padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) h = 0
simp
p : ℕ
hp : Fact (Nat.Prime p)
H : const (padicNorm p) 1 ≈ 0
⊢ False
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬const (padicNorm p) 1 ≈ 0
intro H
p : ℕ
hp : Fact (Nat.Prime p)
H : 1 = 0
⊢ False
p : ℕ
hp : Fact (Nat.Prime p)
H : const (padicNorm p) 1 ≈ 0
⊢ False
erw [const_equiv p] at H
no goals
p : ℕ
hp : Fact (Nat.Prime p)
H : 1 = 0
⊢ False
exact one_ne_zero H