Lean4
instance nonUnitalRing [Semigroup α] : NonUnitalRing (FreeAbelianGroup α) :=
{ FreeAbelianGroup.nonUnitalNonAssocRing with
mul_assoc := fun x y z ↦
by
refine
FreeAbelianGroup.induction_on z (by simp only [mul_zero]) (fun L3 ↦ ?_) (fun L3 ih ↦ ?_) fun z₁ z₂ ih₁ ih₂ ↦ ?_
· refine
FreeAbelianGroup.induction_on y (by simp only [mul_zero, zero_mul]) (fun L2 ↦ ?_) (fun L2 ih ↦ ?_)
fun y₁ y₂ ih₁ ih₂ ↦ ?_
· refine
FreeAbelianGroup.induction_on x (by simp only [zero_mul]) (fun L1 ↦ ?_) (fun L1 ih ↦ ?_) fun x₁ x₂ ih₁ ih₂ ↦
?_
· rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
· rw [neg_mul, neg_mul, neg_mul, ih]
· rw [add_mul, add_mul, add_mul, ih₁, ih₂]
· rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
· rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
· rw [mul_neg, mul_neg, mul_neg, ih]
· rw [mul_add, mul_add, mul_add, ih₁, ih₂] }
