case mk
val✝ : ℕ
property✝ : 0 < val✝
⊢ ↑(↑factorizationEquiv { val := val✝, property := property✝ }) = factorization ↑{ val := val✝, property := property✝ }
n : ℕ+
⊢ ↑(↑factorizationEquiv n) = factorization ↑n
cases n
no goals
case mk
val✝ : ℕ
property✝ : 0 < val✝
⊢ ↑(↑factorizationEquiv { val := val✝, property := property✝ }) = factorization ↑{ val := val✝, property := property✝ }
rfl