import order.monotone.basic

import tactic.simps

import tactic.pi_instances

set_option old_structure_cmd true

universes u v w

variables {α : Type u} {β : Type v}

attribute [ematch] le_trans lt_of_le_of_lt lt_of_lt_of_le lt_trans

@[ematch] theorem le_antisymm' [partial_order α] : ∀ {a b : α}, (: a ≤ b :) → b ≤ a → a = b :=

@le_antisymm _ _

class semilattice_sup (α : Type u) extends has_sup α, partial_order α :=

(le_sup_left : ∀ a b : α, a ≤ a ⊔ b)

(le_sup_right : ∀ a b : α, b ≤ a ⊔ b)

(sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c)

def semilattice_sup.mk' {α : Type*} [has_sup α]

(sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a)

(sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))

(sup_idem : ∀ (a : α), a ⊔ a = a) : semilattice_sup α :=

{ sup := (⊔),

le := λ a b, a ⊔ b = b,

le_refl := sup_idem,

le_trans := λ a b c hab hbc,

begin

dsimp only [(≤)] at *,

rwa [←hbc, ←sup_assoc, hab],

end,

le_antisymm := λ a b hab hba,

begin

dsimp only [(≤)] at *,

rwa [←hba, sup_comm],

end,

le_sup_left := λ a b, show a ⊔ (a ⊔ b) = (a ⊔ b), by rw [←sup_assoc, sup_idem],

le_sup_right := λ a b, show b ⊔ (a ⊔ b) = (a ⊔ b), by rw [sup_comm, sup_assoc, sup_idem],

sup_le := λ a b c hac hbc,

begin

dsimp only [(≤), preorder.le] at *,

rwa [sup_assoc, hbc],

end }

instance (α : Type*) [has_inf α] : has_sup αᵒᵈ := ⟨((⊓) : α → α → α)⟩

instance (α : Type*) [has_sup α] : has_inf αᵒᵈ := ⟨((⊔) : α → α → α)⟩

section semilattice_sup

variables [semilattice_sup α] {a b c d : α}

@[simp] theorem le_sup_left : a ≤ a ⊔ b :=

semilattice_sup.le_sup_left a b

@[ematch] theorem le_sup_left' : a ≤ (: a ⊔ b :) :=

le_sup_left

@[simp] theorem le_sup_right : b ≤ a ⊔ b :=

semilattice_sup.le_sup_right a b

@[ematch] theorem le_sup_right' : b ≤ (: a ⊔ b :) :=

le_sup_right

theorem le_sup_of_le_left (h : c ≤ a) : c ≤ a ⊔ b :=

le_trans h le_sup_left

theorem le_sup_of_le_right (h : c ≤ b) : c ≤ a ⊔ b :=

le_trans h le_sup_right

theorem lt_sup_of_lt_left (h : c < a) : c < a ⊔ b :=

h.trans_le le_sup_left

theorem lt_sup_of_lt_right (h : c < b) : c < a ⊔ b :=

h.trans_le le_sup_right

theorem sup_le : a ≤ c → b ≤ c → a ⊔ b ≤ c :=

semilattice_sup.sup_le a b c

@[simp] theorem sup_le_iff : a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c :=

⟨assume h : a ⊔ b ≤ c, ⟨le_trans le_sup_left h, le_trans le_sup_right h⟩,

assume ⟨h₁, h₂⟩, sup_le h₁ h₂⟩

@[simp] lemma sup_eq_left : a ⊔ b = a ↔ b ≤ a := le_antisymm_iff.trans $ by simp [le_rfl]

@[simp] lemma sup_eq_right : a ⊔ b = b ↔ a ≤ b := le_antisymm_iff.trans $ by simp [le_rfl]

@[simp] lemma left_eq_sup : a = a ⊔ b ↔ b ≤ a := eq_comm.trans sup_eq_left

@[simp] lemma right_eq_sup : b = a ⊔ b ↔ a ≤ b := eq_comm.trans sup_eq_right

alias sup_eq_left ↔ _ sup_of_le_left

alias sup_eq_right ↔ le_of_sup_eq sup_of_le_right

attribute [simp] sup_of_le_left sup_of_le_right

@[simp] theorem left_lt_sup : a < a ⊔ b ↔ ¬b ≤ a :=

le_sup_left.lt_iff_ne.trans $ not_congr left_eq_sup

@[simp] theorem right_lt_sup : b < a ⊔ b ↔ ¬a ≤ b :=

le_sup_right.lt_iff_ne.trans $ not_congr right_eq_sup

lemma left_or_right_lt_sup (h : a ≠ b) : (a < a ⊔ b ∨ b < a ⊔ b) :=

h.not_le_or_not_le.symm.imp left_lt_sup.2 right_lt_sup.2

theorem le_iff_exists_sup : a ≤ b ↔ ∃ c, b = a ⊔ c :=

split,

{ intro h, exact ⟨b, (sup_eq_right.mpr h).symm⟩ },

{ rintro ⟨c, (rfl : _ = _ ⊔ _)⟩,

exact le_sup_left }

theorem sup_le_sup (h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊔ c ≤ b ⊔ d :=

sup_le (le_sup_of_le_left h₁) (le_sup_of_le_right h₂)

theorem sup_le_sup_left (h₁ : a ≤ b) (c) : c ⊔ a ≤ c ⊔ b :=

sup_le_sup le_rfl h₁

theorem sup_le_sup_right (h₁ : a ≤ b) (c) : a ⊔ c ≤ b ⊔ c :=

sup_le_sup h₁ le_rfl

@[simp] theorem sup_idem : a ⊔ a = a :=

by apply le_antisymm; simp

instance sup_is_idempotent : is_idempotent α (⊔) := ⟨@sup_idem _ _⟩

theorem sup_comm : a ⊔ b = b ⊔ a :=

by apply le_antisymm; simp

instance sup_is_commutative : is_commutative α (⊔) := ⟨@sup_comm _ _⟩

theorem sup_assoc : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) :=

