Theorem: QuadRing.coe_add (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 = ({ 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
State after:
no goals