What is tauto doing?

Stream: new members

[Mike]

The first example is solved by applying tauto,
but I don't know why it works.

example {α : Type*} (n : α → Filter α)
  (H : ∀ a : α, ∀ p : α → Prop, (∀ᶠ x in n a, p x) → ∀ᶠ y in n a, ∀ᶠ x in n y, p x) :
  ∀ a, ∀ s ∈ n a, {y | s ∈ n y} ∈ n a := by
  intro a s s_in_na
  tauto

The second example is nearly the same, but
tauto won't work on its own. Is there a
way to see what tauto is doing in the above
example, so it can be mimicked in the second?

example {α : Type*}
  (n : α → Filter α)
  (H : ∀ a : α, ∀ p : α → Prop, (∀ᶠ x in n a, p x) → ∀ᶠ y in n a, ∀ᶠ x in n y, p x)
  (a : α)
  (s : Set α)
  (s_in_na : s ∈ n a)
  (t : Set α)
  (t_def : t = {x | s ∈ n x})
  :
  t ∈ n a := by
  sorry

[Kyle Miller]

tauto doesn't know about equations. Maybe start with subst t then do tauto?