α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t, t ∈ l ∧ Rel.preimage s t ⊆ t_1) ∧ Rel.preimage r t_1 ⊆ t) ↔
    ∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ t ∈ rcomap' r (rcomap' s l) ↔ t ∈ rcomap' (Rel.comp r s) l
simp only [mem_rcomap', Rel.preimage_comp]
case mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t, t ∈ l ∧ Rel.preimage s t ⊆ t_1) ∧ Rel.preimage r t_1 ⊆ t) →
    ∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t

case mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t) →
    ∃ t_1, (∃ t, t ∈ l ∧ Rel.preimage s t ⊆ t_1) ∧ Rel.preimage r t_1 ⊆ t
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t, t ∈ l ∧ Rel.preimage s t ⊆ t_1) ∧ Rel.preimage r t_1 ⊆ t) ↔
    ∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t
constructor
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t✝ : Set α
t : Set γ
tsets : t ∈ l
ht : Rel.preimage r (Rel.preimage s t) ⊆ t✝
⊢ ∃ t, (∃ t_1, t_1 ∈ l ∧ Rel.preimage s t_1 ⊆ t) ∧ Rel.preimage r t ⊆ t✝
case mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t) →
    ∃ t_1, (∃ t, t ∈ l ∧ Rel.preimage s t ⊆ t_1) ∧ Rel.preimage r t_1 ⊆ t
rintro ⟨t, tsets, ht⟩
no goals
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t✝ : Set α
t : Set γ
tsets : t ∈ l
ht : Rel.preimage r (Rel.preimage s t) ⊆ t✝
⊢ ∃ t, (∃ t_1, t_1 ∈ l ∧ Rel.preimage s t_1 ⊆ t) ∧ Rel.preimage r t ⊆ t✝
exact ⟨s.preimage t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
u : Set β
h : Rel.preimage r u ⊆ t
v : Set γ
vsets : v ∈ l
hv : Rel.preimage s v ⊆ u
⊢ ∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t
case mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ t_1, (∃ t, t ∈ l ∧ Rel.preimage s t ⊆ t_1) ∧ Rel.preimage r t_1 ⊆ t) →
    ∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t
rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
no goals
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
u : Set β
h : Rel.preimage r u ⊆ t
v : Set γ
vsets : v ∈ l
hv : Rel.preimage s v ⊆ u
⊢ ∃ t_1, t_1 ∈ l ∧ Rel.preimage r (Rel.preimage s t_1) ⊆ t
exact ⟨v, vsets, (Rel.preimage_mono _ hv).trans h⟩