R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) -
      4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    0
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)
rw [← sub_eq_zero]
no goals
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) -
      4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    0
repeat'
  ring_nf
  simp only [A₁_inv, B₁_inv, sub_eq_add_neg, add_mul, mul_add, sub_mul, mul_sub, add_assoc,
    neg_add, neg_sub, sub_add, sub_sub, neg_mul, ← sq, A₀_inv, B₀_inv, ← sq, ← mul_assoc, one_mul,
    mul_one, add_right_neg, add_zero, sub_eq_add_neg, A₀_inv, mul_one, add_right_neg,
    MulZeroClass.zero_mul]
no goals
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ -4 + (B₀ * B₁ * 2 + (1 ^ 2 + (1 ^ 2 + (-(B₀ * B₁ * 2) + (1 ^ 2 + 1 ^ 2))))) = 0
ring_nf