Theorem: Set.inter_subset_inter (GMLInit/Data/Set/Subset.lean)

State before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
⊢ s₁.Subset s₂ → t₁.Subset t₂ → (s₁.inter t₁).Subset (s₂.inter t₂)
Tactic:
intro hs ht x ⟨hs₁,ht₁⟩
State after:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂.inter t₂

State before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂.inter t₂
Tactic:
constructor
State after:
case left
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂

case right
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ t₂

State before:
case left
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂
Tactic:
exact hs x hs₁
State after:
no goals

State before:
case right
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
hs₁ : x ∈ s₁
ht₁ : x ∈ t₁
⊢ x ∈ t₂
Tactic:
exact ht x ht₁
State after:
no goals