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

State before:
F : Type u_1
a b : F
inst✝ : Zero F
z w : F
⊢ z = w → { b1 := z, b2 := 0 } = { b1 := w, b2 := 0 }
Tactic:
aesop
State after:
no goals