Theorem: QuadRing.coe_mul (ECTate/Algebra/QuadRing/Basic.lean)

State before:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : F
⊢ { b1 := r * s, b2 := 0 } = { b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }
Tactic:
apply (QuadRing.ext_iff _ _).2
State after:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : F
⊢ { b1 := r * s, b2 := 0 }.b1 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b1 ∧
    { b1 := r * s, b2 := 0 }.b2 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b2

State before:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : F
⊢ { b1 := r * s, b2 := 0 }.b1 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b1 ∧
    { b1 := r * s, b2 := 0 }.b2 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b2
Tactic:
simp [mul_comm]
State after:
no goals