α : Type u_1
β : Type u_2
γ : Type ?u.17832
δ : Type ?u.17835
ι : Sort ?u.17838
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
α : Type u_1
β : Type u_2
γ : Type ?u.17832
δ : Type ?u.17835
ι : Sort ?u.17838
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
⊢ f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂
refine' ⟨fun h => _, fun h => h.1 ▸ h.2 ▸ rfl⟩
α : Type u_1
β : Type u_2
γ : Type ?u.17832
δ : Type ?u.17835
ι : Sort ?u.17838
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
α : Type u_1
β : Type u_2
γ : Type ?u.17832
δ : Type ?u.17835
ι : Sort ?u.17838
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le
α : Type u_1
β : Type u_2
γ : Type ?u.17832
δ : Type ?u.17835
ι : Sort ?u.17838
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this : NeBot f₂
⊢ f₁ = f₂ ∧ g₁ = g₂
α : Type u_1
β : Type u_2
γ : Type ?u.17832
δ : Type ?u.17835
ι : Sort ?u.17838
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
haveI := neBot_of_le hle.1
α : Type u_1
β : Type u_2
γ : Type ?u.17832
δ : Type ?u.17835
ι : Sort ?u.17838
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this✝ : NeBot f₂
this : NeBot g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
α : Type u_1
β : Type u_2
γ : Type ?u.17832
δ : Type ?u.17835
ι : Sort ?u.17838
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this : NeBot f₂
⊢ f₁ = f₂ ∧ g₁ = g₂
haveI := neBot_of_le hle.2
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.17832
δ : Type ?u.17835
ι : Sort ?u.17838
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this✝ : NeBot f₂
this : NeBot g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
exact ⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