Lean4
instance : SubNegMonoid (Completion α) :=
{ (inferInstance : AddMonoid <| Completion α), (inferInstance : Neg <| Completion α),
(inferInstance :
Sub <|
Completion
α) with
sub_eq_add_neg := fun a b ↦
Completion.induction_on₂ a b
(isClosed_eq (continuous_map₂ continuous_fst continuous_snd)
(continuous_map₂ continuous_fst (Completion.continuous_map.comp continuous_snd)))
fun a b ↦ mod_cast congr_arg ((↑) : α → Completion α) (sub_eq_add_neg a b)
zsmul := (· • ·)
zsmul_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]
zsmul_succ' := fun n a ↦
Completion.induction_on a (isClosed_eq continuous_map <| continuous_map₂ continuous_map continuous_id) fun a ↦
show (n.succ : ℤ) • (a : Completion α) = _ by
rw [← coe_smul, show (n.succ : ℤ) • a = (n : ℤ) • a + a from SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
zsmul_neg' := fun n a ↦
Completion.induction_on a (isClosed_eq continuous_map <| Completion.continuous_map.comp continuous_map) fun a ↦
show (Int.negSucc n) • (a : Completion α) = _ by
rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from SubNegMonoid.zsmul_neg' n a, coe_neg,
coe_smul] }
