[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
g✝ g₁ g₂ g : Set α → Filter β
⊢ Filter.lift ⊤ g = g univ
[PROOFSTEP]
simp [Filter.lift]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι✝ : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : HasBasis f p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s✝ i)) (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ s ∈ Filter.lift f g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
[PROOFSTEP]
refine' (mem_biInf_of_directed _ ⟨univ, univ_sets _⟩).trans _
[GOAL]
case refine'_1
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι✝ : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : HasBasis f p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s✝ i)) (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ DirectedOn ((fun s => g s) ⁻¹'o fun x x_1 => x ≥ x_1) f.sets
[PROOFSTEP]
intro t₁ ht₁ t₂ ht₂
[GOAL]
case refine'_1
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι✝ : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : HasBasis f p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s✝ i)) (pg i) (sg i)
gm : Monotone g
s : Set γ
t₁ : Set α
ht₁ : t₁ ∈ f.sets
t₂ : Set α
ht₂ : t₂ ∈ f.sets
⊢ ∃ z, z ∈ f.sets ∧ ((fun s => g s) ⁻¹'o fun x x_1 => x ≥ x_1) t₁ z ∧ ((fun s => g s) ⁻¹'o fun x x_1 => x ≥ x_1) t₂ z
[PROOFSTEP]
exact ⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm <| inter_subset_left _ _, gm <| inter_subset_right _ _⟩
[GOAL]
case refine'_2
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι✝ : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : HasBasis f p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s✝ i)) (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ (∃ i, i ∈ f.sets ∧ s ∈ g i) ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
[PROOFSTEP]
simp only [← (hg _).mem_iff]
[GOAL]
case refine'_2
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι✝ : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : HasBasis f p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s✝ i)) (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ (∃ i, i ∈ f.sets ∧ s ∈ g i) ↔ ∃ i, p i ∧ s ∈ g (s✝ i)
[PROOFSTEP]
exact hf.exists_iff fun t₁ t₂ ht H => gm ht H
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι✝ : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : HasBasis f p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s i)) (pg i) (sg i)
gm : Monotone g
⊢ HasBasis (Filter.lift f g) (fun i => p i.fst ∧ pg i.fst i.snd) fun i => sg i.fst i.snd
[PROOFSTEP]
refine' ⟨fun t => (hf.mem_lift_iff hg gm).trans _⟩
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι✝ : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β✝
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : HasBasis f p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), HasBasis (g (s i)) (pg i) (sg i)
gm : Monotone g
t : Set γ
⊢ (∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ t) ↔ ∃ i, (p i.fst ∧ pg i.fst i.snd) ∧ sg i.fst i.snd ⊆ t
[PROOFSTEP]
simp [Sigma.exists, and_assoc, exists_and_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
hg : Monotone g
s : Set β
⊢ (∃ i, i ∈ f ∧ ∃ x, x ∈ g i ∧ id x ⊆ s) ↔ ∃ t, t ∈ f ∧ s ∈ g t
[PROOFSTEP]
simp only [id, exists_mem_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
hg : Monotone g
⊢ ⋂₀ {s | s ∈ Filter.lift f g} = ⋂ (s : Set α) (_ : s ∈ f), ⋂₀ {t | t ∈ g s}
[PROOFSTEP]
simp only [sInter_eq_biInter, mem_setOf_eq, Filter.mem_sets, mem_lift_sets hg, iInter_exists, iInter_and,
  @iInter_comm _ (Set β)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
m : γ → β
l : Filter γ
⊢ Tendsto m l (Filter.lift f g) ↔ ∀ (s : Set α), s ∈ f → Tendsto m l (g s)
[PROOFSTEP]
simp only [Filter.lift, tendsto_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
m : β → γ
hg : Monotone g
this : Monotone (map m ∘ g)
s : Set γ
⊢ s ∈ map m (Filter.lift f g) ↔ s ∈ Filter.lift f (map m ∘ g)
[PROOFSTEP]
simp only [mem_lift_sets hg, mem_lift_sets this, exists_prop, mem_map, Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
m : γ → β
⊢ comap m (Filter.lift f g) = Filter.lift f (comap m ∘ g)
[PROOFSTEP]
simp only [Filter.lift, comap_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
m : γ → β
⊢ ⨅ (i : Set α) (_ : i ∈ f), comap m (g i) = ⨅ (s : Set α) (_ : s ∈ f), (comap m ∘ g) s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
hm : Monotone g
⊢ NeBot (Filter.lift f g) ↔ ∀ (s : Set α), s ∈ f → NeBot (g s)
[PROOFSTEP]
simp only [neBot_iff, Ne.def, ← empty_mem_iff_bot, mem_lift_sets hm, not_exists, not_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : Filter α
g h : Set α → Filter β
⊢ (Filter.lift f fun x => g x ⊓ h x) = Filter.lift f g ⊓ Filter.lift f h
[PROOFSTEP]
simp only [Filter.lift, iInf_inf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
f : Filter α
s : Set α
hs : s ∈ f
⊢ f ≤ 𝓟 s
[PROOFSTEP]
simp only [hs, le_principal_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g
[PROOFSTEP]
refine' lift_iInf_le.antisymm fun s => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
⊢ s ∈ Filter.lift (iInf f) g → s ∈ ⨅ (i : ι), Filter.lift (f i) g
[PROOFSTEP]
have H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t := by
  intro t ht
  refine' iInf_sets_induct ht _ fun hs ht => _
  · inhabit ι
    exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)
  · rw [hg]
    exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
⊢ ∀ (t : Set α), t ∈ iInf f → ⨅ (i : ι), Filter.lift (f i) g ≤ g t
[PROOFSTEP]
intro t ht
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ ⨅ (i : ι), Filter.lift (f i) g ≤ g t
[PROOFSTEP]
refine' iInf_sets_induct ht _ fun hs ht => _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ ⨅ (i : ι), Filter.lift (f i) g ≤ g univ
[PROOFSTEP]
inhabit ι
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
inhabited_h : Inhabited ι
⊢ ⨅ (i : ι), Filter.lift (f i) g ≤ g univ
[PROOFSTEP]
exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : ⨅ (i : ι), Filter.lift (f i) g ≤ g s₂✝
⊢ ⨅ (i : ι), Filter.lift (f i) g ≤ g (s₁✝ ∩ s₂✝)
[PROOFSTEP]
rw [hg]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : ⨅ (i : ι), Filter.lift (f i) g ≤ g s₂✝
⊢ ⨅ (i : ι), Filter.lift (f i) g ≤ g s₁✝ ⊓ g s₂✝
[PROOFSTEP]
exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ (t : Set α), t ∈ iInf f → ⨅ (i : ι), Filter.lift (f i) g ≤ g t
⊢ s ∈ Filter.lift (iInf f) g → s ∈ ⨅ (i : ι), Filter.lift (f i) g
[PROOFSTEP]
simp only [mem_lift_sets (Monotone.of_map_inf hg), exists_imp, and_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ (t : Set α), t ∈ iInf f → ⨅ (i : ι), Filter.lift (f i) g ≤ g t
⊢ ∀ (x : Set α), x ∈ iInf f → s ∈ g x → s ∈ ⨅ (i : ι), Filter.lift (f i) g
[PROOFSTEP]
exact fun t ht hs => H t ht hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x x_1 => x ≥ x_1) f
hg : Monotone g
s : Set β
⊢ s ∈ Filter.lift (iInf f) g → s ∈ ⨅ (i : ι), Filter.lift (f i) g
[PROOFSTEP]
simp only [mem_lift_sets hg, exists_imp, and_imp, mem_iInf_of_directed hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x x_1 => x ≥ x_1) f
hg : Monotone g
s : Set β
⊢ ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → s ∈ ⨅ (i : ι), Filter.lift (f i) g
[PROOFSTEP]
exact fun t i ht hs => mem_iInf_of_mem i <| mem_lift ht hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : IsEmpty ι
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g
[PROOFSTEP]
simp [iInf_of_empty, hg']
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : Nonempty ι
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g
[PROOFSTEP]
exact lift_iInf hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
m : γ → β
l : Filter γ
⊢ Tendsto m l (Filter.lift' f h) ↔ ∀ (s : Set α), s ∈ f → ∀ᶠ (a : γ) in l, m a ∈ h s
[PROOFSTEP]
simp only [Filter.lift', tendsto_lift, tendsto_principal, comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
ι : Sort u_5
p : ι → Prop
s : ι → Set α
hf : HasBasis f p s
hh : Monotone h
t : Set β
⊢ (∃ i, p i ∧ ∃ x, True ∧ h (s i) ⊆ t) ↔ ∃ i, p i ∧ (h ∘ s) i ⊆ t
[PROOFSTEP]
simp only [exists_const, true_and, comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
m : β → γ
hh : Monotone h
⊢ Filter.lift f (map m ∘ 𝓟 ∘ h) = Filter.lift' f (image m ∘ h)
[PROOFSTEP]
simp only [comp, Filter.lift', map_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
m : γ → β
⊢ comap m (Filter.lift' f h) = Filter.lift' f (preimage m ∘ h)
[PROOFSTEP]
simp only [Filter.lift', comap_lift_eq, (· ∘ ·), comap_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
a : α
hh : Monotone h
⊢ Filter.lift' (pure a) h = 𝓟 (h {a})
[PROOFSTEP]
rw [← principal_singleton, lift'_principal hh]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
hh : Monotone h
⊢ Filter.lift' ⊥ h = 𝓟 (h ∅)
[PROOFSTEP]
rw [← principal_empty, lift'_principal hh]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
h✝ h₁ h₂ g : Set α → Set β
h : Set β → Filter γ
hg : Monotone g
hh : Monotone h
⊢ (Filter.lift f fun s => Filter.lift (𝓟 (g s)) h) = Filter.lift f fun s => h (g s)
[PROOFSTEP]
simp only [lift_principal, hh, eq_self_iff_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
h✝ h₁ h₂ h : Set α → Set β
s : Set β
⊢ Filter.lift' f h ⊓ 𝓟 s = Filter.lift' f fun t => h t ∩ s
[PROOFSTEP]
simp only [Filter.lift', Filter.lift, (· ∘ ·), ← inf_principal, iInf_subtype', ← iInf_inf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
hh : Monotone h
⊢ (∀ (s : Set α), s ∈ f → NeBot (𝓟 (h s))) ↔ ∀ (s : Set α), s ∈ f → Set.Nonempty (h s)
[PROOFSTEP]
simp only [principal_neBot_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Set β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ∩ g t
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t
[PROOFSTEP]
simp only [inf_principal, comp, hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t
[PROOFSTEP]
simp only [inf_principal, comp, hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ (𝓟 ∘ g) univ = ⊤
[PROOFSTEP]
rw [Function.comp_apply, hg', principal_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
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
[PROOFSTEP]
rw [inf_eq_iInf, inf_eq_iInf, lift'_iInf hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
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
[PROOFSTEP]
refine iInf_congr ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
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
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
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' (bif false then f else g) s = bif false then Filter.lift' f s else Filter.lift' g s
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
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' (bif true then f else g) s = bif true then Filter.lift' f s else Filter.lift' g s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ f : Filter α
g : Filter β
⊢ f ×ˢ g = Filter.lift f fun s => Filter.lift' g fun t => s ×ˢ t
[PROOFSTEP]
simpa only [Filter.lift', Filter.lift, (f.basis_sets.prod g.basis_sets).eq_biInf, iInf_prod, iInf_and] using
  iInf_congr fun i => iInf_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f✝ : Filter α
f : α × α → β
x : Filter α
y : Filter β
⊢ Tendsto f (x ×ˢ x) y ↔ ∀ (W : Set β), W ∈ y → ∃ U, U ∈ x ∧ ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W
[PROOFSTEP]
simp only [tendsto_def, mem_prod_same_iff, prod_sub_preimage_iff, exists_prop, iff_self_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f : Filter α
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
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
[PROOFSTEP]
simp only [prod_def, lift_assoc hg₁]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f : Filter α
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
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
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f : Filter α
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
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
[PROOFSTEP]
funext x
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f : Filter α
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
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
[PROOFSTEP]
rw [lift_comm]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f : Filter α
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
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
[PROOFSTEP]
apply congr_arg
[GOAL]
case h.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f : Filter α
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
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
[PROOFSTEP]
funext y
[GOAL]
case h.h.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f : Filter α
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
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
[PROOFSTEP]
apply lift'_lift_assoc hg₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f : Filter α
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Set β₁
g₂ : Set α₂ → Set β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ (Filter.lift f₁ fun s => Filter.lift f₂ fun t => 𝓟 (g₁ s) ×ˢ 𝓟 (g₂ t)) =
    Filter.lift f₁ fun s => Filter.lift f₂ fun t => 𝓟 (g₁ s ×ˢ g₂ t)
[PROOFSTEP]
{simp only [prod_principal_principal]
}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f : Filter α
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Set β₁
g₂ : Set α₂ → Set β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ (Filter.lift f₁ fun s => Filter.lift f₂ fun t => 𝓟 (g₁ s) ×ˢ 𝓟 (g₂ t)) =
    Filter.lift f₁ fun s => Filter.lift f₂ fun t => 𝓟 (g₁ s ×ˢ g₂ t)
[PROOFSTEP]
simp only [prod_principal_principal]
