The { } structure constructor is taking far longer than `mk` for some reason

slow.lean

-- see https://github.com/leanprover-community/mathlib4/pull/1099#discussion_r1051747996
import Mathlib.Mathport.Notation -- I don't understand this file well enough to remove it, but it's only notation

set_option autoImplicit false

universe u v

instance {ι : Type u} {α : ι → Type v} [∀ i, LE (α i)] : LE (∀ i, α i) where
  le x y := ∀ i, x i ≤ y i

class Top (α : Type u) where
  /-- The top (`⊤`, `\top`) element -/
  top : α

/-- Typeclass for the `⊥` (`\bot`) notation -/
class Bot (α : Type u) where
  /-- The bot (`⊥`, `\bot`) element -/
  bot : α

/-- The top (`⊤`, `\top`) element -/
notation "⊤" => Top.top

/-- The bot (`⊥`, `\bot`) element -/
notation "⊥" => Bot.bot


class Preorder (α : Type u) extends LE α, LT α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
  lt := λ a b => a ≤ b ∧ ¬ b ≤ a
  lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := by intros; rfl

class PartialOrder (α : Type u) extends Preorder α :=
(le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)

def Set (α : Type u) := α → Prop

def setOf {α : Type u} (p : α → Prop) : Set α :=
p

namespace Set

variable {α ι : Type _}

/-- Membership in a set -/
protected def Mem (a : α) (s : Set α) : Prop :=
s a

instance : Membership α (Set α) :=
⟨Set.Mem⟩

def range (f : ι → α) : Set α :=
  setOf (λ x => ∃ y, f y = x)

end Set

class InfSet (α : Type _) where
  infₛ : Set α → α

class SupSet (α : Type _) where
  supₛ : Set α → α

export SupSet (supₛ)

export InfSet (infₛ)

open Set

def supᵢ {α : Type _} [SupSet α] {ι} (s : ι → α) : α :=
  supₛ (range s)

def infᵢ {α : Type _} [InfSet α] {ι} (s : ι → α) : α :=
  infₛ (range s)

open Std.ExtendedBinder in
syntax "⨆ " extBinder ", " term:51 : term

macro_rules
  | `(⨆ $x:ident, $p) => `(supᵢ fun $x:ident ↦ $p)
  | `(⨆ $x:ident : $t, $p) => `(supᵢ fun $x:ident : $t ↦ $p)
  | `(⨆ $x:ident $b:binderPred, $p) =>
    `(supᵢ fun $x:ident ↦ satisfiesBinderPred% $x $b ∧ $p)

notation3 "⨅ "(...)", "r:(scoped f => infᵢ f) => r

class HasSup (α : Type u) where
  /-- Least upper bound (`\lub` notation) -/
  sup : α → α → α

class HasInf (α : Type u) where
  /-- Greatest lower bound (`\glb` notation) -/
  inf : α → α → α

@[inherit_doc]
infixl:68 " ⊔ " => HasSup.sup

@[inherit_doc]
infixl:69 " ⊓ " => HasInf.inf

class SemilatticeSup (α : Type u) extends HasSup α, PartialOrder α where
  /-- The supremum is an upper bound on the first argument -/
  protected le_sup_left : ∀ a b : α, a ≤ a ⊔ b
  /-- The supremum is an upper bound on the second argument -/
  protected le_sup_right : ∀ a b : α, b ≤ a ⊔ b
  /-- The supremum is the *least* upper bound -/
  protected sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c

class SemilatticeInf (α : Type u) extends HasInf α, PartialOrder α where
  /-- The infimum is a lower bound on the first argument -/
  protected inf_le_left : ∀ a b : α, a ⊓ b ≤ a
  /-- The infimum is a lower bound on the second argument -/
  protected inf_le_right : ∀ a b : α, a ⊓ b ≤ b
  /-- The infimum is the *greatest* lower bound -/
  protected le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c

class Lattice (α : Type u) extends SemilatticeSup α, SemilatticeInf α

class CompleteSemilatticeInf (α : Type _) extends PartialOrder α, InfSet α where
  /-- Any element of a set is more than the set infimum. -/
  infₛ_le : ∀ s, ∀ a ∈ s, infₛ s ≤ a
  /-- Any lower bound is less than the set infimum. -/
  le_infₛ : ∀ s a, (∀ b ∈ s, a ≤ b) → a ≤ infₛ s

class CompleteSemilatticeSup (α : Type _) extends PartialOrder α, SupSet α where
  /-- Any element of a set is less than the set supremum. -/
  le_supₛ : ∀ s, ∀ a ∈ s, a ≤ supₛ s
  /-- Any upper bound is more than the set supremum. -/
  supₛ_le : ∀ s a, (∀ b ∈ s, b ≤ a) → supₛ s ≤ a

class CompleteLattice (α : Type _) extends Lattice α, CompleteSemilatticeSup α,
  CompleteSemilatticeInf α, Top α, Bot α where
  /-- Any element is less than the top one. -/
  protected le_top : ∀ x : α, x ≤ ⊤
  /-- Any element is more than the bottom one. -/
  protected bot_le : ∀ x : α, ⊥ ≤ x

