case refine'_1
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ ∅ → P x y

case refine'_2
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∀ ⦃s t : Set β⦄, s ⊆ t → (∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y) → ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y

case refine'_3
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∀ ⦃s t : Set β⦄,
    (∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y) →
      (∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y) → ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s ∪ t → P x y

case refine'_4
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∀ (x : β), x ∈ K → ∃ t, t ∈ 𝓝[K] x ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ K → P x y
refine' hK.induction_on _ _ _ _
no goals
case refine'_1
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ ∅ → P x y
exact eventually_of_forall fun x y => False.elim
case refine'_2
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hst : s ⊆ t
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
⊢ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
case refine'_2
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∀ ⦃s t : Set β⦄, s ⊆ t → (∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y) → ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
intro s t hst ht
no goals
case refine'_2
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hst : s ⊆ t
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
⊢ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
refine' ht.mono fun x h y hys => h y <| hst hys
case refine'_3
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hs : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
⊢ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s ∪ t → P x y
case refine'_3
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∀ ⦃s t : Set β⦄,
    (∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y) →
      (∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y) → ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s ∪ t → P x y
intro s t hs ht
case h
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hs : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
⊢ ∀ (a : α), (∀ (y : β), y ∈ s → P a y) → (∀ (y : β), y ∈ t → P a y) → ∀ (y : β), y ∈ s ∪ t → P a y
case refine'_3
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hs : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
⊢ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s ∪ t → P x y
filter_upwards [hs, ht]
case h.inl
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hs : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
x : α
h1 : ∀ (y : β), y ∈ s → P x y
h2 : ∀ (y : β), y ∈ t → P x y
y : β
hys : y ∈ s
⊢ P x y

case h.inr
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hs : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
x : α
h1 : ∀ (y : β), y ∈ s → P x y
h2 : ∀ (y : β), y ∈ t → P x y
y : β
hyt : y ∈ t
⊢ P x y
case h
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hs : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
⊢ ∀ (a : α), (∀ (y : β), y ∈ s → P a y) → (∀ (y : β), y ∈ t → P a y) → ∀ (y : β), y ∈ s ∪ t → P a y
rintro x h1 h2 y (hys | hyt)
no goals
case h.inl
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hs : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
x : α
h1 : ∀ (y : β), y ∈ s → P x y
h2 : ∀ (y : β), y ∈ t → P x y
y : β
hys : y ∈ s
⊢ P x y

case h.inr
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
s t : Set β
hs : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ s → P x y
ht : ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
x : α
h1 : ∀ (y : β), y ∈ s → P x y
h2 : ∀ (y : β), y ∈ t → P x y
y : β
hyt : y ∈ t
⊢ P x y
exacts [h1 y hys, h2 y hyt]
case refine'_4
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
y : β
hyK : y ∈ K
⊢ ∃ t, t ∈ 𝓝[K] y ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
case refine'_4
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∀ (x : β), x ∈ K → ∃ t, t ∈ 𝓝[K] x ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
intro y hyK
case refine'_4
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
y : β
hyK : y ∈ K
hP : ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∃ t, t ∈ 𝓝[K] y ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
case refine'_4
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
hP : ∀ (y : β), y ∈ K → ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
y : β
hyK : y ∈ K
⊢ ∃ t, t ∈ 𝓝[K] y ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
specialize hP y hyK
case refine'_4
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
y : β
hyK : y ∈ K
hP :
  ∃ pa,
    (∀ᶠ (x : α) in 𝓝 x₀, pa x) ∧
      ∃ pb, (∀ᶠ (y : β) in 𝓝 y, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → P (x, y).fst (x, y).snd
⊢ ∃ t, t ∈ 𝓝[K] y ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
case refine'_4
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
y : β
hyK : y ∈ K
hP : ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.fst z.snd
⊢ ∃ t, t ∈ 𝓝[K] y ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
rw [nhds_prod_eq, eventually_prod_iff] at hP
case refine'_4.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
y : β
hyK : y ∈ K
p : α → Prop
hp : ∀ᶠ (x : α) in 𝓝 x₀, p x
q : β → Prop
hq : ∀ᶠ (y : β) in 𝓝 y, q y
hpq : ∀ {x : α}, p x → ∀ {y : β}, q y → P (x, y).fst (x, y).snd
⊢ ∃ t, t ∈ 𝓝[K] y ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
case refine'_4
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
y : β
hyK : y ∈ K
hP :
  ∃ pa,
    (∀ᶠ (x : α) in 𝓝 x₀, pa x) ∧
      ∃ pb, (∀ᶠ (y : β) in 𝓝 y, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → P (x, y).fst (x, y).snd
⊢ ∃ t, t ∈ 𝓝[K] y ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
rcases hP with ⟨p, hp, q, hq, hpq⟩
no goals
case refine'_4.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.29509
π : ι → Type ?u.29514
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x₀ : α
K : Set β
hK : IsCompact K
P : α → β → Prop
y : β
hyK : y ∈ K
p : α → Prop
hp : ∀ᶠ (x : α) in 𝓝 x₀, p x
q : β → Prop
hq : ∀ᶠ (y : β) in 𝓝 y, q y
hpq : ∀ {x : α}, p x → ∀ {y : β}, q y → P (x, y).fst (x, y).snd
⊢ ∃ t, t ∈ 𝓝[K] y ∧ ∀ᶠ (x : α) in 𝓝 x₀, ∀ (y : β), y ∈ t → P x y
exact ⟨{ y | q y }, mem_nhdsWithin_of_mem_nhds hq, eventually_of_mem hp @hpq⟩