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
Cmd instead of
Ctrl .
/-
Copyright (c) 2020 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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 }
--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 { h : LE α } { h' : LE α } ( c : @ BoundedOrder : (α : Type ?u.12) → [inst : LE α Type ?u.12 α h' )
( top : α ) ( eq_top : top = ( by infer_instance : Top α). top : {α : Type ?u.22} → [self : Top α α top )
( bot : α ) ( eq_bot : bot = ( by infer_instance : Bot α). bot : {α : Type ?u.34} → [self : Bot α α bot )
( le_eq : ∀ (x y : α ), x ≤ y ↔ x ≤ y le_eq : ∀ x y : α , (@ LE.le : {α : Type ?u.45} → [self : LE α α → α → Prop α h ) x y ↔ x ≤ y ) : @ BoundedOrder : (α : Type ?u.54) → [inst : LE α Type ?u.54 α h :=
@ BoundedOrder.mk α h (@ OrderTop.mk : {α : Type ?u.246} → [inst : LE α [toTop : Top α (∀ (a : α ), a ≤ ⊤ ) → OrderTop α α h { top := top } ( fun _ ↦ by simp [ eq_top , le_eq : ∀ (x y : α ), x ≤ y ↔ x ≤ y le_eq ] ))
(@ OrderBot.mk : {α : Type ?u.256} → [inst : LE α [toBot : Bot α (∀ (a : α ), ⊥ ≤ a ) → OrderBot α α h { bot := bot } ( fun _ ↦ by simp [ eq_bot , le_eq : ∀ (x y : α ), x ≤ y ↔ x ≤ y le_eq ] ))
#align bounded_order.copy 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 α )
( le : α → α → Prop ) ( eq_le : le = ( by infer_instance : LE α). le : {α : Type ?u.1105} → [self : LE α α → α → Prop le )
( sup : α → α → α ) ( eq_sup : sup = ( by infer_instance : Sup α). sup : {α : Type ?u.1129} → [self : Sup α α → α → α sup )
( inf : α → α → α ) ( eq_inf : inf = ( by α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α infer_instance : Inf α). inf : {α : Type ?u.1153} → [self : Inf α α → α → α inf ) : Lattice α := by
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine' { le := le , sup := sup , inf := inf , lt := fun a b ↦ le a b ∧ ¬ le b a .. } α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c : α ), a ≤ c b ≤ c a ⊔ b ≤ c α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c : α ), a ≤ b a ≤ c a ≤ b ⊓ c
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c : α ), a ≤ c b ≤ c a ⊔ b ≤ c α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c : α ), a ≤ b a ≤ c a ≤ b ⊓ c intros α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝ : α refine'_1 ; α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝ : α refine'_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_1 simp [ eq_le ]
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 intro _ _ _ hab hbc α : Type uc : 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✝ refine'_2 ; α : Type uc : 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✝ refine'_2 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c rw [ α : Type uc : 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✝ refine'_2 eq_le α : Type uc : 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✝ refine'_2 ] α : Type uc : 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✝ refine'_2 at hab hbc ⊢ α : Type uc : 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✝ refine'_2 ; α : Type uc : 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✝ refine'_2 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c exact le_trans : ∀ {α : Type ?u.1552} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c hab hbc
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 intros α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_3 ; α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_3 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a simp [ eq_le ]
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 intro _ _ hab hba α : Type uc : 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✝ refine'_4 ; α : Type uc : 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✝ refine'_4 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b simp_rw [ α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α hab : le a✝ b✝ hba : le b✝ a✝ refine'_4 eq_le α : Type uc : 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✝ refine'_4 ] at hab hba α : Type uc : 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✝ refine'_4 ; α : Type uc : 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✝ refine'_4 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b exact le_antisymm hab hba
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 intros α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_5 ; α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_5 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 simp [ eq_le , eq_sup ]
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 intros α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_6 ; α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_6 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 simp [ eq_le , eq_sup ]
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 intro _ _ _ hac hbc α : Type uc : 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✝ refine'_7 ; α : Type uc : 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✝ refine'_7 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 simp_rw [ α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝, c✝ : α hac : le a✝ c✝ hbc : le b✝ c✝ refine'_7 le (sup a✝ b✝ c✝
eq_le α : Type uc : 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✝ refine'_7 ] at hac hbc ⊢ α : Type uc : 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✝ refine'_7 ; α : Type uc : 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✝ refine'_7 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 simp [ eq_sup , hac , hbc ]
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 intros α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_8 ; α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_8 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 simp [ eq_le , eq_inf ]
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 intros α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_9 ; α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_9 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 simp [ eq_le , eq_inf ]
α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 intro _ _ _ hac hbc α : Type uc : 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✝ refine'_10 ; α : Type uc : 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✝ refine'_10 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 simp_rw [ α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝, c✝ : α hac : le a✝ b✝ hbc : le a✝ c✝ refine'_10 le a✝ (inf b✝ c✝
eq_le α : Type uc : 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✝ refine'_10 ] at hac hbc ⊢ α : Type uc : 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✝ refine'_10 ; α : Type uc : 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✝ refine'_10 α : Type uc : Lattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 simp [ eq_inf , hac , hbc ]
#align lattice.copy Lattice.copy : {α : Type u} →
(c : Lattice α (le : α → α → Prop le = LE.le (sup : α → α → α sup = Sup.sup (inf : α → α → α inf = Inf.inf Lattice α
--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 : Type ?u.13050 → Type ?u.13050 α )
( le : α → α → Prop ) ( eq_le : le = ( by infer_instance : LE α). le : {α : Type ?u.13065} → [self : LE α α → α → Prop le )
( sup : α → α → α ) ( eq_sup : sup = ( by infer_instance : Sup α). sup : {α : Type ?u.13089} → [self : Sup α α → α → α sup )
( inf : α → α → α ) ( eq_inf : inf = ( by infer_instance : Inf α). inf : {α : Type ?u.13113} → [self : Inf α α → α → α inf ) : DistribLattice : Type ?u.13125 → Type ?u.13125 α := by
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine' { le := le , sup := sup , inf := inf , lt := fun a b ↦ le a b ∧ ¬ le b a .. } α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c : α ), a ≤ c b ≤ c a ⊔ b ≤ c α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c : α ), a ≤ b a ≤ c a ≤ b ⊓ c α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c : α ), a ≤ c b ≤ c a ⊔ b ≤ c α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c : α ), a ≤ b a ≤ c a ≤ b ⊓ c α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intros α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝ : α refine'_1 ; α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝ : α refine'_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_1 simp [ eq_le ]
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intro _ _ _ hab hbc α : Type uc : 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✝ refine'_2 ; α : Type uc : 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✝ refine'_2 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c rw [ α : Type uc : 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✝ refine'_2 eq_le α : Type uc : 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✝ refine'_2 ] α : Type uc : 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✝ refine'_2 at hab hbc ⊢ α : Type uc : 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✝ refine'_2 ; α : Type uc : 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✝ refine'_2 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_2 ∀ (a b c : α ), a ≤ b b ≤ c a ≤ c exact le_trans : ∀ {α : Type ?u.13795} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c hab hbc
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intros α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_3 ; α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_3 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_3 ∀ (a b : α ), a < b ↔ a ≤ b ∧ ¬ b ≤ a simp [ eq_le ]
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intro _ _ hab hba α : Type uc : 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✝ refine'_4 ; α : Type uc : 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✝ refine'_4 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b simp_rw [ α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α hab : le a✝ b✝ hba : le b✝ a✝ refine'_4 eq_le α : Type uc : 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✝ refine'_4 ] at hab hba α : Type uc : 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✝ refine'_4 ; α : Type uc : 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✝ refine'_4 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_4 ∀ (a b : α ), a ≤ b b ≤ a a = b exact le_antisymm hab hba
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intros α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_5 ; α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_5 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_5 simp [ eq_le , eq_sup ]
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intros α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_6 ; α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_6 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_6 simp [ eq_le , eq_sup ]
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intro _ _ _ hac hbc α : Type uc : 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✝ refine'_7 ; α : Type uc : 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✝ refine'_7 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 simp_rw [ α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝, c✝ : α hac : le a✝ c✝ hbc : le b✝ c✝ refine'_7 le (sup a✝ b✝ c✝
eq_le α : Type uc : 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✝ refine'_7 ] at hac hbc ⊢ α : Type uc : 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✝ refine'_7 ; α : Type uc : 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✝ refine'_7 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_7 ∀ (a b c_1 : α ), a ≤ c_1 b ≤ c_1 a ⊔ b ≤ c_1 simp [ eq_sup , hac , hbc ]
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intros α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_8 ; α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_8 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_8 simp [ eq_le , eq_inf ]
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intros α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_9 ; α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝ : α refine'_9 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_9 simp [ eq_le , eq_inf ]
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intro _ _ _ hac hbc α : Type uc : 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✝ refine'_10 ; α : Type uc : 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✝ refine'_10 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 simp_rw [ α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf a✝, b✝, c✝ : α hac : le a✝ b✝ hbc : le a✝ c✝ refine'_10 le a✝ (inf b✝ c✝
eq_le α : Type uc : 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✝ refine'_10 ] at hac hbc ⊢ α : Type uc : 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✝ refine'_10 ; α : Type uc : 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✝ refine'_10 α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_10 ∀ (a b c_1 : α ), a ≤ b a ≤ c_1 a ≤ b ⊓ c_1 simp [ eq_inf , hac , hbc ]
α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf · α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z intros α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf x✝, y✝, z✝ : α refine'_11 (x✝ ⊔ y✝ ⊓ (x✝ ⊔ z✝ ≤ x✝ ⊔ y✝ ⊓ z✝ ; α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf x✝, y✝, z✝ : α refine'_11 (x✝ ⊔ y✝ ⊓ (x✝ ⊔ z✝ ≤ x✝ ⊔ y✝ ⊓ z✝ α : Type uc : DistribLattice α le : α → α → Prop eq_le : le = LE.le sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α eq_inf : inf = Inf.inf refine'_11 ∀ (x y z : α ), (x ⊔ y ⊓ (x ⊔ z ≤ x ⊔ y ⊓ z simp [ eq_le , eq_inf , eq_sup , le_sup_inf ]
#align distrib_lattice.copy 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 : Type ?u.44069 → Type ?u.44069 α )
( le : α → α → Prop ) ( eq_le : le = ( by infer_instance : LE α). le : {α : Type ?u.44084} → [self : LE α α → α → Prop le )
( top : α ) ( eq_top : top = ( by infer_instance : Top α). top : {α : Type ?u.44102} → [self : Top α α top )
( bot : α ) ( eq_bot : bot = ( by infer_instance : Bot α). bot : {α : Type ?u.44114} → [self : Bot α α bot )
( sup : α → α → α ) ( eq_sup : sup = ( by infer_instance : Sup α). sup : {α : Type ?u.44132} → [self : Sup α α → α → α sup )
( inf : α → α → α ) ( eq_inf : inf = ( by α : Type uc : CompleteLattice α le : α → α → Prop eq_le : le = LE.le top : α eq_top : top = ⊤ bot : α eq_bot : bot = ⊥ sup : α → α → α eq_sup : sup = Sup.sup inf : α → α → α infer_instance : Inf α). inf : {α : Type ?u.44156} → [self : Inf α α → α → α inf )
( sSup : Set α → α ) ( eq_sSup : sSup = SupSet.sSup eq_sSup : sSup = ( by α : Type uc : 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 α α infer_instance : SupSet α). sSup )
( sInf : Set α → α ) ( eq_sInf : sInf = InfSet.sInf eq_sInf : sInf = ( by α : Type uc : 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 α α infer_instance : InfSet α). sInf ) :
CompleteLattice : Type ?u.44207 → Type ?u.44207 α := by
α : Type uc : 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 refine' { Lattice.copy : {α : Type ?u.44425} →
(c : Lattice α (le : α → α → Prop le = LE.le (sup : α → α → α sup = Sup.sup (inf : α → α → α inf = Inf.inf Lattice α (@ 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 .. } α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_1 α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_2 α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_3 α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_4 α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_5 α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_6
α : Type uc : 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 · α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_1 α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_1 α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_2 α : Type uc : 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.copy toLattice le eq_le sup eq_sup inf eq_inf : Lattice α refine'_3 ∀ (s : Set α a : α ), a ∈ s