α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets,
        univ_sets := (_ : ∃ x, x ∈ l₂.sets ∧ (fun s t => Rel.preimage r s ⊆ t) x Set.univ),
        sets_of_superset :=
          (_ :
            ∀ {x y : Set α},
              x ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets →
                x ⊆ y → y ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets →
                y ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets →
                  x ∩ y ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets) } ↔
    ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto' r l₁ l₂ ↔ ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
unfold RTendsto' rcomap'
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.preimage r x_1 ⊆ x → x ∈ l₁) ↔
    ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets,
        univ_sets := (_ : ∃ x, x ∈ l₂.sets ∧ (fun s t => Rel.preimage r s ⊆ t) x Set.univ),
        sets_of_superset :=
          (_ :
            ∀ {x y : Set α},
              x ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets →
                x ⊆ y → y ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets),
        inter_sets :=
          (_ :
            ∀ {x y : Set α},
              x ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets →
                y ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets →
                  x ∩ y ∈ Rel.image (fun s t => Rel.preimage r s ⊆ t) l₂.sets) } ↔
    ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
simp [le_def, Rel.mem_image]
case mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.preimage r x_1 ⊆ x → x ∈ l₁) →
    ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁

case mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁) →
    ∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.preimage r x_1 ⊆ x → x ∈ l₁
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.preimage r x_1 ⊆ x → x ∈ l₁) ↔
    ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
constructor
no goals
case mp
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.preimage r x_1 ⊆ x → x ∈ l₁) →
    ∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁
exact fun h s hs => h _ _ hs Set.Subset.rfl
no goals
case mpr
α : Type u
β : Type v
γ : Type w
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ (s : Set β), s ∈ l₂ → Rel.preimage r s ∈ l₁) →
    ∀ (x : Set α) (x_1 : Set β), x_1 ∈ l₂ → Rel.preimage r x_1 ⊆ x → x ∈ l₁
exact fun h s t ht => mem_of_superset (h t ht)