Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Johan Commelin

! This file was ported from Lean 3 source module order.copy
! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.ConditionallyCompleteLattice.Basic

/-!
# Tooling to make copies of lattice structures

Sometimes it is useful to make a copy of a lattice structure
where one replaces the data parts with provably equal definitions
that have better definitional properties.
-/

open Order

universe u

variable {α: Type uα : Type u: Type (u+1)Type u}

--Porting note: mathlib3 proof uses `refine { top := top, bot := bot, .. }` but this does not work
-- anymore
/-- A function to create a provable equal copy of a bounded order
with possibly different definitional equalities. -/
def BoundedOrder.copy: {α : Type u} →
{h h' : LE α} →
(c : BoundedOrder α) → (top : α) → top = ⊤ → (bot : α) → bot = ⊥ → (∀ (x y : α), x ≤ y ↔ x ≤ y) → BoundedOrder αBoundedOrder.copy {h: LE αh : LE: Type ?u.6 → Type ?u.6LE α: Type uα} {h': LE αh' : LE: Type ?u.9 → Type ?u.9LE α: Type uα} (c: BoundedOrder αc : @BoundedOrder: (α : Type ?u.12) → [inst : LE α] → Type ?u.12BoundedOrder α: Type uα h': LE αh')
(top: αtop : α: Type uα) (eq_top: top = ⊤eq_top : top: αtop = (byGoals accomplished! 🐙 α: Type uh, h': LE αc: BoundedOrder αtop: αTop αinfer_instanceGoals accomplished! 🐙 : Top α).top: {α : Type ?u.22} → [self : Top α] → αtop)
(bot: αbot : α: Type uα) (eq_bot: bot = ⊥eq_bot : bot: αbot = (byGoals accomplished! 🐙 α: Type uh, h': LE αc: BoundedOrder αtop: αeq_top: top = ⊤bot: αBot αinfer_instanceGoals accomplished! 🐙 : Bot α).bot: {α : Type ?u.34} → [self : Bot α] → αbot)
(le_eq: ∀ (x y : α), x ≤ y ↔ x ≤ yle_eq : ∀ x: αx y: αy : α: Type uα, (@LE.le: {α : Type ?u.45} → [self : LE α] → α → α → PropLE.le α: Type uα h: LE αh) x: αx y: αy ↔ x: αx ≤ y: αy) : @BoundedOrder: (α : Type ?u.54) → [inst : LE α] → Type ?u.54BoundedOrder α: Type uα h: LE αh :=
@BoundedOrder.mk: {α : Type ?u.245} → [inst : LE α] → [toOrderTop : OrderTop α] → [toOrderBot : OrderBot α] → BoundedOrder αBoundedOrder.mk α: Type uα h: LE αh (@OrderTop.mk: {α : Type ?u.246} → [inst : LE α] → [toTop : Top α] → (∀ (a : α), a ≤ ⊤) → OrderTop αOrderTop.mk α: Type uα h: LE αh { top := top: αtop } (fun _: ?m.250_ ↦ byGoals accomplished! 🐙 α: Type uh, h': LE αc: BoundedOrder αtop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥le_eq: ∀ (x y : α), x ≤ y ↔ x ≤ yx✝: αx✝ ≤ ⊤simp [eq_top: top = ⊤eq_top, le_eq: ∀ (x y : α), x ≤ y ↔ x ≤ yle_eq]Goals accomplished! 🐙))
(@OrderBot.mk: {α : Type ?u.256} → [inst : LE α] → [toBot : Bot α] → (∀ (a : α), ⊥ ≤ a) → OrderBot αOrderBot.mk α: Type uα h: LE αh { bot := bot: αbot } (fun _: ?m.260_ ↦ byGoals accomplished! 🐙 α: Type uh, h': LE αc: BoundedOrder αtop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥le_eq: ∀ (x y : α), x ≤ y ↔ x ≤ yx✝: α⊥ ≤ x✝simp [eq_bot: bot = ⊥eq_bot, le_eq: ∀ (x y : α), x ≤ y ↔ x ≤ yle_eq]Goals accomplished! 🐙))
#align bounded_order.copy BoundedOrder.copy: {α : Type u} →
{h h' : LE α} →
(c : BoundedOrder α) → (top : α) → top = ⊤ → (bot : α) → bot = ⊥ → (∀ (x y : α), x ≤ y ↔ x ≤ y) → BoundedOrder αBoundedOrder.copy

--Porting note: original proof uses
-- `all_goals { abstract { subst_vars, casesI c, simp_rw le_eq, assumption } }`
/-- A function to create a provable equal copy of a lattice
with possibly different definitional equalities. -/
def Lattice.copy: {α : Type u} →
(c : Lattice α) →
(le : α → α → Prop) → le = LE.le → (sup : α → α → α) → sup = Sup.sup → (inf : α → α → α) → inf = Inf.inf → Lattice αLattice.copy (c: Lattice αc : Lattice: Type ?u.1090 → Type ?u.1090Lattice α: Type uα)
(le: α → α → Prople : α: Type uα → α: Type uα → Prop: TypeProp) (eq_le: le = LE.leeq_le : le: α → α → Prople = (byGoals accomplished! 🐙 α: Type uc: Lattice αle: α → α → PropLE αinfer_instanceGoals accomplished! 🐙 : LE α).le: {α : Type ?u.1105} → [self : LE α] → α → α → Prople)
(sup: α → α → αsup : α: Type uα → α: Type uα → α: Type uα) (eq_sup: sup = Sup.supeq_sup : sup: α → α → αsup = (byGoals accomplished! 🐙 α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αSup αinfer_instanceGoals accomplished! 🐙 : Sup α).sup: {α : Type ?u.1129} → [self : Sup α] → α → α → αsup)
(inf: α → α → αinf : α: Type uα → α: Type uα → α: Type uα) (eq_inf: inf = Inf.infeq_inf : inf: α → α → αinf = (byGoals accomplished! 🐙 α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αInf αinfer_instanceGoals accomplished! 🐙 : Inf α).inf: {α : Type ?u.1153} → [self : Inf α] → α → α → αinf) : Lattice: Type ?u.1165 → Type ?u.1165Lattice α: Type uα := byGoals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice αrefine' { le := le: α → α → Prople, sup := sup: α → α → αsup, inf := inf: α → α → αinf, lt := fun a: ?m.1313a b: ?m.1316b ↦ le: α → α → Prople a: ?m.1313a b: ?m.1316b ∧ ¬ le: α → α → Prople b: ?m.1316b a: ?m.1313a.. }α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_1∀ (a : α), a ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ cα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ cα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_1∀ (a : α), a ≤ a α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_1∀ (a : α), a ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ cα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ cα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ cintrosα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝: αrefine'_1a✝ ≤ a✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝: αrefine'_1a✝ ≤ a✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_1∀ (a : α), a ≤ asimp [eq_le: le = LE.leeq_le]Goals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ cα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1intro _: ?m.1300_ _: ?m.1300_ _: ?m.1300_ hab: a✝ ≤ b✝hab hbc: b✝ ≤ c✝hbcα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ crw [α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝eq_le: le = LE.leeq_leα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝]α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝ at hab: a✝ ≤ b✝hab hbc: b✝ ≤ c✝hbc ⊢α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ cexact le_trans: ∀ {α : Type ?u.1552} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_trans hab: a✝ ≤ b✝hab hbc: b✝ ≤ c✝hbcGoals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1introsα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_3a✝ < b✝ ↔ a✝ ≤ b✝ ∧ ¬b✝ ≤ a✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_3a✝ < b✝ ↔ a✝ ≤ b✝ ∧ ¬b✝ ≤ a✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ asimp [eq_le: le = LE.leeq_le]Goals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = b α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1intro _: ?m.1298_ _: ?m.1298_ hab: a✝ ≤ b✝hab hba: b✝ ≤ a✝hbaα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bsimp_rw [α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: le a✝ b✝hba: le b✝ a✝refine'_4a✝ = b✝eq_leα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝] at hab: a✝ ≤ b✝hab hba: le b✝ a✝hbaα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bexact le_antisymm: ∀ {α : Type ?u.2434} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm hab: a✝ ≤ b✝hab hba: b✝ ≤ a✝hbaGoals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ b α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1introsα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_5a✝ ≤ a✝ ⊔ b✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_5a✝ ≤ a✝ ⊔ b✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bsimp [eq_le: le = LE.leeq_le, eq_sup: sup = Sup.supeq_sup]Goals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ b α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1introsα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_6b✝ ≤ a✝ ⊔ b✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_6b✝ ≤ a✝ ⊔ b✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bsimp [eq_le: le = LE.leeq_le, eq_sup: sup = Sup.supeq_sup]Goals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1 α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1intro _: ?m.1288_ _: ?m.1288_ _: ?m.1288_ hac: a✝ ≤ c✝hac hbc: b✝ ≤ c✝hbcα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7a✝ ⊔ b✝ ≤ c✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7a✝ ⊔ b✝ ≤ c✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1simp_rw [α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: le a✝ c✝hbc: le b✝ c✝refine'_7le (sup a✝ b✝) c✝eq_le: le = LE.leeq_leα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7sup a✝ b✝ ≤ c✝] at hac: le a✝ c✝hac hbc: b✝ ≤ c✝hbc ⊢α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7sup a✝ b✝ ≤ c✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7sup a✝ b✝ ≤ c✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1simp [eq_sup: sup = Sup.supeq_sup, hac: a✝ ≤ c✝hac, hbc: b✝ ≤ c✝hbc]Goals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ a α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1introsα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_8a✝ ⊓ b✝ ≤ a✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_8a✝ ⊓ b✝ ≤ a✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ asimp [eq_le: le = LE.leeq_le, eq_inf: inf = Inf.infeq_inf]Goals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ b α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1introsα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_9a✝ ⊓ b✝ ≤ b✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_9a✝ ⊓ b✝ ≤ b✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bsimp [eq_le: le = LE.leeq_le, eq_inf: inf = Inf.infeq_inf]Goals accomplished! 🐙
α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infLattice α·α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1 α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1intro _: ?m.1286_ _: ?m.1286_ _: ?m.1286_ hac: a✝ ≤ b✝hac hbc: a✝ ≤ c✝hbcα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ b✝ ⊓ c✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ b✝ ⊓ c✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1simp_rw [α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: le a✝ b✝hbc: le a✝ c✝refine'_10le a✝ (inf b✝ c✝)eq_le: le = LE.leeq_leα: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ inf b✝ c✝] at hac: le a✝ b✝hac hbc: a✝ ≤ c✝hbc ⊢α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ inf b✝ c✝;α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ inf b✝ c✝ α: Type uc: Lattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1simp [eq_inf: inf = Inf.infeq_inf, hac: a✝ ≤ b✝hac, hbc: a✝ ≤ c✝hbc]Goals accomplished! 🐙
#align lattice.copy Lattice.copy: {α : Type u} →
(c : Lattice α) →
(le : α → α → Prop) → le = LE.le → (sup : α → α → α) → sup = Sup.sup → (inf : α → α → α) → inf = Inf.inf → Lattice αLattice.copy

--Porting note: original proof uses
-- `all_goals { abstract { subst_vars, casesI c, simp_rw le_eq, assumption } }`
/-- A function to create a provable equal copy of a distributive lattice
with possibly different definitional equalities. -/
def DistribLattice.copy: (c : DistribLattice α) →
(le : α → α → Prop) →
le = LE.le → (sup : α → α → α) → sup = Sup.sup → (inf : α → α → α) → inf = Inf.inf → DistribLattice αDistribLattice.copy (c: DistribLattice αc : DistribLattice: Type ?u.13050 → Type ?u.13050DistribLattice α: Type uα)
(le: α → α → Prople : α: Type uα → α: Type uα → Prop: TypeProp) (eq_le: le = LE.leeq_le : le: α → α → Prople = (byGoals accomplished! 🐙 α: Type uc: DistribLattice αle: α → α → PropLE αinfer_instanceGoals accomplished! 🐙 : LE α).le: {α : Type ?u.13065} → [self : LE α] → α → α → Prople)
(sup: α → α → αsup : α: Type uα → α: Type uα → α: Type uα) (eq_sup: sup = Sup.supeq_sup : sup: α → α → αsup = (byGoals accomplished! 🐙 α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αSup αinfer_instanceGoals accomplished! 🐙 : Sup α).sup: {α : Type ?u.13089} → [self : Sup α] → α → α → αsup)
(inf: α → α → αinf : α: Type uα → α: Type uα → α: Type uα) (eq_inf: inf = Inf.infeq_inf : inf: α → α → αinf = (byGoals accomplished! 🐙 α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αInf αinfer_instanceGoals accomplished! 🐙 : Inf α).inf: {α : Type ?u.13113} → [self : Inf α] → α → α → αinf) : DistribLattice: Type ?u.13125 → Type ?u.13125DistribLattice α: Type uα := byGoals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice αrefine' { le := le: α → α → Prople, sup := sup: α → α → αsup, inf := inf: α → α → αinf, lt := fun a: ?m.13495a b: ?m.13498b ↦ le: α → α → Prople a: ?m.13495a b: ?m.13498b ∧ ¬ le: α → α → Prople b: ?m.13498b a: ?m.13495a.. }α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_1∀ (a : α), a ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ cα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ cα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ cα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_1∀ (a : α), a ≤ a α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_1∀ (a : α), a ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ cα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ cα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ cα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintrosα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝: αrefine'_1a✝ ≤ a✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝: αrefine'_1a✝ ≤ a✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_1∀ (a : α), a ≤ asimp [eq_le: le = LE.leeq_le]Goals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ cα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintro _: ?m.13482_ _: ?m.13482_ _: ?m.13482_ hab: a✝ ≤ b✝hab hbc: b✝ ≤ c✝hbcα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ crw [α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝eq_le: le = LE.leeq_leα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝]α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝ at hab: a✝ ≤ b✝hab hbc: b✝ ≤ c✝hbc ⊢α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhab: a✝ ≤ b✝hbc: b✝ ≤ c✝refine'_2a✝ ≤ c✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_2∀ (a b c : α), a ≤ b → b ≤ c → a ≤ cexact le_trans: ∀ {α : Type ?u.13795} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ cle_trans hab: a✝ ≤ b✝hab hbc: b✝ ≤ c✝hbcGoals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintrosα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_3a✝ < b✝ ↔ a✝ ≤ b✝ ∧ ¬b✝ ≤ a✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_3a✝ < b✝ ↔ a✝ ≤ b✝ ∧ ¬b✝ ≤ a✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_3∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ asimp [eq_le: le = LE.leeq_le]Goals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = b α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintro _: ?m.13480_ _: ?m.13480_ hab: a✝ ≤ b✝hab hba: b✝ ≤ a✝hbaα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bsimp_rw [α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: le a✝ b✝hba: le b✝ a✝refine'_4a✝ = b✝eq_leα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝] at hab: le a✝ b✝hab hba: le b✝ a✝hbaα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αhab: a✝ ≤ b✝hba: b✝ ≤ a✝refine'_4a✝ = b✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_4∀ (a b : α), a ≤ b → b ≤ a → a = bexact le_antisymm: ∀ {α : Type ?u.14727} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm hab: a✝ ≤ b✝hab hba: b✝ ≤ a✝hbaGoals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ b α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintrosα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_5a✝ ≤ a✝ ⊔ b✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_5a✝ ≤ a✝ ⊔ b✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_5∀ (a b : α), a ≤ a ⊔ bsimp [eq_le: le = LE.leeq_le, eq_sup: sup = Sup.supeq_sup]Goals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ b α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintrosα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_6b✝ ≤ a✝ ⊔ b✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_6b✝ ≤ a✝ ⊔ b✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_6∀ (a b : α), b ≤ a ⊔ bsimp [eq_le: le = LE.leeq_le, eq_sup: sup = Sup.supeq_sup]Goals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1 α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintro _: ?m.13470_ _: ?m.13470_ _: ?m.13470_ hac: a✝ ≤ c✝hac hbc: b✝ ≤ c✝hbcα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7a✝ ⊔ b✝ ≤ c✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7a✝ ⊔ b✝ ≤ c✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1simp_rw [α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: le a✝ c✝hbc: le b✝ c✝refine'_7le (sup a✝ b✝) c✝eq_le: le = LE.leeq_leα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7sup a✝ b✝ ≤ c✝] at hac: a✝ ≤ c✝hac hbc: b✝ ≤ c✝hbc ⊢α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7sup a✝ b✝ ≤ c✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ c✝hbc: b✝ ≤ c✝refine'_7sup a✝ b✝ ≤ c✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_7∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1simp [eq_sup: sup = Sup.supeq_sup, hac: a✝ ≤ c✝hac, hbc: b✝ ≤ c✝hbc]Goals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ a α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ aα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintrosα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_8a✝ ⊓ b✝ ≤ a✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_8a✝ ⊓ b✝ ≤ a✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_8∀ (a b : α), a ⊓ b ≤ asimp [eq_le: le = LE.leeq_le, eq_inf: inf = Inf.infeq_inf]Goals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ b α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintrosα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_9a✝ ⊓ b✝ ≤ b✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝: αrefine'_9a✝ ⊓ b✝ ≤ b✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_9∀ (a b : α), a ⊓ b ≤ bsimp [eq_le: le = LE.leeq_le, eq_inf: inf = Inf.infeq_inf]Goals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1 α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintro _: ?m.13468_ _: ?m.13468_ _: ?m.13468_ hac: a✝ ≤ b✝hac hbc: a✝ ≤ c✝hbcα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ b✝ ⊓ c✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ b✝ ⊓ c✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1simp_rw [α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: le a✝ b✝hbc: le a✝ c✝refine'_10le a✝ (inf b✝ c✝)eq_le: le = LE.leeq_leα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ inf b✝ c✝] at hac: le a✝ b✝hac hbc: le a✝ c✝hbc ⊢α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ inf b✝ c✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infa✝, b✝, c✝: αhac: a✝ ≤ b✝hbc: a✝ ≤ c✝refine'_10a✝ ≤ inf b✝ c✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_10∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1simp [eq_inf: inf = Inf.infeq_inf, hac: a✝ ≤ b✝hac, hbc: a✝ ≤ c✝hbc]Goals accomplished! 🐙
α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infDistribLattice α·α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zintrosα: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infx✝, y✝, z✝: αrefine'_11(x✝ ⊔ y✝) ⊓ (x✝ ⊔ z✝) ≤ x✝ ⊔ y✝ ⊓ z✝;α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infx✝, y✝, z✝: αrefine'_11(x✝ ⊔ y✝) ⊓ (x✝ ⊔ z✝) ≤ x✝ ⊔ y✝ ⊓ z✝ α: Type uc: DistribLattice αle: α → α → Propeq_le: le = LE.lesup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infrefine'_11∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zsimp [eq_le: le = LE.leeq_le, eq_inf: inf = Inf.infeq_inf, eq_sup: sup = Sup.supeq_sup, le_sup_inf: ∀ {α : Type ?u.24826} [inst : DistribLattice α] {x y z : α}, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ zle_sup_inf]Goals accomplished! 🐙
#align distrib_lattice.copy DistribLattice.copy: {α : Type u} →
(c : DistribLattice α) →
(le : α → α → Prop) →
le = LE.le → (sup : α → α → α) → sup = Sup.sup → (inf : α → α → α) → inf = Inf.inf → DistribLattice αDistribLattice.copy

--Porting note: original proof uses
-- `all_goals { abstract { subst_vars, casesI c, simp_rw le_eq, assumption } }`
/-- A function to create a provable equal copy of a complete lattice
with possibly different definitional equalities. -/
def CompleteLattice.copy: {α : Type u} →
(c : CompleteLattice α) →
(le : α → α → Prop) →
le = LE.le →
(top : α) →
top = ⊤ →
(bot : α) →
bot = ⊥ →
(sup : α → α → α) →
sup = Sup.sup →
(inf : α → α → α) →
inf = Inf.inf →
(sSup : Set α → α) →
sSup = SupSet.sSup → (sInf : Set α → α) → sInf = InfSet.sInf → CompleteLattice αCompleteLattice.copy (c: CompleteLattice αc : CompleteLattice: Type ?u.44069 → Type ?u.44069CompleteLattice α: Type uα)
(le: α → α → Prople : α: Type uα → α: Type uα → Prop: TypeProp) (eq_le: le = LE.leeq_le : le: α → α → Prople = (byGoals accomplished! 🐙 α: Type uc: CompleteLattice αle: α → α → PropLE αinfer_instanceGoals accomplished! 🐙 : LE α).le: {α : Type ?u.44084} → [self : LE α] → α → α → Prople)
(top: αtop : α: Type uα) (eq_top: top = ⊤eq_top : top: αtop = (byGoals accomplished! 🐙 α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αTop αinfer_instanceGoals accomplished! 🐙 : Top α).top: {α : Type ?u.44102} → [self : Top α] → αtop)
(bot: αbot : α: Type uα) (eq_bot: bot = ⊥eq_bot : bot: αbot = (byGoals accomplished! 🐙 α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αBot αinfer_instanceGoals accomplished! 🐙 : Bot α).bot: {α : Type ?u.44114} → [self : Bot α] → αbot)
(sup: α → α → αsup : α: Type uα → α: Type uα → α: Type uα) (eq_sup: sup = Sup.supeq_sup : sup: α → α → αsup = (byGoals accomplished! 🐙 α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αSup αinfer_instanceGoals accomplished! 🐙 : Sup α).sup: {α : Type ?u.44132} → [self : Sup α] → α → α → αsup)
(inf: α → α → αinf : α: Type uα → α: Type uα → α: Type uα) (eq_inf: inf = Inf.infeq_inf : inf: α → α → αinf = (byGoals accomplished! 🐙 α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αInf αinfer_instanceGoals accomplished! 🐙 : Inf α).inf: {α : Type ?u.44156} → [self : Inf α] → α → α → αinf)
(sSup: Set α → αsSup : Set: Type ?u.44169 → Type ?u.44169Set α: Type uα → α: Type uα) (eq_sSup: sSup = SupSet.sSupeq_sSup : sSup: Set α → αsSup = (byGoals accomplished! 🐙 α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αSupSet αinfer_instanceGoals accomplished! 🐙 : SupSet α).sSup: {α : Type ?u.44178} → [self : SupSet α] → Set α → αsSup)
(sInf: Set α → αsInf : Set: Type ?u.44189 → Type ?u.44189Set α: Type uα → α: Type uα) (eq_sInf: sInf = InfSet.sInfeq_sInf : sInf: Set α → αsInf = (byGoals accomplished! 🐙 α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αInfSet αinfer_instanceGoals accomplished! 🐙 : InfSet α).sInf: {α : Type ?u.44198} → [self : InfSet α] → Set α → αsInf) :
CompleteLattice: Type ?u.44207 → Type ?u.44207CompleteLattice α: Type uα := byGoals accomplished! 🐙
α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfCompleteLattice αrefine' { Lattice.copy: {α : Type ?u.44425} →
(c : Lattice α) →
(le : α → α → Prop) → le = LE.le → (sup : α → α → α) → sup = Sup.sup → (inf : α → α → α) → inf = Inf.inf → Lattice αLattice.copy (@CompleteLattice.toLattice: {α : Type ?u.44427} → [self : CompleteLattice α] → Lattice αCompleteLattice.toLattice α: Type uα c: CompleteLattice αc) le: α → α → Prople eq_le: le = LE.leeq_le sup: α → α → αsup eq_sup: sup = Sup.supeq_sup inf: α → α → αinf eq_inf: inf = Inf.infeq_inf with
le := le: α → α → Prople, top := top: αtop, bot := bot: αbot, sup := sup: α → α → αsup, inf := inf: α → α → αinf, sSup := sSup: Set α → αsSup, sInf := sInf: Set α → αsInf.. }α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_1∀ (s : Set α) (a : α), a ∈ s → a ≤ SupSet.sSup sα: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_2∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → SupSet.sSup s ≤ aα: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_3∀ (s : Set α) (a : α), a ∈ s → InfSet.sInf s ≤ aα: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_4∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ InfSet.sInf sα: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_5∀ (x : α), x ≤ ⊤α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_6∀ (x : α), ⊥ ≤ x
α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfCompleteLattice α·α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_1∀ (s : Set α) (a : α), a ∈ s → a ≤ SupSet.sSup s α: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_1∀ (s : Set α) (a : α), a ∈ s → a ≤ SupSet.sSup sα: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_2∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → SupSet.sSup s ≤ aα: Type uc: CompleteLattice αle: α → α → Propeq_le: le = LE.letop: αeq_top: top = ⊤bot: αeq_bot: bot = ⊥sup: α → α → αeq_sup: sup = Sup.supinf: α → α → αeq_inf: inf = Inf.infsSup: Set α → αeq_sSup: sSup = SupSet.sSupsInf: Set α → αeq_sInf: sInf = InfSet.sInfsrc✝:= Lattice.copy toLattice le eq_le sup eq_sup inf eq_inf: Lattice αrefine'_3∀ (s : Set α) (a : α), a ∈ s → ```