[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ Tendsto m l (pi f) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)
[PROOFSTEP]
simp only [pi, tendsto_iInf, tendsto_comap_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
⊢ Set.pi I s ∈ pi f
[PROOFSTEP]
rw [pi_def, biInter_eq_iInter]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
⊢ ⋂ (x : ↑I), eval ↑x ⁻¹' s ↑x ∈ pi f
[PROOFSTEP]
refine' mem_iInf_of_iInter hI (fun i => _) Subset.rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : Set.Finite I
h : ∀ (i : ι), i ∈ I → s i ∈ f i
i : ↑I
⊢ eval ↑i ⁻¹' s ↑i ∈ comap (eval ↑i) (f ↑i)
[PROOFSTEP]
exact preimage_mem_comap (h i i.2)
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f ↔ ∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ Set.pi I t ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f → ∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ Set.pi I t ⊆ s
[PROOFSTEP]
simp only [pi, mem_iInf', mem_comap, pi_def]
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I,
      Set.Finite I ∧
        ∃ V,
          (∀ (i : ι), ∃ t, t ∈ f i ∧ eval i ⁻¹' t ⊆ V i) ∧
            (∀ (i : ι), ¬i ∈ I → V i = univ) ∧ s = ⋂ (i : ι) (_ : i ∈ I), V i ∧ s = ⋂ (i : ι), V i) →
    ∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ (a : ι) (_ : a ∈ I), eval a ⁻¹' t a ⊆ s
[PROOFSTEP]
rintro ⟨I, If, V, hVf, -, rfl, -⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
If : Set.Finite I
V : ι → Set ((i : ι) → α i)
hVf : ∀ (i : ι), ∃ t, t ∈ f i ∧ eval i ⁻¹' t ⊆ V i
⊢ ∃ I_1,
    Set.Finite I_1 ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ (a : ι) (_ : a ∈ I_1), eval a ⁻¹' t a ⊆ ⋂ (i : ι) (_ : i ∈ I), V i
[PROOFSTEP]
choose t htf htV using hVf
[GOAL]
case mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
If : Set.Finite I
V : ι → Set ((i : ι) → α i)
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
htV : ∀ (i : ι), eval i ⁻¹' t i ⊆ V i
⊢ ∃ I_1,
    Set.Finite I_1 ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ (a : ι) (_ : a ∈ I_1), eval a ⁻¹' t a ⊆ ⋂ (i : ι) (_ : i ∈ I), V i
[PROOFSTEP]
exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ Set.pi I t ⊆ s) → s ∈ pi f
[PROOFSTEP]
rintro ⟨I, If, t, htf, hts⟩
[GOAL]
case mpr.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
I : Set ι
If : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I t ⊆ s
⊢ s ∈ pi f
[PROOFSTEP]
exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
⊢ s i ∈ f i
[PROOFSTEP]
rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
⊢ s i ∈ f i
[PROOFSTEP]
refine' mem_of_superset (htf i) fun x hx => _
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
⊢ x ∈ s i
[PROOFSTEP]
have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
this : ∀ (i : ι), Set.Nonempty (t i)
⊢ x ∈ s i
[PROOFSTEP]
choose g hg using this
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
⊢ x ∈ s i
[PROOFSTEP]
have : update g i x ∈ I'.pi t := fun j _ => by rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
⊢ update g i x j ∈ t j
[PROOFSTEP]
rcases eq_or_ne j i with (rfl | hne)
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
hi : j ∈ I
x : α j
hx : x ∈ t j
⊢ update g j x j ∈ t j
[PROOFSTEP]
simp [*]
[GOAL]
case inr
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
hne : j ≠ i
⊢ update g i x j ∈ t j
[PROOFSTEP]
simp [*]
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
h : Set.pi I s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I' t ⊆ Set.pi I s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
this : update g i x ∈ Set.pi I' t
⊢ x ∈ s i
[PROOFSTEP]
simpa using hts this i hi
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
ι' : ι → Type
s : (i : ι) → ι' i → Set (α i)
p : (i : ι) → ι' i → Prop
h : ∀ (i : ι), HasBasis (f i) (p i) (s i)
⊢ HasBasis (pi f) (fun If => Set.Finite If.fst ∧ ∀ (i : ι), i ∈ If.fst → p i (Prod.snd If i)) fun If =>
    Set.pi If.fst fun i => s i (Prod.snd If i)
[PROOFSTEP]
simpa [Set.pi_def] using hasBasis_iInf' fun i => (h i).comap (eval i : (∀ j, α j) → α i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f ⊓ 𝓟 (Set.pi univ s) = ⊥ ↔ ∃ i, f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f ⊓ 𝓟 (Set.pi univ s) = ⊥ → ∃ i, f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
simp only [inf_principal_eq_bot, mem_pi]
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ I, Set.Finite I ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ Set.pi I t ⊆ (Set.pi univ s)ᶜ) → ∃ i, (s i)ᶜ ∈ f i
[PROOFSTEP]
contrapose!
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∀ (i : ι), ¬(s i)ᶜ ∈ f i) →
    ∀ (I : Set ι), Set.Finite I → ∀ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) → ¬Set.pi I t ⊆ (Set.pi univ s)ᶜ
