α : Type u
β : Type v
γ : Type w
δ : Type ?u.256455
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
m : α → β
⊢ f ⊓ 𝓟 (range m) ≤ map m (comap m f)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.256455
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
m : α → β
⊢ map m (comap m f) = f ⊓ 𝓟 (range m)
refine' le_antisymm (le_inf map_comap_le <| le_principal_iff.2 range_mem_map) _
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.256455
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t✝ : Set β
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t' ∈ f ⊓ 𝓟 (range m)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.256455
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
m : α → β
⊢ f ⊓ 𝓟 (range m) ≤ map m (comap m f)
rintro t' ⟨t, ht, sub⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.256455
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t✝ : Set β
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t ⊆ {x | x ∈ range m → x ∈ t'}
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.256455
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t✝ : Set β
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t' ∈ f ⊓ 𝓟 (range m)
refine' mem_inf_principal.2 (mem_of_superset ht _)
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.256455
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t✝ : Set β
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
x : α
hxt : m x ∈ t
⊢ m x ∈ t'
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.256455
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t✝ : Set β
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t ⊆ {x | x ∈ range m → x ∈ t'}
rintro _ hxt ⟨x, rfl⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.256455
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t✝ : Set β
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
x : α
hxt : m x ∈ t
⊢ m x ∈ t'
exact sub hxt