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

State before:
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 } = { b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }
Tactic:
ext
State after:
case b1
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b1 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b1

case b2
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b2 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b2

State before:
case b1
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b1 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b1

case b2
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b2 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b2
Tactic:
simp
State after:
case b2
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b2 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b2

State before:
case b2
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b2 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b2
Tactic:
sorry
State after:
no goals