α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
⊢ a ∈ maximals r s ∪ maximals r t
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
⊢ maximals r (s ∪ t) ⊆ maximals r s ∪ maximals r t
intro a ha
case inl
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
h : a ∈ s
⊢ a ∈ maximals r s ∪ maximals r t

case inr
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
h : a ∈ t
⊢ a ∈ maximals r s ∪ maximals r t
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
⊢ a ∈ maximals r s ∪ maximals r t
obtain h | h := ha.1
no goals
case inl
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
h : a ∈ s
⊢ a ∈ maximals r s ∪ maximals r t
exact Or.inl ⟨h, fun b hb => ha.2 <| Or.inl hb⟩
no goals
case inr
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
h : a ∈ t
⊢ a ∈ maximals r s ∪ maximals r t
exact Or.inr ⟨h, fun b hb => ha.2 <| Or.inr hb⟩