partial_order (with_bot X) is so unrflly

Stream: general

[Kevin Buzzard]

From order.bounded_lattice:

instance partial_order [partial_order α] : partial_order (with_bot α) :=
{ le          := λ o₁ o₂ : option α, ∀ a ∈ o₁, ∃ b ∈ o₂, a ≤ b,
...

This definition of le on with_bot alpha means that stuff like a <= b iff some a <= some b is not proved by iff.rfl. If this proof had been done with pattern matching would this not have made life easier? Oh -- can one not pattern match in a structure field? Lean is complaining that my set_of is broken -- it thinks { ... | ... is a set.

[Mario Carneiro]

it is defined that way so that you don't have to deal with pattern matching on option all the time

[Kevin Buzzard]

import algebra.group order.bounded_lattice

variable {α : Type*}

instance meh [partial_order α] : partial_order (with_bot α) :=
{ le := λ o₁ o₂, match (o₁, o₂) with
         | (none, _) := true
         | (some x, none) := false
         | (some x, some y) := x ≤ y
         end,
--:= λ o₁ o₂ : option α, ∀ a ∈ o₁, ∃ b ∈ o₂, a ≤ b,
  le_refl := sorry,
  le_trans := sorry,
  le_antisymm := sorry
}

example [partial_order α] (x y : α) : (x : with_bot α) ≤ y ↔ x ≤ y := iff.rfl

[Kevin Buzzard]

But instead I'm having to deal with other things.

[Kevin Buzzard]

like having to use change then rw a lot