Theorem: nat_subset_real (meetings/ex1.lean)

State before:
⊢ heterogeneous_subset Set.univ Set.univ
Tactic:
intro n _
State after:
n : ℕ
a✝ : n ∈ Set.univ
⊢ Coe.coe n ∈ Set.univ

State before:
n : ℕ
a✝ : n ∈ Set.univ
⊢ Coe.coe n ∈ Set.univ
Tactic:
simp only [Set.mem_univ]
State after:
no goals