no goals
α : Type ?u.103890
β : Type ?u.103893
γ : Type ?u.103896
n : ℕ
⊢ ¬0 ∈ map { toFun := succ, inj' := (_ : Injective succ) } univ
simp [map_eq_image]
no goals
α : Type ?u.103890
β : Type ?u.103893
γ : Type ?u.103896
n : ℕ
⊢ univ =
    cons 0 (map { toFun := succ, inj' := (_ : Injective succ) } univ)
      (_ : ¬0 ∈ map { toFun := succ, inj' := (_ : Injective succ) } univ)
simp [map_eq_image]