-- Mathlib/LinearAlgebra/Basis/Basic.lean
/-- An element of a non-unital-non-associative algebra is in the center exactly when it commutes
with the basis elements. -/
lemma Basis.mem_center_iff {A}
    [Semiring R] [NonUnitalNonAssocSemiring A]
    [Module R A] [SMulCommClass R A A] [SMulCommClass R R A] [IsScalarTower R A A]
    (b : Basis ι R A) {z : A} :
    z ∈ Set.center A ↔
      (∀ i, Commute (b i) z) ∧ ∀ i j,
        z * (b i * b j) = (z * b i) * b j
          ∧ (b i * z) * b j = b i * (z * b j)
          ∧ (b i * b j) * z = b i * (b j * z)

Proof state:
case mpr.right_assoc
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a b : A), a * b * z = a * (b * z)

Tactic:
case right_assoc =>
  intro c d
  rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
      linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]
  simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
           Finset.smul_sum, smul_mul_assoc, mul_smul_comm, Finset.sum_mul, smul_mul_assoc,
           (h.2 _ _).2.2]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ i ∈ (b.repr d).support, (∑ i ∈ (b.repr c).support, (b.repr c) i • b i * z) * (b.repr d) i • b i =
    ∑ i ∈ (b.repr d).support, (∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * (z * (b.repr d) i • b i)

Tactic:
simp_rw [smul_mul_assoc, Finset.sum_mul, mul_smul_comm, smul_mul_assoc, (h.2 _ _).2.1]

Result:
no goals

Proof state:
case mpr.mid_assoc
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a c : A), a * z * c = a * (z * c)

case mpr.right_assoc
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a b : A), a * b * z = a * (b * z)

Tactic:
case mid_assoc =>
  intro c d
  rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
      linearCombination_apply, sum, sum, Finset.sum_mul, Finset.mul_sum, Finset.mul_sum,
      Finset.mul_sum]
  simp_rw [smul_mul_assoc, Finset.sum_mul, mul_smul_comm, smul_mul_assoc, (h.2 _ _).2.1]

Result:
case mpr.right_assoc
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a b : A), a * b * z = a * (b * z)

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ ∑ i ∈ (b.repr y).support, z * (b.repr y) i • b i = ∑ i ∈ (b.repr y).support, (b.repr y) i • b i * z

Tactic:
simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]

Result:
no goals

Proof state:
case mpr
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
⊢ ((∀ (i : ι), Commute (b i) z) ∧
      ∀ (i j : ι),
        z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)) →
    z ∈ center A

Tactic:
intro h

Result:
case mpr
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
⊢ z ∈ center A

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a : A), z * a = a * z

Tactic:
intro y

Result:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ z * y = y * z

Proof state:
case mp
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : z ∈ center A
⊢ (∀ (i : ι), Commute (b i) z) ∧
    ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)

Tactic:
constructor

Result:
case mp.left
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : z ∈ center A
⊢ ∀ (i : ι), Commute (b i) z

case mp.right
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : z ∈ center A
⊢ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)