Lean4
instance : AddMonoid (Completion α) :=
{ (inferInstance : Zero <| Completion α),
(inferInstance :
Add <|
Completion
α) with
zero_add := fun a ↦
Completion.induction_on a (isClosed_eq (continuous_map₂ continuous_const continuous_id) continuous_id) fun a ↦
show 0 + (a : Completion α) = a by rw [← coe_zero, ← coe_add, zero_add]
add_zero := fun a ↦
Completion.induction_on a (isClosed_eq (continuous_map₂ continuous_id continuous_const) continuous_id) fun a ↦
show (a : Completion α) + 0 = a by rw [← coe_zero, ← coe_add, add_zero]
add_assoc := fun a b c ↦
Completion.induction_on₃ a b c
(isClosed_eq
(continuous_map₂ (continuous_map₂ continuous_fst (continuous_fst.comp continuous_snd))
(continuous_snd.comp continuous_snd))
(continuous_map₂ continuous_fst
(continuous_map₂ (continuous_fst.comp continuous_snd) (continuous_snd.comp continuous_snd))))
fun a b c ↦ show (a : Completion α) + b + c = a + (b + c) by repeat' rw_mod_cast [add_assoc]
nsmul := (· • ·)
nsmul_zero := fun a ↦
Completion.induction_on a (isClosed_eq continuous_map continuous_const) fun a ↦
show 0 • (a : Completion α) = 0 by rw [← coe_smul, ← coe_zero, zero_smul]
nsmul_succ := fun n a ↦
Completion.induction_on a (isClosed_eq continuous_map <| continuous_map₂ continuous_map continuous_id) fun a ↦
show (n + 1) • (a : Completion α) = n • (a : Completion α) + (a : Completion α) by
rw [← coe_smul, succ_nsmul, coe_add, coe_smul] }
