unnecessary suffering in galois insertion

Stream: maths

[Kevin Buzzard]

/-- A Galois insertion is a Galois connection where `l ∘ u = id`. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. -/
structure galois_insertion {α β : Type*} [preorder α] [preorder β] (l : α → β) (u : β → α) :=
(choice : Πx:α, u (l x) ≤ x → β)
(gc : galois_connection l u)
(le_l_u : ∀x, x ≤ l (u x))
(choice_eq : ∀a h, choice a h = l a)

Why not choice : Πx:α, u (l x) ≤ x → β := lam a h, l a and choice_eq : ∀a h, choice a h = l a := rfl like in

set_option auto_param.check_exists false
/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
class preorder (α : Type u) extends has_le α, has_lt α :=
(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) . order_laws_tac)

? Looking through mathlib this seems to be a common situation and it would save users from having to write these two extra lines. Is this worth a PR or are there subtleties I'm missing? Do I need a . refl_tac or something?

[Mario Carneiro]

order_laws_tac is just a simple tactic that does try {refl}

[Mario Carneiro]

unfortunately you can't pass a tactic expression there, only the name of a previously defined tactic, so that's why it's order_laws_tac

[Mario Carneiro]

You can't put := rfl because that doesn't typecheck

[Kevin Buzzard]

Oh of course. But if I use order_laws_tac then is there anything particularly wrong with this? I'm just teaching someone about closures and told them to make a Galois insertion and it was just more complicated than I'd expected.