Lean4
instance : KleeneAlgebra (Language α) :=
{ instSemiring, instCompleteAtomicBooleanAlgebra with kstar := fun L ↦ L∗,
one_le_kstar := fun a _ hl ↦ ⟨[], hl, by simp⟩,
mul_kstar_le_kstar := fun a ↦ (one_add_self_mul_kstar_eq_kstar a).le.trans' le_sup_right,
kstar_mul_le_kstar := fun a ↦ (one_add_kstar_mul_self_eq_kstar a).le.trans' le_sup_right,
kstar_mul_le_self := fun l m h ↦ by
rw [kstar_eq_iSup_pow, iSup_mul]
refine iSup_le (fun n ↦ ?_)
induction n with
| zero => simp
| succ n ih =>
rw [pow_succ, mul_assoc (l ^ n) l m]
exact le_trans (le_mul_congr le_rfl h) ih,
mul_kstar_le_self := fun l m h ↦ by
rw [kstar_eq_iSup_pow, mul_iSup]
refine iSup_le (fun n ↦ ?_)
induction n with
| zero => simp
| succ n ih =>
rw [pow_succ, ← mul_assoc m (l ^ n) l]
exact le_trans (le_mul_congr ih le_rfl) h }