eq_of_forall_ge_iff $ λ x, by simp only [sup_le_iff, and_assoc]

instance sup_is_associative : is_associative α (⊔) := ⟨@sup_assoc _ _⟩

lemma sup_left_right_swap (a b c : α) : a ⊔ b ⊔ c = c ⊔ b ⊔ a :=

by rw [sup_comm, @sup_comm _ _ a, sup_assoc]

@[simp] lemma sup_left_idem : a ⊔ (a ⊔ b) = a ⊔ b :=

by rw [← sup_assoc, sup_idem]

@[simp] lemma sup_right_idem : (a ⊔ b) ⊔ b = a ⊔ b :=

by rw [sup_assoc, sup_idem]

lemma sup_left_comm (a b c : α) : a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c) :=

by rw [← sup_assoc, ← sup_assoc, @sup_comm α _ a]

lemma sup_right_comm (a b c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ b :=

by rw [sup_assoc, sup_assoc, @sup_comm _ _ b]

lemma sup_sup_sup_comm (a b c d : α) : a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d) :=

by rw [sup_assoc, sup_left_comm b, ←sup_assoc]

lemma sup_sup_distrib_left (a b c : α) : a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ (a ⊔ c) :=

by rw [sup_sup_sup_comm, sup_idem]

lemma sup_sup_distrib_right (a b c : α) : (a ⊔ b) ⊔ c = (a ⊔ c) ⊔ (b ⊔ c) :=

by rw [sup_sup_sup_comm, sup_idem]

lemma sup_congr_left (hb : b ≤ a ⊔ c) (hc : c ≤ a ⊔ b) : a ⊔ b = a ⊔ c :=

(sup_le le_sup_left hb).antisymm $ sup_le le_sup_left hc

