[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ (i : ι) (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
[PROOFSTEP]
rw [biInter_eq_iInter]
[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
[PROOFSTEP]
haveI := hS.toEncodable
[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
s : (i : ι) → i ∈ S → Set α
this : Encodable ↑S
⊢ ⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
[PROOFSTEP]
exact countable_iInter_mem.trans Subtype.forall
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
inst✝ : Countable ι
p : α → ι → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
[PROOFSTEP]
simpa only [Filter.Eventually, setOf_forall] using @countable_iInter_mem _ _ l _ _ fun i => {x | p x i}
[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi
[PROOFSTEP]
simpa only [Filter.Eventually, setOf_forall] using @countable_bInter_mem _ l _ _ _ hS fun i hi => {x | p x i hi}
[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ (i : ι) (h : i ∈ S), s i h ≤ᶠ[l] ⋃ (i : ι) (h : i ∈ S), t i h
[PROOFSTEP]
simp only [biUnion_eq_iUnion]
[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ (x : ↑S), s ↑x (_ : ↑x ∈ S) ≤ᶠ[l] ⋃ (x : ↑S), t ↑x (_ : ↑x ∈ S)
[PROOFSTEP]
haveI := hS.toEncodable
[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable ↑S
⊢ ⋃ (x : ↑S), s ↑x (_ : ↑x ∈ S) ≤ᶠ[l] ⋃ (x : ↑S), t ↑x (_ : ↑x ∈ S)
[PROOFSTEP]
exact EventuallyLE.countable_iUnion fun i => h i i.2
[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ (i : ι) (h : i ∈ S), s i h ≤ᶠ[l] ⋂ (i : ι) (h : i ∈ S), t i h
[PROOFSTEP]
simp only [biInter_eq_iInter]
[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S) ≤ᶠ[l] ⋂ (x : ↑S), t ↑x (_ : ↑x ∈ S)
[PROOFSTEP]
haveI := hS.toEncodable
[GOAL]
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : Set.Countable S
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable ↑S
⊢ ⋂ (x : ↑S), s ↑x (_ : ↑x ∈ S) ≤ᶠ[l] ⋂ (x : ↑S), t ↑x (_ : ↑x ∈ S)
[PROOFSTEP]
exact EventuallyLE.countable_iInter fun i => h i i.2
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter ⊥
[PROOFSTEP]
rw [← principal_empty]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter (𝓟 ∅)
[PROOFSTEP]
apply countableInterFilter_principal
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter ⊤
[PROOFSTEP]
rw [← principal_univ]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter (𝓟 univ)
[PROOFSTEP]
apply countableInterFilter_principal
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (comap f l)
[PROOFSTEP]
refine' ⟨fun S hSc hS => _⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : Set.Countable S
hS : ∀ (s : Set α), s ∈ S → s ∈ comap f l
⊢ ⋂₀ S ∈ comap f l
[PROOFSTEP]
choose! t htl ht using hS
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : Set.Countable S
t : Set α → Set β
htl : ∀ (s : Set α), s ∈ S → t s ∈ l
ht : ∀ (s : Set α), s ∈ S → f ⁻¹' t s ⊆ s
⊢ ⋂₀ S ∈ comap f l
[PROOFSTEP]
have : (⋂ s ∈ S, t s) ∈ l := (countable_bInter_mem hSc).2 htl
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : Set.Countable S
t : Set α → Set β
htl : ∀ (s : Set α), s ∈ S → t s ∈ l
ht : ∀ (s : Set α), s ∈ S → f ⁻¹' t s ⊆ s
this : ⋂ (s : Set α) (_ : s ∈ S), t s ∈ l
⊢ ⋂₀ S ∈ comap f l
[PROOFSTEP]
refine' ⟨_, this, _⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : Set.Countable S
t : Set α → Set β
htl : ∀ (s : Set α), s ∈ S → t s ∈ l
ht : ∀ (s : Set α), s ∈ S → f ⁻¹' t s ⊆ s
this : ⋂ (s : Set α) (_ : s ∈ S), t s ∈ l
⊢ f ⁻¹' ⋂ (s : Set α) (_ : s ∈ S), t s ⊆ ⋂₀ S
[PROOFSTEP]
simpa [preimage_iInter] using iInter₂_mono ht
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (map f l)
[PROOFSTEP]
refine' ⟨fun S hSc hS => _⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : Set.Countable S
hS : ∀ (s : Set β), s ∈ S → s ∈ map f l
⊢ ⋂₀ S ∈ map f l
[PROOFSTEP]
simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : Set.Countable S
hS : ∀ (s : Set β), s ∈ S → f ⁻¹' s ∈ l
⊢ ⋂ (i : Set β) (_ : i ∈ S), f ⁻¹' i ∈ l
[PROOFSTEP]
exact (countable_bInter_mem hSc).2 hS
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊓ l₂)
[PROOFSTEP]
refine' ⟨fun S hSc hS => _⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
hS : ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊓ l₂
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
[PROOFSTEP]
choose s hs t ht hst using hS
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
s : (s : Set α) → s ∈ S → Set α
hs : ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁
t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
[PROOFSTEP]
replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem hSc).2 hs
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
s t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α) (h : i ∈ S), s i h ∈ l₁
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
[PROOFSTEP]
replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (countable_bInter_mem hSc).2 ht
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α) (h : i ∈ S), s i h ∈ l₁
ht : ⋂ (i : Set α) (h : i ∈ S), t i h ∈ l₂
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
[PROOFSTEP]
refine' mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => _)
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α) (h : i ∈ S), s i h ∈ l₁
ht : ⋂ (i : Set α) (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ (⋂ (i : Set α) (h : i ∈ S), s i h) ∩ ⋂ (i : Set α) (h : i ∈ S), t i h ⊆ i
[PROOFSTEP]
rw [hst i hi]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α) (h : i ∈ S), s i h ∈ l₁
ht : ⋂ (i : Set α) (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ (⋂ (i : Set α) (h : i ∈ S), s i h) ∩ ⋂ (i : Set α) (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi
[PROOFSTEP]
apply inter_subset_inter
[GOAL]
case h₁
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α) (h : i ∈ S), s i h ∈ l₁
ht : ⋂ (i : Set α) (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ ⋂ (i : Set α) (h : i ∈ S), s i h ⊆ s i hi
[PROOFSTEP]
exact iInter_subset_of_subset i (iInter_subset _ _)
[GOAL]
case h₂
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α) (h : i ∈ S), s i h ∈ l₁
ht : ⋂ (i : Set α) (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ ⋂ (i : Set α) (h : i ∈ S), t i h ⊆ t i hi
[PROOFSTEP]
exact iInter_subset_of_subset i (iInter_subset _ _)
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊔ l₂)
[PROOFSTEP]
refine' ⟨fun S hSc hS => ⟨_, _⟩⟩
[GOAL]
case refine'_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
hS : ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₁.sets
[PROOFSTEP]
refine' (countable_sInter_mem hSc).2 fun s hs => _
[GOAL]
case refine'_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
hS : ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₂.sets
[PROOFSTEP]
refine' (countable_sInter_mem hSc).2 fun s hs => _
[GOAL]
case refine'_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
hS : ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₁
case refine'_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : Set.Countable S
hS : ∀ (s : Set α), s ∈ S → s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₂
[PROOFSTEP]
exacts [(hS s hs).1, (hS s hs).2]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
⊢ CountableInterFilter (countableGenerate g)
[PROOFSTEP]
delta countableGenerate
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
⊢ CountableInterFilter
    (ofCountableInter (CountableGenerateSets g)
      (_ :
        ∀ (x : Set (Set α)),
          Set.Countable x → (∀ (s : Set α), s ∈ x → CountableGenerateSets g s) → CountableGenerateSets g (⋂₀ x))
      (_ : ∀ (x x_1 : Set α), CountableGenerateSets g x → x ⊆ x_1 → CountableGenerateSets g x_1))
[PROOFSTEP]
infer_instance
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
⊢ s ∈ countableGenerate g ↔ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
⊢ s ∈ countableGenerate g → ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
[PROOFSTEP]
intro h
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
⊢ (∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s) → s ∈ countableGenerate g
[PROOFSTEP]
intro h
[GOAL]
case mp
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
h : s ∈ countableGenerate g
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
[PROOFSTEP]
induction' h with s hs s t _ st ih S Sct _ ih
[GOAL]
case mp.basic
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ s : Set α
hs : s ∈ g
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
[PROOFSTEP]
exact ⟨{ s }, by simp [hs, subset_refl]⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ s : Set α
hs : s ∈ g
⊢ {s} ⊆ g ∧ Set.Countable {s} ∧ ⋂₀ {s} ⊆ s
[PROOFSTEP]
simp [hs, subset_refl]
[GOAL]
case mp.univ
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ univ
[PROOFSTEP]
exact ⟨∅, by simp⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
⊢ ∅ ⊆ g ∧ Set.Countable ∅ ∧ ⋂₀ ∅ ⊆ univ
[PROOFSTEP]
simp
[GOAL]
case mp.superset
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ s t : Set α
a✝ : CountableGenerateSets g s
st : s ⊆ t
ih : ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
⊢ ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ t
[PROOFSTEP]
refine' Exists.imp (fun S => _) ih
[GOAL]
case mp.superset
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ s t : Set α
a✝ : CountableGenerateSets g s
st : s ⊆ t
ih : ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
S : Set (Set α)
⊢ S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s → S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ t
[PROOFSTEP]
tauto
[GOAL]
case mp.sInter
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : Set.Countable S
a✝ : ∀ (s : Set α), s ∈ S → CountableGenerateSets g s
ih : ∀ (s : Set α), s ∈ S → ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
⊢ ∃ S_1, S_1 ⊆ g ∧ Set.Countable S_1 ∧ ⋂₀ S_1 ⊆ ⋂₀ S
[PROOFSTEP]
choose T Tg Tct hT using ih
[GOAL]
case mp.sInter
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : Set.Countable S
a✝ : ∀ (s : Set α), s ∈ S → CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∃ S_1, S_1 ⊆ g ∧ Set.Countable S_1 ∧ ⋂₀ S_1 ⊆ ⋂₀ S
[PROOFSTEP]
refine' ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, _⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : Set.Countable S
a✝ : ∀ (s : Set α), s ∈ S → CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ⋃ (s : Set α) (H : s ∈ S), T s H ⊆ g
[PROOFSTEP]
simpa
[GOAL]
case mp.sInter
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : Set.Countable S
a✝ : ∀ (s : Set α), s ∈ S → CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ⋂₀ ⋃ (s : Set α) (H : s ∈ S), T s H ⊆ ⋂₀ S
[PROOFSTEP]
apply subset_sInter
[GOAL]
case mp.sInter.h
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : Set.Countable S
a✝ : ∀ (s : Set α), s ∈ S → CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
⊢ ∀ (t' : Set α), t' ∈ S → ⋂₀ ⋃ (s : Set α) (H : s ∈ S), T s H ⊆ t'
[PROOFSTEP]
intro s H
[GOAL]
case mp.sInter.h
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sct : Set.Countable S
a✝ : ∀ (s : Set α), s ∈ S → CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), Set.Countable (T s a)
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
s : Set α
H : s ∈ S
⊢ ⋂₀ ⋃ (s : Set α) (H : s ∈ S), T s H ⊆ s
[PROOFSTEP]
refine' subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
h : ∃ S, S ⊆ g ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
[PROOFSTEP]
rcases h with ⟨S, Sg, Sct, hS⟩
[GOAL]
case mpr.intro.intro.intro
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : Set.Countable S
hS : ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
[PROOFSTEP]
refine' mem_of_superset ((countable_sInter_mem Sct).mpr _) hS
[GOAL]
case mpr.intro.intro.intro
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : Set.Countable S
hS : ⋂₀ S ⊆ s
⊢ ∀ (s : Set α), s ∈ S → s ∈ countableGenerate g
[PROOFSTEP]
intro s H
[GOAL]
case mpr.intro.intro.intro
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : Set.Countable S
hS : ⋂₀ S ⊆ s✝
s : Set α
H : s ∈ S
⊢ s ∈ countableGenerate g
[PROOFSTEP]
exact CountableGenerateSets.basic (Sg H)
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g ↔ g ⊆ f.sets
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g → g ⊆ f.sets
[PROOFSTEP]
intro h
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ g ⊆ f.sets → f ≤ countableGenerate g
[PROOFSTEP]
intro h
[GOAL]
case mp
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : f ≤ countableGenerate g
⊢ g ⊆ f.sets
[PROOFSTEP]
exact subset_trans (fun s => CountableGenerateSets.basic) h
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
⊢ f ≤ countableGenerate g
[PROOFSTEP]
intro s hs
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
hs : s ∈ countableGenerate g
⊢ s ∈ f
[PROOFSTEP]
induction' hs with s hs s t _ st ih S Sct _ ih
[GOAL]
case mpr.basic
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s✝ s : Set α
hs : s ∈ g
⊢ s ∈ f
[PROOFSTEP]
exact h hs
[GOAL]
case mpr.univ
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
⊢ univ ∈ f
[PROOFSTEP]
exact univ_mem
[GOAL]
case mpr.superset
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s✝ s t : Set α
a✝ : CountableGenerateSets g s
st : s ⊆ t
ih : s ∈ f
⊢ t ∈ f
[PROOFSTEP]
exact mem_of_superset ih st
[GOAL]
case mpr.sInter
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝¹ : CountableInterFilter l
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
S : Set (Set α)
Sct : Set.Countable S
a✝ : ∀ (s : Set α), s ∈ S → CountableGenerateSets g s
ih : ∀ (s : Set α), s ∈ S → s ∈ f
⊢ ⋂₀ S ∈ f
[PROOFSTEP]
exact (countable_sInter_mem Sct).mpr ih
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
⊢ IsGreatest {f | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)
[PROOFSTEP]
refine' ⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, _⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
⊢ countableGenerate g ∈ upperBounds {f | CountableInterFilter f ∧ g ⊆ f.sets}
[PROOFSTEP]
rintro f ⟨fct, hf⟩
[GOAL]
case intro
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ f ≤ countableGenerate g
[PROOFSTEP]
rwa [@le_countableGenerate_iff_of_countableInterFilter _ _ _ fct]


[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
f : Filter α
h₁ : NeBot f
h₂ : ∀ (g : Filter α), NeBot g → g ≤ f → f ≤ g
g : Filter α
neBot'✝ : NeBot g
le_of_le✝ : ∀ (g_1 : Filter α), NeBot g_1 → g_1 ≤ g → g ≤ g_1
x✝ : ↑{ toFilter := f, neBot' := h₁, le_of_le := h₂ } = ↑{ toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
⊢ { toFilter := f, neBot' := h₁, le_of_le := h₂ } = { toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
g : Filter α
hg : NeBot (g ⊓ ↑f)
⊢ NeBot (↑f ⊓ g)
[PROOFSTEP]
rwa [inf_comm]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ¬↑f ≤ g
[PROOFSTEP]
rw [← inf_neBot_iff, neBot_iff, Ne.def, not_not, disjoint_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
hsc : ¬sᶜ ∈ f
h : ↑f ⊓ 𝓟 s = ⊥
⊢ ↑f ⊓ 𝓟 sᶜᶜ = ⊥
[PROOFSTEP]
rwa [compl_compl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
⊢ sᶜ ∈ f ↔ ¬s ∈ f
[PROOFSTEP]
rw [← compl_not_mem_iff, compl_compl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Filter α
h : ∀ (s : Set α), ¬sᶜ ∈ f ↔ s ∈ f
hf : f = ⊥
⊢ False
[PROOFSTEP]
simp [hf] at h
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
u : Ultrafilter α
f g : Filter α
⊢ ¬↑u ≤ f ⊔ g ↔ ¬(↑u ≤ f ∨ ↑u ≤ g)
[PROOFSTEP]
simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
⊢ s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f
[PROOFSTEP]
simp only [← mem_coe, ← le_principal_iff, ← sup_principal, le_sup_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
⊢ (∀ᶠ (x : α) in ↑f, p x → q x) ↔ (∀ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, q x
[PROOFSTEP]
simp only [imp_iff_not_or, eventually_or, eventually_not]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
s : Set (Set α)
hs : Set.Finite s
⊢ ⋃₀ ∅ ∈ f ↔ ∃ t, t ∈ ∅ ∧ t ∈ f
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝¹ t : Set α
p q : α → Prop
s : Set (Set α)
hs : Set.Finite s
a✝ : Set α
s✝ : Set (Set α)
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
his : ⋃₀ s✝ ∈ f ↔ ∃ t, t ∈ s✝ ∧ t ∈ f
⊢ ⋃₀ insert a✝ s✝ ∈ f ↔ ∃ t, t ∈ insert a✝ s✝ ∧ t ∈ f
[PROOFSTEP]
simp [union_mem_iff, his, or_and_right, exists_or]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
is : Set β
s : β → Set α
his : Set.Finite is
⊢ ⋃ (i : β) (_ : i ∈ is), s i ∈ f ↔ ∃ i, i ∈ is ∧ s i ∈ f
[PROOFSTEP]
simp only [← sUnion_image, finite_sUnion_mem_iff (his.image s), bex_image_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
m : α → β
u : Ultrafilter β
inj : Injective m
large : range m ∈ u
g : Filter α
hg : NeBot g
hgu : g ≤ Filter.comap m ↑u
⊢ Filter.comap m ↑u ≤ g
[PROOFSTEP]
simp only [← u.unique (map_le_iff_le_comap.2 hgu), comap_map inj, le_rfl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) (_ : Injective id)
⊢ range id ∈ f
[PROOFSTEP]
rw [range_id]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective id) (_ : Injective id)
⊢ univ ∈ f
[PROOFSTEP]
exact univ_mem
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ comap f inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) (_ : Injective (n ∘ m))
⊢ range (n ∘ m) ∈ f
[PROOFSTEP]
rw [range_comp]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ comap f inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) (_ : Injective (n ∘ m))
⊢ n '' range m ∈ f
[PROOFSTEP]
exact image_mem_of_mem_comap large₀ large₁
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
α✝ : Type ?u.19487
a : α✝
s : Set α✝
⊢ ¬sᶜ ∈ pure a ↔ s ∈ pure a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = ↑(pure a)
[PROOFSTEP]
rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : s ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
[PROOFSTEP]
rw [← biUnion_of_singleton s] at h'
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : ⋃ (x : α) (_ : x ∈ s), {x} ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
[PROOFSTEP]
rcases(Ultrafilter.finite_biUnion_mem_iff h).mp h' with ⟨a, has, haf⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
h : Set.Finite s
h' : ⋃ (x : α) (_ : x ∈ s), {x} ∈ f
a : α
has : a ∈ s
haf : {a} ∈ f
⊢ ∃ x, x ∈ s ∧ f = pure x
[PROOFSTEP]
exact ⟨a, has, eq_of_le (Filter.le_pure_iff.2 haf)⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s✝ t : Set α
p q : α → Prop
f : Ultrafilter α
m : α → Ultrafilter β
s : Set β
⊢ (¬sᶜ ∈ Filter.bind ↑f fun x => ↑(m x)) ↔ s ∈ Filter.bind ↑f fun x => ↑(m x)
[PROOFSTEP]
simp only [mem_bind', mem_coe, ← compl_mem_iff_not_mem, compl_setOf, compl_compl]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
[PROOFSTEP]
refine' ⟨fun hf g hg => hg hf, fun H => by_contra fun hf => _⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
⊢ False
[PROOFSTEP]
set g : Filter (sᶜ : Set α) := comap (↑) f
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑sᶜ := comap Subtype.val f
⊢ False
[PROOFSTEP]
haveI : NeBot g := comap_neBot_iff_compl_range.2 (by simpa [compl_setOf])
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑sᶜ := comap Subtype.val f
⊢ ¬(range Subtype.val)ᶜ ∈ f
[PROOFSTEP]
simpa [compl_setOf]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
hf : ¬s ∈ f
g : Filter ↑sᶜ := comap Subtype.val f
this : NeBot g
⊢ False
[PROOFSTEP]
simpa using H ((of g).map (↑)) (map_le_iff_le_comap.mpr (of_le g))
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : Filter α
s : Set α
a : α
f f' : Filter α
⊢ ⨆ (g : Ultrafilter α) (_ : ↑g ≤ f), ↑g ≤ f' ↔ f ≤ f'
[PROOFSTEP]
simp only [iSup_le_iff, ← le_iff_ultrafilter]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : Filter α
s : Set α
a : α
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Tendsto f (↑g) l₂
[PROOFSTEP]
simpa only [tendsto_iff_comap] using le_iff_ultrafilter
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Filter α), NeBot f → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
[PROOFSTEP]
refine' ⟨fun H f hf => H f f.neBot hf, _⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f) → ∀ (f : Filter α), NeBot f → f ≤ g → p f
[PROOFSTEP]
intro H f hf hfg
[GOAL]
α : Type u
β : Type v
γ : Type u_1
f✝ : Filter α
s : Set α
a : α
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
f : Filter α
hf : NeBot f
hfg : f ≤ g
⊢ p f
[PROOFSTEP]
exact hp (of_le f) (H _ ((of_le f).trans hfg))
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ s ∈ ofComapInfPrincipal h
[PROOFSTEP]
let f := Filter.comap m g ⊓ 𝓟 s
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ s ∈ ofComapInfPrincipal h
[PROOFSTEP]
haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ s ∈ ofComapInfPrincipal h
[PROOFSTEP]
have : s ∈ f := mem_inf_of_right (mem_principal_self s)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this✝ : NeBot f
this : s ∈ f
⊢ s ∈ ofComapInfPrincipal h
[PROOFSTEP]
exact le_def.mp (of_le _) s this
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ map m (ofComapInfPrincipal h) = g
[PROOFSTEP]
let f := Filter.comap m g ⊓ 𝓟 s
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ map m (ofComapInfPrincipal h) = g
[PROOFSTEP]
haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ map m (ofComapInfPrincipal h) = g
[PROOFSTEP]
apply eq_of_le
[GOAL]
case h
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ ↑(map m (ofComapInfPrincipal h)) ≤ ↑g
[PROOFSTEP]
calc
  Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
  _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
  _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
  _ ≤ ↑g ⊓ (𝓟 <| m '' s) := (inf_le_inf_right _ map_comap_le)
  _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ Filter.map m (Filter.comap m ↑g) ⊓ Filter.map m (𝓟 s) = Filter.map m (Filter.comap m ↑g) ⊓ 𝓟 (m '' s)
[PROOFSTEP]
rw [map_principal]


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ StrictMonoOn f (s ∪ t)
[PROOFSTEP]
have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s := by
  intro x hx hxc
  cases hx
  · assumption
  rcases eq_or_lt_of_le hxc with (rfl | h'x)
  · exact hs.1
  exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
[PROOFSTEP]
intro x hx hxc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hx : x ∈ s ∪ t
hxc : x ≤ c
⊢ x ∈ s
[PROOFSTEP]
cases hx
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ s
⊢ x ∈ s
[PROOFSTEP]
assumption
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
⊢ x ∈ s
[PROOFSTEP]
rcases eq_or_lt_of_le hxc with (rfl | h'x)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
x : α
h✝ : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s
[PROOFSTEP]
exact hs.1
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ s
[PROOFSTEP]
exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ t
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
⊢ StrictMonoOn f (s ∪ t)
[PROOFSTEP]
have B : ∀ x, x ∈ s ∪ t → c ≤ x → x ∈ t := by
  intro x hx hxc
  match hx with
  | Or.inr hx => exact hx
  | Or.inl hx =>
    rcases eq_or_lt_of_le hxc with (rfl | h'x)
    · exact ht.1
    exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
⊢ ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
[PROOFSTEP]
intro x hx hxc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx : x ∈ s ∪ t
hxc : c ≤ x
⊢ x ∈ t
[PROOFSTEP]
match hx with
| Or.inr hx => exact hx
| Or.inl hx =>
  rcases eq_or_lt_of_le hxc with (rfl | h'x)
  · exact ht.1
  exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ t
⊢ x ∈ t
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
⊢ x ∈ t
[PROOFSTEP]
rcases eq_or_lt_of_le hxc with (rfl | h'x)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
hx✝ : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t
[PROOFSTEP]
exact ht.1
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
h'x : c < x
⊢ x ∈ t
[PROOFSTEP]
exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
⊢ StrictMonoOn f (s ∪ t)
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
⊢ f x < f y
[PROOFSTEP]
rcases lt_or_le x c with (hxc | hcx)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hxc : x < c
⊢ f x < f y
[PROOFSTEP]
have xs : x ∈ s := A _ hx hxc.le
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hxc : x < c
xs : x ∈ s
⊢ f x < f y
[PROOFSTEP]
rcases lt_or_le y c with (hyc | hcy)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hxc : x < c
xs : x ∈ s
hyc : y < c
⊢ f x < f y
[PROOFSTEP]
exact h₁ xs (A _ hy hyc.le) hxy
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hxc : x < c
xs : x ∈ s
hcy : c ≤ y
⊢ f x < f y
[PROOFSTEP]
exact (h₁ xs hs.1 hxc).trans_le (h₂.monotoneOn ht.1 (B _ hy hcy) hcy)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hcx : c ≤ x
⊢ f x < f y
[PROOFSTEP]
have xt : x ∈ t := B _ hx hcx
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hcx : c ≤ x
xt : x ∈ t
⊢ f x < f y
[PROOFSTEP]
have yt : y ∈ t := B _ hy (hcx.trans hxy.le)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hcx : c ≤ x
xt : x ∈ t
yt : y ∈ t
⊢ f x < f y
[PROOFSTEP]
exact h₂ xt yt hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMono f
[PROOFSTEP]
rw [← strictMonoOn_univ, ← @Iic_union_Ici _ _ a]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMonoOn f (Iic a ∪ Ici a)
[PROOFSTEP]
exact StrictMonoOn.union h₁ h₂ isGreatest_Iic isLeast_Ici
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ MonotoneOn f (s ∪ t)
[PROOFSTEP]
have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s := by
  intro x hx hxc
  cases hx
  · assumption
  rcases eq_or_lt_of_le hxc with (rfl | h'x)
  · exact hs.1
  exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
[PROOFSTEP]
intro x hx hxc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hx : x ∈ s ∪ t
hxc : x ≤ c
⊢ x ∈ s
[PROOFSTEP]
cases hx
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ s
⊢ x ∈ s
[PROOFSTEP]
assumption
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
⊢ x ∈ s
[PROOFSTEP]
rcases eq_or_lt_of_le hxc with (rfl | h'x)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
x : α
h✝ : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s
[PROOFSTEP]
exact hs.1
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ s
[PROOFSTEP]
exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ t
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
⊢ MonotoneOn f (s ∪ t)
[PROOFSTEP]
have B : ∀ x, x ∈ s ∪ t → c ≤ x → x ∈ t := by
  intro x hx hxc
  match hx with
  | Or.inr hx => exact hx
  | Or.inl hx =>
    rcases eq_or_lt_of_le hxc with (rfl | h'x)
    · exact ht.1
    exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
⊢ ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
[PROOFSTEP]
intro x hx hxc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx : x ∈ s ∪ t
hxc : c ≤ x
⊢ x ∈ t
[PROOFSTEP]
match hx with
| Or.inr hx => exact hx
| Or.inl hx =>
  rcases eq_or_lt_of_le hxc with (rfl | h'x)
  · exact ht.1
  exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ t
⊢ x ∈ t
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
⊢ x ∈ t
[PROOFSTEP]
rcases eq_or_lt_of_le hxc with (rfl | h'x)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
hx✝ : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t
[PROOFSTEP]
exact ht.1
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
h'x : c < x
⊢ x ∈ t
[PROOFSTEP]
exact (lt_irrefl _ (h'x.trans_le (hs.2 hx))).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
⊢ MonotoneOn f (s ∪ t)
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
⊢ f x ≤ f y
[PROOFSTEP]
rcases lt_or_le x c with (hxc | hcx)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
⊢ f x ≤ f y
[PROOFSTEP]
have xs : x ∈ s := A _ hx hxc.le
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
⊢ f x ≤ f y
[PROOFSTEP]
rcases lt_or_le y c with (hyc | hcy)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
hyc : y < c
⊢ f x ≤ f y
[PROOFSTEP]
exact h₁ xs (A _ hy hyc.le) hxy
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
hcy : c ≤ y
⊢ f x ≤ f y
[PROOFSTEP]
exact (h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
⊢ f x ≤ f y
[PROOFSTEP]
have xt : x ∈ t := B _ hx hcx
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
xt : x ∈ t
⊢ f x ≤ f y
[PROOFSTEP]
have yt : y ∈ t := B _ hy (hcx.trans hxy)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ (x : α), x ∈ s ∪ t → x ≤ c → x ∈ s
B : ∀ (x : α), x ∈ s ∪ t → c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
xt : x ∈ t
yt : y ∈ t
⊢ f x ≤ f y
[PROOFSTEP]
exact h₂ xt yt hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ Monotone f
[PROOFSTEP]
rw [← monotoneOn_univ, ← @Iic_union_Ici _ _ a]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ MonotoneOn f (Iic a ∪ Ici a)
[PROOFSTEP]
exact MonotoneOn.union_right h₁ h₂ isGreatest_Iic isLeast_Ici


[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
⊢ StrictMono f
[PROOFSTEP]
refine' StrictMonoOn.Iic_union_Ici (fun x hx y hy hxy => neg_lt_neg_iff.1 _) h₂
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ -f y < -f x
[PROOFSTEP]
rw [← h₁, ← h₁]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ f (-y) < f (-x)
[PROOFSTEP]
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_lt_neg hxy)
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
⊢ Monotone f
[PROOFSTEP]
refine' MonotoneOn.Iic_union_Ici (fun x hx y hy hxy => neg_le_neg_iff.1 _) h₂
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ -f y ≤ -f x
[PROOFSTEP]
rw [← h₁, ← h₁]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ f (-y) ≤ f (-x)
[PROOFSTEP]
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)


[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : GroupWithZero β
src✝¹ : DivInvMonoid (Germ (↑φ) β) := divInvMonoid
src✝ : MonoidWithZero (Germ (↑φ) β) := monoidWithZero
⊢ ((fun x x_1 => x ∘ x_1) Inv.inv fun x => 0) =ᶠ[↑φ] fun x => 0
[PROOFSTEP]
simp only [Function.comp, inv_zero]
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : GroupWithZero β
src✝¹ : DivInvMonoid (Germ (↑φ) β) := divInvMonoid
src✝ : MonoidWithZero (Germ (↑φ) β) := monoidWithZero
⊢ (fun x => 0) =ᶠ[↑φ] fun x => 0
[PROOFSTEP]
exact EventuallyEq.refl _ fun _ => 0
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
f g : α → β
⊢ ↑f < ↑g ↔ ∀* (x : α), f x < g x
[PROOFSTEP]
simp only [lt_iff_le_not_le, eventually_and, coe_le, eventually_not, EventuallyLE]
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
⊢ (fun x x_1 => x < x_1) = LiftRel fun x x_1 => x < x_1
[PROOFSTEP]
ext ⟨f⟩ ⟨g⟩
[GOAL]
case h.mk.h.mk.a
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
x✝¹ : Germ (↑φ) β
f : α → β
x✝ : Germ (↑φ) β
g : α → β
⊢ Quot.mk Setoid.r f < Quot.mk Setoid.r g ↔ LiftRel (fun x x_1 => x < x_1) (Quot.mk Setoid.r f) (Quot.mk Setoid.r g)
[PROOFSTEP]
exact coe_lt
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
⊢ max ↑a ↑b = map₂ max ↑a ↑b
[PROOFSTEP]
cases' le_total (a : β*) b with h h
[GOAL]
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ max ↑a ↑b = map₂ max ↑a ↑b
[PROOFSTEP]
rw [max_eq_right h, map₂_coe, coe_eq]
[GOAL]
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ b =ᶠ[↑φ] fun x => max (a x) (b x)
[PROOFSTEP]
exact h.mono fun i hi => (max_eq_right hi).symm
[GOAL]
case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ max ↑a ↑b = map₂ max ↑a ↑b
[PROOFSTEP]
rw [max_eq_left h, map₂_coe, coe_eq]
[GOAL]
case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ a =ᶠ[↑φ] fun x => max (a x) (b x)
[PROOFSTEP]
exact h.mono fun i hi => (max_eq_left hi).symm
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
⊢ min ↑a ↑b = map₂ min ↑a ↑b
[PROOFSTEP]
cases' le_total (a : β*) b with h h
[GOAL]
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ min ↑a ↑b = map₂ min ↑a ↑b
[PROOFSTEP]
rw [min_eq_left h, map₂_coe, coe_eq]
[GOAL]
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑a ≤ ↑b
⊢ a =ᶠ[↑φ] fun x => min (a x) (b x)
[PROOFSTEP]
exact h.mono fun i hi => (min_eq_left hi).symm
[GOAL]
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ min ↑a ↑b = map₂ min ↑a ↑b
[PROOFSTEP]
rw [min_eq_right h, map₂_coe, coe_eq]
[GOAL]
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : Germ (↑φ) β
a b : α → β
h : ↑b ≤ ↑a
⊢ b =ᶠ[↑φ] fun x => min (a x) (b x)
[PROOFSTEP]
exact h.mono fun i hi => (min_eq_right hi).symm
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(max x y) = max ↑x ↑y
[PROOFSTEP]
rw [max_def, map₂_const]
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(min x y) = min ↑x ↑y
[PROOFSTEP]
rw [min_def, map₂_const]
[GOAL]
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrderedAddCommGroup β
x : β
⊢ ↑|x| = |↑x|
[PROOFSTEP]
rw [abs_def, map_const]


[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ (i : α), i ∈ Ico n m → r i (succ i)
hnm : n ≤ m
⊢ ReflTransGen r n m
[PROOFSTEP]
revert h
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
[PROOFSTEP]
refine' Succ.rec _ _ hnm
[GOAL]
case refine'_1
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ (i : α), i ∈ Ico n n → r i (succ i)) → ReflTransGen r n n
[PROOFSTEP]
intro _
[GOAL]
case refine'_1
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
h✝ : ∀ (i : α), i ∈ Ico n n → r i (succ i)
⊢ ReflTransGen r n n
[PROOFSTEP]
exact ReflTransGen.refl
[GOAL]
case refine'_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ ∀ (n_1 : α),
    n ≤ n_1 →
      ((∀ (i : α), i ∈ Ico n n_1 → r i (succ i)) → ReflTransGen r n n_1) →
        (∀ (i : α), i ∈ Ico n (succ n_1) → r i (succ i)) → ReflTransGen r n (succ n_1)
[PROOFSTEP]
intro m hnm ih h
[GOAL]
case refine'_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
h : ∀ (i : α), i ∈ Ico n (succ m) → r i (succ i)
⊢ ReflTransGen r n (succ m)
[PROOFSTEP]
have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩
[GOAL]
case refine'_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
h : ∀ (i : α), i ∈ Ico n (succ m) → r i (succ i)
this : ReflTransGen r n m
⊢ ReflTransGen r n (succ m)
[PROOFSTEP]
cases' (le_succ m).eq_or_lt with hm hm
[GOAL]
case refine'_2.inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
h : ∀ (i : α), i ∈ Ico n (succ m) → r i (succ i)
this : ReflTransGen r n m
hm : m = succ m
⊢ ReflTransGen r n (succ m)
[PROOFSTEP]
rwa [← hm]
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ (i : α), i ∈ Ico n m → r i (succ i)) → ReflTransGen r n m
h : ∀ (i : α), i ∈ Ico n (succ m) → r i (succ i)
this : ReflTransGen r n m
hm : m < succ m
⊢ ReflTransGen r n (succ m)
[PROOFSTEP]
exact this.tail (h m ⟨hnm, hm⟩)
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen r n m
[PROOFSTEP]
rw [← reflTransGen_swap]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen (swap r) m n
[PROOFSTEP]
exact reflTransGen_of_succ_of_le (swap r) h hmn
[GOAL]
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hr : Reflexive r
h1 : ∀ (i : α), i ∈ Ico n m → r i (succ i)
h2 : ∀ (i : α), i ∈ Ico m n → r (succ i) i
⊢ TransGen r n m
[PROOFSTEP]
rcases eq_or_ne m n with (rfl | hmn)
[GOAL]
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
m : α
hr : Reflexive r
h1 : ∀ (i : α), i ∈ Ico m m → r i (succ i)
h2 : ∀ (i : α), i ∈ Ico m m → r (succ i) i
⊢ TransGen r m m
[PROOFSTEP]
exact TransGen.single (hr m)
[GOAL]
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hr : Reflexive r
h1 : ∀ (i : α), i ∈ Ico n m → r i (succ i)
h2 : ∀ (i : α), i ∈ Ico m n → r (succ i) i
hmn : m ≠ n
⊢ TransGen r n m
[PROOFSTEP]
exact transGen_of_succ_of_ne r h1 h2 hmn.symm


[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s t : Set α
Ixx : α → α → Set α
⊢ Tendsto (fun p => Ixx p.fst p.snd) (𝓟 s ×ˢ 𝓟 s) (smallSets (𝓟 t)) ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → Ixx x y ⊆ t
[PROOFSTEP]
simp only [smallSets_principal, prod_principal_principal, tendsto_principal_principal, forall_prod_set,
  mem_powerset_iff, mem_principal]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
l₁ l₁' l₂ l₂' : Filter α
Ixx : α → α → Set α
h : TendstoIxxClass Ixx l₁ l₂
h' : TendstoIxxClass Ixx l₁' l₂'
⊢ Tendsto (fun p => Ixx p.fst p.snd) ((l₁ ⊓ l₁') ×ˢ (l₁ ⊓ l₁')) (smallSets (l₂ ⊓ l₂'))
[PROOFSTEP]
simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ TendstoIxxClass Icc (pure a) (pure a)
[PROOFSTEP]
rw [← principal_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ TendstoIxxClass Icc (𝓟 {a}) (𝓟 {a})
[PROOFSTEP]
exact tendstoIxxClass_principal.2 ordConnected_singleton.out
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ Tendsto (fun p => Ico p.fst p.snd) (pure a ×ˢ pure a) (smallSets ⊥)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ Tendsto (fun p => Ioc p.fst p.snd) (pure a ×ˢ pure a) (smallSets ⊥)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a : α
⊢ Tendsto (fun p => Ioo p.fst p.snd) (pure a ×ˢ pure a) (smallSets ⊥)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
⊢ TendstoIxxClass uIcc l l
[PROOFSTEP]
refine' ⟨fun s hs => mem_map.2 <| mem_prod_self_iff.2 _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
⊢ ∃ t, t ∈ l ∧ t ×ˢ t ⊆ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
obtain ⟨t, htl, hts⟩ : ∃ t ∈ l, ∀ p ∈ (t : Set α) ×ˢ t, Icc (p : α × α).1 p.2 ∈ s
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
⊢ ∃ t, t ∈ l ∧ ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
⊢ ∃ t, t ∈ l ∧ t ×ˢ t ⊆ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
exact mem_prod_self_iff.1 (mem_map.1 (tendsto_fst.Icc tendsto_snd hs))
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
⊢ ∃ t, t ∈ l ∧ t ×ˢ t ⊆ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
refine' ⟨t, htl, fun p hp => _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
⊢ p ∈ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
cases' le_total p.1 p.2 with h h
[GOAL]
case intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.fst ≤ p.snd
⊢ p ∈ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
rw [mem_preimage, uIcc_of_le h]
[GOAL]
case intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.fst ≤ p.snd
⊢ Icc p.fst p.snd ∈ s
[PROOFSTEP]
exact hts p hp
[GOAL]
case intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.snd ≤ p.fst
⊢ p ∈ (fun p => [[p.fst, p.snd]]) ⁻¹' s
[PROOFSTEP]
rw [mem_preimage, uIcc_of_ge h]
[GOAL]
case intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ smallSets l
t : Set α
htl : t ∈ l
hts : ∀ (p : α × α), p ∈ t ×ˢ t → Icc p.fst p.snd ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.snd ≤ p.fst
⊢ Icc p.snd p.fst ∈ s
[PROOFSTEP]
exact hts ⟨p.2, p.1⟩ ⟨hp.2, hp.1⟩