[GOAL]
α : Type u
h h' : LE α
c : BoundedOrder α
top : α
⊢ Top α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝ : α
⊢ x✝ ≤ ⊤
[PROOFSTEP]
simp [eq_top, le_eq]
[GOAL]
α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝ : α
⊢ ⊥ ≤ x✝
[PROOFSTEP]
simp [eq_bot, le_eq]
[GOAL]
α : Type u
c : Lattice α
le : α → α → Prop
⊢ LE α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
⊢ Sup α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
⊢ Inf α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ Lattice α
[PROOFSTEP]
refine' { le := le, sup := sup, inf := inf, lt := fun a b ↦ le a b ∧ ¬le b a .. }
[GOAL]
case refine'_1
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a : α), a ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ : α
⊢ a✝ ≤ a✝
[PROOFSTEP]
simp [eq_le]
[GOAL]
case refine'_2
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
intro _ _ _ hab hbc
[GOAL]
case refine'_2
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hab : a✝ ≤ b✝
hbc : b✝ ≤ c✝
⊢ a✝ ≤ c✝
[PROOFSTEP]
rw [eq_le] at hab hbc ⊢
[GOAL]
case refine'_2
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hab : a✝ ≤ b✝
hbc : b✝ ≤ c✝
⊢ a✝ ≤ c✝
[PROOFSTEP]
exact le_trans hab hbc
[GOAL]
case refine'_3
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ a✝ < b✝ ↔ a✝ ≤ b✝ ∧ ¬b✝ ≤ a✝
[PROOFSTEP]
simp [eq_le]
[GOAL]
case refine'_4
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
intro _ _ hab hba
[GOAL]
case refine'_4
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
hab : a✝ ≤ b✝
hba : b✝ ≤ a✝
⊢ a✝ = b✝
[PROOFSTEP]
simp_rw [eq_le] at hab hba
[GOAL]
case refine'_4
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
hab : a✝ ≤ b✝
hba : b✝ ≤ a✝
⊢ a✝ = b✝
[PROOFSTEP]
exact le_antisymm hab hba
[GOAL]
case refine'_5
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a ≤ a ⊔ b
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ a✝ ≤ a✝ ⊔ b✝
[PROOFSTEP]
simp [eq_le, eq_sup]
[GOAL]
case refine'_6
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), b ≤ a ⊔ b
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ b✝ ≤ a✝ ⊔ b✝
[PROOFSTEP]
simp [eq_le, eq_sup]
[GOAL]
case refine'_7
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
[PROOFSTEP]
intro _ _ _ hac hbc
[GOAL]
case refine'_7
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hac : a✝ ≤ c✝
hbc : b✝ ≤ c✝
⊢ a✝ ⊔ b✝ ≤ c✝
[PROOFSTEP]
simp_rw [eq_le] at hac hbc ⊢
[GOAL]
case refine'_7
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hac : a✝ ≤ c✝
hbc : b✝ ≤ c✝
⊢ sup a✝ b✝ ≤ c✝
[PROOFSTEP]
simp [eq_sup, hac, hbc]
[GOAL]
case refine'_8
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a ⊓ b ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ a✝ ⊓ b✝ ≤ a✝
[PROOFSTEP]
simp [eq_le, eq_inf]
[GOAL]
case refine'_9
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a ⊓ b ≤ b
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ a✝ ⊓ b✝ ≤ b✝
[PROOFSTEP]
simp [eq_le, eq_inf]
[GOAL]
case refine'_10
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
[PROOFSTEP]
intro _ _ _ hac hbc
[GOAL]
case refine'_10
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hac : a✝ ≤ b✝
hbc : a✝ ≤ c✝
⊢ a✝ ≤ b✝ ⊓ c✝
[PROOFSTEP]
simp_rw [eq_le] at hac hbc ⊢
[GOAL]
case refine'_10
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hac : a✝ ≤ b✝
hbc : a✝ ≤ c✝
⊢ a✝ ≤ inf b✝ c✝
[PROOFSTEP]
simp [eq_inf, hac, hbc]
[GOAL]
α : Type u
c : DistribLattice α
le : α → α → Prop
⊢ LE α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
⊢ Sup α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
⊢ Inf α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ DistribLattice α
[PROOFSTEP]
refine' { le := le, sup := sup, inf := inf, lt := fun a b ↦ le a b ∧ ¬le b a .. }
[GOAL]
case refine'_1
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a : α), a ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ : α
⊢ a✝ ≤ a✝
[PROOFSTEP]
simp [eq_le]
[GOAL]
case refine'_2
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
intro _ _ _ hab hbc
[GOAL]
case refine'_2
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hab : a✝ ≤ b✝
hbc : b✝ ≤ c✝
⊢ a✝ ≤ c✝
[PROOFSTEP]
rw [eq_le] at hab hbc ⊢
[GOAL]
case refine'_2
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hab : a✝ ≤ b✝
hbc : b✝ ≤ c✝
⊢ a✝ ≤ c✝
[PROOFSTEP]
exact le_trans hab hbc
[GOAL]
case refine'_3
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ a✝ < b✝ ↔ a✝ ≤ b✝ ∧ ¬b✝ ≤ a✝
[PROOFSTEP]
simp [eq_le]
[GOAL]
case refine'_4
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
intro _ _ hab hba
[GOAL]
case refine'_4
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
hab : a✝ ≤ b✝
hba : b✝ ≤ a✝
⊢ a✝ = b✝
[PROOFSTEP]
simp_rw [eq_le] at hab hba
[GOAL]
case refine'_4
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
hab : a✝ ≤ b✝
hba : b✝ ≤ a✝
⊢ a✝ = b✝
[PROOFSTEP]
exact le_antisymm hab hba
[GOAL]
case refine'_5
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a ≤ a ⊔ b
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ a✝ ≤ a✝ ⊔ b✝
[PROOFSTEP]
simp [eq_le, eq_sup]
[GOAL]
case refine'_6
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), b ≤ a ⊔ b
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ b✝ ≤ a✝ ⊔ b✝
[PROOFSTEP]
simp [eq_le, eq_sup]
[GOAL]
case refine'_7
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
[PROOFSTEP]
intro _ _ _ hac hbc
[GOAL]
case refine'_7
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hac : a✝ ≤ c✝
hbc : b✝ ≤ c✝
⊢ a✝ ⊔ b✝ ≤ c✝
[PROOFSTEP]
simp_rw [eq_le] at hac hbc ⊢
[GOAL]
case refine'_7
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hac : a✝ ≤ c✝
hbc : b✝ ≤ c✝
⊢ sup a✝ b✝ ≤ c✝
[PROOFSTEP]
simp [eq_sup, hac, hbc]
[GOAL]
case refine'_8
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a ⊓ b ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ a✝ ⊓ b✝ ≤ a✝
[PROOFSTEP]
simp [eq_le, eq_inf]
[GOAL]
case refine'_9
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b : α), a ⊓ b ≤ b
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ : α
⊢ a✝ ⊓ b✝ ≤ b✝
[PROOFSTEP]
simp [eq_le, eq_inf]
[GOAL]
case refine'_10
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
[PROOFSTEP]
intro _ _ _ hac hbc
[GOAL]
case refine'_10
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hac : a✝ ≤ b✝
hbc : a✝ ≤ c✝
⊢ a✝ ≤ b✝ ⊓ c✝
[PROOFSTEP]
simp_rw [eq_le] at hac hbc ⊢
[GOAL]
case refine'_10
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
a✝ b✝ c✝ : α
hac : a✝ ≤ b✝
hbc : a✝ ≤ c✝
⊢ a✝ ≤ inf b✝ c✝
[PROOFSTEP]
simp [eq_inf, hac, hbc]
[GOAL]
case refine'_11
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
⊢ ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
[PROOFSTEP]
intros
[GOAL]
case refine'_11
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
x✝ y✝ z✝ : α
⊢ (x✝ ⊔ y✝) ⊓ (x✝ ⊔ z✝) ≤ x✝ ⊔ y✝ ⊓ z✝
[PROOFSTEP]
simp [eq_le, eq_inf, eq_sup, le_sup_inf]
[GOAL]
α : Type u
c : CompleteLattice α
le : α → α → Prop
⊢ LE α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Sup α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
⊢ Inf α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
⊢ SupSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ CompleteLattice α
[PROOFSTEP]
refine'
  { Lattice.copy (@CompleteLattice.toLattice α c) le eq_le sup eq_sup inf eq_inf with le := le, top := top, bot := bot,
    sup := sup, inf := inf, sSup := sSup, sInf := sInf .. }
