Theorem: Set.inter_assoc (GMLInit/Data/Set/Basic.lean)

State before:
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
⊢ (s.inter t).inter u = s.inter (t.inter u)
Tactic:
apply Set.ext
State after:
case a
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
⊢ ∀ (x : α), x ∈ (s.inter t).inter u ↔ x ∈ s.inter (t.inter u)

State before:
case a
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
⊢ ∀ (x : α), x ∈ (s.inter t).inter u ↔ x ∈ s.inter (t.inter u)
Tactic:
intro x
State after:
case a
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
⊢ x ∈ (s.inter t).inter u ↔ x ∈ s.inter (t.inter u)

State before:
case a
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
⊢ x ∈ (s.inter t).inter u ↔ x ∈ s.inter (t.inter u)
Tactic:
constructor
State after:
case a.mp
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
⊢ x ∈ (s.inter t).inter u → x ∈ s.inter (t.inter u)

case a.mpr
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
⊢ x ∈ s.inter (t.inter u) → x ∈ (s.inter t).inter u

State before:
case a.mp
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
⊢ x ∈ (s.inter t).inter u → x ∈ s.inter (t.inter u)
Tactic:
intro ⟨⟨hs, ht⟩, hu⟩
State after:
case a.mp
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
hs : x ∈ s
ht : x ∈ t
hu : x ∈ u
⊢ x ∈ s.inter (t.inter u)

State before:
case a.mp
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
hs : x ∈ s
ht : x ∈ t
hu : x ∈ u
⊢ x ∈ s.inter (t.inter u)
Tactic:
exact ⟨hs, ⟨ht, hu⟩⟩
State after:
no goals

State before:
case a.mpr
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
⊢ x ∈ s.inter (t.inter u) → x ∈ (s.inter t).inter u
Tactic:
intro ⟨hs, ⟨ht, hu⟩⟩
State after:
case a.mpr
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
hs : x ∈ s
ht : x ∈ t
hu : x ∈ u
⊢ x ∈ (s.inter t).inter u

State before:
case a.mpr
α : Sort u_1
β : ?m.20437
γ : ?m.20440
s t u : Set α
x : α
hs : x ∈ s
ht : x ∈ t
hu : x ∈ u
⊢ x ∈ (s.inter t).inter u
Tactic:
exact ⟨⟨hs, ht⟩, hu⟩
State after:
no goals