Theorem: MyDefs.Set.ext' (HausdorffSchool/Session2_Sets_Fns_Logic/Tutorial2.lean)

State before:
α : Type u_1
s t : Set α
⊢ s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
Tactic:
conv =>
  rhs
  ext
  rw [← eq_iff_iff]
State after:
α : Type u_1
s t : Set α
⊢ s = t ↔ ∀ (x : α), (x ∈ s) = (x ∈ t)

State before:
α : Type u_1
s t : Set α
⊢ s = t ↔ ∀ (x : α), (x ∈ s) = (x ∈ t)
Tactic:
exact Function.funext_iff
State after:
no goals