class Frame (α : Type _) extends CompleteLattice α where

class Coframe (α : Type _) extends CompleteLattice α where
  infᵢ_sup_le_sup_infₛ (a : α) (s : Set α) : (⨅ b, a ⊔ b) ≤ a ⊔ infₛ s -- should be ⨅ b ∈ s but I had problems with notation

class CompleteDistribLattice (α : Type _) extends Frame α where
  infᵢ_sup_le_sup_infₛ : ∀ a s, (⨅ b, a ⊔ b) ≤ a ⊔ infₛ s

-- See note [lower instance priority]
instance (priority := 100) CompleteDistribLattice.toCoframe {α : Type _} [CompleteDistribLattice α] :
    Coframe α :=
  { ‹CompleteDistribLattice α› with }

class OrderTop (α : Type u) [LE α] extends Top α where
  /-- `⊤` is the greatest element -/
  le_top : ∀ a : α, a ≤ ⊤

class OrderBot (α : Type u) [LE α] extends Bot α where
  /-- `⊥` is the least element -/
  bot_le : ∀ a : α, ⊥ ≤ a

class BoundedOrder (α : Type u) [LE α] extends OrderTop α, OrderBot α

instance(priority := 100) CompleteLattice.toBoundedOrder  {α : Type _} [h : CompleteLattice α] :
    BoundedOrder α :=
  { h with }

section

variable {α : Type _} [CompleteSemilatticeSup α] {s t : Set α} {a b : α}

-- --@[ematch] Porting note: attribute removed  Porting note: attribute removed
theorem le_supₛ : a ∈ s → a ≤ supₛ s :=
  CompleteSemilatticeSup.le_supₛ s a

theorem supₛ_le : (∀ b ∈ s, b ≤ a) → supₛ s ≤ a :=
  CompleteSemilatticeSup.supₛ_le s a

end

section

variable {α : Type _} [CompleteSemilatticeInf α] {s t : Set α} {a b : α}

-- --@[ematch] Porting note: attribute removed  Porting note: attribute removed
theorem infₛ_le : a ∈ s → infₛ s ≤ a :=
  CompleteSemilatticeInf.infₛ_le s a

theorem le_infₛ : (∀ b ∈ s, a ≤ b) → a ≤ infₛ s :=
  CompleteSemilatticeInf.le_infₛ s a

end

section

variable {α ι : Type _} [CompleteLattice α] {f g s t : ι → α} {a b : α}

theorem le_supᵢ (f : ι → α) (i : ι) : f i ≤ supᵢ f :=
  le_supₛ ⟨i, rfl⟩

theorem infᵢ_le (f : ι → α) (i : ι) : infᵢ f ≤ f i :=
  infₛ_le ⟨i, rfl⟩

-- --@[ematch] Porting note: attribute removed Porting note
theorem le_supᵢ' (f : ι → α) (i : ι) : f i ≤ supᵢ f :=
  le_supₛ ⟨i, rfl⟩

----@[ematch] Porting note: attribute removed Porting note: attribute removed
theorem infᵢ_le' (f : ι → α) (i : ι) : infᵢ f ≤ f i :=
  infₛ_le ⟨i, rfl⟩

theorem supᵢ_le (h : ∀ i, f i ≤ a) : supᵢ f ≤ a :=
  supₛ_le fun _ ⟨i, Eq⟩ => Eq ▸ h i

theorem le_infᵢ (h : ∀ i, a ≤ f i) : a ≤ infᵢ f :=
  le_infₛ fun _ ⟨i, Eq⟩ => Eq ▸ h i

end section

namespace Pi

