Lean4
instance (priority := 100) toSubtractionMonoid : SubtractionMonoid α
where
neg_neg
a := by
by_cases h : a = ⊤
· simp [h]
· have h2 : ¬-a = ⊤ := fun nh ↦ h <| neg_eq_top.mp nh
replace h2 : a + (-a + - -a) = a + 0 := congrArg (a + ·) (add_neg_cancel_of_ne_top h2)
rw [← add_assoc, add_neg_cancel_of_ne_top h] at h2
simp only [zero_add, add_zero] at h2
exact h2
neg_add_rev a
b := by
by_cases ha : a = ⊤
· simp [ha]
by_cases hb : b = ⊤
· simp [hb]
apply (_ : Function.Injective (a + b + ·))
· dsimp
rw [add_neg_cancel_of_ne_top, ← add_assoc, add_assoc a, add_neg_cancel_of_ne_top hb, add_zero,
add_neg_cancel_of_ne_top ha]
simp [ha, hb]
· apply Function.LeftInverse.injective (g := (-(a + b) + ·))
intro x
dsimp only
rw [← add_assoc, add_comm (-(a + b)), add_neg_cancel_of_ne_top, zero_add]
simp [ha, hb]
neg_eq_of_add a b
h := by
have oh := congrArg (-a + ·) h
dsimp only at oh
rw [add_zero, ← add_assoc, add_comm (-a), add_neg_cancel_of_ne_top, zero_add] at oh
· exact oh.symm
intro v
simp [v] at h
