case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.12185
r s t : Set (α × α)
a b : α
⊢ (a, b) ∈ r ○ s ○ t ↔ (a, b) ∈ r ○ (s ○ t)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.12185
r s t : Set (α × α)
⊢ r ○ s ○ t = r ○ (s ○ t)
ext ⟨a, b⟩
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.12185
r s t : Set (α × α)
a b : α
⊢ (∃ z, (∃ z_1, (a, z_1) ∈ r ∧ (z_1, z) ∈ s) ∧ (z, b) ∈ t) ↔ ∃ z, (a, z) ∈ r ∧ ∃ z_1, (z, z_1) ∈ s ∧ (z_1, b) ∈ t
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.12185
r s t : Set (α × α)
a b : α
⊢ (a, b) ∈ r ○ s ○ t ↔ (a, b) ∈ r ○ (s ○ t)
simp only [mem_compRel]
no goals
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.12185
r s t : Set (α × α)
a b : α
⊢ (∃ z, (∃ z_1, (a, z_1) ∈ r ∧ (z_1, z) ∈ s) ∧ (z, b) ∈ t) ↔ ∃ z, (a, z) ∈ r ∧ ∃ z_1, (z, z_1) ∈ s ∧ (z_1, b) ∈ t
tauto