[GOAL]
A : Type u_1
inst✝¹ : Mul A
inst✝ : IsCommJordan A
a b : A
⊢ a * b * a = a * (b * a)
[PROOFSTEP]
rw [IsCommJordan.mul_comm, IsCommJordan.mul_comm a b]
[GOAL]
A : Type u_1
inst✝¹ : Mul A
inst✝ : IsCommJordan A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)
[PROOFSTEP]
rw [IsCommJordan.mul_comm (a * a) (a * b), IsCommJordan.lmul_comm_rmul_rmul, IsCommJordan.mul_comm b (a * a)]
[GOAL]
A : Type u_1
inst✝¹ : Mul A
inst✝ : IsCommJordan A
a b : A
⊢ a * a * (b * a) = a * a * b * a
[PROOFSTEP]
rw [IsCommJordan.mul_comm (a * a) (b * a), IsCommJordan.mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul,
  IsCommJordan.mul_comm, IsCommJordan.mul_comm b (a * a)]
[GOAL]
A : Type u_1
inst✝¹ : Mul A
inst✝ : IsCommJordan A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a
[PROOFSTEP]
rw [IsCommJordan.mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul, IsCommJordan.mul_comm]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * b * a = a * (b * a)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)
[PROOFSTEP]
rw [mul_assoc, mul_assoc]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * a * (b * a) = a * a * b * a
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * b * (a * a) = a * (b * (a * a))
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) = ⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆
[PROOFSTEP]
suffices 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0 by
  rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (b * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ = 0
⊢ 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) = ⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆
[PROOFSTEP]
rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (b * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ = 0
[PROOFSTEP]
convert (commute_lmul_lmul_sq (a + b)).lie_eq using 1
[GOAL]
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (b * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ =
    ⁅↑L (a + b), ↑L ((a + b) * (a + b))⁆
[PROOFSTEP]
simp only [add_mul, mul_add, map_add, lie_add, add_lie, IsCommJordan.mul_comm b a, (commute_lmul_lmul_sq a).lie_eq,
  (commute_lmul_lmul_sq b).lie_eq, zero_add, add_zero, two_smul]
[GOAL]
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ ⁅↑L a, ↑L (a * b)⁆ + ⁅↑L a, ↑L (a * b)⁆ + (⁅↑L b, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) + ⁅↑L b, ↑L (a * a)⁆ +
      ⁅↑L a, ↑L (b * b)⁆ =
    ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
      (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L a, ↑L (b * b)⁆)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b : A
⊢ ⁅↑L a, ↑L (a * b)⁆ + ⁅↑L a, ↑L (a * b)⁆ + (⁅↑L b, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) + ⁅↑L b, ↑L (a * a)⁆ +
      ⁅↑L a, ↑L (b * b)⁆ =
    ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
      (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L a, ↑L (b * b)⁆)
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L ((a + b + c) * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [add_mul, add_mul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * (a + b + c) + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
iterate 6 rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * (a + b + c) + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * (a + b) + a * c + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * (a + b) + b * c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + c * (a + b + c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * (a + b) + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [mul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
iterate 10 rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b) + ↑L c, ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a + a * b + a * c + (b * a + b * b + b * c)) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a + a * b + a * c) + ↑L (b * a + b * b + b * c) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a + a * b) + ↑L (a * c) + ↑L (b * a + b * b + b * c) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + ↑L (b * a + b * b + b * c) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (b * a + b * b) + ↑L (b * c)) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (b * a) + ↑L (b * b) + ↑L (b * c)) + ↑L (c * a + c * b + c * c)⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (b * a) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (c * a + c * b) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [map_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (b * a) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (c * a) + ↑L (c * b) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [IsCommJordan.mul_comm b a, IsCommJordan.mul_comm c a, IsCommJordan.mul_comm c b]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (a * c) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
iterate 3 rw [two_smul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (a * c) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [two_smul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + (↑L (a * b) + ↑L (a * b)) + 2 • ↑L (a * c) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [two_smul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + (↑L (a * b) + ↑L (a * b)) + (↑L (a * c) + ↑L (a * c)) + 2 • ↑L (b * c)⁆
[PROOFSTEP]
rw [two_smul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (a * b) + ↑L (a * c) + (↑L (a * b) + ↑L (b * b) + ↑L (b * c)) +
        (↑L (a * c) + ↑L (b * c) + ↑L (c * c))⁆ =
    ⁅↑L a + ↑L b + ↑L c,
      ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + (↑L (a * b) + ↑L (a * b)) + (↑L (a * c) + ↑L (a * c)) +
        (↑L (b * c) + ↑L (b * c))⁆
[PROOFSTEP]
simp only [lie_add, add_lie, commute_lmul_lmul_sq, zero_add, add_zero]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L c, ↑L (a * a)⁆ +
            (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆) +
        (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆ +
            (⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L c, ↑L (b * b)⁆) +
          (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆ +
          (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (c * c)⁆)) =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L c, ↑L (a * a)⁆ +
              (⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L c, ↑L (b * b)⁆) +
            (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (c * c)⁆) +
          (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆ +
            (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆)) +
        (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆ +
          (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆)) +
      (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆ +
        (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L c, ↑L (a * a)⁆ +
            (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆) +
        (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆ +
            (⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L c, ↑L (b * b)⁆) +
          (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆ +
          (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (c * c)⁆)) =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L b, ↑L (a * a)⁆ + ⁅↑L c, ↑L (a * a)⁆ +
              (⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L c, ↑L (b * b)⁆) +
            (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (c * c)⁆) +
          (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆ +
            (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆ + ⁅↑L c, ↑L (a * b)⁆)) +
        (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆ +
          (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L b, ↑L (a * c)⁆ + ⁅↑L c, ↑L (a * c)⁆)) +
      (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆ +
        (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a + ↑L b + ↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [add_lie, add_lie]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
iterate 15 rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a)⁆ + ⁅↑L a, 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ + ⁅↑L a, 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b) + ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a) + ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        ⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a)⁆ + ⁅↑L b, 2 • ↑L (b * c)⁆) +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b)⁆ + ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a) + ↑L (b * b) + ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ + ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a) + ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ + ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      ⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a) + 2 • ↑L (b * c)⁆ =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b) + 2 • ↑L (c * a)⁆ + ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c) + 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a) + ↑L (b * b) + ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a) + ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆)
[PROOFSTEP]
rw [lie_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (a * a)⁆ + ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ +
          ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (b * b)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ +
            ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, ↑L (c * c)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆)