variable {ι : Type _} {α' : ι → Type _}

instance [∀ i, Bot (α' i)] : Bot (∀ i, α' i) :=
  ⟨fun _ => ⊥⟩

@[simp]
theorem bot_apply [∀ i, Bot (α' i)] (i : ι) : (⊥ : ∀ i, α' i) i = ⊥ :=
  rfl

theorem bot_def [∀ i, Bot (α' i)] : (⊥ : ∀ i, α' i) = fun _ => ⊥ :=
  rfl

instance [∀ i, Top (α' i)] : Top (∀ i, α' i) :=
  ⟨fun _ => ⊤⟩

@[simp]
theorem top_apply [∀ i, Top (α' i)] (i : ι) : (⊤ : ∀ i, α' i) i = ⊤ :=
  rfl

theorem top_def [∀ i, Top (α' i)] : (⊤ : ∀ i, α' i) = fun _ => ⊤ :=
  rfl

end Pi

section LE

variable {α : Type _} [LE α] [OrderTop α] {a : α}

@[simp]
theorem le_top : a ≤ ⊤ :=
  OrderTop.le_top a

end LE

section LE

variable {α : Type _} [LE α] [OrderBot α] {a : α}

@[simp]
theorem bot_le : ⊥ ≤ a :=
  OrderBot.bot_le a

end LE

section SemilatticeInf

variable {α : Type _} [SemilatticeInf α] {a b c d : α}

theorem inf_le_left : a ⊓ b ≤ a :=
  SemilatticeInf.inf_le_left a b

theorem inf_le_left' : a ⊓ b ≤ a :=
  SemilatticeInf.inf_le_left a b

theorem inf_le_right : a ⊓ b ≤ b :=
  SemilatticeInf.inf_le_right a b

theorem inf_le_right' : a ⊓ b ≤ b :=
  SemilatticeInf.inf_le_right a b

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

end SemilatticeInf

section SemilatticeSup

variable {α : Type _} [SemilatticeSup α] {a b c d : α}

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

-- Porting note: no ematch attribute
--@[ematch]
theorem le_sup_left' : a ≤ a ⊔ b :=
  le_sup_left

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

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

end SemilatticeSup

theorem le_refl {α : Type _} [Preorder α] : ∀ (a : α), a ≤ a :=
Preorder.le_refl

theorem le_trans {α : Type _} [Preorder α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
Preorder.le_trans _ _ _

theorem le_antisymm {α : Type _} [PartialOrder α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
PartialOrder.le_antisymm _ _

namespace Pi

variable {ι : Type _} {α' : ι → Type _}

protected instance LE {ι : Type u} {α : ι → Type v} [∀ i, LE (α i)] : LE (∀ i, α i) where
  le x y := ∀ i, x i ≤ y i

instance Preorder {ι : Type u} {α : ι → Type v} [∀ i, Preorder (α i)] : Preorder (∀ i, α i) :=
  { Pi.LE with
  le_refl := fun a i ↦ le_refl (a i)
  le_trans := fun a b c h₁ h₂ i ↦ le_trans (h₁ i) (h₂ i) }

instance PartialOrder {ι : Type u} {α : ι → Type v} [∀ i, PartialOrder (α i)] :
    PartialOrder (∀ i, α i) :=
  { Pi.Preorder with
  le_antisymm := fun _ _ h1 h2 ↦ funext fun b ↦ le_antisymm (h1 b) (h2 b) }

instance semilatticeSup [∀ i, SemilatticeSup (α' i)] : SemilatticeSup (∀ i, α' i) where
  le_sup_left _ _ _ := le_sup_left
  le_sup_right _ _ _ := le_sup_right
  sup_le _ _ _ ac bc i := sup_le (ac i) (bc i)

instance semilatticeInf [∀ i, SemilatticeInf (α' i)] : SemilatticeInf (∀ i, α' i) where
  inf_le_left _ _ _ := inf_le_left
  inf_le_right _ _ _ := inf_le_right
  le_inf _ _ _ ac bc i := le_inf (ac i) (bc i)

instance lattice [∀ i, Lattice (α' i)] : Lattice (∀ i, α' i) :=
{ Pi.semilatticeSup, Pi.semilatticeInf with }

instance orderTop [∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i) :=
  { inferInstanceAs (Top (∀ i, α' i)) with le_top := fun _ _ => le_top }

instance orderBot [∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i) :=
  { inferInstanceAs (Bot (∀ i, α' i)) with bot_le := fun _ _ => bot_le }

instance boundedOrder [∀ i, LE (α' i)] [∀ i, BoundedOrder (α' i)] : BoundedOrder (∀ i, α' i) :=
{ Pi.orderTop, Pi.orderBot with }

instance SupSet {α : Type _} {β : α → Type _} [∀ i, SupSet (β i)] : SupSet (∀ i, β i) :=
  sorry

instance InfSet {α : Type _} {β : α → Type _} [∀ i, InfSet (β i)] : InfSet (∀ i, β i) :=
  sorry

instance completeLattice {α : Type _} {β : α → Type _} [∀ i, CompleteLattice (β i)] :
    CompleteLattice (∀ i, β i) :=
  { Pi.boundedOrder, Pi.lattice with
    le_supₛ := sorry
    infₛ_le := sorry
    supₛ_le := sorry
    le_infₛ := sorry
  }

instance frame {ι : Type _} {π : ι → Type _} [∀ i, Frame (π i)] : Frame (∀ i, π i) :=
  { Pi.completeLattice with }

instance coframe {ι : Type _} {π : ι → Type _} [∀ i, Coframe (π i)] : Coframe (∀ i, π i) :=
  { Pi.completeLattice with infᵢ_sup_le_sup_infₛ := sorry }

end Pi

-- very quick
instance Pi.completeDistribLattice' {ι : Type _} {π : ι → Type _}
    [∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) :=
CompleteDistribLattice.mk (Pi.coframe.infᵢ_sup_le_sup_infₛ)

-- takes a long time
instance Pi.completeDistribLattice'' {ι : Type _} {π : ι → Type _}
    [∀ i, CompleteDistribLattice (π i)] : CompleteDistribLattice (∀ i, π i) :=
  { Pi.frame, Pi.coframe with }