[GOAL]
case refine'_1
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
⊢ ∀ (s : Set α) (a : α), a ∈ s → a ≤ SupSet.sSup s
[PROOFSTEP]
intro _ _ h
[GOAL]
case refine'_1
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
s✝ : Set α
a✝ : α
h : a✝ ∈ s✝
⊢ a✝ ≤ SupSet.sSup s✝
[PROOFSTEP]
simp [eq_le, eq_sSup, le_sSup _ _ h]
[GOAL]
case refine'_2
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
⊢ ∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → SupSet.sSup s ≤ a
[PROOFSTEP]
intro _ _ h
[GOAL]
case refine'_2
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
s✝ : Set α
a✝ : α
h : ∀ (b : α), b ∈ s✝ → b ≤ a✝
⊢ SupSet.sSup s✝ ≤ a✝
[PROOFSTEP]
simpa [eq_le, eq_sSup] using h
[GOAL]
case refine'_3
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
⊢ ∀ (s : Set α) (a : α), a ∈ s → InfSet.sInf s ≤ a
[PROOFSTEP]
intro _ _ h
[GOAL]
case refine'_3
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
s✝ : Set α
a✝ : α
h : a✝ ∈ s✝
⊢ InfSet.sInf s✝ ≤ a✝
[PROOFSTEP]
simp [eq_le, eq_sInf, sInf_le _ _ h]
[GOAL]
case refine'_4
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
⊢ ∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ InfSet.sInf s
[PROOFSTEP]
intro _ _ h
[GOAL]
case refine'_4
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
s✝ : Set α
a✝ : α
h : ∀ (b : α), b ∈ s✝ → a✝ ≤ b
⊢ a✝ ≤ InfSet.sInf s✝
[PROOFSTEP]
simpa [eq_le, eq_sInf] using h
[GOAL]
case refine'_5
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
⊢ ∀ (x : α), x ≤ ⊤
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
x✝ : α
⊢ x✝ ≤ ⊤
[PROOFSTEP]
simp [eq_le, eq_top]
[GOAL]
case refine'_6
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
⊢ ∀ (x : α), ⊥ ≤ x
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : Lattice α := Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf
x✝ : α
⊢ ⊥ ≤ x✝
[PROOFSTEP]
simp [eq_le, eq_bot]
[GOAL]
α : Type u
c : Frame α
le : α → α → Prop
⊢ LE α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Sup α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
⊢ Inf α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
⊢ SupSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Frame α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : CompleteLattice α :=
  CompleteLattice.copy Frame.toCompleteLattice le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sSup eq_sSup sInf
    eq_sInf
