case h
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ z ∈ image (r • s) t ↔ z ∈ image s (image r t)
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
⊢ image (r • s) t = image s (image r t)
ext z
case h
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, x ∈ t ∧ (r • s) x z) ↔ ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
case h
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ z ∈ image (r • s) t ↔ z ∈ image s (image r t)
simp only [mem_image]
case h.mp
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, x ∈ t ∧ (r • s) x z) → ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z

case h.mpr
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z) → ∃ x, x ∈ t ∧ (r • s) x z
case h
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, x ∈ t ∧ (r • s) x z) ↔ ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
constructor
case h.mp.intro.intro.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
x : α
xt : x ∈ t
y : β
rxy : r x y
syz : s y z
⊢ ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
case h.mp
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, x ∈ t ∧ (r • s) x z) → ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
rintro ⟨x, xt, y, rxy, syz⟩
no goals
case h.mp.intro.intro.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
x : α
xt : x ∈ t
y : β
rxy : r x y
syz : s y z
⊢ ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
exact ⟨y, ⟨x, xt, rxy⟩, syz⟩
case h.mpr.intro.intro.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
y : β
syz : s y z
x : α
xt : x ∈ t
rxy : r x y
⊢ ∃ x, x ∈ t ∧ (r • s) x z
case h.mpr
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z) → ∃ x, x ∈ t ∧ (r • s) x z
rintro ⟨y, ⟨x, xt, rxy⟩, syz⟩
no goals
case h.mpr.intro.intro.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
r : Rel α β
s : Rel β γ
t : Set α
z : γ
y : β
syz : s y z
x : α
xt : x ∈ t
rxy : r x y
⊢ ∃ x, x ∈ t ∧ (r • s) x z
exact ⟨x, xt, y, rxy, syz⟩