lemma sup_congr_right (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ⊔ c = b ⊔ c :=

(sup_le ha le_sup_right).antisymm $ sup_le hb le_sup_right

lemma sup_eq_sup_iff_left : a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b :=

⟨λ h, ⟨h ▸ le_sup_right, h.symm ▸ le_sup_right⟩, λ h, sup_congr_left h.1 h.2⟩

lemma sup_eq_sup_iff_right : a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c :=

⟨λ h, ⟨h ▸ le_sup_left, h.symm ▸ le_sup_left⟩, λ h, sup_congr_right h.1 h.2⟩

lemma ne.lt_sup_or_lt_sup (hab : a ≠ b) : a < a ⊔ b ∨ b < a ⊔ b :=

hab.symm.not_le_or_not_le.imp left_lt_sup.2 right_lt_sup.2

theorem monotone.forall_le_of_antitone {β : Type*} [preorder β] {f g : α → β}

(hf : monotone f) (hg : antitone g) (h : f ≤ g) (m n : α) :

f m ≤ g n :=

calc f m ≤ f (m ⊔ n) : hf le_sup_left

... ≤ g (m ⊔ n) : h _

... ≤ g n : hg le_sup_right

theorem semilattice_sup.ext_sup {α} {A B : semilattice_sup α}

(H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y)

(x y : α) : (by haveI := A; exact (x ⊔ y)) = x ⊔ y :=

eq_of_forall_ge_iff $ λ c,

by simp only [sup_le_iff]; rw [← H, @sup_le_iff α A, H, H]

theorem semilattice_sup.ext {α} {A B : semilattice_sup α}

(H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y) : A = B :=

have := partial_order.ext H,

have ss := funext (λ x, funext $ semilattice_sup.ext_sup H x),

casesI A, casesI B,

injection this; congr'

lemma ite_le_sup (s s' : α) (P : Prop) [decidable P] : ite P s s' ≤ s ⊔ s' :=

if h : P then (if_pos h).trans_le le_sup_left else (if_neg h).trans_le le_sup_right

end semilattice_sup

class semilattice_inf (α : Type u) extends has_inf α, partial_order α :=

(inf_le_left : ∀ a b : α, a ⊓ b ≤ a)

(inf_le_right : ∀ a b : α, a ⊓ b ≤ b)

(le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c)

instance (α) [semilattice_inf α] : semilattice_sup αᵒᵈ :=

{ le_sup_left := semilattice_inf.inf_le_left,

le_sup_right := semilattice_inf.inf_le_right,

sup_le := assume a b c hca hcb, @semilattice_inf.le_inf α _ _ _ _ hca hcb,

.. order_dual.partial_order α, .. order_dual.has_sup α }

instance (α) [semilattice_sup α] : semilattice_inf αᵒᵈ :=

{ inf_le_left := @le_sup_left α _,

inf_le_right := @le_sup_right α _,

le_inf := assume a b c hca hcb, @sup_le α _ _ _ _ hca hcb,

.. order_dual.partial_order α, .. order_dual.has_inf α }

theorem semilattice_sup.dual_dual (α : Type*) [H : semilattice_sup α] :

order_dual.semilattice_sup αᵒᵈ = H :=

semilattice_sup.ext $ λ _ _, iff.rfl

section semilattice_inf

variables [semilattice_inf α] {a b c d : α}

@[simp] theorem inf_le_left : a ⊓ b ≤ a :=

semilattice_inf.inf_le_left a b

@[ematch] theorem inf_le_left' : (: a ⊓ b :) ≤ a :=

semilattice_inf.inf_le_left a b

@[simp] theorem inf_le_right : a ⊓ b ≤ b :=

semilattice_inf.inf_le_right a b

@[ematch] theorem inf_le_right' : (: a ⊓ b :) ≤ b :=

semilattice_inf.inf_le_right a b

theorem le_inf : a ≤ b → a ≤ c → a ≤ b ⊓ c :=

semilattice_inf.le_inf a b c

theorem inf_le_of_left_le (h : a ≤ c) : a ⊓ b ≤ c :=

le_trans inf_le_left h

theorem inf_le_of_right_le (h : b ≤ c) : a ⊓ b ≤ c :=

le_trans inf_le_right h

theorem inf_lt_of_left_lt (h : a < c) : a ⊓ b < c :=

lt_of_le_of_lt inf_le_left h

theorem inf_lt_of_right_lt (h : b < c) : a ⊓ b < c :=

lt_of_le_of_lt inf_le_right h

@[simp] theorem le_inf_iff : a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c := @sup_le_iff αᵒᵈ _ _ _ _

@[simp] lemma inf_eq_left : a ⊓ b = a ↔ a ≤ b := le_antisymm_iff.trans $ by simp [le_rfl]

@[simp] lemma inf_eq_right : a ⊓ b = b ↔ b ≤ a := le_antisymm_iff.trans $ by simp [le_rfl]

@[simp] lemma left_eq_inf : a = a ⊓ b ↔ a ≤ b := eq_comm.trans inf_eq_left

@[simp] lemma right_eq_inf : b = a ⊓ b ↔ b ≤ a := eq_comm.trans inf_eq_right

alias inf_eq_left ↔ le_of_inf_eq inf_of_le_left

alias inf_eq_right ↔ _ inf_of_le_right

attribute [simp] inf_of_le_left inf_of_le_right

@[simp] theorem inf_lt_left : a ⊓ b < a ↔ ¬a ≤ b := @left_lt_sup αᵒᵈ _ _ _

@[simp] theorem inf_lt_right : a ⊓ b < b ↔ ¬b ≤ a := @right_lt_sup αᵒᵈ _ _ _

theorem inf_lt_left_or_right (h : a ≠ b) : a ⊓ b < a ∨ a ⊓ b < b :=

@left_or_right_lt_sup αᵒᵈ _ _ _ h

theorem inf_le_inf (h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊓ c ≤ b ⊓ d :=

@sup_le_sup αᵒᵈ _ _ _ _ _ h₁ h₂

lemma inf_le_inf_right (a : α) {b c : α} (h : b ≤ c) : b ⊓ a ≤ c ⊓ a := inf_le_inf h le_rfl

lemma inf_le_inf_left (a : α) {b c : α} (h : b ≤ c) : a ⊓ b ≤ a ⊓ c := inf_le_inf le_rfl h

@[simp] lemma inf_idem : a ⊓ a = a := @sup_idem αᵒᵈ _ _

instance inf_is_idempotent : is_idempotent α (⊓) := ⟨@inf_idem _ _⟩

lemma inf_comm : a ⊓ b = b ⊓ a := @sup_comm αᵒᵈ _ _ _

instance inf_is_commutative : is_commutative α (⊓) := ⟨@inf_comm _ _⟩

lemma inf_assoc : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := @sup_assoc αᵒᵈ _ a b c

instance inf_is_associative : is_associative α (⊓) := ⟨@inf_assoc _ _⟩

lemma inf_left_right_swap (a b c : α) : a ⊓ b ⊓ c = c ⊓ b ⊓ a := @sup_left_right_swap αᵒᵈ _ _ _ _

@[simp] lemma inf_left_idem : a ⊓ (a ⊓ b) = a ⊓ b := @sup_left_idem αᵒᵈ _ a b

@[simp] lemma inf_right_idem : (a ⊓ b) ⊓ b = a ⊓ b := @sup_right_idem αᵒᵈ _ a b

lemma inf_left_comm (a b c : α) : a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c) := @sup_left_comm αᵒᵈ _ a b c

lemma inf_right_comm (a b c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ b := @sup_right_comm αᵒᵈ _ a b c

lemma inf_inf_inf_comm (a b c d : α) : a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d) :=

@sup_sup_sup_comm αᵒᵈ _ _ _ _ _

lemma inf_inf_distrib_left (a b c : α) : a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ (a ⊓ c) :=

@sup_sup_distrib_left αᵒᵈ _ _ _ _

lemma inf_inf_distrib_right (a b c : α) : (a ⊓ b) ⊓ c = (a ⊓ c) ⊓ (b ⊓ c) :=

@sup_sup_distrib_right αᵒᵈ _ _ _ _

lemma inf_congr_left (hb : a ⊓ c ≤ b) (hc : a ⊓ b ≤ c) : a ⊓ b = a ⊓ c :=

@sup_congr_left αᵒᵈ _ _ _ _ hb hc

lemma inf_congr_right (h1 : b ⊓ c ≤ a) (h2 : a ⊓ c ≤ b) : a ⊓ c = b ⊓ c :=

@sup_congr_right αᵒᵈ _ _ _ _ h1 h2

lemma inf_eq_inf_iff_left : a ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c :=

@sup_eq_sup_iff_left αᵒᵈ _ _ _ _

lemma inf_eq_inf_iff_right : a ⊓ c = b ⊓ c ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b :=

@sup_eq_sup_iff_right αᵒᵈ _ _ _ _

lemma ne.inf_lt_or_inf_lt : a ≠ b → a ⊓ b < a ∨ a ⊓ b < b := @ne.lt_sup_or_lt_sup αᵒᵈ _ _ _

theorem semilattice_inf.ext_inf {α} {A B : semilattice_inf α}

(H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y)

(x y : α) : (by haveI := A; exact (x ⊓ y)) = x ⊓ y :=

eq_of_forall_le_iff $ λ c,

by simp only [le_inf_iff]; rw [← H, @le_inf_iff α A, H, H]

theorem semilattice_inf.ext {α} {A B : semilattice_inf α}

(H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y) : A = B :=

have := partial_order.ext H,

have ss := funext (λ x, funext $ semilattice_inf.ext_inf H x),

casesI A, casesI B,

injection this; congr'

theorem semilattice_inf.dual_dual (α : Type*) [H : semilattice_inf α] :

order_dual.semilattice_inf αᵒᵈ = H :=

semilattice_inf.ext $ λ _ _, iff.rfl

lemma inf_le_ite (s s' : α) (P : Prop) [decidable P] : s ⊓ s' ≤ ite P s s' :=

@ite_le_sup αᵒᵈ _ _ _ _ _

end semilattice_inf

def semilattice_inf.mk' {α : Type*} [has_inf α]

(inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a)

(inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c))

(inf_idem : ∀ (a : α), a ⊓ a = a) : semilattice_inf α :=

haveI : semilattice_sup αᵒᵈ := semilattice_sup.mk' inf_comm inf_assoc inf_idem,

haveI i := order_dual.semilattice_inf αᵒᵈ,

exact i,

class lattice (α : Type u) extends semilattice_sup α, semilattice_inf α

instance (α) [lattice α] : lattice αᵒᵈ :=

{ .. order_dual.semilattice_sup α, .. order_dual.semilattice_inf α }

lemma semilattice_sup_mk'_partial_order_eq_semilattice_inf_mk'_partial_order {α : Type*}

[has_sup α] [has_inf α]

(sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a)

(sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))

(sup_idem : ∀ (a : α), a ⊔ a = a)

(inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a)

(inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c))

