Theorem: Set.ext (CategoryTheory/Set.lean)

State before:
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
⊢ a = b
Tactic:
rw [mk.injEq]
State after:
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
⊢ a.mem = b.mem

State before:
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
⊢ a.mem = b.mem
Tactic:
funext x
State after:
case h
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
x : α
⊢ mem a x = mem b x

State before:
case h
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
x : α
⊢ mem a x = mem b x
Tactic:
exact propext (h x)
State after:
no goals