α : Type u
β : Type v
γ : Type w
δ : Type ?u.312157
ι : Sort x
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ a ≤ comap f b
α : Type u
β : Type v
γ : Type w
δ : Type ?u.312157
ι : Sort x
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : Tendsto (g ∘ f) a c
hg : comap g c ≤ b
⊢ Tendsto f a b
rw [tendsto_iff_comap] at hfg⊢
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.312157
ι : Sort x
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ a ≤ comap f b
calc
  a ≤ comap (g ∘ f) c := hfg
  _ ≤ comap f b := by simpa [comap_comap] using comap_mono hg
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.312157
ι : Sort x
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ comap (g ∘ f) c ≤ comap f b
simpa [comap_comap] using comap_mono hg