[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
