case h
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ t ∈ (rcomap r (rcomap s l)).sets ↔ t ∈ (rcomap (Rel.comp r s) l).sets
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
⊢ (rcomap r (rcomap s l)).sets = (rcomap (Rel.comp r s) l).sets
ext t
case h
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x, (∃ x_1, x_1 ∈ l ∧ Rel.core s x_1 ⊆ x) ∧ Rel.core r x ⊆ t) ↔ ∃ x, x ∈ l ∧ Rel.core r (Rel.core s x) ⊆ t
case h
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ t ∈ (rcomap r (rcomap s l)).sets ↔ t ∈ (rcomap (Rel.comp r s) l).sets
simp [rcomap_sets, Rel.image, Rel.core_comp]
case h.mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x, (∃ x_1, x_1 ∈ l ∧ Rel.core s x_1 ⊆ x) ∧ Rel.core r x ⊆ t) → ∃ x, x ∈ l ∧ Rel.core r (Rel.core s x) ⊆ t

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