(inf_idem : ∀ (a : α), a ⊓ a = a)

(sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a)

(inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a) :

@semilattice_sup.to_partial_order _ (semilattice_sup.mk' sup_comm sup_assoc sup_idem) =

@semilattice_inf.to_partial_order _ (semilattice_inf.mk' inf_comm inf_assoc inf_idem) :=

partial_order.ext $ λ a b, show a ⊔ b = b ↔ b ⊓ a = a, from

⟨λ h, by rw [←h, inf_comm, inf_sup_self],

λ h, by rw [←h, sup_comm, sup_inf_self]⟩

def lattice.mk' {α : Type*} [has_sup α] [has_inf α]

(sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a)

(sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))

(inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a)

(inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c))

(sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a)

(inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a) : lattice α :=

have sup_idem : ∀ (b : α), b ⊔ b = b := λ b,

calc b ⊔ b = b ⊔ b ⊓ (b ⊔ b) : by rw inf_sup_self

... = b : by rw sup_inf_self,

have inf_idem : ∀ (b : α), b ⊓ b = b := λ b,

calc b ⊓ b = b ⊓ (b ⊔ b ⊓ b) : by rw sup_inf_self

... = b : by rw inf_sup_self,

let semilatt_inf_inst := semilattice_inf.mk' inf_comm inf_assoc inf_idem,

semilatt_sup_inst := semilattice_sup.mk' sup_comm sup_assoc sup_idem,

partial_order_inst := @semilattice_sup.to_partial_order _ semilatt_sup_inst in

have partial_order_eq :

partial_order_inst = @semilattice_inf.to_partial_order _ semilatt_inf_inst :=

semilattice_sup_mk'_partial_order_eq_semilattice_inf_mk'_partial_order _ _ _ _ _ _

sup_inf_self inf_sup_self,

{ inf_le_left := λ a b, by { rw partial_order_eq, apply inf_le_left },

inf_le_right := λ a b, by { rw partial_order_eq, apply inf_le_right },

le_inf := λ a b c, by { rw partial_order_eq, apply le_inf },

..partial_order_inst,

..semilatt_sup_inst,

..semilatt_inf_inst, }

section lattice

variables [lattice α] {a b c d : α}

lemma inf_le_sup : a ⊓ b ≤ a ⊔ b := inf_le_left.trans le_sup_left

@[simp] lemma sup_le_inf : a ⊔ b ≤ a ⊓ b ↔ a = b :=

⟨λ h, le_antisymm (le_sup_left.trans $ h.trans inf_le_right)

(le_sup_right.trans $ h.trans inf_le_left), by { rintro rfl, simp }⟩

@[simp] lemma inf_eq_sup : a ⊓ b = a ⊔ b ↔ a = b := by rw [←inf_le_sup.ge_iff_eq, sup_le_inf]

@[simp] lemma sup_eq_inf : a ⊔ b = a ⊓ b ↔ a = b := eq_comm.trans inf_eq_sup

@[simp] lemma inf_lt_sup : a ⊓ b < a ⊔ b ↔ a ≠ b := by rw [inf_le_sup.lt_iff_ne, ne.def, inf_eq_sup]

lemma inf_eq_and_sup_eq_iff : a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c :=

refine ⟨λ h, _, _⟩,

{ obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm),

simpa using h },

{ rintro ⟨rfl, rfl⟩,

exact ⟨inf_idem, sup_idem⟩ }

theorem sup_inf_le : a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c) :=

le_inf (sup_le_sup_left inf_le_left _) (sup_le_sup_left inf_le_right _)

theorem le_inf_sup : (a ⊓ b) ⊔ (a ⊓ c) ≤ a ⊓ (b ⊔ c) :=

