Theorem: Set.union_subset_union (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₁.union t₁).Subset (s₂.union t₂)
Tactic:
intro hs ht x
State after:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
⊢ x ∈ s₁.union t₁ → x ∈ s₂.union t₂

State before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
⊢ x ∈ s₁.union t₁ → x ∈ s₂.union t₂
Tactic:
intro
| Or.inl hs₁ =>
  left
  exact hs x hs₁
| Or.inr ht₁ =>
  right
  exact ht x ht₁
State after:
no goals

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

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

State before:
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
x✝ : x ∈ s₁.union t₁
ht₁ : x ∈ t₁
⊢ x ∈ s₂.union t₂
Tactic:
right
State after:
case h
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
x✝ : x ∈ s₁.union t₁
ht₁ : x ∈ t₁
⊢ x ∈ t₂

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