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:
constructor
State after:
case mp
α : Type u_1
s t : Set α
⊢ s = t → ∀ (x : α), x ∈ s ↔ x ∈ t

case mpr
α : Type u_1
s t : Set α
⊢ (∀ (x : α), x ∈ s ↔ x ∈ t) → s = t

State before:
case mp
α : Type u_1
s t : Set α
⊢ s = t → ∀ (x : α), x ∈ s ↔ x ∈ t
Tactic:
intro h x
State after:
case mp
α : Type u_1
s t : Set α
h : s = t
x : α
⊢ x ∈ s ↔ x ∈ t

State before:
case mp
α : Type u_1
s t : Set α
h : s = t
x : α
⊢ x ∈ s ↔ x ∈ t
Tactic:
rw [h]
State after:
no goals

State before:
case mpr
α : Type u_1
s t : Set α
⊢ (∀ (x : α), x ∈ s ↔ x ∈ t) → s = t
Tactic:
intro h
State after:
case mpr
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
⊢ s = t

State before:
case mpr
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
⊢ s = t
Tactic:
funext x
State after:
case mpr.h
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
x : α
⊢ s x = t x

State before:
case mpr.h
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
x : α
⊢ s x = t x
Tactic:
apply propext
State after:
case mpr.h.a
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
x : α
⊢ s x ↔ t x

State before:
case mpr.h.a
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
x : α
⊢ s x ↔ t x
Tactic:
exact h x
State after:
no goals