[PROOFSTEP]
rw [(commute_lmul_lmul_sq a).lie_eq, (commute_lmul_lmul_sq b).lie_eq, (commute_lmul_lmul_sq c).lie_eq, zero_add,
  add_zero, add_zero]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + ⁅↑L a, 2 • ↑L (a * b)⁆ + ⁅↑L a, 2 • ↑L (c * a)⁆ + ⁅↑L a, 2 • ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (c * c)⁆ + ⁅↑L b, 2 • ↑L (a * b)⁆ + ⁅↑L b, 2 • ↑L (c * a)⁆ +
          ⁅↑L b, 2 • ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + ⁅↑L c, 2 • ↑L (a * b)⁆ + ⁅↑L c, 2 • ↑L (c * a)⁆ +
        ⁅↑L c, 2 • ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆)
[PROOFSTEP]
simp only [lie_nsmul]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L a, ↑L (c * a)⁆ + 2 • ⁅↑L a, ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (c * c)⁆ + 2 • ⁅↑L b, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ +
          2 • ⁅↑L b, ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆ + 2 • ⁅↑L c, ↑L (c * a)⁆ +
        2 • ⁅↑L c, ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆)
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L a, ↑L (c * c)⁆ + 2 • ⁅↑L a, ↑L (a * b)⁆ + 2 • ⁅↑L a, ↑L (c * a)⁆ + 2 • ⁅↑L a, ↑L (b * c)⁆ +
        (⁅↑L b, ↑L (a * a)⁆ + ⁅↑L b, ↑L (c * c)⁆ + 2 • ⁅↑L b, ↑L (a * b)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ +
          2 • ⁅↑L b, ↑L (b * c)⁆) +
      (⁅↑L c, ↑L (a * a)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆ + 2 • ⁅↑L c, ↑L (c * a)⁆ +
        2 • ⁅↑L c, ↑L (b * c)⁆) =
    ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆)
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
          (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
        (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) +
      (2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆) =
    2 • ⁅↑L a, ↑L (b * c)⁆ + 2 • ⁅↑L b, ↑L (c * a)⁆ + 2 • ⁅↑L c, ↑L (a * b)⁆
[PROOFSTEP]
rw [add_left_eq_self]
  -- Porting note: was `nth_rw` instead of `conv_lhs`
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) =
    0
