[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
convert (Finset.sup_inf_distrib_left s.toFinset id a).le using 1
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = sup (Set.toFinset s) fun i => a ⊓ id i
[PROOFSTEP]
rw [Finset.sup_eq_iSup]
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = ⨆ (a_1 : α) (_ : a_1 ∈ Set.toFinset s), a ⊓ id a_1
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = ⨆ (a_1 : α) (_ : a_1 ∈ s), a ⊓ id a_1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b ≤ a ⊔ sInf s
[PROOFSTEP]
convert (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = inf (Set.toFinset s) fun i => a ⊔ id i
[PROOFSTEP]
rw [Finset.inf_eq_iInf]
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = ⨅ (a_1 : α) (_ : a_1 ∈ Set.toFinset s), a ⊔ id a_1
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = ⨅ (a_1 : α) (_ : a_1 ∈ s), a ⊔ id a_1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
convert (Finset.sup_inf_distrib_left s.toFinset id a).le using 1
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = sup (Set.toFinset s) fun i => a ⊓ id i
[PROOFSTEP]
rw [Finset.sup_eq_iSup]
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = ⨆ (a_1 : α) (_ : a_1 ∈ Set.toFinset s), a ⊓ id a_1
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = ⨆ (a_1 : α) (_ : a_1 ∈ s), a ⊓ id a_1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b ≤ a ⊔ sInf s
[PROOFSTEP]
convert (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = inf (Set.toFinset s) fun i => a ⊔ id i
[PROOFSTEP]
rw [Finset.inf_eq_iInf]
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = ⨅ (a_1 : α) (_ : a_1 ∈ Set.toFinset s), a ⊔ id a_1
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = ⨅ (a_1 : α) (_ : a_1 ∈ s), a ⊔ id a_1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
[PROOFSTEP]
classical
obtain ⟨z, hz⟩ := D.finset_le (Finset.image g Finset.univ)
exact ⟨z, fun i => hz (g i) (Finset.mem_image_of_mem g (Finset.mem_univ i))⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
[PROOFSTEP]
obtain ⟨z, hz⟩ := D.finset_le (Finset.image g Finset.univ)
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
z : γ
hz : ∀ (i : γ), i ∈ image g univ → r (f i) (f z)
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
[PROOFSTEP]
exact ⟨z, fun i => hz (g i) (Finset.mem_image_of_mem g (Finset.mem_univ i))⟩
[GOAL]
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
⊢ BddAbove (Set.range f)
[PROOFSTEP]
obtain ⟨M, hM⟩ := Fintype.exists_le f
[GOAL]
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
⊢ BddAbove (Set.range f)
[PROOFSTEP]
refine' ⟨M, fun a ha => _⟩
[GOAL]
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
a : α
ha : a ∈ Set.range f
⊢ a ≤ M
[PROOFSTEP]
obtain ⟨b, rfl⟩ := ha
[GOAL]
case intro.intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
b : β
⊢ f b ≤ M
[PROOFSTEP]
exact hM b
[GOAL]
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≥ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
⊢ BddBelow (Set.range f)
[PROOFSTEP]
obtain ⟨M, hM⟩ := Fintype.exists_ge f
[GOAL]
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≥ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
⊢ BddBelow (Set.range f)
[PROOFSTEP]
refine' ⟨M, fun a ha => _⟩
[GOAL]
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≥ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
a : α
ha : a ∈ Set.range f
⊢ M ≤ a
[PROOFSTEP]
obtain ⟨b, rfl⟩ := ha
[GOAL]
case intro.intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≥ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
b : β
⊢ M ≤ f b
[PROOFSTEP]
exact hM b