a : α
s : Set α
⊢ a ⊓ SupSet.sSup s ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
simp [eq_le, eq_sup, eq_inf, eq_sSup, @Order.Frame.inf_sSup_le_iSup_inf α _ a s]
[GOAL]
α : Type u
c : Coframe α
le : α → α → Prop
⊢ LE α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Sup α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
⊢ Inf α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
⊢ SupSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : Coframe α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
src✝ : CompleteLattice α :=
  CompleteLattice.copy Coframe.toCompleteLattice le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sSup eq_sSup sInf
    eq_sInf
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b ≤ a ⊔ InfSet.sInf s
[PROOFSTEP]
simp [eq_le, eq_sup, eq_inf, eq_sInf, @Order.Coframe.iInf_sup_le_sup_sInf α _ a s]
[GOAL]
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
⊢ LE α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Sup α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
⊢ Inf α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
⊢ SupSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : CompleteDistribLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
⊢ LE α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
⊢ Sup α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
⊢ Inf α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
⊢ SupSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
⊢ InfSet α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ConditionallyCompleteLattice α
[PROOFSTEP]
refine' { le := le, sup := sup, inf := inf, sSup := sSup, sInf := sInf .. }
[GOAL]
case refine'_1
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ α → α → Prop
[PROOFSTEP]
intro a b
[GOAL]
case refine'_1
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a b : α
⊢ Prop
[PROOFSTEP]
exact le a b ∧ ¬le b a
[GOAL]
case refine'_2
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a : α), a ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ : α
⊢ a✝ ≤ a✝
[PROOFSTEP]
simp [eq_le]
[GOAL]
case refine'_3
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
intro _ _ _ hab hbc
[GOAL]
case refine'_3
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ c✝ : α
hab : a✝ ≤ b✝
hbc : b✝ ≤ c✝
⊢ a✝ ≤ c✝
[PROOFSTEP]
rw [eq_le] at hab hbc ⊢
[GOAL]
case refine'_3
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ c✝ : α
hab : a✝ ≤ b✝
hbc : b✝ ≤ c✝
⊢ a✝ ≤ c✝
[PROOFSTEP]
exact le_trans hab hbc
[GOAL]
case refine'_4
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ : α
⊢ a✝ < b✝ ↔ a✝ ≤ b✝ ∧ ¬b✝ ≤ a✝
[PROOFSTEP]
simp [eq_le]
[GOAL]
case refine'_5
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a b : α), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
intro _ _ hab hba
[GOAL]
case refine'_5
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ : α
hab : a✝ ≤ b✝
hba : b✝ ≤ a✝
⊢ a✝ = b✝
[PROOFSTEP]
simp_rw [eq_le] at hab hba
[GOAL]
case refine'_5
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ : α
hab : a✝ ≤ b✝
hba : b✝ ≤ a✝
⊢ a✝ = b✝
[PROOFSTEP]
exact le_antisymm hab hba
[GOAL]
case refine'_6
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a b : α), a ≤ a ⊔ b
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ : α
⊢ a✝ ≤ a✝ ⊔ b✝
[PROOFSTEP]
simp [eq_le, eq_sup]
[GOAL]
case refine'_7
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a b : α), b ≤ a ⊔ b
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ : α
⊢ b✝ ≤ a✝ ⊔ b✝
[PROOFSTEP]
simp [eq_le, eq_sup]
[GOAL]
case refine'_8
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
[PROOFSTEP]
intro _ _ _ hac hbc
[GOAL]
case refine'_8
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ c✝ : α
hac : a✝ ≤ c✝
hbc : b✝ ≤ c✝
⊢ a✝ ⊔ b✝ ≤ c✝
[PROOFSTEP]
simp_rw [eq_le] at hac hbc ⊢
[GOAL]
case refine'_8
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ c✝ : α
hac : a✝ ≤ c✝
hbc : b✝ ≤ c✝
⊢ sup a✝ b✝ ≤ c✝
[PROOFSTEP]
simp [eq_sup, hac, hbc]
[GOAL]
case refine'_9
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a b : α), a ⊓ b ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ : α
⊢ a✝ ⊓ b✝ ≤ a✝
[PROOFSTEP]
simp [eq_le, eq_inf]
[GOAL]
case refine'_10
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a b : α), a ⊓ b ≤ b
[PROOFSTEP]
intros
[GOAL]
case refine'_10
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ : α
⊢ a✝ ⊓ b✝ ≤ b✝
[PROOFSTEP]
simp [eq_le, eq_inf]
[GOAL]
case refine'_11
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
[PROOFSTEP]
intro _ _ _ hac hbc
[GOAL]
case refine'_11
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ c✝ : α
hac : a✝ ≤ b✝
hbc : a✝ ≤ c✝
⊢ a✝ ≤ b✝ ⊓ c✝
[PROOFSTEP]
simp_rw [eq_le] at hac hbc ⊢
[GOAL]
case refine'_11
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ b✝ c✝ : α
hac : a✝ ≤ b✝
hbc : a✝ ≤ c✝
⊢ a✝ ≤ inf b✝ c✝
[PROOFSTEP]
simp [eq_inf, hac, hbc]
[GOAL]
case refine'_12
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ SupSet.sSup s
[PROOFSTEP]
intro _ _ hb h
[GOAL]
case refine'_12
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
s✝ : Set α
a✝ : α
hb : BddAbove s✝
h : a✝ ∈ s✝
⊢ a✝ ≤ SupSet.sSup s✝
[PROOFSTEP]
subst_vars
[GOAL]
case refine'_12
α : Type u
c : ConditionallyCompleteLattice α
s✝ : Set α
a✝ : α
h : a✝ ∈ s✝
hb : BddAbove s✝
⊢ a✝ ≤ sSup s✝
[PROOFSTEP]
exact le_csSup _ _ hb h
[GOAL]
case refine'_13
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ upperBounds s → SupSet.sSup s ≤ a
[PROOFSTEP]
intro _ _ hb h
[GOAL]
case refine'_13
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
s✝ : Set α
a✝ : α
hb : Set.Nonempty s✝
h : a✝ ∈ upperBounds s✝
⊢ SupSet.sSup s✝ ≤ a✝
[PROOFSTEP]
subst_vars
[GOAL]
case refine'_13
α : Type u
c : ConditionallyCompleteLattice α
s✝ : Set α
a✝ : α
hb : Set.Nonempty s✝
h : a✝ ∈ upperBounds s✝
⊢ sSup s✝ ≤ a✝
[PROOFSTEP]
exact csSup_le _ _ hb h
[GOAL]
case refine'_14
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (s : Set α) (a : α), BddBelow s → a ∈ s → InfSet.sInf s ≤ a
[PROOFSTEP]
intro _ _ hb h
[GOAL]
case refine'_14
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
s✝ : Set α
a✝ : α
hb : BddBelow s✝
h : a✝ ∈ s✝
⊢ InfSet.sInf s✝ ≤ a✝
[PROOFSTEP]
subst_vars
[GOAL]
case refine'_14
α : Type u
c : ConditionallyCompleteLattice α
s✝ : Set α
a✝ : α
h : a✝ ∈ s✝
hb : BddBelow s✝
⊢ sInf s✝ ≤ a✝
[PROOFSTEP]
exact csInf_le _ _ hb h
[GOAL]
case refine'_15
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (s : Set α) (a : α), Set.Nonempty s → a ∈ lowerBounds s → a ≤ InfSet.sInf s
[PROOFSTEP]
intro _ _ hb h
[GOAL]
case refine'_15
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = Sup.sup
inf : α → α → α
eq_inf : inf = Inf.inf
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
s✝ : Set α
a✝ : α
hb : Set.Nonempty s✝
h : a✝ ∈ lowerBounds s✝
⊢ a✝ ≤ InfSet.sInf s✝
[PROOFSTEP]
subst_vars
[GOAL]
case refine'_15
α : Type u
c : ConditionallyCompleteLattice α
s✝ : Set α
a✝ : α
hb : Set.Nonempty s✝
h : a✝ ∈ lowerBounds s✝
⊢ a✝ ≤ sInf s✝
[PROOFSTEP]
exact le_csInf _ _ hb h