sup_le (inf_le_inf_left _ le_sup_left) (inf_le_inf_left _ le_sup_right)

theorem inf_sup_self : a ⊓ (a ⊔ b) = a :=

by simp

theorem sup_inf_self : a ⊔ (a ⊓ b) = a :=

by simp

theorem sup_eq_iff_inf_eq : a ⊔ b = b ↔ a ⊓ b = a :=

by rw [sup_eq_right, ←inf_eq_left]

theorem lattice.ext {α} {A B : lattice α}

(H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y) : A = B :=

have SS : @lattice.to_semilattice_sup α A =

@lattice.to_semilattice_sup α B := semilattice_sup.ext H,

have II := semilattice_inf.ext H,

casesI A, casesI B,

injection SS; injection II; congr'

end lattice

class distrib_lattice α extends lattice α :=

(le_sup_inf : ∀x y z : α, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z))

section distrib_lattice

variables [distrib_lattice α] {x y z : α}

theorem le_sup_inf : ∀{x y z : α}, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z) :=

distrib_lattice.le_sup_inf

theorem sup_inf_left : x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) :=

le_antisymm sup_inf_le le_sup_inf

theorem sup_inf_right : (y ⊓ z) ⊔ x = (y ⊔ x) ⊓ (z ⊔ x) :=

by simp only [sup_inf_left, λy:α, @sup_comm α _ y x, eq_self_iff_true]

theorem inf_sup_left : x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z) :=

calc x ⊓ (y ⊔ z) = (x ⊓ (x ⊔ z)) ⊓ (y ⊔ z) : by rw [inf_sup_self]

... = x ⊓ ((x ⊓ y) ⊔ z) : by simp only [inf_assoc, sup_inf_right,

eq_self_iff_true]

... = (x ⊔ (x ⊓ y)) ⊓ ((x ⊓ y) ⊔ z) : by rw [sup_inf_self]

... = ((x ⊓ y) ⊔ x) ⊓ ((x ⊓ y) ⊔ z) : by rw [sup_comm]

... = (x ⊓ y) ⊔ (x ⊓ z) : by rw [sup_inf_left]

instance (α : Type*) [distrib_lattice α] : distrib_lattice αᵒᵈ :=

{ le_sup_inf := assume x y z, le_of_eq inf_sup_left.symm,

.. order_dual.lattice α }

theorem inf_sup_right : (y ⊔ z) ⊓ x = (y ⊓ x) ⊔ (z ⊓ x) :=

by simp only [inf_sup_left, λy:α, @inf_comm α _ y x, eq_self_iff_true]

lemma le_of_inf_le_sup_le (h₁ : x ⊓ z ≤ y ⊓ z) (h₂ : x ⊔ z ≤ y ⊔ z) : x ≤ y :=

calc x ≤ (y ⊓ z) ⊔ x : le_sup_right

... = (y ⊔ x) ⊓ (x ⊔ z) : by rw [sup_inf_right, @sup_comm _ _ x]

... ≤ (y ⊔ x) ⊓ (y ⊔ z) : inf_le_inf_left _ h₂

... = y ⊔ (x ⊓ z) : sup_inf_left.symm

... ≤ y ⊔ (y ⊓ z) : sup_le_sup_left h₁ _

... ≤ _ : sup_le (le_refl y) inf_le_left

lemma eq_of_inf_eq_sup_eq {α : Type u} [distrib_lattice α] {a b c : α}

(h₁ : b ⊓ a = c ⊓ a) (h₂ : b ⊔ a = c ⊔ a) : b = c :=

le_antisymm

(le_of_inf_le_sup_le (le_of_eq h₁) (le_of_eq h₂))

(le_of_inf_le_sup_le (le_of_eq h₁.symm) (le_of_eq h₂.symm))

end distrib_lattice

@[reducible] -- See note [reducible non-instances]

def distrib_lattice.of_inf_sup_le [lattice α]

(inf_sup_le : ∀ a b c : α, a ⊓ (b ⊔ c) ≤ (a ⊓ b) ⊔ (a ⊓ c)) : distrib_lattice α :=

{ ..‹lattice α›,

..@order_dual.distrib_lattice αᵒᵈ { le_sup_inf := inf_sup_le, ..order_dual.lattice _ } }

@[priority 100] -- see Note [lower instance priority]

instance linear_order.to_lattice {α : Type u} [o : linear_order α] :

lattice α :=

{ sup := max,

le_sup_left := le_max_left,

le_sup_right := le_max_right,

sup_le := assume a b c, max_le,

inf := min,

inf_le_left := min_le_left,

inf_le_right := min_le_right,

le_inf := assume a b c, le_min,

..o }

section linear_order

variables [linear_order α] {a b c d : α}

lemma sup_eq_max : a ⊔ b = max a b := rfl

lemma inf_eq_min : a ⊓ b = min a b := rfl

lemma sup_ind (a b : α) {p : α → Prop} (ha : p a) (hb : p b) : p (a ⊔ b) :=

(is_total.total a b).elim (λ h : a ≤ b, by rwa sup_eq_right.2 h) (λ h, by rwa sup_eq_left.2 h)

@[simp] lemma le_sup_iff : a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c :=

⟨λ h, (total_of (≤) c b).imp

(λ bc, by rwa sup_eq_left.2 bc at h)

(λ bc, by rwa sup_eq_right.2 bc at h),

λ h, h.elim le_sup_of_le_left le_sup_of_le_right⟩

@[simp] lemma lt_sup_iff : a < b ⊔ c ↔ a < b ∨ a < c :=

⟨λ h, (total_of (≤) c b).imp

(λ bc, by rwa sup_eq_left.2 bc at h)

