α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (fun x z => ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y z) = fun x z => ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 z
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (r • s) • t = r • s • t
unfold comp
case a.h.a
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) ↔ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (fun x z => ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y z) = fun x z => ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 z
ext (x w)
case a.h.a.mp
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) → ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w

case a.h.a.mpr
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w) → ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w
case a.h.a
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) ↔ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
constructor
case a.h.a.mp.intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
z : γ
tzw : t z w
y : β
rxy : r x y
syz : s y z
⊢ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
case a.h.a.mp
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) → ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
rintro ⟨z, ⟨y, rxy, syz⟩, tzw⟩
no goals
case a.h.a.mp.intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
z : γ
tzw : t z w
y : β
rxy : r x y
syz : s y z
⊢ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
exact ⟨y, rxy, z, syz, tzw⟩
case a.h.a.mpr.intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
y : β
rxy : r x y
z : γ
syz : s y z
tzw : t z w
⊢ ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w
case a.h.a.mpr
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w) → ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w
rintro ⟨y, rxy, z, syz, tzw⟩
no goals
case a.h.a.mpr.intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
r✝ : Rel α β
δ : Type u_1
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
y : β
rxy : r x y
z : γ
syz : s y z
tzw : t z w
⊢ ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w
exact ⟨z, ⟨y, rxy, syz⟩, tzw⟩