Lean4
/-- Relations for the enveloping group. This is a type-valued relation because
`toEnvelGroup.mapAux.well_def` inducts on it to show `toEnvelGroup.map`
is well-defined. The relation `PreEnvelGroupRel` is the `Prop`-valued version,
which is used to define `EnvelGroup` itself.
-/
inductive PreEnvelGroupRel' (R : Type u) [Rack R] : PreEnvelGroup R → PreEnvelGroup R → Type u
| refl {a : PreEnvelGroup R} : PreEnvelGroupRel' R a a
| symm {a b : PreEnvelGroup R} (hab : PreEnvelGroupRel' R a b) : PreEnvelGroupRel' R b a
|
trans {a b c : PreEnvelGroup R} (hab : PreEnvelGroupRel' R a b) (hbc : PreEnvelGroupRel' R b c) :
PreEnvelGroupRel' R a c
|
congr_mul {a b a' b' : PreEnvelGroup R} (ha : PreEnvelGroupRel' R a a') (hb : PreEnvelGroupRel' R b b') :
PreEnvelGroupRel' R (mul a b) (mul a' b')
| congr_inv {a a' : PreEnvelGroup R} (ha : PreEnvelGroupRel' R a a') : PreEnvelGroupRel' R (inv a) (inv a')
| assoc (a b c : PreEnvelGroup R) : PreEnvelGroupRel' R (mul (mul a b) c) (mul a (mul b c))
| one_mul (a : PreEnvelGroup R) : PreEnvelGroupRel' R (mul unit a) a
| mul_one (a : PreEnvelGroup R) : PreEnvelGroupRel' R (mul a unit) a
| inv_mul_cancel (a : PreEnvelGroup R) : PreEnvelGroupRel' R (mul (inv a) a) unit
| act_incl (x y : R) : PreEnvelGroupRel' R (mul (mul (incl x) (incl y)) (inv (incl x))) (incl (x ◃ y))