[PROOFSTEP]
conv_lhs => enter [1, 1, 2, 2, 2]; rw [IsCommJordan.mul_comm a b]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
      (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
    (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
enter [1, 1, 2, 2, 2]; rw [IsCommJordan.mul_comm a b]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
      (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
    (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
enter [1, 1, 2, 2, 2]; rw [IsCommJordan.mul_comm a b]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (a * b)⁆) +
      (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
    (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
enter [1, 1, 2, 2, 2]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L b, ↑L (a * b)⁆
[PROOFSTEP]
rw [IsCommJordan.mul_comm a b]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) =
    0
[PROOFSTEP]
conv_lhs => enter [1, 2, 2, 2, 1]; rw [IsCommJordan.mul_comm c a]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
      (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
    (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
enter [1, 2, 2, 2, 1]; rw [IsCommJordan.mul_comm c a]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
      (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
    (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
enter [1, 2, 2, 2, 1]; rw [IsCommJordan.mul_comm c a]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
      (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (c * a)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
    (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
enter [1, 2, 2, 2, 1]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (c * a)⁆
[PROOFSTEP]
rw [IsCommJordan.mul_comm c a]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆)) =
    0
[PROOFSTEP]
conv_lhs => enter [2, 2, 2, 2]; rw [IsCommJordan.mul_comm b c]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
      (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
    (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
enter [2, 2, 2, 2]; rw [IsCommJordan.mul_comm b c]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
      (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
    (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
enter [2, 2, 2, 2]; rw [IsCommJordan.mul_comm b c]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
      (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
    (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (b * c)⁆))
[PROOFSTEP]
enter [2, 2, 2, 2]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
| ⁅↑L c, ↑L (b * c)⁆
[PROOFSTEP]
rw [IsCommJordan.mul_comm b c]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (c * b)⁆)) =
    0
[PROOFSTEP]
iterate 3 rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * b)⁆ + ⁅↑L b, ↑L (b * a)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (c * b)⁆)) =
    0
[PROOFSTEP]
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + 2 • (⁅↑L a, ↑L (a * c)⁆ + ⁅↑L c, ↑L (c * a)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (c * b)⁆)) =
    0
[PROOFSTEP]
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L c⁆ + ⁅↑L (c * c), ↑L a⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + 2 • (⁅↑L b, ↑L (b * c)⁆ + ⁅↑L c, ↑L (c * b)⁆)) =
    0
[PROOFSTEP]
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L c⁆ + ⁅↑L (c * c), ↑L a⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (⁅↑L (b * b), ↑L c⁆ + ⁅↑L (c * c), ↑L b⁆)) =
    0
[PROOFSTEP]
iterate 2 rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L b⁆ + ⁅↑L (b * b), ↑L a⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L c⁆ + ⁅↑L (c * c), ↑L a⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (⁅↑L (b * b), ↑L c⁆ + ⁅↑L (c * c), ↑L b⁆)) =
    0
[PROOFSTEP]
rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (-⁅↑L b, ↑L (a * a)⁆ + -⁅↑L a, ↑L (b * b)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (⁅↑L (a * a), ↑L c⁆ + -⁅↑L a, ↑L (c * c)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (⁅↑L (b * b), ↑L c⁆ + ⁅↑L (c * c), ↑L b⁆)) =
    0
[PROOFSTEP]
rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (-⁅↑L b, ↑L (a * a)⁆ + -⁅↑L a, ↑L (b * b)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (-⁅↑L c, ↑L (a * a)⁆ + -⁅↑L a, ↑L (c * c)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (-⁅↑L c, ↑L (b * b)⁆ + -⁅↑L b, ↑L (c * c)⁆)) =
    0
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L a, ↑L (b * b)⁆ + ⁅↑L b, ↑L (a * a)⁆ + (-⁅↑L b, ↑L (a * a)⁆ + -⁅↑L a, ↑L (b * b)⁆) +
        (⁅↑L a, ↑L (c * c)⁆ + ⁅↑L c, ↑L (a * a)⁆ + (-⁅↑L c, ↑L (a * a)⁆ + -⁅↑L a, ↑L (c * c)⁆)) +
      (⁅↑L b, ↑L (c * c)⁆ + ⁅↑L c, ↑L (b * b)⁆ + (-⁅↑L c, ↑L (b * b)⁆ + -⁅↑L b, ↑L (c * c)⁆)) =
    0
[PROOFSTEP]
abel
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 2 • (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (c * a)⁆ + ⁅↑L c, ↑L (a * b)⁆) = 0
[PROOFSTEP]
symm
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = 2 • (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (c * a)⁆ + ⁅↑L c, ↑L (a * b)⁆)
[PROOFSTEP]
calc
  0 = ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ := by rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]
  _ = _ := by rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = ⁅↑L (a + b + c), ↑L ((a + b + c) * (a + b + c))⁆
[PROOFSTEP]
rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]
[GOAL]
A : Type u_1
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅↑L (a + b + c), ↑L ((a + b + c) * (a + b + c))⁆ = 2 • (⁅↑L a, ↑L (b * c)⁆ + ⁅↑L b, ↑L (c * a)⁆ + ⁅↑L c, ↑L (a * b)⁆)
[PROOFSTEP]
rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]


[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (r • ↑↑ₐ s - a)
⊢ (↑↑ₐ s - r⁻¹ • a) * r • ↑(IsUnit.unit h)⁻¹ = 1
[PROOFSTEP]
rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (r • ↑↑ₐ s - a)
⊢ r • ↑(IsUnit.unit h)⁻¹ * (↑↑ₐ s - r⁻¹ • a) = 1
[PROOFSTEP]
rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ ¬r ∈ σ a ↔ IsUnit (↑↑ₐ r - a)
[PROOFSTEP]
apply not_iff_not.mp
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ ¬¬r ∈ σ a ↔ ¬IsUnit (↑↑ₐ r - a)
[PROOFSTEP]
simp [Set.not_not_mem, mem_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ 0 ∈ σ a ↔ ¬IsUnit a
[PROOFSTEP]
rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ ¬0 ∈ σ a ↔ IsUnit a
[PROOFSTEP]
rw [zero_mem_iff, Classical.not_not]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a b c : A
h₁ : (↑↑ₐ r - a) * b = 1
h₂ : c * (↑↑ₐ r - a) = 1
⊢ b * (↑↑ₐ r - a) = 1
[PROOFSTEP]
rwa [← left_inv_eq_right_inv h₂ h₁]
[GOAL]
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ resolventSet R a = univ
[PROOFSTEP]
simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.setOf_true]
[GOAL]
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ σ a = ∅
[PROOFSTEP]
rw [spectrum, resolventSet_of_subsingleton, Set.compl_univ]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
[PROOFSTEP]
by_cases h : s ∈ spectrum R a
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
[PROOFSTEP]
rw [mem_iff] at h
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (↑↑ₐ s - a)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
[PROOFSTEP]
simp only [resolvent, Algebra.algebraMap_eq_smul_one] at *
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse ((r⁻¹ • s) • 1 - r⁻¹ • a)
[PROOFSTEP]
rw [smul_assoc, ← smul_sub]
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))
[PROOFSTEP]
have h' : ¬IsUnit (r⁻¹ • (s • (1 : A) - a)) := fun hu => h (by simpa only [smul_inv_smul] using IsUnit.smul r hu)
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
hu : IsUnit (r⁻¹ • (s • 1 - a))
⊢ IsUnit (s • 1 - a)
[PROOFSTEP]
simpa only [smul_inv_smul] using IsUnit.smul r hu
[GOAL]
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
h' : ¬IsUnit (r⁻¹ • (s • 1 - a))
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))
[PROOFSTEP]
simp only [Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ h', smul_zero]
[GOAL]
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
[PROOFSTEP]
simp only [resolvent]
[GOAL]
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ r • Ring.inverse (↑↑ₐ s - a) = Ring.inverse (↑↑ₐ (r⁻¹ • s) - r⁻¹ • a)
[PROOFSTEP]
have h' : IsUnit (r • algebraMap R A (r⁻¹ • s) - a) := by
  simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using not_mem_iff.mp h
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
⊢ IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
[PROOFSTEP]
simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using not_mem_iff.mp h
[GOAL]
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
h' : IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
⊢ r • Ring.inverse (↑↑ₐ s - a) = Ring.inverse (↑↑ₐ (r⁻¹ • s) - r⁻¹ • a)
[PROOFSTEP]
rw [← h'.subInvSMul_val, ← (not_mem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit, ←
  h'.subInvSMul.inv_eq_val_inv, h'.subInvSMul_inv]
[GOAL]
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬s ∈ σ a
h' : IsUnit (r • ↑↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑(IsUnit.unit (_ : IsUnit (↑↑ₐ s - a)))⁻¹ = r • ↑(IsUnit.unit h')⁻¹
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : A
⊢ r • resolvent a ↑r = resolvent (r⁻¹ • a) 1
[PROOFSTEP]
simpa only [Units.smul_def, Algebra.id.smul_eq_mul, Units.inv_mul] using @units_smul_resolvent _ _ _ _ _ r r a
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : ↑r ∈ resolventSet R ↑a
⊢ ↑r⁻¹ ∈ resolventSet R ↑a⁻¹
[PROOFSTEP]
rw [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, ← Units.smul_def] at h ⊢
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r⁻¹ • 1 - ↑a⁻¹)
[PROOFSTEP]
rw [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv, IsUnit.sub_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r • ↑a⁻¹ - 1)
[PROOFSTEP]
have h₁ : (a : A) * (r • (↑a⁻¹ : A) - 1) = r • (1 : A) - a := by rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
[PROOFSTEP]
rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ IsUnit (r • ↑a⁻¹ - 1)
[PROOFSTEP]
have h₂ : (r • (↑a⁻¹ : A) - 1) * a = r • (1 : A) - a := by rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
[PROOFSTEP]
rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
⊢ IsUnit (r • ↑a⁻¹ - 1)
[PROOFSTEP]
have hcomm : Commute (a : A) (r • (↑a⁻¹ : A) - 1) := by rwa [← h₂] at h₁
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
⊢ Commute (↑a) (r • ↑a⁻¹ - 1)
[PROOFSTEP]
rwa [← h₂] at h₁
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
hcomm : Commute (↑a) (r • ↑a⁻¹ - 1)
⊢ IsUnit (r • ↑a⁻¹ - 1)
[PROOFSTEP]
exact (hcomm.isUnit_mul_iff.mp (h₁.symm ▸ h)).2
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : Aˣ
⊢ 0 ∈ resolventSet R ↑a
[PROOFSTEP]
simpa only [mem_resolventSet_iff, ← not_mem_iff, zero_not_mem_iff] using a.isUnit
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r s : R
⊢ r + s ∈ σ a ↔ r ∈ σ (-↑↑ₐ s + a)
[PROOFSTEP]
simp only [mem_iff, sub_neg_eq_add, ← sub_sub, map_add]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r s : R
⊢ r + s ∈ σ (↑↑ₐ s + a) ↔ r ∈ σ a
[PROOFSTEP]
rw [add_mem_iff, neg_add_cancel_left]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
s : R
r : Rˣ
⊢ r • s ∈ σ (r • a) ↔ s ∈ σ a
[PROOFSTEP]
simp only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, smul_assoc, ← smul_sub, isUnit_smul_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
⊢ σ (r • a) = r • σ a
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
⊢ x ∈ σ (r • a) ↔ x ∈ r • σ a
[PROOFSTEP]
have x_eq : x = r • r⁻¹ • x := by simp
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
⊢ x = r • r⁻¹ • x
[PROOFSTEP]
simp
[GOAL]
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ x ∈ σ (r • a) ↔ x ∈ r • σ a
[PROOFSTEP]
nth_rw 1 [x_eq]
[GOAL]
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r • r⁻¹ • x ∈ σ (r • a) ↔ x ∈ r • σ a
[PROOFSTEP]
rw [smul_mem_smul_iff]
[GOAL]
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r⁻¹ • x ∈ σ a ↔ x ∈ r • σ a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r⁻¹ • x ∈ σ a → x ∈ r • σ a
[PROOFSTEP]
exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
h : r⁻¹ • x ∈ σ a
⊢ r • r⁻¹ • x = x
[PROOFSTEP]
simp
[GOAL]
case h.mpr
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ x ∈ r • σ a → r⁻¹ • x ∈ σ a
[PROOFSTEP]
rintro ⟨w, _, (x'_eq : r • w = x)⟩
[GOAL]
case h.mpr.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
w : R
left✝ : w ∈ σ a
x'_eq : r • w = x
⊢ r⁻¹ • x ∈ σ a
[PROOFSTEP]
simpa [← x'_eq]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
[PROOFSTEP]
have h₁ : ∀ x y : A, IsUnit (1 - x * y) → IsUnit (1 - y * x) :=
  by
  refine' fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, _, _⟩, rfl⟩
  calc
    (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
    _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
  calc
    (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
    _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
⊢ ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
[PROOFSTEP]
refine' fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, _, _⟩, rfl⟩
[GOAL]
case refine'_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1
case refine'_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1
[PROOFSTEP]
calc
  (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
  _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1 - y * x + y * ((1 - x * y) * (IsUnit.unit h).inv) * x
[PROOFSTEP]
noncomm_ring
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * ((1 - x * y) * (IsUnit.unit h).inv) * x = 1
[PROOFSTEP]
simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
[GOAL]
case refine'_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1
[PROOFSTEP]
calc
  (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
  _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1 - y * x + y * ((IsUnit.unit h).inv * (1 - x * y)) * x
[PROOFSTEP]
noncomm_ring
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * ((IsUnit.unit h).inv * (1 - x * y)) * x = 1
[PROOFSTEP]
simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
[PROOFSTEP]
have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
[PROOFSTEP]
rw [mul_smul_comm r⁻¹ b a] at this
[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
[PROOFSTEP]
simpa only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, ← Units.smul_def, IsUnit.smul_sub_iff_sub_inv_smul,
  smul_mul_assoc]
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : star r ∈ resolventSet R a
⊢ r ∈ resolventSet R (star a)
[PROOFSTEP]
simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul, star_star, star_one] using
  IsUnit.star h
[GOAL]
case refine'_2
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : r ∈ resolventSet R (star a)
⊢ star r ∈ resolventSet R a
[PROOFSTEP]
simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul, star_star, star_one] using
  IsUnit.star h
[GOAL]
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
a : A
⊢ σ (star a) = star (σ a)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
a : A
x✝ : R
⊢ x✝ ∈ σ (star a) ↔ x✝ ∈ star (σ a)
[PROOFSTEP]
simpa only [Set.mem_star, mem_iff, not_iff_not] using star_mem_resolventSet_iff.symm
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ x ∈ {r} + σ a ↔ x ∈ σ (↑↑ₐ r + a)
[PROOFSTEP]
rw [singleton_add, image_add_left, mem_preimage]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ (fun x x_1 => x + x_1) (-r) x ∈ σ a ↔ x ∈ σ (↑↑ₐ r + a)
[PROOFSTEP]
simp only
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ -r + x ∈ σ a ↔ x ∈ σ (↑↑ₐ r + a)
[PROOFSTEP]
rw [add_comm, add_mem_iff, map_neg, neg_neg]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
x : R
⊢ x ∈ -σ a ↔ x ∈ σ (-a)
[PROOFSTEP]
simp only [mem_neg, mem_iff, map_neg, ← neg_add', IsUnit.neg_iff, sub_neg_eq_add]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ {r} - σ a = σ (↑↑ₐ r - a)
[PROOFSTEP]
rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ σ a - {r} = σ (a - ↑↑ₐ r)
[PROOFSTEP]
simpa only [neg_sub, neg_eq] using congr_arg Neg.neg (singleton_sub_eq a r)
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 0 = {0}
[PROOFSTEP]
refine' Set.Subset.antisymm _ (by simp [Algebra.algebraMap_eq_smul_one, mem_iff])
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ {0} ⊆ σ 0
[PROOFSTEP]
simp [Algebra.algebraMap_eq_smul_one, mem_iff]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 0 ⊆ {0}
[PROOFSTEP]
rw [spectrum, Set.compl_subset_comm]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ {0}ᶜ ⊆ resolventSet 𝕜 0
[PROOFSTEP]
intro k hk
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ∈ {0}ᶜ
⊢ k ∈ resolventSet 𝕜 0
[PROOFSTEP]
rw [Set.mem_compl_singleton_iff] at hk
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ≠ 0
⊢ k ∈ resolventSet 𝕜 0
[PROOFSTEP]
have : IsUnit (Units.mk0 k hk • (1 : A)) := IsUnit.smul (Units.mk0 k hk) isUnit_one
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
hk : k ≠ 0
this : IsUnit (Units.mk0 k hk • 1)
⊢ k ∈ resolventSet 𝕜 0
[PROOFSTEP]
simpa [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
⊢ σ (↑↑ₐ k) = {k}
[PROOFSTEP]
rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 1 = σ (↑↑ₐ 1)
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one, one_smul]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : Set.Nonempty (σ a)
⊢ σ (k • a) = k • σ a
[PROOFSTEP]
rcases eq_or_ne k 0 with (rfl | h)
[GOAL]
case inl
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
ha : Set.Nonempty (σ a)
⊢ σ (0 • a) = 0 • σ a
[PROOFSTEP]
simpa [ha, zero_smul_set] using (show {(0 : 𝕜)} = (0 : Set 𝕜) from rfl)
[GOAL]
case inr
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : Set.Nonempty (σ a)
h : k ≠ 0
⊢ σ (k • a) = k • σ a
[PROOFSTEP]
exact unit_smul_eq_smul a (Units.mk0 k h)
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ σ (a * b) \ {0} = σ (b * a) \ {0}
[PROOFSTEP]
suffices h : ∀ x y : A, σ (x * y) \ {0} ⊆ σ (y * x) \ {0}
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
h : ∀ (x y : A), σ (x * y) \ {0} ⊆ σ (y * x) \ {0}
⊢ σ (a * b) \ {0} = σ (b * a) \ {0}
[PROOFSTEP]
exact Set.eq_of_subset_of_subset (h a b) (h b a)
[GOAL]
case h
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ ∀ (x y : A), σ (x * y) \ {0} ⊆ σ (y * x) \ {0}
[PROOFSTEP]
rintro _ _ k ⟨k_mem, k_neq⟩
[GOAL]
case h.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_mem : k ∈ σ (x✝ * y✝)
k_neq : ¬k ∈ {0}
⊢ k ∈ σ (y✝ * x✝) \ {0}
[PROOFSTEP]
change ((Units.mk0 k k_neq) : 𝕜) ∈ _ at k_mem
[GOAL]
case h.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_neq : ¬k ∈ {0}
k_mem : ↑(Units.mk0 k k_neq) ∈ σ (x✝ * y✝)
⊢ k ∈ σ (y✝ * x✝) \ {0}
[PROOFSTEP]
exact ⟨unit_mem_mul_iff_mem_swap_mul.mp k_mem, k_neq⟩
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
⊢ (σ ↑a)⁻¹ = σ ↑a⁻¹
[PROOFSTEP]
refine' Set.eq_of_subset_of_subset (fun k hk => _) fun k hk => _
[GOAL]
case refine'_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k ∈ (σ ↑a)⁻¹
⊢ k ∈ σ ↑a⁻¹
[PROOFSTEP]
rw [Set.mem_inv] at hk
[GOAL]
case refine'_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
⊢ k ∈ σ ↑a⁻¹
[PROOFSTEP]
have : k ≠ 0 := by simpa only [inv_inv] using inv_ne_zero (ne_zero_of_mem_of_unit hk)
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
⊢ k ≠ 0
[PROOFSTEP]
simpa only [inv_inv] using inv_ne_zero (ne_zero_of_mem_of_unit hk)
[GOAL]
case refine'_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
this : k ≠ 0
⊢ k ∈ σ ↑a⁻¹
[PROOFSTEP]
lift k to 𝕜ˣ using isUnit_iff_ne_zero.mpr this
[GOAL]
case refine'_1.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : (↑k)⁻¹ ∈ σ ↑a
this : ↑k ≠ 0
⊢ ↑k ∈ σ ↑a⁻¹
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val k] at hk
[GOAL]
case refine'_1.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : ↑k⁻¹ ∈ σ ↑a
this : ↑k ≠ 0
⊢ ↑k ∈ σ ↑a⁻¹
[PROOFSTEP]
exact inv_mem_iff.mp hk
[GOAL]
case refine'_2
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k ∈ σ ↑a⁻¹
⊢ k ∈ (σ ↑a)⁻¹
[PROOFSTEP]
lift k to 𝕜ˣ using isUnit_iff_ne_zero.mpr (ne_zero_of_mem_of_unit hk)
[GOAL]
case refine'_2.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : ↑k ∈ σ ↑a⁻¹
⊢ ↑k ∈ (σ ↑a)⁻¹
[PROOFSTEP]
simpa only [Units.val_inv_eq_inv_val] using inv_mem_iff.mp hk
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Ring B
inst✝¹ : Algebra R B
inst✝ : AlgHomClass F R A B
φ : F
a : A
r : R
h : r ∈ resolventSet R a
⊢ r ∈ resolventSet R (↑φ a)
[PROOFSTEP]
simpa only [map_sub, AlgHomClass.commutes] using h.map φ
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ ↑φ a ∈ σ a
[PROOFSTEP]
have h : ↑ₐ (φ a) - a ∈ RingHom.ker (φ : A →+* R) := by
  simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply,
    sub_self]
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ ↑↑ₐ (↑φ a) - a ∈ RingHom.ker ↑φ
[PROOFSTEP]
simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply,
  sub_self]
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
h : ↑↑ₐ (↑φ a) - a ∈ RingHom.ker ↑φ
⊢ ↑φ a ∈ σ a
[PROOFSTEP]
simp only [spectrum.mem_iff, ← mem_nonunits_iff, coe_subset_nonunits (RingHom.ker_ne_top (φ : A →+* R)) h]
[GOAL]
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Ring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : AlgEquivClass F R A B
f : F
a : A
⊢ spectrum R a ⊆ spectrum R (↑f a)
[PROOFSTEP]
simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
  AlgHom.spectrum_apply_subset (f : A ≃ₐ[R] B).symm (f a)


[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
x✝ :
  m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
⊢ 0 • m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa only [zero_smul] using p.zero_mem
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
a : A
b : B
hm :
  m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
⊢ a ⊗ₜ[R] b • m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa only [TensorProduct.Algebra.smul_def] using hA a (hB b hm)
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz :
  m ∈
      {
            toAddSubsemigroup :=
              { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
            zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier →
    z • m ∈
      {
            toAddSubsemigroup :=
              { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
            zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
hw :
  m ∈
      {
            toAddSubsemigroup :=
              { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
            zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier →
    w • m ∈
      {
            toAddSubsemigroup :=
              { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
            zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
hm :
  m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
⊢ (z + w) • m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa only [add_smul] using p.add_mem (hz hm) (hw hm)
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m ∈ p
[PROOFSTEP]
suffices a • m = a ⊗ₜ[R] (1 : B) • m by exact this.symm ▸ p.smul_mem _ hm
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
this : a • m = a ⊗ₜ[R] 1 • m
⊢ a • m ∈ p
[PROOFSTEP]
exact this.symm ▸ p.smul_mem _ hm
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m = a ⊗ₜ[R] 1 • m
[PROOFSTEP]
simp [TensorProduct.Algebra.smul_def]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m ∈ p
[PROOFSTEP]
suffices b • m = (1 : A) ⊗ₜ[R] b • m by exact this.symm ▸ p.smul_mem _ hm
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
this : b • m = 1 ⊗ₜ[R] b • m
⊢ b • m ∈ p
[PROOFSTEP]
exact this.symm ▸ p.smul_mem _ hm
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m = 1 ⊗ₜ[R] b • m
[PROOFSTEP]
simp [TensorProduct.Algebra.smul_def]


[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.1349, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
⊢ (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) y
[PROOFSTEP]
cases h
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.1349, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) x
[PROOFSTEP]
rfl
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
⊢ objEqToHom X h ≫ d X y =
    d X x ≫ objEqToHom X (_ : (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) y)
[PROOFSTEP]
cases h
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ objEqToHom X (_ : x = x) ≫ d X x =
    d X x ≫ objEqToHom X (_ : (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) x)
[PROOFSTEP]
dsimp
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ 𝟙 (obj X x) ≫ d X x = d X x ≫ 𝟙 (obj X (x + 1 • b))
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X✝ X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x y : β
h : x = y
⊢ objEqToHom X h ≫ Hom.f f y = Hom.f f x ≫ objEqToHom Y h
[PROOFSTEP]
cases h
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X✝ X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x : β
⊢ objEqToHom X (_ : x = x) ≫ Hom.f f x = Hom.f f x ≫ objEqToHom Y (_ : x = x)
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y z : β
h : y = z
⊢ d X x y ≫ eqToHom (_ : HomologicalComplex.X X y = HomologicalComplex.X X z) = d X x z
[PROOFSTEP]
cases h
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y : β
⊢ d X x y ≫ eqToHom (_ : HomologicalComplex.X X y = HomologicalComplex.X X y) = d X x y
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
h : i + b = j
⊢ i + 1 • b = j
[PROOFSTEP]
simp [h]
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
w : ¬ComplexShape.Rel (ComplexShape.up' b) i j
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i j = 0
[PROOFSTEP]
dsimp at w
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
w : ¬i + b = j
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i j = 0
[PROOFSTEP]
convert dif_neg w
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j k : β
hij : ComplexShape.Rel (ComplexShape.up' b) i j
hjk : ComplexShape.Rel (ComplexShape.up' b) j k
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i j ≫
      (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) j k =
    0
[PROOFSTEP]
dsimp at hij hjk
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j k : β
hij : i + b = j
hjk : j + b = k
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i j ≫
      (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) j k =
    0
[PROOFSTEP]
substs hij hjk
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i : β
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i (i + b) ≫
      (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) (i + b)
        (i + b + b) =
    0
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i j : β
h : ComplexShape.Rel (ComplexShape.up' b) i j
⊢ DifferentialObject.Hom.f f i ≫
      d
        ((fun X =>
            mk (fun i => obj X i) fun i j =>
              if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0)
          Y)
        i j =
    d
        ((fun X =>
            mk (fun i => obj X i) fun i j =>
              if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0)
          X)
        i j ≫
      DifferentialObject.Hom.f f j
[PROOFSTEP]
dsimp at h ⊢
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i j : β
h : i + b = j
⊢ (DifferentialObject.Hom.f f i ≫
      if h : i + b = j then DifferentialObject.d Y i ≫ objEqToHom Y (_ : i + 1 • b = j) else 0) =
    (if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) ≫
      DifferentialObject.Hom.f f j
[PROOFSTEP]
subst h
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i : β
⊢ (DifferentialObject.Hom.f f i ≫
      if h : i + b = i + b then DifferentialObject.d Y i ≫ objEqToHom Y (_ : i + 1 • b = i + b) else 0) =
    (if h : i + b = i + b then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = i + b) else 0) ≫
      DifferentialObject.Hom.f f (i + b)
[PROOFSTEP]
simp only [dite_true, Category.assoc, eqToHom_f']
  -- Porting note: this `rw` used to be part of the `simp`.
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i : β
⊢ DifferentialObject.Hom.f f i ≫ DifferentialObject.d Y i ≫ objEqToHom Y (_ : i + 1 • b = i + b) =
    DifferentialObject.d X i ≫ DifferentialObject.Hom.f f (i + 1 • b) ≫ objEqToHom Y (_ : i + 1 • b = i + b)
[PROOFSTEP]
have : f.f i ≫ Y.d i = X.d i ≫ f.f _ := (congr_fun f.comm i).symm
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i : β
this :
  DifferentialObject.Hom.f f i ≫ DifferentialObject.d Y i =
    DifferentialObject.d X i ≫ DifferentialObject.Hom.f f ((fun b_1 => b_1 + { as := 1 }.as • b) i)
⊢ DifferentialObject.Hom.f f i ≫ DifferentialObject.d Y i ≫ objEqToHom Y (_ : i + 1 • b = i + b) =
    DifferentialObject.d X i ≫ DifferentialObject.Hom.f f (i + 1 • b) ≫ objEqToHom Y (_ : i + 1 • b = i + b)
[PROOFSTEP]
rw [reassoc_of% this]