[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
⊢ ∀ {x y : Set γ},
    x ∈ {s | ∃ u v, u ∈ f ∧ v ∈ g ∧ image2 m u v ⊆ s} →
      y ∈ {s | ∃ u v, u ∈ f ∧ v ∈ g ∧ image2 m u v ⊆ s} → x ∩ y ∈ {s | ∃ u v, u ∈ f ∧ v ∈ g ∧ image2 m u v ⊆ s}
[PROOFSTEP]
simp only [exists_prop, Set.mem_setOf_eq, subset_inter_iff]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
⊢ ∀ {x y : Set γ},
    (∃ u v, u ∈ f ∧ v ∈ g ∧ image2 m u v ⊆ x) →
      (∃ u v, u ∈ f ∧ v ∈ g ∧ image2 m u v ⊆ y) → ∃ u v, u ∈ f ∧ v ∈ g ∧ image2 m u v ⊆ x ∧ image2 m u v ⊆ y
[PROOFSTEP]
rintro _ _ ⟨s₁, s₂, hs₁, hs₂, hs⟩ ⟨t₁, t₂, ht₁, ht₂, ht⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
x✝ y✝ : Set γ
s₁ : Set α
s₂ : Set β
hs₁ : s₁ ∈ f
hs₂ : s₂ ∈ g
hs : image2 m s₁ s₂ ⊆ x✝
t₁ : Set α
t₂ : Set β
ht₁ : t₁ ∈ f
ht₂ : t₂ ∈ g
ht : image2 m t₁ t₂ ⊆ y✝
⊢ ∃ u v, u ∈ f ∧ v ∈ g ∧ image2 m u v ⊆ x✝ ∧ image2 m u v ⊆ y✝
[PROOFSTEP]
exact
  ⟨s₁ ∩ t₁, s₂ ∩ t₂, inter_sets f hs₁ ht₁, inter_sets g hs₂ ht₂,
    (image2_subset (inter_subset_left _ _) <| inter_subset_left _ _).trans hs,
    (image2_subset (inter_subset_right _ _) <| inter_subset_right _ _).trans ht⟩
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (fun p => m p.fst p.snd) (f ×ˢ g) = map₂ m f g
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ s ∈ map (fun p => m p.fst p.snd) (f ×ˢ g) ↔ s ∈ map₂ m f g
[PROOFSTEP]
simp [mem_prod_iff, prod_subset_iff]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
f : Filter α
g : Filter β
⊢ map₂ Prod.mk f g = f ×ˢ g
[PROOFSTEP]
simp only [← map_prod_eq_map₂, map_id']
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥
[PROOFSTEP]
simp only [← empty_mem_iff_bot, mem_map₂_iff, subset_empty_iff, image2_eq_empty_iff]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ (∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)) ↔ ∅ ∈ f ∨ ∅ ∈ g
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ (∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)) → ∅ ∈ f ∨ ∅ ∈ g
[PROOFSTEP]
rintro ⟨s, t, hs, ht, rfl | rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.inl
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
t : Set β
ht : t ∈ g
hs : ∅ ∈ f
⊢ ∅ ∈ f ∨ ∅ ∈ g
[PROOFSTEP]
exact Or.inl hs
[GOAL]
case mp.intro.intro.intro.intro.inr
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
s : Set α
hs : s ∈ f
ht : ∅ ∈ g
⊢ ∅ ∈ f ∨ ∅ ∈ g
[PROOFSTEP]
exact Or.inr ht
[GOAL]
case mpr
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ ∅ ∈ f ∨ ∅ ∈ g → ∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)
[PROOFSTEP]
rintro (h | h)
[GOAL]
case mpr.inl
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
h : ∅ ∈ f
⊢ ∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)
[PROOFSTEP]
exact ⟨_, _, h, univ_mem, Or.inl rfl⟩
[GOAL]
case mpr.inr
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
h : ∅ ∈ g
⊢ ∃ s t, s ∈ f ∧ t ∈ g ∧ (s = ∅ ∨ t = ∅)
[PROOFSTEP]
exact ⟨_, _, univ_mem, h, Or.inr rfl⟩
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ NeBot (map₂ m f g) ↔ NeBot f ∧ NeBot g
[PROOFSTEP]
simp_rw [neBot_iff]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ map₂ m f g ≠ ⊥ ↔ f ≠ ⊥ ∧ g ≠ ⊥
[PROOFSTEP]
exact map₂_eq_bot_iff.not.trans not_or
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g
[PROOFSTEP]
ext u
[GOAL]
case a
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
⊢ u ∈ map₂ m (f₁ ⊔ f₂) g ↔ u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
⊢ u ∈ map₂ m (f₁ ⊔ f₂) g → u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g
[PROOFSTEP]
rintro ⟨s, t, ⟨h₁, h₂⟩, ht, hu⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁✝ h₂✝ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
s : Set α
t : Set β
h₁ : s ∈ f₁.sets
h₂ : s ∈ f₂.sets
ht : t ∈ g
hu : image2 m s t ⊆ u
⊢ u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g
[PROOFSTEP]
exact ⟨mem_of_superset (image2_mem_map₂ h₁ ht) hu, mem_of_superset (image2_mem_map₂ h₂ ht) hu⟩
[GOAL]
case a.mpr
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
⊢ u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g → u ∈ map₂ m (f₁ ⊔ f₂) g
[PROOFSTEP]
rintro ⟨⟨s₁, t₁, hs₁, ht₁, hu₁⟩, s₂, t₂, hs₂, ht₂, hu₂⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f₁
ht₁ : t₁ ∈ g
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f₂
ht₂ : t₂ ∈ g
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ u ∈ map₂ m (f₁ ⊔ f₂) g
[PROOFSTEP]
refine' ⟨s₁ ∪ s₂, t₁ ∩ t₂, union_mem_sup hs₁ hs₂, inter_mem ht₁ ht₂, _⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f₁
ht₁ : t₁ ∈ g
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f₂
ht₂ : t₂ ∈ g
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ image2 m (s₁ ∪ s₂) (t₁ ∩ t₂) ⊆ u
[PROOFSTEP]
rw [image2_union_left]
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f₁
ht₁ : t₁ ∈ g
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f₂
ht₂ : t₂ ∈ g
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ image2 m s₁ (t₁ ∩ t₂) ∪ image2 m s₂ (t₁ ∩ t₂) ⊆ u
[PROOFSTEP]
exact
  union_subset ((image2_subset_left <| inter_subset_left _ _).trans hu₁)
    ((image2_subset_left <| inter_subset_right _ _).trans hu₂)
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂
[PROOFSTEP]
ext u
[GOAL]
case a
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
⊢ u ∈ map₂ m f (g₁ ⊔ g₂) ↔ u ∈ map₂ m f g₁ ⊔ map₂ m f g₂
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
⊢ u ∈ map₂ m f (g₁ ⊔ g₂) → u ∈ map₂ m f g₁ ⊔ map₂ m f g₂
[PROOFSTEP]
rintro ⟨s, t, hs, ⟨h₁, h₂⟩, hu⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁✝ h₂✝ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
s : Set α
t : Set β
hs : s ∈ f
hu : image2 m s t ⊆ u
h₁ : t ∈ g₁.sets
h₂ : t ∈ g₂.sets
⊢ u ∈ map₂ m f g₁ ⊔ map₂ m f g₂
[PROOFSTEP]
exact ⟨mem_of_superset (image2_mem_map₂ hs h₁) hu, mem_of_superset (image2_mem_map₂ hs h₂) hu⟩
[GOAL]
case a.mpr
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
⊢ u ∈ map₂ m f g₁ ⊔ map₂ m f g₂ → u ∈ map₂ m f (g₁ ⊔ g₂)
[PROOFSTEP]
rintro ⟨⟨s₁, t₁, hs₁, ht₁, hu₁⟩, s₂, t₂, hs₂, ht₂, hu₂⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f
ht₁ : t₁ ∈ g₁
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f
ht₂ : t₂ ∈ g₂
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ u ∈ map₂ m f (g₁ ⊔ g₂)
[PROOFSTEP]
refine' ⟨s₁ ∩ s₂, t₁ ∪ t₂, inter_mem hs₁ hs₂, union_mem_sup ht₁ ht₂, _⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f
ht₁ : t₁ ∈ g₁
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f
ht₂ : t₂ ∈ g₂
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ image2 m (s₁ ∩ s₂) (t₁ ∪ t₂) ⊆ u
[PROOFSTEP]
rw [image2_union_right]
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f
ht₁ : t₁ ∈ g₁
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f
ht₂ : t₂ ∈ g₂
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ image2 m (s₁ ∩ s₂) t₁ ∪ image2 m (s₁ ∩ s₂) t₂ ⊆ u
[PROOFSTEP]
exact
  union_subset ((image2_subset_right <| inter_subset_left _ _).trans hu₁)
    ((image2_subset_right <| inter_subset_right _ _).trans hu₂)
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
h : u ∈ map (fun b => m a b) g
⊢ image2 m {a} ((fun b => m a b) ⁻¹' u) ⊆ u
[PROOFSTEP]
rw [image2_singleton_left, image_subset_iff]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
u : Set γ
h : u ∈ map (fun a => m a b) f
⊢ image2 m ((fun a => m a b) ⁻¹' u) {b} ⊆ u
[PROOFSTEP]
rw [image2_singleton_right, image_subset_iff]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
⊢ map₂ m (pure a) (pure b) = pure (m a b)
[PROOFSTEP]
rw [map₂_pure_right, map_pure]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
⊢ map₂ m f g = map₂ (fun a b => m b a) g f
[PROOFSTEP]
ext u
[GOAL]
case a
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
u : Set γ
⊢ u ∈ map₂ m f g ↔ u ∈ map₂ (fun a b => m b a) g f
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
u : Set γ
⊢ u ∈ map₂ m f g → u ∈ map₂ (fun a b => m b a) g f
[PROOFSTEP]
rintro ⟨s, t, hs, ht, hu⟩
[GOAL]
case a.mpr
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
u : Set γ
⊢ u ∈ map₂ (fun a b => m b a) g f → u ∈ map₂ m f g
[PROOFSTEP]
rintro ⟨s, t, hs, ht, hu⟩
[GOAL]
case a.mp.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
u : Set γ
s : Set α
t : Set β
hs : s ∈ f
ht : t ∈ g
hu : image2 m s t ⊆ u
⊢ u ∈ map₂ (fun a b => m b a) g f
[PROOFSTEP]
refine' ⟨t, s, ht, hs, by rwa [image2_swap]⟩
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
u : Set γ
s : Set α
t : Set β
hs : s ∈ f
ht : t ∈ g
hu : image2 m s t ⊆ u
⊢ image2 (fun a b => m b a) t s ⊆ u
[PROOFSTEP]
rwa [image2_swap]
[GOAL]
case a.mpr.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
u : Set γ
s : Set β
t : Set α
hs : s ∈ g
ht : t ∈ f
hu : image2 (fun a b => m b a) s t ⊆ u
⊢ u ∈ map₂ m f g
[PROOFSTEP]
refine' ⟨t, s, ht, hs, by rwa [image2_swap]⟩
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
u : Set γ
s : Set β
t : Set α
hs : s ∈ g
ht : t ∈ f
hu : image2 (fun a b => m b a) s t ⊆ u
⊢ image2 m t s ⊆ u
[PROOFSTEP]
rwa [image2_swap]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
h : NeBot g
⊢ map₂ (fun x x_1 => x) f g = f
[PROOFSTEP]
ext u
[GOAL]
case a
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
h : NeBot g
u : Set α
⊢ u ∈ map₂ (fun x x_1 => x) f g ↔ u ∈ f
[PROOFSTEP]
refine' ⟨_, fun hu => ⟨_, _, hu, univ_mem, (image2_left <| h.nonempty_of_mem univ_mem).subset⟩⟩
[GOAL]
case a
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
h : NeBot g
u : Set α
⊢ u ∈ map₂ (fun x x_1 => x) f g → u ∈ f
[PROOFSTEP]
rintro ⟨s, t, hs, ht, hu⟩
[GOAL]
case a.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
h : NeBot g
u s : Set α
t : Set β
hs : s ∈ f
ht : t ∈ g
hu : image2 (fun x x_1 => x) s t ⊆ u
⊢ u ∈ f
[PROOFSTEP]
rw [image2_left (h.nonempty_of_mem ht)] at hu
[GOAL]
case a.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
h : NeBot g
u s : Set α
t : Set β
hs : s ∈ f
ht : t ∈ g
hu : s ⊆ u
⊢ u ∈ f
[PROOFSTEP]
exact mem_of_superset hs hu
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
h : NeBot f
⊢ map₂ (fun x y => y) f g = g
[PROOFSTEP]
rw [map₂_swap, map₂_left h]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ → δ
f : Filter α
g : Filter β
h : Filter γ
⊢ ∀ {x y : Set δ},
    x ∈ {s | ∃ u v w, u ∈ f ∧ v ∈ g ∧ w ∈ h ∧ image3 m u v w ⊆ s} →
      y ∈ {s | ∃ u v w, u ∈ f ∧ v ∈ g ∧ w ∈ h ∧ image3 m u v w ⊆ s} →
        x ∩ y ∈ {s | ∃ u v w, u ∈ f ∧ v ∈ g ∧ w ∈ h ∧ image3 m u v w ⊆ s}
[PROOFSTEP]
simp only [exists_prop, mem_setOf_eq, subset_inter_iff]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ → δ
f : Filter α
g : Filter β
h : Filter γ
⊢ ∀ {x y : Set δ},
    (∃ u v w, u ∈ f ∧ v ∈ g ∧ w ∈ h ∧ image3 m u v w ⊆ x) →
      (∃ u v w, u ∈ f ∧ v ∈ g ∧ w ∈ h ∧ image3 m u v w ⊆ y) →
        ∃ u v w, u ∈ f ∧ v ∈ g ∧ w ∈ h ∧ image3 m u v w ⊆ x ∧ image3 m u v w ⊆ y
[PROOFSTEP]
rintro _ _ ⟨s₁, s₂, s₃, hs₁, hs₂, hs₃, hs⟩ ⟨t₁, t₂, t₃, ht₁, ht₂, ht₃, ht⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ → δ
f : Filter α
g : Filter β
h : Filter γ
x✝ y✝ : Set δ
s₁ : Set α
s₂ : Set β
s₃ : Set γ
hs₁ : s₁ ∈ f
hs₂ : s₂ ∈ g
hs₃ : s₃ ∈ h
hs : image3 m s₁ s₂ s₃ ⊆ x✝
t₁ : Set α
t₂ : Set β
t₃ : Set γ
ht₁ : t₁ ∈ f
ht₂ : t₂ ∈ g
ht₃ : t₃ ∈ h
ht : image3 m t₁ t₂ t₃ ⊆ y✝
⊢ ∃ u v w, u ∈ f ∧ v ∈ g ∧ w ∈ h ∧ image3 m u v w ⊆ x✝ ∧ image3 m u v w ⊆ y✝
[PROOFSTEP]
exact
  ⟨s₁ ∩ t₁, s₂ ∩ t₂, s₃ ∩ t₃, inter_mem hs₁ ht₁, inter_mem hs₂ ht₂, inter_mem hs₃ ht₃,
    (image3_mono (inter_subset_left _ _) (inter_subset_left _ _) <| inter_subset_left _ _).trans hs,
    (image3_mono (inter_subset_right _ _) (inter_subset_right _ _) <| inter_subset_right _ _).trans ht⟩
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
⊢ map₂ m (map₂ n f g) h = map₃ (fun a b c => m (n a b) c) f g h
[PROOFSTEP]
ext w
[GOAL]
case a
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
w : Set ε
⊢ w ∈ map₂ m (map₂ n f g) h ↔ w ∈ map₃ (fun a b c => m (n a b) c) f g h
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
w : Set ε
⊢ w ∈ map₂ m (map₂ n f g) h → w ∈ map₃ (fun a b c => m (n a b) c) f g h
[PROOFSTEP]
rintro ⟨s, t, ⟨u, v, hu, hv, hs⟩, ht, hw⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
w : Set ε
s : Set δ
t : Set γ
u : Set α
v : Set β
hu : u ∈ f
hv : v ∈ g
hs : image2 n u v ⊆ s
ht : t ∈ h
hw : image2 m s t ⊆ w
⊢ w ∈ map₃ (fun a b c => m (n a b) c) f g h
[PROOFSTEP]
refine' ⟨u, v, t, hu, hv, ht, _⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
w : Set ε
s : Set δ
t : Set γ
u : Set α
v : Set β
hu : u ∈ f
hv : v ∈ g
hs : image2 n u v ⊆ s
ht : t ∈ h
hw : image2 m s t ⊆ w
⊢ image3 (fun a b c => m (n a b) c) u v t ⊆ w
[PROOFSTEP]
rw [← image2_image2_left]
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
w : Set ε
s : Set δ
t : Set γ
u : Set α
v : Set β
hu : u ∈ f
hv : v ∈ g
hs : image2 n u v ⊆ s
ht : t ∈ h
hw : image2 m s t ⊆ w
⊢ image2 m (image2 (fun a b => n a b) u v) t ⊆ w
[PROOFSTEP]
exact (image2_subset_right hs).trans hw
[GOAL]
case a.mpr
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
w : Set ε
⊢ w ∈ map₃ (fun a b c => m (n a b) c) f g h → w ∈ map₂ m (map₂ n f g) h
[PROOFSTEP]
rintro ⟨s, t, u, hs, ht, hu, hw⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
w : Set ε
s : Set α
t : Set β
u : Set γ
hs : s ∈ f
ht : t ∈ g
hu : u ∈ h
hw : image3 (fun a b c => m (n a b) c) s t u ⊆ w
⊢ w ∈ map₂ m (map₂ n f g) h
[PROOFSTEP]
exact ⟨_, u, image2_mem_map₂ hs ht, hu, by rwa [image2_image2_left]⟩
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
w : Set ε
s : Set α
t : Set β
u : Set γ
hs : s ∈ f
ht : t ∈ g
hu : u ∈ h
hw : image3 (fun a b c => m (n a b) c) s t u ⊆ w
⊢ image2 m (image2 n s t) u ⊆ w
[PROOFSTEP]
rwa [image2_image2_left]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
⊢ map₂ m f (map₂ n g h) = map₃ (fun a b c => m a (n b c)) f g h
[PROOFSTEP]
ext w
[GOAL]
case a
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
w : Set ε
⊢ w ∈ map₂ m f (map₂ n g h) ↔ w ∈ map₃ (fun a b c => m a (n b c)) f g h
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
w : Set ε
⊢ w ∈ map₂ m f (map₂ n g h) → w ∈ map₃ (fun a b c => m a (n b c)) f g h
[PROOFSTEP]
rintro ⟨s, t, hs, ⟨u, v, hu, hv, ht⟩, hw⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
w : Set ε
s : Set α
t : Set δ
hs : s ∈ f
hw : image2 m s t ⊆ w
u : Set β
v : Set γ
hu : u ∈ g
hv : v ∈ h
ht : image2 n u v ⊆ t
⊢ w ∈ map₃ (fun a b c => m a (n b c)) f g h
[PROOFSTEP]
refine' ⟨s, u, v, hs, hu, hv, _⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
w : Set ε
s : Set α
t : Set δ
hs : s ∈ f
hw : image2 m s t ⊆ w
u : Set β
v : Set γ
hu : u ∈ g
hv : v ∈ h
ht : image2 n u v ⊆ t
⊢ image3 (fun a b c => m a (n b c)) s u v ⊆ w
[PROOFSTEP]
rw [← image2_image2_right]
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
w : Set ε
s : Set α
t : Set δ
hs : s ∈ f
hw : image2 m s t ⊆ w
u : Set β
v : Set γ
hu : u ∈ g
hv : v ∈ h
ht : image2 n u v ⊆ t
⊢ image2 (fun a => m a) s (image2 (fun b c => n b c) u v) ⊆ w
[PROOFSTEP]
exact (image2_subset_left ht).trans hw
[GOAL]
case a.mpr
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
w : Set ε
⊢ w ∈ map₃ (fun a b c => m a (n b c)) f g h → w ∈ map₂ m f (map₂ n g h)
[PROOFSTEP]
rintro ⟨s, t, u, hs, ht, hu, hw⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
w : Set ε
s : Set α
t : Set β
u : Set γ
hs : s ∈ f
ht : t ∈ g
hu : u ∈ h
hw : image3 (fun a b c => m a (n b c)) s t u ⊆ w
⊢ w ∈ map₂ m f (map₂ n g h)
[PROOFSTEP]
exact ⟨s, _, hs, image2_mem_map₂ ht hu, by rwa [image2_image2_right]⟩
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
u✝ : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
w : Set ε
s : Set α
t : Set β
u : Set γ
hs : s ∈ f
ht : t ∈ g
hu : u ∈ h
hw : image3 (fun a b c => m a (n b c)) s t u ⊆ w
⊢ image2 m s (image2 n t u) ⊆ w
[PROOFSTEP]
rwa [image2_image2_right]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
n : γ → δ
⊢ map n (map₂ m f g) = map₂ (fun a b => n (m a b)) f g
[PROOFSTEP]
rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, map_map]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
n : γ → δ
⊢ map (n ∘ fun p => m p.fst p.snd) (f ×ˢ g) = map (fun p => n (m p.fst p.snd)) (f ×ˢ g)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : γ → β → δ
n : α → γ
⊢ map₂ m (map n f) g = map₂ (fun a b => m (n a) b) f g
[PROOFSTEP]
rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, ← @map_id _ g, prod_map_map_eq, map_map, map_id]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : γ → β → δ
n : α → γ
⊢ map ((fun p => m p.fst p.snd) ∘ fun p => (n p.fst, id p.snd)) (f ×ˢ g) = map (fun p => m (n p.fst) p.snd) (f ×ˢ g)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → γ → δ
n : β → γ
⊢ map₂ m f (map n g) = map₂ (fun a b => m a (n b)) f g
[PROOFSTEP]
rw [map₂_swap, map₂_map_left, map₂_swap]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)
[PROOFSTEP]
simp only [map₂_map₂_left, map₂_map₂_right, h_assoc]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
n : β → α → γ
h_comm : ∀ (a : α) (b : β), m a b = n b a
⊢ map₂ (fun a b => m b a) g f = map₂ n g f
[PROOFSTEP]
simp_rw [h_comm]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h)
[PROOFSTEP]
rw [map₂_swap m', map₂_swap m]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ (fun a b => m b a) (map₂ n g h) f = map₂ n' g (map₂ (fun a b => m' b a) h f)
[PROOFSTEP]
exact map₂_assoc fun _ _ _ => h_left_comm _ _ _
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g
[PROOFSTEP]
rw [map₂_swap n, map₂_swap n']
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ (fun a b => n b a) g f) h = map₂ (fun a b => n' b a) g (map₂ m' f h)
[PROOFSTEP]
exact map₂_assoc fun _ _ _ => h_right_comm _ _ _
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)
[PROOFSTEP]
simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
⊢ map₂ m f (map₂ n g h) ≤ map₂ n' (map₂ m₁ f g) (map₂ m₂ f h)
[PROOFSTEP]
rintro s ⟨t₁, t₂, ⟨u₁, v, hu₁, hv, ht₁⟩, ⟨u₂, w, hu₂, hw, ht₂⟩, hs⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁✝ t₂✝ : Set β
u : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ s ∈ map₂ m f (map₂ n g h)
[PROOFSTEP]
refine' ⟨u₁ ∩ u₂, _, inter_mem hu₁ hu₂, image2_mem_map₂ hv hw, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁✝ t₂✝ : Set β
u : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s
[PROOFSTEP]
refine' (image2_distrib_subset_left h_distrib).trans ((image2_subset _ _).trans hs)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁✝ t₂✝ : Set β
u : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 (fun a b => m₁ a b) (u₁ ∩ u₂) v ⊆ t₁
[PROOFSTEP]
exact (image2_subset_right <| inter_subset_left _ _).trans ht₁
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁✝ t₂✝ : Set β
u : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 (fun a c => m₂ a c) (u₁ ∩ u₂) w ⊆ t₂
[PROOFSTEP]
exact (image2_subset_right <| inter_subset_right _ _).trans ht₂
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
⊢ map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h)
[PROOFSTEP]
rintro s ⟨t₁, t₂, ⟨u, w₁, hu, hw₁, ht₁⟩, ⟨v, w₂, hv, hw₂, ht₂⟩, hs⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
t₂ : Set β'
u : Set α
w₁ : Set γ
hu : u ∈ f
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
w₂ : Set γ
hv : v ∈ g
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ s ∈ map₂ m (map₂ n f g) h
[PROOFSTEP]
refine' ⟨_, w₁ ∩ w₂, image2_mem_map₂ hu hv, inter_mem hw₁ hw₂, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
t₂ : Set β'
u : Set α
w₁ : Set γ
hu : u ∈ f
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
w₂ : Set γ
hv : v ∈ g
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m (image2 n u v) (w₁ ∩ w₂) ⊆ s
[PROOFSTEP]
refine' (image2_distrib_subset_right h_distrib).trans ((image2_subset _ _).trans hs)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
t₂ : Set β'
u : Set α
w₁ : Set γ
hu : u ∈ f
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
w₂ : Set γ
hv : v ∈ g
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 (fun a c => m₁ a c) u (w₁ ∩ w₂) ⊆ t₁
[PROOFSTEP]
exact (image2_subset_left <| inter_subset_left _ _).trans ht₁
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m✝ : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁✝ t₂✝ : Set β
u✝ : Set γ
v✝ : Set δ
a : α
b : β
c : γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
t₂ : Set β'
u : Set α
w₁ : Set γ
hu : u ∈ f
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
w₂ : Set γ
hv : v ∈ g
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 (fun b c => m₂ b c) v (w₁ ∩ w₂) ⊆ t₂
[PROOFSTEP]
exact (image2_subset_left <| inter_subset_right _ _).trans ht₂
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
n : γ → δ
m' : β' → α' → δ
n₁ : β → β'
n₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ g) (map n₂ f)
[PROOFSTEP]
rw [map₂_swap m]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
n : γ → δ
m' : β' → α' → δ
n₁ : β → β'
n₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)
⊢ map n (map₂ (fun a b => m b a) g f) = map₂ m' (map n₁ g) (map n₂ f)
[PROOFSTEP]
exact map_map₂_distrib fun _ _ => h_antidistrib _ _
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a✝ : α
b : β
c : γ
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
l : Filter β
⊢ map₂ f (pure a) l = l
[PROOFSTEP]
rw [map₂_pure_left, show f a = id from funext h, map_id]
[GOAL]
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b✝ : β
c : γ
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
l : Filter α
⊢ map₂ f l (pure b) = l
[PROOFSTEP]
rw [map₂_pure_right, funext h, map_id']


[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℕ) in atTop, p ↑n
[PROOFSTEP]
rw [← Nat.comap_cast_atTop (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℕ) in Filter.comap Nat.cast atTop, p ↑n
[PROOFSTEP]
exact h.comap _
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : r ≤ ↑n
⊢ r ≤ ↑↑n
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ ↑(-↑n) ≤ r
[PROOFSTEP]
simpa [neg_le] using hn
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto f l atTop
[PROOFSTEP]
rw [← @Int.comap_cast_atTop R, tendsto_comap_iff]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Int.cast ∘ f) l atTop
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto f l atBot
[PROOFSTEP]
rw [← @Int.comap_cast_atBot R, tendsto_comap_iff]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Int.cast ∘ f) l atBot
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in atTop, p ↑n
[PROOFSTEP]
rw [← Int.comap_cast_atTop (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atTop, p ↑n
[PROOFSTEP]
exact h.comap _
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in atBot, p ↑n
[PROOFSTEP]
rw [← Int.comap_cast_atBot (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n
[PROOFSTEP]
exact h.comap _
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
r : R
n : ℕ
hn : r ≤ ↑n
⊢ r ≤ ↑↑n
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ ↑(-↑n) ≤ r
[PROOFSTEP]
simpa [neg_le]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto f l atTop
[PROOFSTEP]
rw [← @Rat.comap_cast_atTop R, tendsto_comap_iff]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Rat.cast ∘ f) l atTop
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto f l atBot
[PROOFSTEP]
rw [← @Rat.comap_cast_atBot R, tendsto_comap_iff]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Rat.cast ∘ f) l atBot
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in atTop, p ↑n
[PROOFSTEP]
rw [← Rat.comap_cast_atTop (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atTop, p ↑n
[PROOFSTEP]
exact h.comap _
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in atBot, p ↑n
[PROOFSTEP]
rw [← Rat.comap_cast_atBot (R := R)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atBot, p ↑n
[PROOFSTEP]
exact
  h.comap
    _
      -- porting note: new lemma
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => r * f x) l atTop
[PROOFSTEP]
refine' tendsto_atTop.2 fun b => _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
[PROOFSTEP]
obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
[PROOFSTEP]
rw [nsmul_eq_mul'] at hn
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
[PROOFSTEP]
filter_upwards [tendsto_atTop.1 hf (n * max b 0)] with x hx
[GOAL]
case h
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ r * f x
[PROOFSTEP]
calc
  b ≤ 1 * max b 0 := by {
    rw [one_mul]
    exact le_max_left _ _
  }
  _ ≤ r * n * max b 0 := by gcongr
  _ = r * (n * max b 0) := by rw [mul_assoc]
  _ ≤ r * f x := by gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ 1 * max b 0
[PROOFSTEP]
{ rw [one_mul]
  exact le_max_left _ _
}
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ 1 * max b 0
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ max b 0
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ 1 * max b 0 ≤ r * ↑n * max b 0
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ r * ↑n * max b 0 = r * (↑n * max b 0)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ r * (↑n * max b 0) ≤ r * f x
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atTop
[PROOFSTEP]
refine' tendsto_atTop.2 fun b => _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
[PROOFSTEP]
obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
[PROOFSTEP]
have hn' : 1 ≤ (n : R) * r := by rwa [nsmul_eq_mul] at hn
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ 1 ≤ ↑n * r
[PROOFSTEP]
rwa [nsmul_eq_mul] at hn
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
[PROOFSTEP]
filter_upwards [tendsto_atTop.1 hf (max b 0 * n)] with x hx
[GOAL]
case h
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ f x * r
[PROOFSTEP]
calc
  b ≤ max b 0 * 1 := by {
    rw [mul_one]
    exact le_max_left _ _
  }
  _ ≤ max b 0 * (n * r) := by gcongr
  _ = max b 0 * n * r := by rw [mul_assoc]
  _ ≤ f x * r := by gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0 * 1
[PROOFSTEP]
{ rw [mul_one]
  exact le_max_left _ _
}
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0 * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * 1 ≤ max b 0 * (↑n * r)
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * (↑n * r) = max b 0 * ↑n * r
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * ↑n * r ≤ f x * r
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atBot
[PROOFSTEP]
simpa only [tendsto_neg_atTop_iff, mul_neg] using hf.atTop_mul_const' (neg_pos.mpr hr)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atBot
[PROOFSTEP]
simp only [← tendsto_neg_atTop_iff, ← neg_mul] at hf ⊢
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto (fun x => -f x) l atTop
⊢ Tendsto (fun x => -f x * r) l atTop
[PROOFSTEP]
exact hf.atTop_mul_const' hr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atTop
[PROOFSTEP]
simpa only [mul_neg, tendsto_neg_atBot_iff] using hf.atBot_mul_const' (neg_pos.2 hr)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atTop
[PROOFSTEP]
refine' tendsto_atTop.mpr fun s => _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
[PROOFSTEP]
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
[PROOFSTEP]
exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (nsmul_le_nsmul hr.le ha)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℕ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atBot
[PROOFSTEP]
simpa using hf.atTop_nsmul_const (neg_pos.2 hr)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atTop
[PROOFSTEP]
refine' tendsto_atTop.mpr fun s => _
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
[PROOFSTEP]
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
[PROOFSTEP]
replace hn : s ≤ (n : ℤ) • r
[GOAL]
case hn
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ s ≤ ↑n • r
[PROOFSTEP]
simpa
[GOAL]
case intro
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ ↑n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
[PROOFSTEP]
exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (zsmul_le_zsmul hr.le ha)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atBot
[PROOFSTEP]
simpa using hf.atTop_zsmul_const (neg_pos.2 hr)
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x • r) l atBot
[PROOFSTEP]
simp only [← tendsto_neg_atTop_iff, ← neg_zsmul] at hf ⊢
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto (fun x => -f x) l atTop
⊢ Tendsto (fun x => -f x • r) l atTop
[PROOFSTEP]
exact hf.atTop_zsmul_const hr
[GOAL]
α : Type u_1
R : Type u_2
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x • r) l atTop
[PROOFSTEP]
simpa using hf.atBot_zsmul_const (neg_pos.2 hr)


[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
inst✝¹ : AddZeroClass β
inst✝ : ContinuousAdd β
l : Filter α
f g : α → β
hf : ZeroAtFilter l f
hg : ZeroAtFilter l g
⊢ ZeroAtFilter l (f + g)
[PROOFSTEP]
simpa using hf.add hg
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : ContinuousNeg β
l : Filter α
f : α → β
hf : ZeroAtFilter l f
⊢ ZeroAtFilter l (-f)
[PROOFSTEP]
simpa using hf.neg
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMulWithZero 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
l : Filter α
f : α → β
c : 𝕜
hf : ZeroAtFilter l f
⊢ ZeroAtFilter l (c • f)
[PROOFSTEP]
simpa using hf.const_smul c
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
l : Filter α
f : α → β
hf : ZeroAtFilter l f
⊢ BoundedAtFilter l f
[PROOFSTEP]
rw [ZeroAtFilter, ← Asymptotics.isLittleO_const_iff (one_ne_zero' ℝ)] at hf
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
l : Filter α
f : α → β
hf : f =o[l] fun _x => 1
⊢ BoundedAtFilter l f
[PROOFSTEP]
exact hf.isBigO
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
⊢ BoundedAtFilter l (f + g)
[PROOFSTEP]
simpa using hf.add hg
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
⊢ BoundedAtFilter l (f * g)
[PROOFSTEP]
refine' (hf.mul hg).trans _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
⊢ (fun x => OfNat.ofNat 1 x * OfNat.ofNat 1 x) =O[l] 1
[PROOFSTEP]
convert Asymptotics.isBigO_refl (E := ℝ) _ l
[GOAL]
case h.e'_8.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
x✝ : α
⊢ OfNat.ofNat 1 x✝ = OfNat.ofNat 1 x✝ * OfNat.ofNat 1 x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
⊢ Subalgebra β (α → β)
[PROOFSTEP]
refine' Submodule.toSubalgebra (boundedFilterSubmodule l) _ fun f g hf hg ↦ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
⊢ 1 ∈ boundedFilterSubmodule l
[PROOFSTEP]
exact const_boundedAtFilter l (1 : β)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : f ∈ boundedFilterSubmodule l
hg : g ∈ boundedFilterSubmodule l
⊢ f * g ∈ boundedFilterSubmodule l
[PROOFSTEP]
simpa only [Pi.one_apply, mul_one, norm_mul] using hf.mul hg


[GOAL]
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
[PROOFSTEP]
rcases exists_nonempty_countable_separating α hp t with ⟨S, hSne, hSc, hS⟩
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : Set (Set α)
hSne : Set.Nonempty S
hSc : Set.Countable S
hS :
  (∀ (s : Set α), s ∈ S → p s) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
[PROOFSTEP]
rcases hSc.exists_eq_range hSne with ⟨S, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : Set.Nonempty (range S)
hSc : Set.Countable (range S)
hS :
  (∀ (s : Set α), s ∈ range S → p s) ∧
    ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (s : Set α), s ∈ range S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
[PROOFSTEP]
use S
[GOAL]
case h
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : Set.Nonempty (range S)
hSc : Set.Countable (range S)
hS :
  (∀ (s : Set α), s ∈ range S → p s) ∧
    ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (s : Set α), s ∈ range S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ (∀ (n : ℕ), p (S n)) ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
[PROOFSTEP]
simpa only [forall_range_iff] using hS
[GOAL]
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
⊢ HasCountableSeparatingOn α p t
[PROOFSTEP]
rcases h.1 with ⟨S, hSc, hSq, hS⟩
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ HasCountableSeparatingOn α p t
[PROOFSTEP]
choose! V hpV hV using fun s hs ↦ hpq s (hSq s hs)
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
V : Set ↑t → Set α
hpV : ∀ (s : Set ↑t), s ∈ S → p (V s)
hV : ∀ (s : Set ↑t), s ∈ S → Subtype.val ⁻¹' V s = s
⊢ HasCountableSeparatingOn α p t
[PROOFSTEP]
refine ⟨⟨V '' S, hSc.image _, ball_image_iff.2 hpV, fun x hx y hy h ↦ ?_⟩⟩
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
V : Set ↑t → Set α
hpV : ∀ (s : Set ↑t), s ∈ S → p (V s)
hV : ∀ (s : Set ↑t), s ∈ S → Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ (s : Set α), s ∈ V '' S → (x ∈ s ↔ y ∈ s)
⊢ x = y
[PROOFSTEP]
refine congr_arg Subtype.val (hS ⟨x, hx⟩ trivial ⟨y, hy⟩ trivial fun U hU ↦ ?_)
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
V : Set ↑t → Set α
hpV : ∀ (s : Set ↑t), s ∈ S → p (V s)
hV : ∀ (s : Set ↑t), s ∈ S → Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ (s : Set α), s ∈ V '' S → (x ∈ s ↔ y ∈ s)
U : Set ↑t
hU : U ∈ S
⊢ { val := x, property := hx } ∈ U ↔ { val := y, property := hy } ∈ U
[PROOFSTEP]
rw [← hV U hU]
[GOAL]
case intro.intro.intro
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : Set.Countable S
hSq : ∀ (s : Set ↑t), s ∈ S → q s
hS : ∀ (x : ↑t), x ∈ univ → ∀ (y : ↑t), y ∈ univ → (∀ (s : Set ↑t), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
V : Set ↑t → Set α
hpV : ∀ (s : Set ↑t), s ∈ S → p (V s)
hV : ∀ (s : Set ↑t), s ∈ S → Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ (s : Set α), s ∈ V '' S → (x ∈ s ↔ y ∈ s)
U : Set ↑t
hU : U ∈ S
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' V U ↔ { val := y, property := hy } ∈ Subtype.val ⁻¹' V U
[PROOFSTEP]
exact h _ (mem_image_of_mem _ hU)
[GOAL]
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ t, t ⊆ s ∧ Set.Subsingleton t ∧ t ∈ l
[PROOFSTEP]
rcases h.1 with ⟨S, hSc, hSp, hS⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ ∃ t, t ⊆ s ∧ Set.Subsingleton t ∧ t ∈ l
[PROOFSTEP]
refine ⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩
[GOAL]
case intro.intro.intro.refine_1
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ ⊆ s
[PROOFSTEP]
exact fun _ h ↦ h.1.1
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ Set.Subsingleton (s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ)
[PROOFSTEP]
intro x hx y hy
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ
y : α
hy : y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ
⊢ x = y
[PROOFSTEP]
simp only [mem_sInter, mem_inter_iff, mem_iInter, mem_compl_iff] at hx hy
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
⊢ x = y
[PROOFSTEP]
refine hS x hx.1.1 y hy.1.1 (fun s hsS ↦ ?_)
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]
cases hl s (hSp s hsS) with
| inl hsl => simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
| inr hsl => simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
x✝ : s ∈ l ∨ sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]
cases hl s (hSp s hsS) with
| inl hsl => simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
| inr hsl => simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
[GOAL]
case intro.intro.intro.refine_2.inl
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
hsl : s ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]

| inl hsl => simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
[GOAL]
case intro.intro.intro.refine_2.inl
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
hsl : s ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]
simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
[GOAL]
case intro.intro.intro.refine_2.inr
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
hsl : sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]

| inr hsl => simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
[GOAL]
case intro.intro.intro.refine_2.inr
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s✝ → ∀ (y : α), y ∈ s✝ → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬x ∈ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α), i ∈ S → iᶜ ∈ l → ¬y ∈ i
s : Set α
hsS : s ∈ S
hsl : sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s
[PROOFSTEP]
simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
[GOAL]
case intro.intro.intro.refine_3
α : Type u_1
β : Sort ?u.5043
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : Set.Countable S
hSp : ∀ (s : Set α), s ∈ S → p s
hS : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U : Set α) (_ : U ∈ S) (_ : Uᶜ ∈ l), Uᶜ ∈ l
[PROOFSTEP]
exact
  inter_mem (inter_mem hs ((countable_sInter_mem (hSc.mono (inter_subset_left _ _))).2 fun _ h ↦ h.2))
    ((countable_bInter_mem hSc).2 fun U hU ↦ iInter_mem.2 id)
