n : PosNum
h : 1 < n
⊢ ↑(Num.casesOn (pred' n) 1 id) = Nat.pred ↑n
n : PosNum
h : 1 < n
⊢ ↑(pred n) = Nat.pred ↑n
unfold pred
case zero
n : PosNum
h : 1 < n
e : pred' n = zero
⊢ ↑(Num.casesOn zero 1 id) = Nat.pred ↑n

case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : pred' n = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = Nat.pred ↑n
n : PosNum
h : 1 < n
⊢ ↑(Num.casesOn (pred' n) 1 id) = Nat.pred ↑n
cases e : pred' n
case zero
n : PosNum
h : 1 < n
e : pred' n = zero
this : 1 ≤ Nat.pred ↑n
⊢ ↑(Num.casesOn zero 1 id) = Nat.pred ↑n
case zero
n : PosNum
h : 1 < n
e : pred' n = zero
⊢ ↑(Num.casesOn zero 1 id) = Nat.pred ↑n
have : (1 : ℕ) ≤ Nat.pred n := Nat.pred_le_pred ((@cast_lt ℕ _ _ _).2 h)
case zero
n : PosNum
h : 1 < n
e : pred' n = zero
this : 1 ≤ ↑zero
⊢ ↑(Num.casesOn zero 1 id) = Nat.pred ↑n
case zero
n : PosNum
h : 1 < n
e : pred' n = zero
this : 1 ≤ Nat.pred ↑n
⊢ ↑(Num.casesOn zero 1 id) = Nat.pred ↑n
rw [← pred'_to_nat, e] at this
no goals
case zero
n : PosNum
h : 1 < n
e : pred' n = zero
this : 1 ≤ ↑zero
⊢ ↑(Num.casesOn zero 1 id) = Nat.pred ↑n
exact absurd this (by decide)
no goals
n : PosNum
h : 1 < n
e : pred' n = zero
this : 1 ≤ ↑zero
⊢ ¬1 ≤ ↑zero
decide
case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : pred' n = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = ↑(pos a✝)
case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : pred' n = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = Nat.pred ↑n
rw [← pred'_to_nat, e]
no goals
case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : pred' n = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = ↑(pos a✝)
rfl