[GOAL]
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderTop α
hs : Set.Finite s
⊢ Set.Finite ↑(upperClosure s)
[PROOFSTEP]
rw [coe_upperClosure]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderTop α
hs : Set.Finite s
⊢ Set.Finite (⋃ (a : α) (_ : a ∈ s), Ici a)
[PROOFSTEP]
exact hs.biUnion fun _ _ => finite_Ici _
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : Set.Finite s
⊢ Set.Finite ↑(lowerClosure s)
[PROOFSTEP]
rw [coe_lowerClosure]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : Set.Finite s
⊢ Set.Finite (⋃ (a : α) (_ : a ∈ s), Iic a)
[PROOFSTEP]
exact hs.biUnion fun _ _ => finite_Iic _


[GOAL]
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
by_cases ha_zero : a = 0
[GOAL]
case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : a = 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
simp_rw [ha_zero, zero_mul, ← ENNReal.bot_eq_zero]
[GOAL]
case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : a = 0
⊢ limsup (fun x => ⊥) f = ⊥
[PROOFSTEP]
exact limsup_const_bot
[GOAL]
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
let g := fun x : ℝ≥0∞ => a * x
[GOAL]
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
have hg_bij : Function.Bijective g :=
  Function.bijective_iff_has_inverse.mpr
    ⟨fun x => a⁻¹ * x,
      ⟨fun x => by simp [← mul_assoc, ENNReal.inv_mul_cancel ha_zero ha_top], fun x => by
        simp [← mul_assoc, ENNReal.mul_inv_cancel ha_zero ha_top]⟩⟩
[GOAL]
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
x : ℝ≥0∞
⊢ (fun x => a⁻¹ * x) (g x) = x
[PROOFSTEP]
simp [← mul_assoc, ENNReal.inv_mul_cancel ha_zero ha_top]
[GOAL]
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
x : ℝ≥0∞
⊢ g ((fun x => a⁻¹ * x) x) = x
[PROOFSTEP]
simp [← mul_assoc, ENNReal.mul_inv_cancel ha_zero ha_top]
[GOAL]
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
have hg_mono : StrictMono g :=
  Monotone.strictMono_of_injective (fun _ _ _ => by rwa [mul_le_mul_left ha_zero ha_top]) hg_bij.1
[GOAL]
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
x✝² x✝¹ : ℝ≥0∞
x✝ : x✝² ≤ x✝¹
⊢ g x✝² ≤ g x✝¹
[PROOFSTEP]
rwa [mul_le_mul_left ha_zero ha_top]
[GOAL]
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
hg_mono : StrictMono g
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
let g_iso := StrictMono.orderIsoOfSurjective g hg_mono hg_bij.2
[GOAL]
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
hg_mono : StrictMono g
g_iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective g hg_mono (_ : Function.Surjective g)
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
exact (OrderIso.limsup_apply g_iso).symm
[GOAL]
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
by_cases ha_top : a ≠ ⊤
[GOAL]
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
exact limsup_const_mul_of_ne_top ha_top
[GOAL]
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : ¬a ≠ ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
push_neg at ha_top
[GOAL]
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
by_cases hu : u =ᶠ[f] 0
[GOAL]
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : u =ᶠ[f] 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
have hau : (a * u ·) =ᶠ[f] 0 := hu.mono fun x hx => by simp [hx]
[GOAL]
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : u =ᶠ[f] 0
x : α
hx : u x = OfNat.ofNat 0 x
⊢ (fun x => a * u x) x = OfNat.ofNat 0 x
[PROOFSTEP]
simp [hx]
[GOAL]
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : u =ᶠ[f] 0
hau : (fun x => a * u x) =ᶠ[f] 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
simp only [limsup_congr hu, limsup_congr hau, Pi.zero_apply, ← ENNReal.bot_eq_zero, limsup_const_bot]
[GOAL]
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : u =ᶠ[f] 0
hau : (fun x => a * u x) =ᶠ[f] 0
⊢ ⊥ = a * ⊥
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
have hu_mul : ∃ᶠ x : α in f, ⊤ ≤ ite (u x = 0) (0 : ℝ≥0∞) ⊤ :=
  by
  rw [EventuallyEq, not_eventually] at hu
  refine' hu.mono fun x hx => _
  rw [Pi.zero_apply] at hx
  simp [hx]
[GOAL]
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
⊢ ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
[PROOFSTEP]
rw [EventuallyEq, not_eventually] at hu
[GOAL]
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ∃ᶠ (x : α) in f, ¬u x = OfNat.ofNat 0 x
⊢ ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
[PROOFSTEP]
refine' hu.mono fun x hx => _
[GOAL]
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ∃ᶠ (x : α) in f, ¬u x = OfNat.ofNat 0 x
x : α
hx : ¬u x = OfNat.ofNat 0 x
⊢ ⊤ ≤ if u x = 0 then 0 else ⊤
[PROOFSTEP]
rw [Pi.zero_apply] at hx
[GOAL]
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ∃ᶠ (x : α) in f, ¬u x = OfNat.ofNat 0 x
x : α
hx : ¬u x = 0
⊢ ⊤ ≤ if u x = 0 then 0 else ⊤
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
have h_top_le : (f.limsup fun x : α => ite (u x = 0) (0 : ℝ≥0∞) ⊤) = ⊤ :=
  eq_top_iff.mpr (le_limsup_of_frequently_le hu_mul)