[GOAL]
α : Type u_1
β : Sort ?u.6801
l : Filter α
inst✝¹ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : Set.Nonempty s
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ a, a ∈ s ∧ {a} ∈ l
[PROOFSTEP]
rcases exists_subset_subsingleton_mem_of_forall_separating p hs hl with ⟨t, hts, ht, htl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Sort ?u.6801
l : Filter α
inst✝¹ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : Set.Nonempty s
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
t : Set α
hts : t ⊆ s
ht : Set.Subsingleton t
htl : t ∈ l
⊢ ∃ a, a ∈ s ∧ {a} ∈ l
[PROOFSTEP]
rcases ht.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
[GOAL]
case intro.intro.intro.inl
α : Type u_1
β : Sort ?u.6801
l : Filter α
inst✝¹ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : Set.Nonempty s
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hts : ∅ ⊆ s
ht : Set.Subsingleton ∅
htl : ∅ ∈ l
⊢ ∃ a, a ∈ s ∧ {a} ∈ l
[PROOFSTEP]
exact hne.imp fun a ha ↦ ⟨ha, mem_of_superset htl (empty_subset _)⟩
[GOAL]
case intro.intro.intro.inr.intro
α : Type u_1
β : Sort ?u.6801
l : Filter α
inst✝¹ : CountableInterFilter l
f g : α → β
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : Set.Nonempty s
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : Set.Subsingleton {x}
htl : {x} ∈ l
⊢ ∃ a, a ∈ s ∧ {a} ∈ l
[PROOFSTEP]
exact ⟨x, hts rfl, htl⟩
[GOAL]
α : Type u_1
β : Sort ?u.7319
l : Filter α
inst✝² : CountableInterFilter l
f g : α → β
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ a, {a} ∈ l
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with rfl | hne
[GOAL]
case inl
α : Type u_1
β : Sort ?u.7319
l : Filter α
inst✝² : CountableInterFilter l
f g : α → β
inst✝¹ : Nonempty α
p : Set α → Prop
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inst✝ : HasCountableSeparatingOn α p ∅
hs : ∅ ∈ l
⊢ ∃ a, {a} ∈ l
[PROOFSTEP]
exact ‹Nonempty α›.elim fun a ↦ ⟨a, mem_of_superset hs (empty_subset _)⟩
[GOAL]
case inr
α : Type u_1
β : Sort ?u.7319
l : Filter α
inst✝² : CountableInterFilter l
f g : α → β
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : Set.Nonempty s
⊢ ∃ a, {a} ∈ l
[PROOFSTEP]
exact (exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating p hs hne hl).imp fun _ ↦ And.right
[GOAL]
α : Type u_2
β : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
⊢ f =ᶠ[l] g
[PROOFSTEP]
rcases h'.1 with ⟨S, hSc, hSp, hS⟩
[GOAL]
case intro.intro.intro
α : Type u_2
β : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : Set.Countable S
hSp : ∀ (s : Set β), s ∈ S → p s
hS : ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → (∀ (s : Set β), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
⊢ f =ᶠ[l] g
[PROOFSTEP]
have H : ∀ᶠ x in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s := (eventually_countable_ball hSc).2 fun s hs ↦ (h _ (hSp _ hs))
[GOAL]
case intro.intro.intro
α : Type u_2
β : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : Set.Countable S
hSp : ∀ (s : Set β), s ∈ S → p s
hS : ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → (∀ (s : Set β), s ∈ S → (x ∈ s ↔ y ∈ s)) → x = y
H : ∀ᶠ (x : α) in l, ∀ (s : Set β), s ∈ S → (f x ∈ s ↔ g x ∈ s)
⊢ f =ᶠ[l] g
[PROOFSTEP]
filter_upwards [H, hf, hg] with x hx hxf hxg using hS _ hxf _ hxg hx


[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
⊢ EventuallyConst f l ↔ ∃ x, Tendsto f l (pure x)
[PROOFSTEP]
simp_rw [EventuallyConst, EventuallyEq, tendsto_pure]
[GOAL]
α : Type u_1
β : Sort ?u.805
l : Filter α
f : α → β
p : α → Prop
⊢ EventuallyConst p l ↔ (p =ᶠ[l] fun x => False) ∨ p =ᶠ[l] fun x => True
[PROOFSTEP]
simp only [EventuallyConst, Prop.exists_iff]
[GOAL]
α : Type u_1
β : Sort ?u.958
l : Filter α
f : α → β
p : α → Prop
⊢ EventuallyConst p l ↔ (∀ᶠ (x : α) in l, p x) ∨ ∀ᶠ (x : α) in l, ¬p x
[PROOFSTEP]
simp [eventuallyConst_pred', or_comm, EventuallyEq]
[GOAL]
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : Nonempty β
⊢ EventuallyConst f ⊥
[PROOFSTEP]
simp [EventuallyConst, EventuallyEq]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : Subsingleton α
inst✝ : Nonempty β
⊢ EventuallyConst f l
[PROOFSTEP]
rcases isEmpty_or_nonempty α with h | h
[GOAL]
case inl
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : Subsingleton α
inst✝ : Nonempty β
h : IsEmpty α
⊢ EventuallyConst f l
[PROOFSTEP]
simp only [l.filter_eq_bot_of_isEmpty, EventuallyConst.bot]
[GOAL]
case inr
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : Subsingleton α
inst✝ : Nonempty β
h : Nonempty α
⊢ EventuallyConst f l
[PROOFSTEP]
inhabit α
[GOAL]
case inr
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : Subsingleton α
inst✝ : Nonempty β
h : Nonempty α
inhabited_h : Inhabited α
⊢ EventuallyConst f l
[PROOFSTEP]
refine ⟨f default, eventually_of_forall fun x ↦ congr_arg f <| Subsingleton.elim _ _⟩
[GOAL]
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
h : EventuallyConst (mulIndicator s fun x => c) l
⊢ EventuallyConst s l
[PROOFSTEP]
rw [eventuallyConst_set]
[GOAL]
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
h : EventuallyConst (mulIndicator s fun x => c) l
⊢ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, ¬x ∈ s
[PROOFSTEP]
rcases h with ⟨d, hd⟩
[GOAL]
case intro
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
d : β
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => d
⊢ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, ¬x ∈ s
[PROOFSTEP]
rcases eq_or_ne d 1 with rfl | hd₁
[GOAL]
case intro.inl
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => 1
⊢ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, ¬x ∈ s
[PROOFSTEP]
refine .inr <| hd.mono fun x hx ↦ ?_
[GOAL]
case intro.inl
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => 1
x : α
hx : mulIndicator s (fun x => c) x = (fun x => 1) x
⊢ ¬x ∈ s
[PROOFSTEP]
simpa only [mulIndicator_apply_eq_one, hc] using hx
[GOAL]
case intro.inr
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
d : β
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => d
hd₁ : d ≠ 1
⊢ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, ¬x ∈ s
[PROOFSTEP]
refine .inl <| hd.mono fun x hx ↦ ?_
[GOAL]
case intro.inr
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
d : β
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => d
hd₁ : d ≠ 1
x : α
hx : mulIndicator s (fun x => c) x = (fun x => d) x
⊢ x ∈ s
[PROOFSTEP]
simpa [hc] using ne_of_eq_of_ne hx hd₁
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
⊢ EventuallyConst f atTop ↔ ∃ i, ∀ (j : α), i ≤ j → f j = f i
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
⊢ EventuallyConst f atTop → ∃ i, ∀ (j : α), i ≤ j → f j = f i
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
c : β
hc : f =ᶠ[atTop] fun x => c
⊢ ∃ i, ∀ (j : α), i ≤ j → f j = f i
[PROOFSTEP]
rcases eventually_atTop.1 hc with ⟨i, hi⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
c : β
hc : f =ᶠ[atTop] fun x => c
i : α
hi : ∀ (b : α), b ≥ i → f b = (fun x => c) b
⊢ ∃ i, ∀ (j : α), i ≤ j → f j = f i
[PROOFSTEP]
exact ⟨i, fun j hj ↦ (hi j hj).trans (hi i le_rfl).symm⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
⊢ (∃ i, ∀ (j : α), i ≤ j → f j = f i) → EventuallyConst f atTop
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
i : α
hi : ∀ (j : α), i ≤ j → f j = f i
⊢ EventuallyConst f atTop
[PROOFSTEP]
exact ⟨f i, eventually_atTop.2 ⟨i, hi⟩⟩
[GOAL]
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
⊢ EventuallyConst f atTop ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
[PROOFSTEP]
rw [eventuallyConst_atTop]
[GOAL]
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
⊢ (∃ i, ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
[PROOFSTEP]
refine exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩
[GOAL]
case refine_1
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (j : ℕ), n ≤ j → f j = f n
m : ℕ
hm : n ≤ m
⊢ f (m + 1) = f m
[PROOFSTEP]
exact (h (m + 1) (hm.trans m.le_succ)).trans (h m hm).symm
[GOAL]
case refine_2
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n
[PROOFSTEP]
induction m, hm using Nat.le_induction with
| base => rfl
| succ m hm ihm => exact (h m hm).trans ihm
[GOAL]
case refine_2
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n
[PROOFSTEP]
induction m, hm using Nat.le_induction with
| base => rfl
| succ m hm ihm => exact (h m hm).trans ihm
[GOAL]
case refine_2.base
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
⊢ f n = f n
[PROOFSTEP]

| base => rfl
[GOAL]
case refine_2.base
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
⊢ f n = f n
[PROOFSTEP]
rfl
[GOAL]
case refine_2.succ
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m✝ m : ℕ
hm : n ≤ m
ihm : f m = f n
⊢ f (m + 1) = f n
[PROOFSTEP]

| succ m hm ihm => exact (h m hm).trans ihm
[GOAL]
case refine_2.succ
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m✝ m : ℕ
hm : n ≤ m
ihm : f m = f n
⊢ f (m + 1) = f n
[PROOFSTEP]
exact (h m hm).trans ihm


[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
s : Set α
l : Filter α
a : α
t✝ : Set α
l' : Filter α
t : Set δ
g : δ → α
b : δ
hf : IsMinOn f s a
hg : MapsTo g t s
ha : g b = a
y : δ
hy : y ∈ t
⊢ y ∈ {x | (fun x => (f ∘ g) b ≤ (f ∘ g) x) x}
[PROOFSTEP]
simpa only [ha, (· ∘ ·)] using hf (hg hy)
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
l : Filter α
hf : IsMinFilter f l a
hg : IsMaxFilter g l a
⊢ IsMinFilter (fun x => f x - g x) l a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMinFilter g l a
⊢ IsMaxFilter (fun x => f x - g x) l a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
l : Filter α
hf : IsMinOn f s a
hg : IsMaxOn g s a
⊢ IsMinOn (fun x => f x - g x) s a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
[GOAL]
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
l : Filter α
hf : IsMaxOn f s a
hg : IsMinOn g s a
⊢ IsMaxOn (fun x => f x - g x) s a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
⊢ IsMaxFilter g l a
[PROOFSTEP]
refine' hle.mp (h.mono fun x hf hgf => _)
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ g a
[PROOFSTEP]
rw [← hfga]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ f a
[PROOFSTEP]
exact le_trans hgf hf
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
h : IsExtrFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsExtrFilter g l a
[PROOFSTEP]
rw [IsExtrFilter] at *
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
h : IsMinFilter f l a ∨ IsMaxFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMinFilter g l a ∨ IsMaxFilter g l a
[PROOFSTEP]
rwa [← heq.isMaxFilter_iff hfga, ← heq.isMinFilter_iff hfga]