[PROOFSTEP]
rintro (hsf : ∀ i, ∃ᶠ x in f i, x ∈ s i) I - t htf hts
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I t ⊆ (Set.pi univ s)ᶜ
⊢ False
[PROOFSTEP]
have : ∀ i, (s i ∩ t i).Nonempty := fun i => ((hsf i).and_eventually (htf i)).exists
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I t ⊆ (Set.pi univ s)ᶜ
this : ∀ (i : ι), Set.Nonempty (s i ∩ t i)
⊢ False
[PROOFSTEP]
choose x hxs hxt using this
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : Set.pi I t ⊆ (Set.pi univ s)ᶜ
x : (i : ι) → α i
hxs : ∀ (i : ι), x i ∈ s i
hxt : ∀ (i : ι), x i ∈ t i
⊢ False
[PROOFSTEP]
exact hts (fun i _ => hxt i) (mem_univ_pi.2 hxs)
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, f i ⊓ 𝓟 (s i) = ⊥) → pi f ⊓ 𝓟 (Set.pi univ s) = ⊥
[PROOFSTEP]
simp only [inf_principal_eq_bot]
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, (s i)ᶜ ∈ f i) → (Set.pi univ s)ᶜ ∈ pi f
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case mpr.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
i : ι
hi : (s i)ᶜ ∈ f i
⊢ (Set.pi univ s)ᶜ ∈ pi f
[PROOFSTEP]
filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
⊢ pi f ⊓ 𝓟 (Set.pi I s) = ⊥ ↔ ∃ i, i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
⊢ (∃ i, f i ⊓ 𝓟 (piecewise I s (fun x => univ) i) = ⊥) ↔ ∃ i, i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
refine' exists_congr fun i => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
i : ι
⊢ f i ⊓ 𝓟 (piecewise I s (fun x => univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
by_cases hi : i ∈ I
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
i : ι
hi : i ∈ I
⊢ f i ⊓ 𝓟 (piecewise I s (fun x => univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
simp [hi, NeBot.ne']
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
i : ι
hi : ¬i ∈ I
⊢ f i ⊓ 𝓟 (piecewise I s (fun x => univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
[PROOFSTEP]
simp [hi, NeBot.ne']
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ NeBot (pi f ⊓ 𝓟 (Set.pi univ s)) ↔ ∀ (i : ι), NeBot (f i ⊓ 𝓟 (s i))
[PROOFSTEP]
simp [neBot_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
⊢ NeBot (pi f ⊓ 𝓟 (Set.pi I s)) ↔ ∀ (i : ι), i ∈ I → NeBot (f i ⊓ 𝓟 (s i))
[PROOFSTEP]
simp [neBot_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f = ⊥ ↔ ∃ i, f i = ⊥
[PROOFSTEP]
simpa using @pi_inf_principal_univ_pi_eq_bot ι α f fun _ => univ
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ NeBot (pi f) ↔ ∀ (i : ι), NeBot (f i)
[PROOFSTEP]
simp [neBot_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
⊢ map (eval i) (pi f) = f i
[PROOFSTEP]
refine' le_antisymm (tendsto_eval_pi f i) fun s hs => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
⊢ s ∈ f i
[PROOFSTEP]
rcases mem_pi.1 (mem_map.1 hs) with ⟨I, hIf, t, htf, hI⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : Set.pi I t ⊆ eval i ⁻¹' s
⊢ s ∈ f i
[PROOFSTEP]
rw [← image_subset_iff] at hI
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' Set.pi I t ⊆ s
⊢ s ∈ f i
[PROOFSTEP]
refine' mem_of_superset (htf i) ((subset_eval_image_pi _ _).trans hI)
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' Set.pi I t ⊆ s
⊢ Set.Nonempty (Set.pi I t)
[PROOFSTEP]
exact nonempty_of_mem (pi_mem_pi hIf fun i _ => htf i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f₁ i)
⊢ pi f₁ = pi f₂ ↔ f₁ = f₂
[PROOFSTEP]
refine' ⟨fun h => _, congr_arg pi⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f₁ i)
h : pi f₁ = pi f₂
⊢ f₁ = f₂
[PROOFSTEP]
have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f₁ i)
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
⊢ f₁ = f₂
[PROOFSTEP]
haveI : ∀ i, NeBot (f₂ i) := fun i => neBot_of_le (hle i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f₁ i)
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
this : ∀ (i : ι), NeBot (f₂ i)
⊢ f₁ = f₂
[PROOFSTEP]
exact hle.antisymm (pi_le_pi.1 h.ge)
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
[PROOFSTEP]
simp [Filter.coprodᵢ]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
s : Set ((i : ι) → α i)
⊢ sᶜ ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), (eval i '' s)ᶜ ∈ f i
[PROOFSTEP]
simp only [Filter.coprodᵢ, mem_iSup, compl_mem_comap]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ NeBot (Filter.coprodᵢ f) ↔ (∀ (i : ι), Nonempty (α i)) ∧ ∃ d, NeBot (f d)
[PROOFSTEP]
simp only [Filter.coprodᵢ, iSup_neBot, ← exists_and_left, ← comap_eval_neBot_iff']
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ NeBot (Filter.coprodᵢ f) ↔ ∃ d, NeBot (f d)
[PROOFSTEP]
simp [coprodᵢ_neBot_iff', *]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥
[PROOFSTEP]
simpa only [not_neBot, not_and_or, funext_iff, not_forall, not_exists, not_nonempty_iff] using coprodᵢ_neBot_iff'.not
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ f = ⊥
[PROOFSTEP]
simpa [funext_iff] using coprodᵢ_neBot_iff.not
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
⊢ map (fun k i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => map (m i) (f i)
[PROOFSTEP]
simp only [le_def, mem_map, mem_coprodᵢ_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
⊢ ∀ (x : Set ((i : ι) → β i)),
    (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ x) →
      ∀ (i : ι), ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' x
[PROOFSTEP]
intro s h i
[GOAL]
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
⊢ ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s
[PROOFSTEP]
obtain ⟨t, H, hH⟩ := h i
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval i ⁻¹' t ⊆ s
⊢ ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s
[PROOFSTEP]
exact ⟨{x : α i | m i x ∈ t}, H, fun x hx => hH hx⟩


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : One α
f : Filter α
s : Set α
inst✝¹ : One β
inst✝ : OneHomClass F α β
φ : F
⊢ map (↑φ) 1 = 1
[PROOFSTEP]
rw [Filter.map_one', map_one, pure_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f g : Filter α
s : Set α
hs : s ∈ f
⊢ s⁻¹ ∈ f⁻¹
[PROOFSTEP]
rwa [mem_inv, inv_preimage, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f✝ g : Filter α
s : Set α
src✝ : Inv (Filter α) := instInv
f : Filter α
⊢ map (Inv.inv ∘ Inv.inv) f = f
[PROOFSTEP]
rw [inv_involutive.comp_self, map_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f g : Filter α
s : Set α
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹
[PROOFSTEP]
rw [← Filter.inv_le_inv_iff, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hs : s ∈ f
⊢ s ^ 0 ∈ f ^ 0
[PROOFSTEP]
rw [pow_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hs : s ∈ f
⊢ 1 ∈ f ^ 0
[PROOFSTEP]
exact one_mem_one
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ : ℕ
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ : ℕ
hs : s ∈ f
n : ℕ
⊢ s * s ^ n ∈ f ^ (n + 1)
[PROOFSTEP]
exact mul_mem_mul hs (pow_mem_pow hs n)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ n : ℕ
hn : n ≠ 0
⊢ ⊥ ^ n = ⊥
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn), pow_succ, bot_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hf : 1 ≤ f
⊢ f * ⊤ = ⊤
[PROOFSTEP]
refine' top_le_iff.1 fun s => _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ s ∈ f * ⊤ → s ∈ ⊤
[PROOFSTEP]
simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ (∃ t₁, t₁ ∈ f ∧ t₁ * univ ⊆ s) → s = univ
[PROOFSTEP]
rintro ⟨t, ht, hs⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
⊢ s = univ
[PROOFSTEP]
rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hf : 1 ≤ f
⊢ ⊤ * f = ⊤
[PROOFSTEP]
refine' top_le_iff.1 fun s => _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ s ∈ ⊤ * f → s ∈ ⊤
[PROOFSTEP]
simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ (∃ x, x ∈ f ∧ univ * x ⊆ s) → s = univ
[PROOFSTEP]
rintro ⟨t, ht, hs⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
⊢ s = univ
[PROOFSTEP]
rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ ^ (n + 2) = ⊤
[PROOFSTEP]
rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
refine' ⟨fun hfg => _, _⟩
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
obtain ⟨t₁, t₂, h₁, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm.subst one_mem_one
[GOAL]
case refine'_1.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
[GOAL]
case refine'_1.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
hfg : NeBot (f * g)
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h
[GOAL]
case refine'_1.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : ∃ a b, t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : NeBot (f * g)
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
obtain ⟨a, b, rfl, rfl, h⟩ := h
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
refine' ⟨a, b, _, _, h⟩
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ f = pure a
[PROOFSTEP]
rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ g = pure b
[PROOFSTEP]
rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1) → f * g = 1
[PROOFSTEP]
rintro ⟨a, b, rfl, rfl, h⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ pure a * pure b = 1
[PROOFSTEP]
rw [pure_mul_pure, h, pure_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
src✝³ : Monoid (Filter α) := Filter.monoid
src✝² : InvolutiveInv (Filter α) := Filter.instInvolutiveInv
src✝¹ : Div (Filter α) := Filter.instDiv
src✝ : Pow (Filter α) ℤ := Filter.instZPow
s t : Filter α
h : s * t = 1
⊢ s⁻¹ = t
[PROOFSTEP]
obtain ⟨a, b, rfl, rfl, hab⟩ := Filter.mul_eq_one_iff.1 h
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
src✝³ : Monoid (Filter α) := Filter.monoid
src✝² : InvolutiveInv (Filter α) := Filter.instInvolutiveInv
src✝¹ : Div (Filter α) := Filter.instDiv
src✝ : Pow (Filter α) ℤ := Filter.instZPow
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ (pure a)⁻¹ = pure b
[PROOFSTEP]
rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ IsUnit f → ∃ a, f = pure a ∧ IsUnit a
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case mp.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
[PROOFSTEP]
obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
[PROOFSTEP]
refine' ⟨a, ha, ⟨a, b, h, pure_injective _⟩, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure (b * a) = pure 1
[PROOFSTEP]
rw [← pure_mul_pure, ← ha, ← hb]
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = pure 1
[PROOFSTEP]
exact u.inv_mul
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a, f = pure a ∧ IsUnit a) → IsUnit f
[PROOFSTEP]
rintro ⟨a, rfl, ha⟩
[GOAL]
case mpr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
a : α
ha : IsUnit a
⊢ IsUnit (pure a)
[PROOFSTEP]
exact ha.filter
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ 1 ≤ f / g ↔ ¬Disjoint f g
[PROOFSTEP]
refine' ⟨fun h hfg => _, _⟩
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : 1 ≤ f / g
hfg : Disjoint f g
⊢ False
[PROOFSTEP]
obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅ ∈ ⊥)
[GOAL]
case refine'_1.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : 1 ≤ f / g
hfg : Disjoint f g
s : Set α
hs : s ∈ f
t : Set α
ht : t ∈ g
hst : ∅ = s ∩ t
⊢ False
[PROOFSTEP]
exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ ¬Disjoint f g → 1 ≤ f / g
[PROOFSTEP]
rintro h s ⟨t₁, t₂, h₁, h₂, hs⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : ¬Disjoint f g
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
[PROOFSTEP]
exact hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
⊢ 1 ≤ f / f
[PROOFSTEP]
rintro s ⟨t₁, t₂, h₁, h₂, hs⟩
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
[PROOFSTEP]
obtain ⟨a, ha₁, ha₂⟩ := Set.not_disjoint_iff.1 (h.not_disjoint h₁ h₂)
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ s ∈ 1
[PROOFSTEP]
rw [mem_one, ← div_self' a]
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ a / a ∈ s
[PROOFSTEP]
exact hs (Set.div_mem_div ha₁ ha₂)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ IsUnit f ↔ ∃ a, f = pure a
[PROOFSTEP]
simp only [isUnit_iff, Group.isUnit, and_true_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ (a • b) • f = a • b • f
[PROOFSTEP]
simp only [← map_smul, map_map, smul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ map (fun b_1 => a • b • b_1) f = map ((fun b => a • b) ∘ fun b_1 => b • b_1) f
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
⊢ (a • f) • g = a • f • g
[PROOFSTEP]
refine' (map_map₂_distrib_left fun _ _ => _).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
x✝¹ : β
x✝ : γ
⊢ (fun x x_1 => x • x_1) a (x✝¹ • x✝) = (fun x x_1 => x • x_1) a x✝¹ • x✝
[PROOFSTEP]
exact (smul_assoc a _ _).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ map (fun b => 1 • b) f = f
[PROOFSTEP]
simp_rw [one_smul, map_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ 1 • f = f
[PROOFSTEP]
simp only [← map_smul, one_smul, map_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
a b : α
f : Filter β
⊢ (a * b) • f = a • b • f
[PROOFSTEP]
simp only [← map_smul, map_map, Function.comp, ← mul_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
x✝ : α
⊢ pure ((fun x x_1 => x • x_1) x✝ 0) = 0
[PROOFSTEP]
dsimp only
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
x✝ : α
⊢ pure (x✝ • 0) = 0
[PROOFSTEP]
rw [smul_zero, pure_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {x✝ • 1} = 1
[PROOFSTEP]
rw [smul_one, singleton_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
⊢ 0 • g ≤ 0
[PROOFSTEP]
refine' fun s hs => mem_smul_filter.2 _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x x_1 => x • x_1) 0 ⁻¹' s ∈ g
[PROOFSTEP]
convert @univ_mem _ g
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x x_1 => x • x_1) 0 ⁻¹' s = univ
[PROOFSTEP]
refine' eq_univ_iff_forall.2 fun a => _
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x x_1 => x • x_1) 0 ⁻¹' s
[PROOFSTEP]
dsimp only
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x => 0 • x) ⁻¹' s
[PROOFSTEP]
rwa [mem_preimage, zero_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
hg : NeBot g
s : Set β
hs : s ∈ g
⊢ (fun x x_1 => x • x_1) 0 '' s ∈ 0
[PROOFSTEP]
simp_rw [zero_smul, (hg.nonempty_of_mem hs).image_const]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
hg : NeBot g
s : Set β
hs : s ∈ g
⊢ {0} ∈ 0
[PROOFSTEP]
exact zero_mem_zero


[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
⊢ ⋃ (i : α) (_ : i ∈ Ico m n), Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
[PROOFSTEP]
cases' le_total n m with hnm hmn
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hnm : n ≤ m
⊢ ⋃ (i : α) (_ : i ∈ Ico m n), Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
[PROOFSTEP]
rw [Ico_eq_empty_of_le hnm, Ioc_eq_empty_of_le (hf hnm), biUnion_empty]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ⋃ (i : α) (_ : i ∈ Ico m n), Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
[PROOFSTEP]
refine' Succ.rec _ _ hmn
[GOAL]
case inr.refine'_1
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ⋃ (i : α) (_ : i ∈ Ico m m), Ioc (f i) (f (succ i)) = Ioc (f m) (f m)
[PROOFSTEP]
simp only [Ioc_self, Ico_self, biUnion_empty]
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ∀ (n : α),
    m ≤ n →
      ⋃ (i : α) (_ : i ∈ Ico m n), Ioc (f i) (f (succ i)) = Ioc (f m) (f n) →
        ⋃ (i : α) (_ : i ∈ Ico m (succ n)), Ioc (f i) (f (succ i)) = Ioc (f m) (f (succ n))
[PROOFSTEP]
intro k hmk ihk
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
⊢ ⋃ (i : α) (_ : i ∈ Ico m (succ k)), Ioc (f i) (f (succ i)) = Ioc (f m) (f (succ k))
[PROOFSTEP]
rw [← Ioc_union_Ioc_eq_Ioc (hf hmk) (hf <| le_succ _), union_comm, ← ihk]
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
⊢ ⋃ (i : α) (_ : i ∈ Ico m (succ k)), Ioc (f i) (f (succ i)) =
    Ioc (f k) (f (succ k)) ∪ ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i))
[PROOFSTEP]
by_cases hk : IsMax k
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
hk : IsMax k
⊢ ⋃ (i : α) (_ : i ∈ Ico m (succ k)), Ioc (f i) (f (succ i)) =
    Ioc (f k) (f (succ k)) ∪ ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i))
[PROOFSTEP]
rw [hk.succ_eq, Ioc_self, empty_union]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
hk : ¬IsMax k
⊢ ⋃ (i : α) (_ : i ∈ Ico m (succ k)), Ioc (f i) (f (succ i)) =
    Ioc (f k) (f (succ k)) ∪ ⋃ (i : α) (_ : i ∈ Ico m k), Ioc (f i) (f (succ i))
[PROOFSTEP]
rw [Ico_succ_right_eq_insert_of_not_isMax hmk hk, biUnion_insert]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise (Disjoint on fun n => Ioc (f (pred n)) (f n))
[PROOFSTEP]
simpa only [(· ∘ ·), dual_Ico] using hf.dual.pairwise_disjoint_on_Ico_succ
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise (Disjoint on fun n => Ico (f (pred n)) (f n))
[PROOFSTEP]
simpa only [(· ∘ ·), dual_Ioc] using hf.dual.pairwise_disjoint_on_Ioc_succ
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise (Disjoint on fun n => Ioo (f (pred n)) (f n))
[PROOFSTEP]
simpa only [(· ∘ ·), dual_Ioo] using hf.dual.pairwise_disjoint_on_Ioo_succ


[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ ⊤ = ⊥
[PROOFSTEP]
rw [boundary, hnot_top, inf_bot_eq]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ∂ (￢￢a) = ∂ (￢a)
[PROOFSTEP]
simp_rw [boundary, hnot_hnot_hnot, inf_comm]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ￢∂ a = ⊤
[PROOFSTEP]
rw [boundary, hnot_inf_distrib, sup_hnot_self]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ a b : α
⊢ ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ b
[PROOFSTEP]
unfold boundary
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ a b : α
⊢ a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
[PROOFSTEP]
rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ b
[PROOFSTEP]
rw [boundary, inf_sup_right]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b
[PROOFSTEP]
exact sup_le_sup (inf_le_inf_left _ <| hnot_anti le_sup_left) (inf_le_inf_left _ <| hnot_anti le_sup_right)
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
⊢ (a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬a
[PROOFSTEP]
rintro ⟨⟨ha, _⟩ | hnab, (ha | hb) | hnab⟩
[GOAL]
case intro.inl.intro.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha✝ : a
right✝ : b
ha : a
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inl.intro.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha✝ : a
right✝ : b
ha : a
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inl.intro.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inl.intro.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inl.intro.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inl.intro.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inr.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
ha : a
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inr.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
ha : a
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
try exact Or.inl ha
[GOAL]
case intro.inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case intro.inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inr fun ha => hnab ⟨ha, hb⟩
[GOAL]
case intro.inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
[PROOFSTEP]
exact Or.inr fun ha => hnab <| Or.inl ha
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
[PROOFSTEP]
simp only [boundary, sup_inf_left, sup_inf_right, sup_right_idem, le_inf_iff, sup_assoc, @sup_comm _ _ _ a]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩
[GOAL]
case refine_1
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_1
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_1
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_2
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_2
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_2
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_3
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_3
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_3
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_5
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_5
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_5
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
try {exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
{exact le_sup_of_le_left inf_le_left
}
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
exact le_sup_of_le_left inf_le_left
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
refine inf_le_of_right_le ?_
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
refine inf_le_of_right_le ?_
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ b
[PROOFSTEP]
rw [hnot_le_iff_codisjoint_right, codisjoint_left_comm]
[GOAL]
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)
[PROOFSTEP]
exact codisjoint_hnot_left
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
[PROOFSTEP]
refine le_sup_of_le_right ?_
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊓ b)
[PROOFSTEP]
rw [hnot_le_iff_codisjoint_right]
[GOAL]
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢(a ⊓ b))
[PROOFSTEP]
exact codisjoint_hnot_right.mono_right (hnot_anti inf_le_left)
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
[PROOFSTEP]
rw [@sup_comm _ _ a, inf_comm]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)
[PROOFSTEP]
exact boundary_le_boundary_sup_sup_boundary_inf_left
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ∂ ∂ a = ∂ a
[PROOFSTEP]
rw [boundary, hnot_boundary, inf_top_eq]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ￢￢a ⊔ ∂ a = a
[PROOFSTEP]
rw [boundary, sup_inf_left, hnot_sup_self, inf_top_eq, sup_eq_right]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ￢￢a ≤ a
[PROOFSTEP]
exact hnot_hnot_le
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
h : ￢a = ⊤
⊢ ∂ a = a
[PROOFSTEP]
rw [boundary, h, inf_top_eq]
[GOAL]
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ (∃ b, ∂ b = a) → ￢a = ⊤
[PROOFSTEP]
rintro ⟨b, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : CoheytingAlgebra α
b✝ b : α
⊢ ￢∂ b = ⊤
[PROOFSTEP]
exact hnot_boundary _


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


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a b : α
h : MonotoneOn f s
hl : BddBelow (f '' s)
hu : BddAbove (f '' s)
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
classical
  /- The extension is defined by `f x = f a` for `x ≤ a`, and `f x` is the supremum of the values
        of `f` to the left of `x` for `x ≥ a`. -/
rcases hl with ⟨a, ha⟩
have hu' : ∀ x, BddAbove (f '' (Iic x ∩ s)) := fun x => hu.mono (image_subset _ (inter_subset_right _ _))
let g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
have hgs : EqOn f g s := by
  intro x hx
  simp only []
  have : IsGreatest (Iic x ∩ s) x := ⟨⟨right_mem_Iic, hx⟩, fun y hy => hy.1⟩
  rw [if_neg this.nonempty.not_disjoint, ((h.mono <| inter_subset_right _ _).map_isGreatest this).csSup_eq]
refine' ⟨g, fun x y hxy => _, hgs⟩
by_cases hx : Disjoint (Iic x) s <;> by_cases hy : Disjoint (Iic y) s <;>
  simp only [if_pos, if_neg, not_false_iff, *, refl]
· rcases not_disjoint_iff_nonempty_inter.1 hy with ⟨z, hz⟩
  exact le_csSup_of_le (hu' _) (mem_image_of_mem _ hz) (ha <| mem_image_of_mem _ hz.2)
· exact (hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim
· rw [not_disjoint_iff_nonempty_inter] at hx hy
  refine' csSup_le_csSup (hu' _) (hx.image _) (image_subset _ _)
  exact inter_subset_inter_left _ (Iic_subset_Iic.2 hxy)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a b : α
h : MonotoneOn f s
hl : BddBelow (f '' s)
hu : BddAbove (f '' s)
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
rcases hl with ⟨a, ha⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
have hu' : ∀ x, BddAbove (f '' (Iic x ∩ s)) := fun x => hu.mono (image_subset _ (inter_subset_right _ _))
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
let g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
have hgs : EqOn f g s := by
  intro x hx
  simp only []
  have : IsGreatest (Iic x ∩ s) x := ⟨⟨right_mem_Iic, hx⟩, fun y hy => hy.1⟩
  rw [if_neg this.nonempty.not_disjoint, ((h.mono <| inter_subset_right _ _).map_isGreatest this).csSup_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
⊢ EqOn f g s
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
⊢ f x = g x
[PROOFSTEP]
simp only []
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
⊢ f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
[PROOFSTEP]
have : IsGreatest (Iic x ∩ s) x := ⟨⟨right_mem_Iic, hx⟩, fun y hy => hy.1⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
this : IsGreatest (Iic x ∩ s) x
⊢ f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
[PROOFSTEP]
rw [if_neg this.nonempty.not_disjoint, ((h.mono <| inter_subset_right _ _).map_isGreatest this).csSup_eq]
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
⊢ ∃ g, Monotone g ∧ EqOn f g s
[PROOFSTEP]
refine' ⟨g, fun x y hxy => _, hgs⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
⊢ g x ≤ g y
[PROOFSTEP]
by_cases hx : Disjoint (Iic x) s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
⊢ g x ≤ g y
[PROOFSTEP]
by_cases hy : Disjoint (Iic y) s
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
⊢ g x ≤ g y
[PROOFSTEP]
by_cases hy : Disjoint (Iic y) s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ g x ≤ g y
[PROOFSTEP]
simp only [if_pos, if_neg, not_false_iff, *, refl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ g x ≤ g y
[PROOFSTEP]
simp only [if_pos, if_neg, not_false_iff, *, refl]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ g x ≤ g y
[PROOFSTEP]
simp only [if_pos, if_neg, not_false_iff, *, refl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ g x ≤ g y
[PROOFSTEP]
simp only [if_pos, if_neg, not_false_iff, *, refl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ a ≤ sSup (f '' (Iic y ∩ s))
[PROOFSTEP]
rcases not_disjoint_iff_nonempty_inter.1 hy with ⟨z, hz⟩
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
z : α
hz : z ∈ Iic y ∩ s
⊢ a ≤ sSup (f '' (Iic y ∩ s))
[PROOFSTEP]
exact le_csSup_of_le (hu' _) (mem_image_of_mem _ hz) (ha <| mem_image_of_mem _ hz.2)
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ a
[PROOFSTEP]
exact (hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
[PROOFSTEP]
rw [not_disjoint_iff_nonempty_inter] at hx hy
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Set.Nonempty (Iic x ∩ s)
hy : Set.Nonempty (Iic y ∩ s)
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
[PROOFSTEP]
refine' csSup_le_csSup (hu' _) (hx.image _) (image_subset _ _)
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
a✝ b : α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Set.Nonempty (Iic x ∩ s)
hy : Set.Nonempty (Iic y ∩ s)
⊢ Iic x ∩ s ⊆ Iic y ∩ s
[PROOFSTEP]
exact inter_subset_inter_left _ (Iic_subset_Iic.2 hxy)