n : ℕ
⊢ decodeNat (encodeNat n) = n
⊢ ∀ (n : ℕ), decodeNat (encodeNat n) = n
intro n
n : ℕ
⊢ decodeNat (encodeNat n) = ↑↑n
n : ℕ
⊢ decodeNat (encodeNat n) = n
conv_rhs => rw [← Num.to_of_nat n]
no goals
n : ℕ
⊢ decodeNat (encodeNat n) = ↑↑n
exact congr_arg ((↑) : Num → ℕ) (decode_encodeNum n)