[GOAL]
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
h_top_le : limsup (fun x => if u x = 0 then 0 else ⊤) f = ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
have hfu : f.limsup u ≠ 0 := mt limsup_eq_zero_iff.1 hu
[GOAL]
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
h_top_le : limsup (fun x => if u x = 0 then 0 else ⊤) f = ⊤
hfu : limsup u f ≠ 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
[PROOFSTEP]
simp only [ha_top, top_mul', hfu, h_top_le]
[GOAL]
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ limsup (u * v) f ≤ limsup (fun x => limsup u f * v x) f
[PROOFSTEP]
refine limsup_le_limsup ?_
[GOAL]
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ u * v ≤ᶠ[f] fun x => limsup u f * v x
[PROOFSTEP]
filter_upwards [@eventually_le_limsup _ f _ u] with x hx using mul_le_mul' hx le_rfl
[GOAL]
α : Type u_1
f✝ : Filter α
β : Type u_2
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ᶠ (a : α) in f, ∀ (b : β), u a b ≤ limsup (fun a' => u a' b) f
[PROOFSTEP]
rw [eventually_countable_forall]
[GOAL]
α : Type u_1
f✝ : Filter α
β : Type u_2
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun a' => u a' i) f
[PROOFSTEP]
exact fun b => ENNReal.eventually_le_limsup fun a => u a b


[GOAL]
n : ℕ
h : n ≠ 0
d m : ℕ
⊢ ((fun a => a + d) ∘ fun x => n • id x) m ≡ d [MOD n]
[PROOFSTEP]
simp [Nat.modEq_iff_dvd, ← sub_sub]
[GOAL]
d n : ℕ
h : d < n
⊢ ∃ᶠ (m : ℕ) in atTop, m % n = d
[PROOFSTEP]
simpa only [Nat.ModEq, mod_eq_of_lt h] using frequently_modEq h.ne_bot d
[GOAL]
⊢ ∃ᶠ (m : ℕ) in atTop, Even m
[PROOFSTEP]
simpa only [even_iff] using frequently_mod_eq zero_lt_two
[GOAL]
⊢ ∃ᶠ (m : ℕ) in atTop, Odd m
[PROOFSTEP]
simpa only [odd_iff] using frequently_mod_eq one_lt_two


