α : Type u_1
β : Type u_2
γ : Type ?u.44318
ι : Sort ?u.44321
f✝ f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (⨅ (i : Bool), Filter.lift' (bif i then f else g) s) = ⨅ (b : Bool), bif b then Filter.lift' f s else Filter.lift' g s
α : Type u_1
β : Type u_2
γ : Type ?u.44318
ι : Sort ?u.44321
f✝ f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ Filter.lift' (f ⊓ g) s = Filter.lift' f s ⊓ Filter.lift' g s
rw [inf_eq_iInf, inf_eq_iInf, lift'_iInf hs]
α : Type u_1
β : Type u_2
γ : Type ?u.44318
ι : Sort ?u.44321
f✝ f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ∀ (i : Bool), Filter.lift' (bif i then f else g) s = bif i then Filter.lift' f s else Filter.lift' g s
α : Type u_1
β : Type u_2
γ : Type ?u.44318
ι : Sort ?u.44321
f✝ f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (⨅ (i : Bool), Filter.lift' (bif i then f else g) s) = ⨅ (b : Bool), bif b then Filter.lift' f s else Filter.lift' g s
refine iInf_congr ?_
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.44318
ι : Sort ?u.44321
f✝ f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ∀ (i : Bool), Filter.lift' (bif i then f else g) s = bif i then Filter.lift' f s else Filter.lift' g s
rintro (_|_) <;> rfl