case intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.282207
ι : Sort x
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter ↑t
⊢ map m (map Subtype.val f ⊓ g) = map m (map Subtype.val f) ⊓ map m g
α : Type u
β : Type v
γ : Type w
δ : Type ?u.282207
ι : Sort x
f g : Filter α
m : α → β
t : Set α
htf : t ∈ f
htg : t ∈ g
h : InjOn m t
⊢ map m (f ⊓ g) = map m f ⊓ map m g
lift f to Filter t using htf
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.282207
ι : Sort x
m : α → β
t : Set α
h : InjOn m t
f g : Filter ↑t
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)
case intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.282207
ι : Sort x
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter ↑t
⊢ map m (map Subtype.val f ⊓ g) = map m (map Subtype.val f) ⊓ map m g
lift g to Filter t using htg
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.282207
ι : Sort x
m : α → β
t : Set α
f g : Filter ↑t
h : Injective (m ∘ Subtype.val)
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.282207
ι : Sort x
m : α → β
t : Set α
h : InjOn m t
f g : Filter ↑t
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)
replace h : Injective (m ∘ ((↑) : t → α)) := h.injective
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.282207
ι : Sort x
m : α → β
t : Set α
f g : Filter ↑t
h : Injective (m ∘ Subtype.val)
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)
simp only [map_map, ← map_inf Subtype.coe_injective, map_inf h]