(λ bc, by rwa sup_eq_right.2 bc at h),

λ h, h.elim lt_sup_of_lt_left lt_sup_of_lt_right⟩

@[simp] lemma sup_lt_iff : b ⊔ c < a ↔ b < a ∧ c < a :=

⟨λ h, ⟨le_sup_left.trans_lt h, le_sup_right.trans_lt h⟩, λ h, sup_ind b c h.1 h.2⟩

lemma inf_ind (a b : α) {p : α → Prop} : p a → p b → p (a ⊓ b) := @sup_ind αᵒᵈ _ _ _ _

@[simp] lemma inf_le_iff : b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a := @le_sup_iff αᵒᵈ _ _ _ _

@[simp] lemma inf_lt_iff : b ⊓ c < a ↔ b < a ∨ c < a := @lt_sup_iff αᵒᵈ _ _ _ _

@[simp] lemma lt_inf_iff : a < b ⊓ c ↔ a < b ∧ a < c := @sup_lt_iff αᵒᵈ _ _ _ _

variables (a b c d)

lemma max_max_max_comm : max (max a b) (max c d) = max (max a c) (max b d) :=

sup_sup_sup_comm _ _ _ _

lemma min_min_min_comm : min (min a b) (min c d) = min (min a c) (min b d) :=

inf_inf_inf_comm _ _ _ _

end linear_order

lemma sup_eq_max_default [semilattice_sup α] [decidable_rel ((≤) : α → α → Prop)]

[is_total α (≤)] : (⊔) = (max_default : α → α → α) :=

ext x y,

dunfold max_default,

split_ifs with h',

exacts [sup_of_le_right h', sup_of_le_left $ (total_of (≤) x y).resolve_left h']

lemma inf_eq_min_default [semilattice_inf α] [decidable_rel ((≤) : α → α → Prop)]

[is_total α (≤)] : (⊓) = (min_default : α → α → α) :=

ext x y,

dunfold min_default,

split_ifs with h',

exacts [inf_of_le_left h', inf_of_le_right $ (total_of (≤) x y).resolve_left h']

@[reducible] def lattice.to_linear_order (α : Type u) [lattice α] [decidable_eq α]

[decidable_rel ((≤) : α → α → Prop)] [decidable_rel ((<) : α → α → Prop)]

[is_total α (≤)] :

linear_order α :=

{ decidable_le := ‹_›, decidable_eq := ‹_›, decidable_lt := ‹_›,

le_total := total_of (≤),

max := (⊔),

max_def := sup_eq_max_default,

min := (⊓),

min_def := inf_eq_min_default,

..‹lattice α› }

@[priority 100] -- see Note [lower instance priority]

instance linear_order.to_distrib_lattice {α : Type u} [o : linear_order α] :

distrib_lattice α :=

{ le_sup_inf := assume a b c,

match le_total b c with

| or.inl h := inf_le_of_left_le $ sup_le_sup_left (le_inf (le_refl b) h) _

| or.inr h := inf_le_of_right_le $ sup_le_sup_left (le_inf h (le_refl c)) _

end,

..linear_order.to_lattice }

instance nat.distrib_lattice : distrib_lattice ℕ :=

by apply_instance

open order_dual

@[simp] lemma of_dual_inf [has_sup α] (a b: αᵒᵈ) : of_dual (a ⊓ b) = of_dual a ⊔ of_dual b := rfl

@[simp] lemma of_dual_sup [has_inf α] (a b : αᵒᵈ) : of_dual (a ⊔ b) = of_dual a ⊓ of_dual b := rfl

@[simp] lemma to_dual_inf [has_inf α] (a b : α) : to_dual (a ⊓ b) = to_dual a ⊔ to_dual b := rfl

@[simp] lemma to_dual_sup [has_sup α] (a b : α) : to_dual (a ⊔ b) = to_dual a ⊓ to_dual b := rfl

section linear_order

variables [linear_order α]

@[simp] lemma of_dual_min (a b : αᵒᵈ) : of_dual (min a b) = max (of_dual a) (of_dual b) := rfl

@[simp] lemma of_dual_max (a b : αᵒᵈ) : of_dual (max a b) = min (of_dual a) (of_dual b) := rfl

@[simp] lemma to_dual_min (a b : α) : to_dual (min a b) = max (to_dual a) (to_dual b) := rfl

@[simp] lemma to_dual_max (a b : α) : to_dual (max a b) = min (to_dual a) (to_dual b) := rfl

end linear_order

namespace pi

