-- Mathlib/Order/Filter/Partial.lean
theorem rcomap_rcomap (r : Rel α β) (s : Rel β γ) (l : Filter γ) :
    rcomap r (rcomap s l) = rcomap (r.comp s) l :=
  filter_eq <| by
    ext t; simp only [rcomap_sets, Rel.image, Filter.mem_sets, Set.mem_setOf_eq, Rel.core_comp]
    constructor
    · rintro ⟨u, ⟨v, vsets, hv⟩, h⟩
      exact ⟨v, vsets, Set.Subset.trans (Rel.core_mono _ hv) h⟩
    rintro ⟨t, tsets, ht⟩
    exact ⟨Rel.core s t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩

Proof state:
case h.mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t) → ∃ x ∈ l, r.core (s.core x) ⊆ t

Tactic:
rintro ⟨u, ⟨v, vsets, hv⟩, h⟩

Result:
case h.mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
u : Set β
h : r.core u ⊆ t
v : Set γ
vsets : v ∈ l
hv : s.core v ⊆ u
⊢ ∃ x ∈ l, r.core (s.core x) ⊆ t

Proof state:
case h.mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
u : Set β
h : r.core u ⊆ t
v : Set γ
vsets : v ∈ l
hv : s.core v ⊆ u
⊢ ∃ x ∈ l, r.core (s.core x) ⊆ t

Tactic:
exact ⟨v, vsets, Set.Subset.trans (Rel.core_mono _ hv) h⟩

Result:
no goals

Proof state:
case h.mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x ∈ l, r.core (s.core x) ⊆ t) → ∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t

Tactic:
rintro ⟨t, tsets, ht⟩

Result:
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 : r.core (s.core t) ⊆ t✝
⊢ ∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t✝

Proof state:
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
⊢ (rcomap r (rcomap s l)).sets = (rcomap (r.comp s) l).sets

Tactic:
ext t

Result:
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 (r.comp s) l).sets

Proof state:
case h
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t) ↔ ∃ x ∈ l, r.core (s.core x) ⊆ t

Tactic:
constructor

Result:
case h.mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t) → ∃ x ∈ l, r.core (s.core x) ⊆ t

case h.mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x ∈ l, r.core (s.core x) ⊆ t) → ∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t

Proof state:
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 (r.comp s) l).sets

Tactic:
simp only [rcomap_sets, Rel.image, Filter.mem_sets, Set.mem_setOf_eq, Rel.core_comp]

Result:
case h
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter γ
t : Set α
⊢ (∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t) ↔ ∃ x ∈ l, r.core (s.core x) ⊆ t

Proof state:
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 : r.core (s.core t) ⊆ t✝
⊢ ∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t✝

Tactic:
exact ⟨Rel.core s t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩

Result:
no goals