α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ (Filter.lift f₁ fun s => Filter.lift (g₁ s) fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) =
    Filter.lift f₁ fun s => Filter.lift f₂ fun t => Filter.lift (g₁ s) fun s => Filter.lift' (g₂ t) fun t => s ×ˢ t
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ Filter.lift f₁ g₁ ×ˢ Filter.lift f₂ g₂ = Filter.lift f₁ fun s => Filter.lift f₂ fun t => g₁ s ×ˢ g₂ t
simp only [prod_def, lift_assoc hg₁]
case h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ (fun s => Filter.lift (g₁ s) fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) = fun s =>
    Filter.lift f₂ fun t => Filter.lift (g₁ s) fun s => Filter.lift' (g₂ t) fun t => s ×ˢ t
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ (Filter.lift f₁ fun s => Filter.lift (g₁ s) fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) =
    Filter.lift f₁ fun s => Filter.lift f₂ fun t => Filter.lift (g₁ s) fun s => Filter.lift' (g₂ t) fun t => s ×ˢ t
apply congr_arg
case h.h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ (Filter.lift (g₁ x) fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) =
    Filter.lift f₂ fun t => Filter.lift (g₁ x) fun s => Filter.lift' (g₂ t) fun t => s ×ˢ t
case h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ (fun s => Filter.lift (g₁ s) fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) = fun s =>
    Filter.lift f₂ fun t => Filter.lift (g₁ s) fun s => Filter.lift' (g₂ t) fun t => s ×ˢ t
funext x
case h.h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ (Filter.lift (g₁ x) fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) =
    Filter.lift (g₁ x) fun t => Filter.lift f₂ fun s => Filter.lift' (g₂ s) fun t_1 => t ×ˢ t_1
case h.h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ (Filter.lift (g₁ x) fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) =
    Filter.lift f₂ fun t => Filter.lift (g₁ x) fun s => Filter.lift' (g₂ t) fun t => s ×ˢ t
rw [lift_comm]
case h.h.h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ (fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) = fun t =>
    Filter.lift f₂ fun s => Filter.lift' (g₂ s) fun t_1 => t ×ˢ t_1
case h.h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ (Filter.lift (g₁ x) fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) =
    Filter.lift (g₁ x) fun t => Filter.lift f₂ fun s => Filter.lift' (g₂ s) fun t_1 => t ×ˢ t_1
apply congr_arg
case h.h.h.h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
y : Set β₁
⊢ (Filter.lift' (Filter.lift f₂ g₂) fun t => y ×ˢ t) = Filter.lift f₂ fun s => Filter.lift' (g₂ s) fun t => y ×ˢ t
case h.h.h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ (fun s => Filter.lift' (Filter.lift f₂ g₂) fun t => s ×ˢ t) = fun t =>
    Filter.lift f₂ fun s => Filter.lift' (g₂ s) fun t_1 => t ×ˢ t_1
funext y
no goals
case h.h.h.h
α : Type ?u.48775
β : Type ?u.48778
γ : Type ?u.48781
ι : Sort ?u.48784
f : Filter α
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
y : Set β₁
⊢ (Filter.lift' (Filter.lift f₂ g₂) fun t => y ×ˢ t) = Filter.lift f₂ fun s => Filter.lift' (g₂ s) fun t => y ×ˢ t
apply lift'_lift_assoc hg₂