case mk
α : Type u_3
β : Type ?u.5122
σ : Type u_1
τ : Type u_2
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
a : τ
f✝ : σ → α
pt✝ : σ
inf✝ : σ → σ → σ
inf_le_left✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ a
inf_le_right✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ b
⊢ f (ofEquiv E { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }) a =
    f { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ } (↑E.symm a)
α : Type u_3
β : Type ?u.5122
σ : Type u_1
τ : Type u_2
inst✝ : PartialOrder α
F✝ : CFilter α σ
E : σ ≃ τ
F : CFilter α σ
a : τ
⊢ f (ofEquiv E F) a = f F (↑E.symm a)
cases F
no goals
case mk
α : Type u_3
β : Type ?u.5122
σ : Type u_1
τ : Type u_2
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
a : τ
f✝ : σ → α
pt✝ : σ
inf✝ : σ → σ → σ
inf_le_left✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ a
inf_le_right✝ : ∀ (a b : σ), f✝ (inf✝ a b) ≤ f✝ b
⊢ f (ofEquiv E { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ }) a =
    f { f := f✝, pt := pt✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝ } (↑E.symm a)
rfl