variables {ι : Type*} {α' : ι → Type*}

instance [Π i, has_sup (α' i)] : has_sup (Π i, α' i) := ⟨λ f g i, f i ⊔ g i⟩

@[simp] lemma sup_apply [Π i, has_sup (α' i)] (f g : Π i, α' i) (i : ι) : (f ⊔ g) i = f i ⊔ g i :=

rfl

lemma sup_def [Π i, has_sup (α' i)] (f g : Π i, α' i) : f ⊔ g = λ i, f i ⊔ g i := rfl

instance [Π i, has_inf (α' i)] : has_inf (Π i, α' i) := ⟨λ f g i, f i ⊓ g i⟩

@[simp] lemma inf_apply [Π i, has_inf (α' i)] (f g : Π i, α' i) (i : ι) : (f ⊓ g) i = f i ⊓ g i :=

rfl

lemma inf_def [Π i, has_inf (α' i)] (f g : Π i, α' i) : f ⊓ g = λ i, f i ⊓ g i := rfl

instance [Π i, semilattice_sup (α' i)] : semilattice_sup (Π i, α' i) :=

by refine_struct { sup := (⊔), .. pi.partial_order }; tactic.pi_instance_derive_field

instance [Π i, semilattice_inf (α' i)] : semilattice_inf (Π i, α' i) :=

by refine_struct { inf := (⊓), .. pi.partial_order }; tactic.pi_instance_derive_field

instance [Π i, lattice (α' i)] : lattice (Π i, α' i) :=

{ .. pi.semilattice_sup, .. pi.semilattice_inf }

instance [Π i, distrib_lattice (α' i)] : distrib_lattice (Π i, α' i) :=

by refine_struct { .. pi.lattice }; tactic.pi_instance_derive_field

end pi

namespace function

variables {ι : Type*} {π : ι → Type*} [decidable_eq ι]

lemma update_sup [Π i, semilattice_sup (π i)] (f : Π i, π i) (i : ι) (a b : π i) :

f.update i (a ⊔ b) = f.update i a ⊔ f.update i b :=

funext $ λ j, by obtain rfl | hji := eq_or_ne j i; simp [update_noteq, *]

lemma update_inf [Π i, semilattice_inf (π i)] (f : Π i, π i) (i : ι) (a b : π i) :

f.update i (a ⊓ b) = f.update i a ⊓ f.update i b :=

funext $ λ j, by obtain rfl | hji := eq_or_ne j i; simp [update_noteq, *]

end function

namespace monotone

protected lemma sup [preorder α] [semilattice_sup β] {f g : α → β} (hf : monotone f)

(hg : monotone g) : monotone (f ⊔ g) :=

λ x y h, sup_le_sup (hf h) (hg h)

protected lemma inf [preorder α] [semilattice_inf β] {f g : α → β} (hf : monotone f)

(hg : monotone g) : monotone (f ⊓ g) :=

λ x y h, inf_le_inf (hf h) (hg h)

protected lemma max [preorder α] [linear_order β] {f g : α → β} (hf : monotone f)

(hg : monotone g) : monotone (λ x, max (f x) (g x)) :=

hf.sup hg

protected lemma min [preorder α] [linear_order β] {f g : α → β} (hf : monotone f)

(hg : monotone g) : monotone (λ x, min (f x) (g x)) :=

hf.inf hg

lemma le_map_sup [semilattice_sup α] [semilattice_sup β]

{f : α → β} (h : monotone f) (x y : α) :

f x ⊔ f y ≤ f (x ⊔ y) :=

sup_le (h le_sup_left) (h le_sup_right)

lemma map_inf_le [semilattice_inf α] [semilattice_inf β]

{f : α → β} (h : monotone f) (x y : α) :

f (x ⊓ y) ≤ f x ⊓ f y :=

le_inf (h inf_le_left) (h inf_le_right)

lemma of_map_inf [semilattice_inf α] [semilattice_inf β] {f : α → β}

(h : ∀ x y, f (x ⊓ y) = f x ⊓ f y) : monotone f :=

λ x y hxy, inf_eq_left.1 $ by rw [← h, inf_eq_left.2 hxy]

lemma of_map_sup [semilattice_sup α] [semilattice_sup β] {f : α → β}

(h : ∀ x y, f (x ⊔ y) = f x ⊔ f y) : monotone f :=

(@of_map_inf (order_dual α) (order_dual β) _ _ _ h).dual

variables [linear_order α]

lemma map_sup [semilattice_sup β] {f : α → β} (hf : monotone f) (x y : α) : f (x ⊔ y) = f x ⊔ f y :=

(is_total.total x y).elim

(λ h : x ≤ y, by simp only [h, hf h, sup_of_le_right])

(λ h, by simp only [h, hf h, sup_of_le_left])

lemma map_inf [semilattice_inf β] {f : α → β} (hf : monotone f) (x y : α) : f (x ⊓ y) = f x ⊓ f y :=

hf.dual.map_sup _ _

end monotone

namespace monotone_on

variables {f : α → β} {s : set α} {x y : α}

protected lemma sup [preorder α] [semilattice_sup β] {f g : α → β} {s : set α}

(hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (f ⊔ g) s :=

λ x hx y hy h, sup_le_sup (hf hx hy h) (hg hx hy h)

protected lemma inf [preorder α] [semilattice_inf β] {f g : α → β} {s : set α}

(hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (f ⊓ g) s :=

(hf.dual.sup hg.dual).dual

protected lemma max [preorder α] [linear_order β] {f g : α → β} {s : set α}

(hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (λ x, max (f x) (g x)) s :=

hf.sup hg

protected lemma min [preorder α] [linear_order β] {f g : α → β} {s : set α}

(hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (λ x, min (f x) (g x)) s :=

hf.inf hg

lemma of_map_inf [semilattice_inf α] [semilattice_inf β]

(h : ∀ (x ∈ s) (y ∈ s), f (x ⊓ y) = f x ⊓ f y) : monotone_on f s :=

λ x hx y hy hxy, inf_eq_left.1 $ by rw [←h _ hx _ hy, inf_eq_left.2 hxy]

lemma of_map_sup [semilattice_sup α] [semilattice_sup β]

(h : ∀ (x ∈ s) (y ∈ s), f (x ⊔ y) = f x ⊔ f y) : monotone_on f s :=

(@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual

variables [linear_order α]

lemma map_sup [semilattice_sup β] (hf : monotone_on f s) (hx : x ∈ s) (hy : y ∈ s) :

f (x ⊔ y) = f x ⊔ f y :=

by cases le_total x y; have := hf _ _ h;

assumption <|> simp only [h, this, sup_of_le_left, sup_of_le_right]

lemma map_inf [semilattice_inf β] (hf : monotone_on f s) (hx : x ∈ s) (hy : y ∈ s) :

f (x ⊓ y) = f x ⊓ f y :=

hf.dual.map_sup hx hy

end monotone_on

namespace antitone

protected lemma sup [preorder α] [semilattice_sup β] {f g : α → β} (hf : antitone f)

(hg : antitone g) : antitone (f ⊔ g) :=

λ x y h, sup_le_sup (hf h) (hg h)

protected lemma inf [preorder α] [semilattice_inf β] {f g : α → β} (hf : antitone f)

(hg : antitone g) : antitone (f ⊓ g) :=

λ x y h, inf_le_inf (hf h) (hg h)

protected lemma max [preorder α] [linear_order β] {f g : α → β} (hf : antitone f)

(hg : antitone g) : antitone (λ x, max (f x) (g x)) :=

hf.sup hg

protected lemma min [preorder α] [linear_order β] {f g : α → β} (hf : antitone f)

(hg : antitone g) : antitone (λ x, min (f x) (g x)) :=

hf.inf hg

lemma map_sup_le [semilattice_sup α] [semilattice_inf β]

{f : α → β} (h : antitone f) (x y : α) :

f (x ⊔ y) ≤ f x ⊓ f y :=

h.dual_right.le_map_sup x y

lemma le_map_inf [semilattice_inf α] [semilattice_sup β]

{f : α → β} (h : antitone f) (x y : α) :

f x ⊔ f y ≤ f (x ⊓ y) :=

h.dual_right.map_inf_le x y

variables [linear_order α]

lemma map_sup [semilattice_inf β] {f : α → β} (hf : antitone f) (x y : α) : f (x ⊔ y) = f x ⊓ f y :=

hf.dual_right.map_sup x y

lemma map_inf [semilattice_sup β] {f : α → β} (hf : antitone f) (x y : α) : f (x ⊓ y) = f x ⊔ f y :=

hf.dual_right.map_inf x y

end antitone

namespace antitone_on

variables {f : α → β} {s : set α} {x y : α}

protected lemma sup [preorder α] [semilattice_sup β] {f g : α → β} {s : set α}

(hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (f ⊔ g) s :=

λ x hx y hy h, sup_le_sup (hf hx hy h) (hg hx hy h)

protected lemma inf [preorder α] [semilattice_inf β] {f g : α → β} {s : set α}

(hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (f ⊓ g) s :=

(hf.dual.sup hg.dual).dual

protected lemma max [preorder α] [linear_order β] {f g : α → β} {s : set α}

(hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (λ x, max (f x) (g x)) s :=

hf.sup hg

protected lemma min [preorder α] [linear_order β] {f g : α → β} {s : set α}

(hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (λ x, min (f x) (g x)) s :=

hf.inf hg

lemma of_map_inf [semilattice_inf α] [semilattice_sup β]

(h : ∀ (x ∈ s) (y ∈ s), f (x ⊓ y) = f x ⊔ f y) : antitone_on f s :=

λ x hx y hy hxy, sup_eq_left.1 $ by rw [←h _ hx _ hy, inf_eq_left.2 hxy]

lemma of_map_sup [semilattice_sup α] [semilattice_inf β]

(h : ∀ (x ∈ s) (y ∈ s), f (x ⊔ y) = f x ⊓ f y) : antitone_on f s :=

(@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual

variables [linear_order α]

lemma map_sup [semilattice_inf β] (hf : antitone_on f s) (hx : x ∈ s) (hy : y ∈ s) :

f (x ⊔ y) = f x ⊓ f y :=

by cases le_total x y; have := hf _ _ h; assumption <|>

simp only [h, this, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

lemma map_inf [semilattice_sup β] (hf : antitone_on f s) (hx : x ∈ s) (hy : y ∈ s) :

f (x ⊓ y) = f x ⊔ f y :=

hf.dual.map_sup hx hy

end antitone_on

namespace prod

variables (α β)

instance [has_sup α] [has_sup β] : has_sup (α × β) := ⟨λp q, ⟨p.1 ⊔ q.1, p.2 ⊔ q.2⟩⟩

instance [has_inf α] [has_inf β] : has_inf (α × β) := ⟨λp q, ⟨p.1 ⊓ q.1, p.2 ⊓ q.2⟩⟩

@[simp] lemma mk_sup_mk [has_sup α] [has_sup β] (a₁ a₂ : α) (b₁ b₂ : β) :

(a₁, b₁) ⊔ (a₂, b₂) = (a₁ ⊔ a₂, b₁ ⊔ b₂) := rfl

@[simp] lemma mk_inf_mk [has_inf α] [has_inf β] (a₁ a₂ : α) (b₁ b₂ : β) :

(a₁, b₁) ⊓ (a₂, b₂) = (a₁ ⊓ a₂, b₁ ⊓ b₂) := rfl

@[simp] lemma fst_sup [has_sup α] [has_sup β] (p q : α × β) : (p ⊔ q).fst = p.fst ⊔ q.fst := rfl

@[simp] lemma fst_inf [has_inf α] [has_inf β] (p q : α × β) : (p ⊓ q).fst = p.fst ⊓ q.fst := rfl

@[simp] lemma snd_sup [has_sup α] [has_sup β] (p q : α × β) : (p ⊔ q).snd = p.snd ⊔ q.snd := rfl

@[simp] lemma snd_inf [has_inf α] [has_inf β] (p q : α × β) : (p ⊓ q).snd = p.snd ⊓ q.snd := rfl

@[simp] lemma swap_sup [has_sup α] [has_sup β] (p q : α × β) : (p ⊔ q).swap = p.swap ⊔ q.swap := rfl