[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y, y ∈ s ∧ ¬y ≤ x
[PROOFSTEP]
simp [BddAbove, upperBounds, Set.Nonempty]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
a b : α✝
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y, y ∈ s ∧ x < y
[PROOFSTEP]
simp only [not_bddAbove_iff', not_le]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ upperBounds s
[PROOFSTEP]
rw [h.upperBounds_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ Ici a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ lowerBounds s
[PROOFSTEP]
rw [h.lowerBounds_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
h : IsGLB s a
⊢ b ≤ a ↔ b ∈ Iic a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t✝ : Set α
a✝ b a : α
s t : Set α
⊢ IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a
[PROOFSTEP]
simp [IsLeast, lowerBounds_union, or_and_right, and_comm (a := a ∈ t), and_assoc]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
⊢ BddAbove s → BddAbove t → BddAbove (s ∪ t)
[PROOFSTEP]
rintro ⟨bs, hs⟩ ⟨bt, ht⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ BddAbove (s ∪ t)
[PROOFSTEP]
use bs ⊔ bt
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ bs ⊔ bt ∈ upperBounds (s ∪ t)
[PROOFSTEP]
rw [upperBounds_union]
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ bs ⊔ bt ∈ upperBounds s ∩ upperBounds t
[PROOFSTEP]
exact ⟨upperBounds_mono_mem le_sup_left hs, upperBounds_mono_mem le_sup_right ht⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
⊢ min a b ∈ s ∪ t
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : a ≤ b
⊢ min a b ∈ s ∪ t
[PROOFSTEP]
simp [h, ha.1, hb.1]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : b ≤ a
⊢ min a b ∈ s ∪ t
[PROOFSTEP]
simp [h, ha.1, hb.1]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsGreatest s a
hb : IsGreatest t b
⊢ max a b ∈ s ∪ t
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsGreatest s a
hb : IsGreatest t b
h : a ≤ b
⊢ max a b ∈ s ∪ t
[PROOFSTEP]
simp [h, ha.1, hb.1]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsGreatest s a
hb : IsGreatest t b
h : b ≤ a
⊢ max a b ∈ s ∪ t
[PROOFSTEP]
simp [h, ha.1, hb.1]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a b : α
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ (y : γ), y ∈ s → y ≤ x
[PROOFSTEP]
rw [bddAbove_def, exists_ge_and_iff_exists]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a b : α
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone fun x => ∀ (y : γ), y ∈ s → y ≤ x
[PROOFSTEP]
exact Monotone.ball fun x _ => monotone_le
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
⊢ j = i ∨ Iio i = Iic j
[PROOFSTEP]
cases' eq_or_lt_of_le (lub_Iio_le i hj) with hj_eq_i hj_lt_i
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_eq_i : j = i
⊢ j = i ∨ Iio i = Iic j
[PROOFSTEP]
exact Or.inl hj_eq_i
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j
[PROOFSTEP]
right
[GOAL]
case inr.h
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ Iio i = Iic j
[PROOFSTEP]
exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
⊢ ∃ j, IsLUB (Iio i) j
[PROOFSTEP]
by_cases h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∃ j, IsLUB (Iio i) j
[PROOFSTEP]
obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt
[GOAL]
case pos.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i j : γ
hj_ub : j ∈ upperBounds (Iio i)
hj_lt_i : j < i
⊢ ∃ j, IsLUB (Iio i) j
[PROOFSTEP]
exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∃ j, IsLUB (Iio i) j
[PROOFSTEP]
refine' ⟨i, fun j hj => le_of_lt hj, _⟩
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ i ∈ lowerBounds (upperBounds (Iio i))
[PROOFSTEP]
rw [mem_lowerBounds]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
[PROOFSTEP]
by_contra h
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ¬∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
⊢ False
[PROOFSTEP]
refine' h_exists_lt _
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ¬∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
⊢ ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ∃ x, x ∈ upperBounds (Iio i) ∧ x < i
⊢ ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
[PROOFSTEP]
exact h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
⊢ x ≤ a
[PROOFSTEP]
cases' eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ h₂
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₁ : a = x ⊔ a
⊢ x ≤ a
[PROOFSTEP]
exact h₁.symm ▸ le_sup_left
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
⊢ x ≤ a
[PROOFSTEP]
obtain ⟨y, lty, ylt⟩ := exists_between h₂
[GOAL]
case inr.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ a
[PROOFSTEP]
apply (not_lt_of_le (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ b
[PROOFSTEP]
obtain ⟨u, au, ub⟩ := exists_between h
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
u : γ
au : a < u
ub : u < b
⊢ x ≤ b
[PROOFSTEP]
apply (hx ⟨au, ub⟩).trans ub.le
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeInf γ
inst✝ : DenselyOrdered γ
a b : γ
hab : a < b
⊢ IsLUB (Ioo a b) b
[PROOFSTEP]
simpa only [dual_Ioo] using isGLB_Ioo hab.dual
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a✝ b✝ : α
inst✝¹ : SemilatticeInf γ
inst✝ : DenselyOrdered γ
a b : γ
hab : a < b
⊢ IsLUB (Ico a b) b
[PROOFSTEP]
simpa only [dual_Ioc] using isGLB_Ioc hab.dual
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b
[PROOFSTEP]
simp [Ici_inter_Iic.symm, subset_inter_iff, bddBelow_iff_subset_Ici, bddAbove_iff_subset_Iic, exists_and_left,
  exists_and_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ IsGreatest univ a ↔ IsTop a
[PROOFSTEP]
simp [IsGreatest, mem_upperBounds, IsTop]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝³ : Preorder α
inst✝² : Preorder β
s t : Set α
a b : α
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ upperBounds univ = {⊤}
[PROOFSTEP]
rw [isGreatest_univ.upperBounds_eq, Ici_top]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : NoMaxOrder α
⊢ ¬BddAbove univ
[PROOFSTEP]
simp [BddAbove]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ upperBounds ∅ = univ
[PROOFSTEP]
simp only [upperBounds, eq_univ_iff_forall, mem_setOf_eq, ball_empty_iff, forall_true_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : Nonempty α
⊢ BddAbove ∅
[PROOFSTEP]
simp only [BddAbove, upperBounds_empty, univ_nonempty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : Nonempty α
⊢ BddBelow ∅
[PROOFSTEP]
simp only [BddBelow, lowerBounds_empty, univ_nonempty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ IsGLB ∅ a ↔ IsTop a
[PROOFSTEP]
simp [IsGLB]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ upperBounds s
[PROOFSTEP]
rw [h, upperBounds_empty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ univ
[PROOFSTEP]
exact mem_univ _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b : α
inst✝ : SemilatticeSup γ
a : γ
s : Set γ
⊢ BddAbove (insert a s) ↔ BddAbove s
[PROOFSTEP]
simp only [insert_eq, bddAbove_union, bddAbove_singleton, true_and_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b : α
inst✝ : SemilatticeInf γ
a : γ
s : Set γ
⊢ BddBelow (insert a s) ↔ BddBelow s
[PROOFSTEP]
simp only [insert_eq, bddBelow_union, bddBelow_singleton, true_and_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB (insert a s) (a ⊔ b)
[PROOFSTEP]
rw [insert_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB ({a} ∪ s) (a ⊔ b)
[PROOFSTEP]
exact isLUB_singleton.union hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : SemilatticeInf γ
a b : γ
s : Set γ
hs : IsGLB s b
⊢ IsGLB (insert a s) (a ⊓ b)
[PROOFSTEP]
rw [insert_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : SemilatticeInf γ
a b : γ
s : Set γ
hs : IsGLB s b
⊢ IsGLB ({a} ∪ s) (a ⊓ b)
[PROOFSTEP]
exact isGLB_singleton.union hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest (insert a s) (max a b)
[PROOFSTEP]
rw [insert_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest ({a} ∪ s) (max a b)
[PROOFSTEP]
exact isGreatest_singleton.union hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsLeast s b
⊢ IsLeast (insert a s) (min a b)
[PROOFSTEP]
rw [insert_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsLeast s b
⊢ IsLeast ({a} ∪ s) (min a b)
[PROOFSTEP]
exact isLeast_singleton.union hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
a✝ b a : α
s : Set α
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s
[PROOFSTEP]
rw [insert_eq, upperBounds_union, upperBounds_singleton]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
a✝ b a : α
s : Set α
⊢ lowerBounds (insert a s) = Iic a ∩ lowerBounds s
[PROOFSTEP]
rw [insert_eq, lowerBounds_union, lowerBounds_singleton]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ b < a ↔ ∃ c, c ∈ s ∧ b < c
[PROOFSTEP]
simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
a : α
Hst✝ Hst : s ⊆ t
⊢ f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
a✝ : α
Hst✝ Hst : s ⊆ t
a : α
ha : a ∈ upperBounds s ∩ t
⊢ f a ∈ upperBounds (f '' s)
[PROOFSTEP]
exact Hf.mem_upperBounds_image Hst ha.1 ha.2
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
Hf : Monotone f
a : α
s : Set α
⊢ f '' upperBounds s ⊆ upperBounds (f '' s)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
Hf : Monotone f
a✝ : α
s : Set α
a : α
ha : a ∈ upperBounds s
⊢ f a ∈ upperBounds (f '' s)
[PROOFSTEP]
exact Hf.mem_upperBounds_image ha
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ upperBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
[PROOFSTEP]
exact mem_upperBounds_image2 h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ lowerBounds t
⊢ f a b ∈ lowerBounds (image2 f s t)
[PROOFSTEP]
exact mem_lowerBounds_image2 h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddAbove s → BddAbove t → BddAbove (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddBelow s → BddBelow t → BddBelow (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddBelow (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_lowerBounds_image2 h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
b : β
ha : a ∈ upperBounds s
hb : b ∈ lowerBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
[PROOFSTEP]
exact mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ lowerBounds (image2 f s t)
[PROOFSTEP]
exact mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddAbove s → BddBelow t → BddAbove (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddBelow s → BddAbove t → BddBelow (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddBelow (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ lowerBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
[PROOFSTEP]
exact mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
b : β
ha : a ∈ upperBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ lowerBounds (image2 f s t)
[PROOFSTEP]
exact mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddAbove s → BddAbove t → BddBelow (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddBelow (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
[PROOFSTEP]
exact mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ upperBounds s
hb : b ∈ lowerBounds t
⊢ f a b ∈ lowerBounds (image2 f s t)
[PROOFSTEP]
exact mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddBelow s → BddAbove t → BddAbove (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddAbove s → BddBelow t → BddBelow (Set.image2 f s t)
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddBelow (Set.image2 f s t)
[PROOFSTEP]
exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ BddAbove (range F) ↔ ∀ (a : α), BddAbove (range fun i => F i a)
[PROOFSTEP]
simp only [bddAbove_pi, ← range_comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ (∀ (a : α), BddAbove (range (eval a ∘ F))) ↔ ∀ (a : α), BddAbove (range fun i => F i a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval a '' s) (f a)
[PROOFSTEP]
classical
refine' ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => _⟩, fun H => ⟨_, _⟩⟩
· suffices h : Function.update f a b ∈ upperBounds s from Function.update_same a b f ▸ H.2 h a
  refine' fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
· exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
· exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval a '' s) (f a)
[PROOFSTEP]
refine' ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => _⟩, fun H => ⟨_, _⟩⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ f a ≤ b
[PROOFSTEP]
suffices h : Function.update f a b ∈ upperBounds s from Function.update_same a b f ▸ H.2 h a
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ update f a b ∈ upperBounds s
[PROOFSTEP]
refine' fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ upperBounds s
[PROOFSTEP]
exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)
[PROOFSTEP]
exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
[PROOFSTEP]
refine'
  ⟨fun H =>
    ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => _⟩, ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => _⟩⟩,
    fun H => ⟨_, _⟩⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ p.fst ≤ a
[PROOFSTEP]
suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ (a, p.snd) ∈ upperBounds s
[PROOFSTEP]
exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ p.snd ≤ a
[PROOFSTEP]
suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ (p.fst, a) ∈ upperBounds s
[PROOFSTEP]
exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
[GOAL]
case refine'_3
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
⊢ p ∈ upperBounds s
[PROOFSTEP]
exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
[GOAL]
case refine'_4
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
⊢ p ∈ lowerBounds (upperBounds s)
[PROOFSTEP]
exact fun q hq => ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq, H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩


[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ univ ∈ {s | Set.Finite sᶜ}
[PROOFSTEP]
simp only [compl_univ, finite_empty, mem_setOf_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
x✝ y✝ : Set α
hs : x✝ ∈ {s | Set.Finite sᶜ}
ht : y✝ ∈ {s | Set.Finite sᶜ}
⊢ x✝ ∩ y✝ ∈ {s | Set.Finite sᶜ}
[PROOFSTEP]
simpa only [compl_inter, mem_setOf_eq] using hs.union ht
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ cofinite = ⊥ ↔ Finite α
[PROOFSTEP]
simp [← empty_mem_iff_bot, finite_univ_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in cofinite, p x) ↔ Set.Infinite {x | p x}
[PROOFSTEP]
simp only [Filter.Frequently, Filter.Eventually, mem_cofinite, compl_setOf, not_not, Set.Infinite]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l
[PROOFSTEP]
refine' ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => _⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : Set.Finite sᶜ
⊢ s ∈ l
[PROOFSTEP]
rw [← compl_compl s, ← biUnion_of_singleton sᶜ, compl_iUnion₂, Filter.biInter_mem hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : Set.Finite sᶜ
⊢ ∀ (i : α), i ∈ sᶜ → {i}ᶜ ∈ l
[PROOFSTEP]
exact fun x _ => h x
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
s : Set (α × β)
⊢ sᶜ ∈ Filter.coprod cofinite cofinite ↔ sᶜ ∈ cofinite
[PROOFSTEP]
simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
l : Filter α✝
α : ι → Type u_4
inst✝ : Finite ι
s : Set ((i : ι) → α i)
⊢ (sᶜ ∈ Filter.coprodᵢ fun i => cofinite) ↔ sᶜ ∈ cofinite
[PROOFSTEP]
simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ Disjoint cofinite l ↔ ∃ s, s ∈ l ∧ Set.Finite s
[PROOFSTEP]
simp only [hasBasis_cofinite.disjoint_iff l.basis_sets, id, disjoint_compl_left_iff_subset]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ (∃ i, Set.Finite i ∧ ∃ i', i' ∈ l ∧ i' ⊆ i) ↔ ∃ s, s ∈ l ∧ Set.Finite s
[PROOFSTEP]
exact ⟨fun ⟨s, hs, t, ht, hts⟩ => ⟨t, ht, hs.subset hts⟩, fun ⟨s, hs, hsf⟩ => ⟨s, hsf, s, hs, Subset.rfl⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : IsCountablyGenerated l
h : cofinite ≤ l
⊢ Set.Countable (⋂₀ l.sets)ᶜ
[PROOFSTEP]
rcases exists_antitone_basis l with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : IsCountablyGenerated l
h : cofinite ≤ l
s : ℕ → Set α
hs : HasAntitoneBasis l s
⊢ Set.Countable (⋂₀ l.sets)ᶜ
[PROOFSTEP]
simp only [hs.sInter_sets, iInter_true, compl_iInter]
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : IsCountablyGenerated l
h : cofinite ≤ l
s : ℕ → Set α
hs : HasAntitoneBasis l s
⊢ Set.Countable (⋃ (i : ℕ), (s i)ᶜ)
[PROOFSTEP]
exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
f : α → β
l : Filter β
inst✝ : IsCountablyGenerated l
h : Tendsto f cofinite l
⊢ Set.Countable (f ⁻¹' ⋂₀ l.sets)ᶜ
[PROOFSTEP]
erw [preimage_sInter, ← sInter_comap_sets]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
f : α → β
l : Filter β
inst✝ : IsCountablyGenerated l
h : Tendsto f cofinite l
⊢ Set.Countable (⋂₀ (comap f l).sets)ᶜ
[PROOFSTEP]
exact countable_compl_sInter_sets h.le_comap
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ cofinite = atTop
[PROOFSTEP]
refine' le_antisymm _ atTop_le_cofinite
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
⊢ cofinite ≤ atTop
[PROOFSTEP]
refine' atTop_basis.ge_iff.2 fun N _ => _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
N : ℕ
x✝ : True
⊢ Ici N ∈ cofinite
[PROOFSTEP]
simpa only [mem_cofinite, compl_Ici] using finite_lt_nat N
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
l : Filter α
p : ℕ → Prop
⊢ (∃ᶠ (n : ℕ) in atTop, p n) ↔ Set.Infinite {n | p n}
[PROOFSTEP]
rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
rcases em (∃ y ∈ s, ∃ x, f y < x) with (⟨y, hys, x, hx⟩ | not_all_top)
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
have : {y | ¬x ≤ f y}.Finite := Filter.eventually_cofinite.mp (tendsto_atTop.1 hf x)
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite {y | ¬x ≤ f y}
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
simp only [not_le] at this
[GOAL]
case inl.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite {y | f y < x}
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
obtain ⟨a₀, ⟨ha₀ : f a₀ < x, ha₀s⟩, others_bigger⟩ := exists_min_image _ f (this.inter_of_left s) ⟨y, hx, hys⟩
[GOAL]
case inl.intro.intro.intro.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite {y | f y < x}
a₀ : α
others_bigger : ∀ (b : α), b ∈ {y | f y < x} ∩ s → f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
refine' ⟨a₀, ha₀s, fun a has => (lt_or_le (f a) x).elim _ (le_trans ha₀.le)⟩
[GOAL]
case inl.intro.intro.intro.intro.intro.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite {y | f y < x}
a₀ : α
others_bigger : ∀ (b : α), b ∈ {y | f y < x} ∩ s → f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
a : α
has : a ∈ s
⊢ f a < x → f a₀ ≤ f a
[PROOFSTEP]
exact fun h => others_bigger a ⟨h, has⟩
[GOAL]
case inr
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ¬∃ y, y ∈ s ∧ ∃ x, f y < x
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
push_neg at not_all_top
[GOAL]
case inr
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : Set.Nonempty s
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ∀ (y : α), y ∈ s → ∀ (x : β), x ≤ f y
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
obtain ⟨a₀, ha₀s⟩ := hs
[GOAL]
case inr.intro
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
l : Filter α✝
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
f : α → β
hf : Tendsto f cofinite atTop
not_all_top : ∀ (y : α), y ∈ s → ∀ (x : β), x ≤ f y
a₀ : α
ha₀s : a₀ ∈ s
⊢ ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → f a₀ ≤ f a
[PROOFSTEP]
exact ⟨a₀, ha₀s, fun a ha => not_all_top a ha (f a₀)⟩


[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One M
s t : Set α
f g : α → M
a : α
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : x ∈ s
⊢ mulIndicator s f x = mulIndicator t g x
[PROOFSTEP]
simp only [*, hst.1 hxs, mulIndicator_of_mem]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One M
s t : Set α
f g : α → M
a : α
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : ¬x ∈ s
⊢ mulIndicator s f x = mulIndicator t g x
[PROOFSTEP]
simp only [mulIndicator_of_not_mem, hxs, mt hst.2 hxs]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun x => mulIndicator (⋃ (i : ι), s i) f a
[PROOFSTEP]
classical exact hs.piecewise_eventually_eq_iUnion f 1 a
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun x => mulIndicator (⋃ (i : ι), s i) f a
[PROOFSTEP]
exact hs.piecewise_eventually_eq_iUnion f 1 a
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun x => mulIndicator (⋂ (i : ι), s i) f a
[PROOFSTEP]
classical exact hs.piecewise_eventually_eq_iInter f 1 a
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun x => mulIndicator (⋂ (i : ι), s i) f a
[PROOFSTEP]
exact hs.piecewise_eventually_eq_iInter f 1 a
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ (fun n => mulIndicator (⋃ (i : ι) (_ : i ∈ n), s i) f a) =ᶠ[atTop] fun x => mulIndicator (iUnion s) f a
[PROOFSTEP]
rw [iUnion_eq_iUnion_finset s]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ (fun n => mulIndicator (⋃ (i : ι) (_ : i ∈ n), s i) f a) =ᶠ[atTop] fun x =>
    mulIndicator (⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), s i) f a
[PROOFSTEP]
apply Monotone.mulIndicator_eventuallyEq_iUnion
[GOAL]
case hs
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ Monotone fun i => ⋃ (i_1 : ι) (_ : i_1 ∈ i), s i_1
[PROOFSTEP]
exact fun _ _ ↦ biUnion_subset_biUnion_left
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 1
⊢ mulIndicator s 1 =ᶠ[l] 1
[PROOFSTEP]
rw [mulIndicator_one']
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : mulIndicator s f =ᶠ[l] mulIndicator t f
⊢ s =ᶠ[l] t
[PROOFSTEP]
have : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s := fun {s} ↦
  by
  rw [mulSupport_mulIndicator]
  exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : mulIndicator s✝ f =ᶠ[l] mulIndicator t f
s : Set α
⊢ Function.mulSupport (mulIndicator s f) =ᶠ[l] s
[PROOFSTEP]
rw [mulSupport_mulIndicator]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : mulIndicator s✝ f =ᶠ[l] mulIndicator t f
s : Set α
⊢ s ∩ Function.mulSupport f =ᶠ[l] s
[PROOFSTEP]
exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : mulIndicator s f =ᶠ[l] mulIndicator t f
this : ∀ {s : Set α}, Function.mulSupport (mulIndicator s f) =ᶠ[l] s
⊢ s =ᶠ[l] t
[PROOFSTEP]
exact this.symm.trans <| h.mulSupport.trans this