α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
⊢ ∀ (t : Set (α × β)), (∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) ↔ ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
⊢ HasBasis (la ×ˢ lb) p fun i => sa i ×ˢ sb i
simp only [hasBasis_iff, (hla.prod_pprod hlb).mem_iff]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
⊢ (∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) → ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
⊢ (∃ i, p i ∧ sa i ×ˢ sb i ⊆ t) → ∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
⊢ ∀ (t : Set (α × β)), (∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) ↔ ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t
refine' fun t => ⟨_, _⟩
case refine'_1.intro.mk.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p { fst := i, snd := j }.fst
hj : p { fst := i, snd := j }.snd
⊢ ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
⊢ (∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) → ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t
rintro ⟨⟨i, j⟩, ⟨hi, hj⟩, hsub : sa i ×ˢ sb j ⊆ t⟩
case refine'_1.intro.mk.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p { fst := i, snd := j }.fst
hj : p { fst := i, snd := j }.snd
k : ι
hk : p k
ki : sa k ⊆ sa { fst := i, snd := j }.fst
kj : sb k ⊆ sb { fst := i, snd := j }.snd
⊢ ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t
case refine'_1.intro.mk.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p { fst := i, snd := j }.fst
hj : p { fst := i, snd := j }.snd
⊢ ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t
rcases h_dir hi hj with ⟨k, hk, ki, kj⟩
no goals
case refine'_1.intro.mk.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p { fst := i, snd := j }.fst
hj : p { fst := i, snd := j }.snd
k : ι
hk : p k
ki : sa k ⊆ sa { fst := i, snd := j }.fst
kj : sb k ⊆ sb { fst := i, snd := j }.snd
⊢ ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t
exact ⟨k, hk, (Set.prod_mono ki kj).trans hsub⟩
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i : ι
hi : p i
h : sa i ×ˢ sb i ⊆ t
⊢ ∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
⊢ (∃ i, p i ∧ sa i ×ˢ sb i ⊆ t) → ∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t
rintro ⟨i, hi, h⟩
no goals
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.77172
ι : Sort u_3
ι' : Sort ?u.77178
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb✝ : ι' → Set β
f : α → β
p : ι → Prop
sb : ι → Set β
hla : HasBasis la p sa
hlb : HasBasis lb p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i : ι
hi : p i
h : sa i ×ˢ sb i ⊆ t
⊢ ∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t
exact ⟨⟨i, i⟩, ⟨hi, hi⟩, h⟩