[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
⊢ DirectedOn r s ↔ Directed r Subtype.val
[PROOFSTEP]
simp [Directed, DirectedOn]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
⊢ (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∃ z, z ∈ s ∧ r x z ∧ r y z) ↔
    ∀ (a : α), a ∈ s → ∀ (a_1 : α), a_1 ∈ s → ∃ a_2, r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2
[PROOFSTEP]
refine' ball_congr fun x _ => by simp [And.comm, and_assoc]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
x : α
x✝ : x ∈ s
⊢ (∀ (y : α), y ∈ s → ∃ z, z ∈ s ∧ r x z ∧ r y z) ↔ ∀ (a : α), a ∈ s → ∃ a_1, r x a_1 ∧ a_1 ∈ s ∧ r a a_1
[PROOFSTEP]
simp [And.comm, and_assoc]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
f : ι → α
⊢ Directed r f ↔ DirectedOn r (Set.range f)
[PROOFSTEP]
simp_rw [Directed, DirectedOn, Set.forall_range_iff, Set.exists_range_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set β
f : β → α
⊢ DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s
[PROOFSTEP]
simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  Order.Preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
⊢ Directed (fun x x_1 => x ≤ x_1) (extend e f ⊥)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
a b : β
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
[PROOFSTEP]
rcases(em (∃ i, e i = a)).symm with (ha | ⟨i, rfl⟩)
[GOAL]
case inl
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
[PROOFSTEP]
use b
[GOAL]
case h
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ (fun x x_1 => x ≤ x_1) (extend e f ⊥ a) (extend e f ⊥ b) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ b)
[PROOFSTEP]
simp [Function.extend_apply' _ _ _ ha]
[GOAL]
case inr.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
b : β
i : ι
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
[PROOFSTEP]
rcases(em (∃ i, e i = b)).symm with (hb | ⟨j, rfl⟩)
[GOAL]
case inr.intro.inl
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
[PROOFSTEP]
use e i
[GOAL]
case h
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ (e i)) ∧
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ (e i))
[PROOFSTEP]
simp [Function.extend_apply' _ _ _ hb]
[GOAL]
case inr.intro.inr.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
i j : ι
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e j)) (extend e f ⊥ z)
[PROOFSTEP]
rcases hf i j with ⟨k, hi, hj⟩
[GOAL]
case inr.intro.inr.intro.intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e j)) (extend e f ⊥ z)
[PROOFSTEP]
use e k
[GOAL]
case h
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ (e k)) ∧
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e j)) (extend e f ⊥ (e k))
[PROOFSTEP]
simp only [he.extend_apply, *, true_and_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝ : IsDirected α r
⊢ Directed r id
[PROOFSTEP]
convert directed_of r
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝ : IsTotal α r
⊢ IsDirected α r
[PROOFSTEP]
rw [← directed_id_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝ : IsTotal α r
⊢ Directed r id
[PROOFSTEP]
exact IsTotal.directed _
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : LE α
inst✝ : IsDirected α fun x x_1 => x ≤ x_1
⊢ IsDirected αᵒᵈ fun x x_1 => x ≥ x_1
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : LE α
inst✝ : IsDirected α fun x x_1 => x ≥ x_1
⊢ IsDirected αᵒᵈ fun x x_1 => x ≤ x_1
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r a c ∧ r b c
⊢ DirectedOn r (insert a s)
[PROOFSTEP]
rintro x (rfl | hx) y (rfl | hy)
[GOAL]
case inl.inl
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
y : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r y c ∧ r b c
⊢ ∃ z, z ∈ insert y s ∧ r y z ∧ r y z
[PROOFSTEP]
exact ⟨y, Set.mem_insert _ _, h _, h _⟩
[GOAL]
case inl.inr
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z, z ∈ insert x s ∧ r x z ∧ r y z
[PROOFSTEP]
obtain ⟨w, hws, hwr⟩ := ha y hy
[GOAL]
case inl.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r x c ∧ r b c
y : α
hy : y ∈ s
w : α
hws : w ∈ s
hwr : r x w ∧ r y w
⊢ ∃ z, z ∈ insert x s ∧ r x z ∧ r y z
[PROOFSTEP]
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩
[GOAL]
case inr.inl
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r y c ∧ r b c
⊢ ∃ z, z ∈ insert y s ∧ r x z ∧ r y z
[PROOFSTEP]
obtain ⟨w, hws, hwr⟩ := ha x hx
[GOAL]
case inr.inl.intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r y c ∧ r b c
w : α
hws : w ∈ s
hwr : r y w ∧ r x w
⊢ ∃ z, z ∈ insert y s ∧ r x z ∧ r y z
[PROOFSTEP]
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩
[GOAL]
case inr.inr
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z, z ∈ insert a s ∧ r x z ∧ r y z
[PROOFSTEP]
obtain ⟨w, hws, hwr⟩ := hd x hx y hy
[GOAL]
case inr.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
w : α
hws : w ∈ s
hwr : r x w ∧ r y w
⊢ ∃ z, z ∈ insert a s ∧ r x z ∧ r y z
[PROOFSTEP]
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {b, a}
[PROOFSTEP]
rw [Set.pair_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {a, b}
[PROOFSTEP]
apply directedOn_pair h hab
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝³ : Preorder α
a : α
inst✝² : PartialOrder β
inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1
inst✝ : Nontrivial β
⊢ ∃ a b, a < b
[PROOFSTEP]
rcases exists_pair_ne β with ⟨a, b, hne⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝³ : Preorder α
a✝ : α
inst✝² : PartialOrder β
inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1
inst✝ : Nontrivial β
a b : β
hne : a ≠ b
⊢ ∃ a b, a < b
[PROOFSTEP]
rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩)
[GOAL]
case intro.intro.inl
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝³ : Preorder α
a✝ : α
inst✝² : PartialOrder β
inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1
inst✝ : Nontrivial β
a b : β
hne : a ≠ b
ha : IsBot a
⊢ ∃ a b, a < b
case intro.intro.inr.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝³ : Preorder α
a✝ : α
inst✝² : PartialOrder β
inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1
inst✝ : Nontrivial β
a b : β
hne : a ≠ b
c : β
hc : c < a
⊢ ∃ a b, a < b
[PROOFSTEP]
exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
⊢ Monotone f
[PROOFSTEP]
intro a b hab
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ f a ≤ f b
[PROOFSTEP]
have e1 : IsLUB (f '' { a, b }) (f b) := by
  apply h
  · exact Set.insert_nonempty _ _
  · exact directedOn_pair le_refl hab
  · rw [IsLUB, upperBounds_insert, upperBounds_singleton,
      Set.inter_eq_self_of_subset_right (Set.Ici_subset_Ici.mpr hab)]
    exact isLeast_Ici
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLUB (f '' {a, b}) (f b)
[PROOFSTEP]
apply h
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ Set.Nonempty {a, b}
[PROOFSTEP]
exact Set.insert_nonempty _ _
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ DirectedOn (fun x x_1 => x ≤ x_1) {a, b}
[PROOFSTEP]
exact directedOn_pair le_refl hab
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLUB {a, b} b
[PROOFSTEP]
rw [IsLUB, upperBounds_insert, upperBounds_singleton, Set.inter_eq_self_of_subset_right (Set.Ici_subset_Ici.mpr hab)]
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLeast (Set.Ici b) b
[PROOFSTEP]
exact isLeast_Ici
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ≤ f b
[PROOFSTEP]
apply e1.1
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ∈ f '' {a, b}
[PROOFSTEP]
rw [Set.image_pair]
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ∈ {f a, f b}
[PROOFSTEP]
exact Set.mem_insert _ _


[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteSemilatticeSup α
s✝ t : Set α
a b : α
s : ι → α
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
[PROOFSTEP]
simp [iSup, le_sSup_iff, upperBounds]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteSemilatticeInf α
s✝ t : Set α
a b : α
s : ι → α
⊢ iInf s ≤ a ↔ ∀ (b : α), (∀ (i : ι), b ≤ s i) → b ≤ a
[PROOFSTEP]
simp [iInf, sInf_le_iff, lowerBounds]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
⊢ ∀ (c : α), c ≤ sInf t → c ≤ sInf s
[PROOFSTEP]
simp only [le_sInf_iff]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
⊢ ∀ (c : α), (∀ (b : α), b ∈ t → c ≤ b) → ∀ (b : α), b ∈ s → c ≤ b
[PROOFSTEP]
introv h₀ h₁
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b✝ : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
c : α
h₀ : ∀ (b : α), b ∈ t → c ≤ b
b : α
h₁ : b ∈ s
⊢ c ≤ b
[PROOFSTEP]
rcases h _ h₁ with ⟨y, hy, hy'⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteSemilatticeInf α
s t : Set α
a b✝ : α
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x
c : α
h₀ : ∀ (b : α), b ∈ t → c ≤ b
b : α
h₁ : b ∈ s
y : α
hy : y ∈ t
hy' : y ≤ b
⊢ c ≤ b
[PROOFSTEP]
solve_by_elim [le_trans _ hy']
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ c ∈ {x | a ≤ x ∧ b ≤ x}
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hab : a ≤ b
hac : a ≤ c
⊢ a ≤ b ⊓ c
[PROOFSTEP]
apply (isGLB_sInf _).2
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hab : a ≤ b
hac : a ≤ c
⊢ a ∈ lowerBounds {b, c}
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a : α
⊢ a ∈ lowerBounds ∅
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ c ∈ upperBounds {a, b}
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
a b c : α
hab : a ≤ b
hac : a ≤ c
⊢ a ∈ {x | x ≤ b ∧ x ≤ c}
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
x : α
⊢ x ∈ upperBounds ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
i : CompleteLinearOrder α
a b : α
⊢ min a b = if a ≤ b then a else b
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b = b
[PROOFSTEP]
simp [(CompleteLinearOrder.le_total a b).resolve_left h]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
i : CompleteLinearOrder α
a b : α
⊢ max a b = if a ≤ b then b else a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ max a b = b
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ max a b = a
[PROOFSTEP]
simp [(CompleteLinearOrder.le_total a b).resolve_left h]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
s✝ t : Set α
a b : α
s : Set α
h_sup : sSup s = ⊥
hne : Set.Nonempty s
⊢ s = {⊥}
[PROOFSTEP]
rw [Set.eq_singleton_iff_nonempty_unique_mem]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
s✝ t : Set α
a b : α
s : Set α
h_sup : sSup s = ⊥
hne : Set.Nonempty s
⊢ Set.Nonempty s ∧ ∀ (x : α), x ∈ s → x = ⊥
[PROOFSTEP]
rw [sSup_eq_bot] at h_sup
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
s✝ t : Set α
a b : α
s : Set α
h_sup : ∀ (a : α), a ∈ s → a = ⊥
hne : Set.Nonempty s
⊢ Set.Nonempty s ∧ ∀ (x : α), x ∈ s → x = ⊥
[PROOFSTEP]
exact ⟨hne, h_sup⟩
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f g : ι → α
s : Set α
⊢ sSup s = ⨆ (a : ↑s), ↑a
[PROOFSTEP]
rw [iSup, Subtype.range_coe]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f✝ g✝ : ι → α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ ⨆ (x : ι), g (f x) = ⨆ (y : ι'), g y
[PROOFSTEP]
simp [iSup]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f✝ g✝ : ι → α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ sSup (range fun x => g (f x)) = sSup (range fun y => g y)
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f✝ g✝ : ι → α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ (range fun x => g (f x)) = range fun y => g y
[PROOFSTEP]
exact hf.range_comp g
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f g✝ : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ ⨆ (x : ι), f x = ⨆ (y : ι'), g y
[PROOFSTEP]
convert h1.iSup_comp g
[GOAL]
case h.e'_2.h.e'_4.h
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f g✝ : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
x✝ : ι
⊢ f x✝ = g (h x✝)
[PROOFSTEP]
exact (h2 _).symm
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f✝ g : ι → α
p q : Prop
f₁ : p → α
f₂ : q → α
pq : p ↔ q
f : ∀ (x : q), f₁ (_ : p) = f₂ x
⊢ iSup f₁ = iSup f₂
[PROOFSTEP]
obtain rfl := propext pq
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f✝ g : ι → α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ (_ : p) = f₂ x
⊢ iSup f₁ = iSup f₂
[PROOFSTEP]
congr with x
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f✝ g : ι → α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ (_ : p) = f₂ x
x : p
⊢ f₁ x = f₂ x
[PROOFSTEP]
apply f
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f✝ g✝ : ι → α
g : β → α
f : ι → β
⊢ ⨆ (b : ↑(range f)), g ↑b = ⨆ (i : ι), g (f i)
[PROOFSTEP]
rw [iSup, iSup, ← image_eq_range, ← range_comp]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f✝ g✝ : ι → α
g : β → α
f : ι → β
⊢ sSup (range (g ∘ f)) = sSup (range fun i => g (f i))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : SupSet α
f✝ g : ι → α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ (a : ↑s), f ↑a
[PROOFSTEP]
rw [iSup, image_eq_range]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : (i : ι) → κ i → α
⊢ ⨆ (i : ι) (j : κ i), f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a
[PROOFSTEP]
simp_rw [iSup_le_iff]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : (i : ι) → κ i → α
⊢ a ≤ ⨅ (i : ι) (j : κ i), f i j ↔ ∀ (i : ι) (j : κ i), a ≤ f i j
[PROOFSTEP]
simp_rw [le_iInf_iff]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ (a : α) (_ : a ∈ s), f a ≤ f (sSup s)
[PROOFSTEP]
rw [sSup_eq_iSup]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ (a : α) (_ : a ∈ s), f a ≤ f (⨆ (a : α) (_ : a ∈ s), a)
[PROOFSTEP]
exact hf.le_map_iSup₂ _
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s t : ι → α
a b : α
inst✝ : CompleteLattice β
f : α ≃o β
x✝ : ι → α
x : α
⊢ ↑f (⨆ (i : ι), x✝ i) ≤ ↑f x ↔ ⨆ (i : ι), ↑f (x✝ i) ≤ ↑f x
[PROOFSTEP]
simp only [f.le_iff_le, iSup_le_iff]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ ↑f (sSup s) = ⨆ (a : α) (_ : a ∈ s), ↑f a
[PROOFSTEP]
simp only [sSup_eq_iSup, OrderIso.map_iSup]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Antitone f
⊢ f (sSup s) ≤ ⨅ (a : α) (_ : a ∈ s), f a
[PROOFSTEP]
rw [sSup_eq_iSup]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Antitone f
⊢ f (⨆ (a : α) (_ : a ∈ s), a) ≤ ⨅ (a : α) (_ : a ∈ s), f a
[PROOFSTEP]
exact hf.map_iSup₂_le _
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f g s t : ι → α
a b : α
inst✝ : Nonempty ι
⊢ ⨆ (x : ι), a = a
[PROOFSTEP]
rw [iSup, range_const, sSup_singleton]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : (i : ι) → κ i → α
⊢ ⨆ (i : ι) (j : κ i), f i j = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : (i : ι) → κ i → α
⊢ ⨅ (i : ι) (j : κ i), f i j = ⊤ ↔ ∀ (i : ι) (j : κ i), f i j = ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f g s t : ι → α
a✝ b : α
p : Prop
inst✝ : Decidable p
a : p → α
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥
[PROOFSTEP]
by_cases h : p
[GOAL]
case pos
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f g s t : ι → α
a✝ b : α
p : Prop
inst✝ : Decidable p
a : p → α
h : p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f g s t : ι → α
a✝ b : α
p : Prop
inst✝ : Decidable p
a : p → α
h : ¬p
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
ι₁ : Sort u_9
ι₂ : Sort u_10
κ₁ : ι₁ → Sort u_11
κ₂ : ι₂ → Sort u_12
f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α
⊢ ⨆ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ =
    ⨆ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
[PROOFSTEP]
simp only [@iSup_comm _ (κ₁ _), @iSup_comm _ ι₁]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
ι₁ : Sort u_9
ι₂ : Sort u_10
κ₁ : ι₁ → Sort u_11
κ₂ : ι₂ → Sort u_12
f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α
⊢ ⨅ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ =
    ⨅ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
[PROOFSTEP]
simp only [@iInf_comm _ (κ₁ _), @iInf_comm _ ι₁]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b✝ : α
b : β
f : (x : β) → x = b → α
c : β
⊢ ∀ (i : c = b), f c i ≤ f b (_ : b = b)
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
c : β
f : (x : β) → x = c → α
⊢ f c (_ : c = c) ≤ f c (_ : c = c)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b✝ : α
b : β
f : (x : β) → b = x → α
c : β
⊢ ∀ (j : b = c), f c j ≤ f b (_ : b = b)
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b✝ : α
b : β
f : (x : β) → b = x → α
⊢ f b (_ : b = b) ≤ f b (_ : b = b)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι✝ : Sort u_5
ι' : Sort u_6
κ : ι✝ → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s✝ t : ι✝ → α
a✝ b : α
ι : Type u_9
a : α
s : Set ι
hs : Set.Nonempty s
⊢ ⨆ (i : ι) (_ : i ∈ s), a = a
[PROOFSTEP]
haveI : Nonempty s := Set.nonempty_coe_sort.mpr hs
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι✝ : Sort u_5
ι' : Sort u_6
κ : ι✝ → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s✝ t : ι✝ → α
a✝ b : α
ι : Type u_9
a : α
s : Set ι
hs : Set.Nonempty s
this : Nonempty ↑s
⊢ ⨆ (i : ι) (_ : i ∈ s), a = a
[PROOFSTEP]
rw [← iSup_subtype'', iSup_const]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ (x : ι), f x) ⊔ a = ⨆ (x : ι), f x ⊔ a
[PROOFSTEP]
rw [iSup_sup_eq, iSup_const]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨅ (x : ι), f x) ⊓ a = ⨅ (x : ι), f x ⊓ a
[PROOFSTEP]
rw [iInf_inf_eq, iInf_const]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ⊔ ⨆ (x : ι), f x = ⨆ (x : ι), a ⊔ f x
[PROOFSTEP]
rw [iSup_sup_eq, iSup_const]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ⊓ ⨅ (x : ι), f x = ⨅ (x : ι), a ⊓ f x
[PROOFSTEP]
rw [iInf_inf_eq, iInf_const]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ (⨆ (i : ι) (h : p i), f i h) ⊔ a = ⨆ (i : ι) (h : p i), f i h ⊔ a
[PROOFSTEP]
haveI : Nonempty { i // p i } :=
  let ⟨i, hi⟩ := h
  ⟨⟨i, hi⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ (i : ι) (h : p i), f i h) ⊔ a = ⨆ (i : ι) (h : p i), f i h ⊔ a
[PROOFSTEP]
rw [iSup_subtype', iSup_subtype', iSup_sup]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ a ⊔ ⨆ (i : ι) (h : p i), f i h = ⨆ (i : ι) (h : p i), a ⊔ f i h
[PROOFSTEP]
simpa only [sup_comm] using @biSup_sup α _ _ p _ _ h
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s✝ t : ι → α
a b : α
s : False → α
⊢ iSup s = ⊥
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s✝ t : ι → α
a b : α
s : False → α
⊢ iInf s = ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ (i : ι), if h : p i then f i h else g i h) = (⨆ (i : ι) (h : p i), f i h) ⊔ ⨆ (i : ι) (h : ¬p i), g i h
[PROOFSTEP]
rw [← iSup_sup_eq]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ (i : ι), if h : p i then f i h else g i h) = ⨆ (x : ι), (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h
[PROOFSTEP]
congr 1 with i
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
⊢ (if h : p i then f i h else g i h) = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : p i
⊢ f i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : ¬p i
⊢ g i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
g : β → α
f : ι → β
⊢ ⨆ (b : β) (_ : b ∈ range f), g b = ⨆ (i : ι), g (f i)
[PROOFSTEP]
rw [← iSup_subtype'', iSup_range']
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ (a : β) (_ : a ∈ s), f a
[PROOFSTEP]
rw [← iSup_subtype'', sSup_image']
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
⊢ ⨆ (x : β) (_ : x ∈ ∅), f x = ⊥
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
⊢ ⨅ (x : β) (_ : x ∈ ∅), f x = ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
⊢ ⨆ (x : β) (_ : x ∈ univ), f x = ⨆ (x : β), f x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
⊢ ⨅ (x : β) (_ : x ∈ univ), f x = ⨅ (x : β), f x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β → α
s t : Set β
⊢ ⨆ (x : β) (_ : x ∈ s ∪ t), f x = (⨆ (x : β) (_ : x ∈ s), f x) ⊔ ⨆ (x : β) (_ : x ∈ t), f x
[PROOFSTEP]
simp_rw [mem_union, iSup_or, iSup_sup_eq]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
p : β → Prop
⊢ ⨆ (i : β), f i = (⨆ (i : β) (_ : p i), f i) ⊔ ⨆ (i : β) (_ : ¬p i), f i
[PROOFSTEP]
simpa [Classical.em] using @iSup_union _ _ _ f {i | p i} {i | ¬p i}
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
i₀ : β
⊢ ⨆ (i : β), f i = f i₀ ⊔ ⨆ (i : β) (_ : i ≠ i₀), f i
[PROOFSTEP]
convert iSup_split f (fun i => i = i₀)
[GOAL]
case h.e'_3.h.e'_3
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
i₀ : β
⊢ f i₀ = ⨆ (i : β) (_ : i = i₀), f i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b✝ : α
f : β → α
b : β
⊢ ⨆ (x : β) (_ : x ∈ {b}), f x = f b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b✝ : α
f : β → α
b : β
⊢ ⨅ (x : β) (_ : x ∈ {b}), f x = f b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b✝ : α
f : β → α
a b : β
⊢ ⨆ (x : β) (_ : x ∈ {a, b}), f x = f a ⊔ f b
[PROOFSTEP]
rw [iSup_insert, iSup_singleton]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b✝ : α
f : β → α
a b : β
⊢ ⨅ (x : β) (_ : x ∈ {a, b}), f x = f a ⊓ f b
[PROOFSTEP]
rw [iInf_insert, iInf_singleton]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ✝ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g✝ s t✝ : ι → α
a b : α
γ : Type u_9
f : β → γ
g : γ → α
t : Set β
⊢ ⨆ (c : γ) (_ : c ∈ f '' t), g c = ⨆ (b : β) (_ : b ∈ t), g (f b)
[PROOFSTEP]
rw [← sSup_image, ← sSup_image, ← image_comp]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ✝ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g✝ s t✝ : ι → α
a b : α
γ : Type u_9
f : β → γ
g : γ → α
t : Set β
⊢ sSup ((fun c => g c) ∘ f '' t) = sSup ((fun b => g (f b)) '' t)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
e : ι → β
he : Injective e
f : ι → α
⊢ ⨆ (j : β), extend e f ⊥ j = ⨆ (i : ι), f i
[PROOFSTEP]
rw [iSup_split _ fun j => ∃ i, e i = j]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
e : ι → β
he : Injective e
f : ι → α
⊢ (⨆ (i : β) (_ : ∃ i_1, e i_1 = i), extend e f ⊥ i) ⊔ ⨆ (i : β) (_ : ¬∃ i_1, e i_1 = i), extend e f ⊥ i =
    ⨆ (i : ι), f i
[PROOFSTEP]
simp (config := { contextual := true }) [he.extend_apply, extend_apply', @iSup_comm _ β ι]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : Bool → α
⊢ ⨆ (b : Bool), f b = f true ⊔ f false
[PROOFSTEP]
rw [iSup, Bool.range_eq, sSup_pair, sup_comm]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b x y : α
⊢ x ⊔ y = ⨆ (b : Bool), bif b then x else y
[PROOFSTEP]
rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
s : Set β
f : β → α
⊢ IsGLB (f '' s) (⨅ (x : β) (_ : x ∈ s), f x)
[PROOFSTEP]
simpa only [range_comp, Subtype.range_coe, iInf_subtype'] using @isGLB_iInf α s _ (f ∘ fun x => (x : β))
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
s : Set β
f : β → α
⊢ IsLUB (f '' s) (⨆ (x : β) (_ : x ∈ s), f x)
[PROOFSTEP]
simpa only [range_comp, Subtype.range_coe, iSup_subtype'] using @isLUB_iSup α s _ (f ∘ fun x => (x : β))
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
p : β → Type u_9
f : Sigma p → α
c : α
⊢ ⨆ (x : Sigma p), f x ≤ c ↔ ⨆ (i : β) (j : p i), f { fst := i, snd := j } ≤ c
[PROOFSTEP]
simp only [iSup_le_iff, Sigma.forall]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β × γ → α
c : α
⊢ ⨆ (x : β × γ), f x ≤ c ↔ ⨆ (i : β) (j : γ), f (i, j) ≤ c
[PROOFSTEP]
simp only [iSup_le_iff, Prod.forall]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ (x : β × γ) (_ : x ∈ s ×ˢ t), f x = ⨆ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f (a, b)
[PROOFSTEP]
simp_rw [iSup_prod, mem_prod, iSup_and]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ (i : β) (j : γ) (_ : i ∈ s) (_ : j ∈ t), f (i, j) = ⨆ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f (a, b)
[PROOFSTEP]
exact iSup_congr fun _ => iSup_comm
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β ⊕ γ → α
c : α
⊢ ⨆ (x : β ⊕ γ), f x ≤ c ↔ (⨆ (i : β), f (Sum.inl i)) ⊔ ⨆ (j : γ), f (Sum.inr j) ≤ c
[PROOFSTEP]
simp only [sup_le_iff, iSup_le_iff, Sum.forall]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : Option β → α
c : α
⊢ ⨆ (o : Option β), f o ≤ c ↔ f none ⊔ ⨆ (b : β), f (some b) ≤ c
[PROOFSTEP]
simp only [iSup_le_iff, sup_le_iff, Option.forall]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b a : α
f : β → α
⊢ ⨆ (o : Option β), Option.elim o a f = a ⊔ ⨆ (b : β), f b
[PROOFSTEP]
simp [iSup_option]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
⊢ ⨆ (i : { i // f i ≠ ⊥ }), f ↑i = ⨆ (i : ι), f i
[PROOFSTEP]
by_cases htriv : ∀ i, f i = ⊥
[GOAL]
case pos
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ∀ (i : ι), f i = ⊥
⊢ ⨆ (i : { i // f i ≠ ⊥ }), f ↑i = ⨆ (i : ι), f i
[PROOFSTEP]
simp only [iSup_bot, (funext htriv : f = _)]
[GOAL]
case neg
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
⊢ ⨆ (i : { i // f i ≠ ⊥ }), f ↑i = ⨆ (i : ι), f i
[PROOFSTEP]
refine' (iSup_comp_le f _).antisymm (iSup_mono' fun i => _)
[GOAL]
case neg
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
⊢ ∃ i', f i ≤ f ↑i'
[PROOFSTEP]
by_cases hi : f i = ⊥
[GOAL]
case pos
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'
[PROOFSTEP]
rw [hi]
[GOAL]
case pos
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'
[PROOFSTEP]
obtain ⟨i₀, hi₀⟩ := not_forall.mp htriv
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : f i = ⊥
i₀ : ι
hi₀ : ¬f i₀ = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'
[PROOFSTEP]
exact ⟨⟨i₀, hi₀⟩, bot_le⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ι → α
htriv : ¬∀ (i : ι), f i = ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'
[PROOFSTEP]
exact ⟨⟨i, hi⟩, rfl.le⟩
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β → γ → α
s : Set β
t : Set γ
⊢ sSup (image2 f s t) = ⨆ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f a b
[PROOFSTEP]
rw [← image_prod, sSup_image, biSup_prod]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β → γ → α
s : Set β
t : Set γ
⊢ sInf (image2 f s t) = ⨅ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f a b
[PROOFSTEP]
rw [← image_prod, sInf_image, biInf_prod]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ ⨆ (i : ℕ) (_ : i ≥ n), u i = ⨆ (i : ℕ), u (i + n)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ ⨆ (i : ℕ) (_ : i ≥ n), u i ≤ ⨆ (i : ℕ), u (i + n)
[PROOFSTEP]
simp only [iSup_le_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ ⨆ (i : ℕ), u (i + n) ≤ ⨆ (i : ℕ) (_ : i ≥ n), u i
[PROOFSTEP]
simp only [iSup_le_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), i ≥ n → u i ≤ ⨆ (i : ℕ), u (i + n)
[PROOFSTEP]
refine fun i hi => le_sSup ⟨i - n, ?_⟩
[GOAL]
case a
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ (fun i => u (i + n)) (i - n) = u i
[PROOFSTEP]
dsimp only
[GOAL]
case a
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ u (i - n + n) = u i
[PROOFSTEP]
rw [Nat.sub_add_cancel hi]
[GOAL]
case a
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ (i : ℕ) (_ : i ≥ n), u i
[PROOFSTEP]
exact fun i => le_sSup ⟨i + n, iSup_pos (Nat.le_add_left _ _)⟩
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ℕ → α
k : ℕ
⊢ ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f (i + k) = ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f i
[PROOFSTEP]
have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => biInf_mono fun i => h.trans
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ℕ → α
k : ℕ
hf : Monotone fun n => ⨅ (i : ℕ) (_ : i ≥ n), f i
⊢ ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f (i + k) = ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f i
[PROOFSTEP]
rw [← Monotone.iSup_nat_add hf k]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ℕ → α
k : ℕ
hf : Monotone fun n => ⨅ (i : ℕ) (_ : i ≥ n), f i
⊢ ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f (i + k) = ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n + k), f i
[PROOFSTEP]
simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ (x : ℕ) (_ : x ∈ {0} ∪ range Nat.succ), u x
[PROOFSTEP]
{rw [iSup_union, iSup_singleton, iSup_range]
}
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ (x : ℕ) (_ : x ∈ {0} ∪ range Nat.succ), u x
[PROOFSTEP]
rw [iSup_union, iSup_singleton, iSup_range]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
⊢ ⨆ (x : ℕ) (_ : x ∈ {0} ∪ range Nat.succ), u x = ⨆ (i : ℕ), u i
[PROOFSTEP]
rw [Nat.zero_union_range_succ, iSup_univ]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ℕ → α
⊢ ⨅ (i : ℕ) (_ : i > 0), f i = ⨅ (i : ℕ), f (i + 1)
[PROOFSTEP]
rw [← iInf_range, Nat.range_succ]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ℕ → α
⊢ ⨅ (i : ℕ) (_ : i > 0), f i = ⨅ (b : ℕ) (_ : b ∈ {i | 0 < i}), f b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ iSup f = ⊤ ↔ ∀ (b : α), b < ⊤ → ∃ i, b < f i
[PROOFSTEP]
simp only [← sSup_range, sSup_eq_top, Set.exists_range_iff]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ iInf f = ⊥ ↔ ∀ (b : α), b > ⊥ → ∃ i, f i < b
[PROOFSTEP]
simp only [← sInf_range, sInf_eq_bot, Set.exists_range_iff]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
β₂ : Type u_3
γ : Type u_4
ι✝ : Sort u_5
ι' : Sort u_6
κ : ι✝ → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
β : α → Type u_10
ι : Sort u_11
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ iSup (fun i => f i) a = ⨆ (i : ι), f i a
[PROOFSTEP]
rw [iSup, sSup_apply, iSup, iSup, ← image_eq_range (fun f : ∀ i, β i => f a) (range f), ← range_comp]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
β₂ : Type u_3
γ : Type u_4
ι✝ : Sort u_5
ι' : Sort u_6
κ : ι✝ → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
β : α → Type u_10
ι : Sort u_11
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ sSup (range ((fun f => f a) ∘ f)) = sSup (range fun i => f i a)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
s : Set (α → Prop)
a : α
⊢ sSup s a ↔ ∃ r, r ∈ s ∧ r a
[PROOFSTEP]
rw [sSup_apply]
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
s : Set (α → Prop)
a : α
⊢ ⨆ (f : ↑s), ↑f a ↔ ∃ r, r ∈ s ∧ r a
[PROOFSTEP]
simp [← eq_iff_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
s : Set (α → Prop)
a : α
⊢ sInf s a ↔ ∀ (r : α → Prop), r ∈ s → r a
[PROOFSTEP]
rw [sInf_apply]
[GOAL]
α✝ : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
s : Set (α → Prop)
a : α
⊢ ⨅ (f : ↑s), ↑f a ↔ ∀ (r : α → Prop), r ∈ s → r a
[PROOFSTEP]
simp [← eq_iff_iff]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
β : Type u_10
s : Set (α → β → Prop)
a : α
b : β
⊢ sSup s a b ↔ ∃ r, r ∈ s ∧ r a b
[PROOFSTEP]
rw [sSup_apply]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
β : Type u_10
s : Set (α → β → Prop)
a : α
b : β
⊢ iSup (fun f => ↑f a) b ↔ ∃ r, r ∈ s ∧ r a b
[PROOFSTEP]
simp [← eq_iff_iff]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
β : Type u_10
s : Set (α → β → Prop)
a : α
b : β
⊢ sInf s a b ↔ ∀ (r : α → β → Prop), r ∈ s → r a b
[PROOFSTEP]
rw [sInf_apply]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
α : Type u_9
β : Type u_10
s : Set (α → β → Prop)
a : α
b : β
⊢ iInf (fun f => ↑f a) b ↔ ∀ (r : α → β → Prop), r ∈ s → r a b
[PROOFSTEP]
simp [← eq_iff_iff]
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : InfSet α
inst✝ : InfSet β
f : ι → α × β
⊢ swap (iInf f) = ⨅ (i : ι), swap (f i)
[PROOFSTEP]
simp_rw [iInf, swap_sInf, ← range_comp, Function.comp]
  -- Porting note: need to unfold `∘`
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝¹ : SupSet α
inst✝ : SupSet β
f : ι → α × β
⊢ swap (iSup f) = ⨆ (i : ι), swap (f i)
[PROOFSTEP]
simp_rw [iSup, swap_sSup, ← range_comp, Function.comp]
  -- Porting note: need to unfold `∘`
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (sSup s).down = ⨆ (a : ULift α) (_ : a ∈ s), a.down
[PROOFSTEP]
rw [sSup_eq_iSup', down_iSup, iSup_subtype'']
[GOAL]
α : Type u_1
β : Type u_2
β₂ : Type u_3
γ : Type u_4
ι : Sort u_5
ι' : Sort u_6
κ : ι → Sort u_7
κ' : ι' → Sort u_8
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (sInf s).down = ⨅ (a : ULift α) (_ : a ∈ s), a.down
[PROOFSTEP]
rw [sInf_eq_iInf', down_iInf, iInf_subtype'']