α : Type u_1
β : Type ?u.34632
γ : Type ?u.34635
p : α → Prop
a b : α
h : p a ∧ p b
c : α
hc : c ∈ Quotient.mk (Rel.setoid α) (a, b)
⊢ p c
α : Type u_1
β : Type ?u.34632
γ : Type ?u.34635
p : α → Prop
a b : α
⊢ (∀ (c : α), c ∈ Quotient.mk (Rel.setoid α) (a, b) → p c) ↔ p a ∧ p b
refine' ⟨fun h => ⟨h _ <| mem_mk''_left _ _, h _ <| mem_mk''_right _ _⟩, fun h c hc => _⟩
case inl
α : Type u_1
β : Type ?u.34632
γ : Type ?u.34635
p : α → Prop
b c : α
h : p c ∧ p b
hc : c ∈ Quotient.mk (Rel.setoid α) (c, b)
⊢ p c

case inr
α : Type u_1
β : Type ?u.34632
γ : Type ?u.34635
p : α → Prop
a c : α
h : p a ∧ p c
hc : c ∈ Quotient.mk (Rel.setoid α) (a, c)
⊢ p c
α : Type u_1
β : Type ?u.34632
γ : Type ?u.34635
p : α → Prop
a b : α
h : p a ∧ p b
c : α
hc : c ∈ Quotient.mk (Rel.setoid α) (a, b)
⊢ p c
obtain rfl | rfl := Sym2.mem_iff.1 hc
no goals
case inl
α : Type u_1
β : Type ?u.34632
γ : Type ?u.34635
p : α → Prop
b c : α
h : p c ∧ p b
hc : c ∈ Quotient.mk (Rel.setoid α) (c, b)
⊢ p c
exact h.1
no goals
case inr
α : Type u_1
β : Type ?u.34632
γ : Type ?u.34635
p : α → Prop
a c : α
h : p a ∧ p c
hc : c ∈ Quotient.mk (Rel.setoid α) (a, c)
⊢ p c
exact h.2