[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c x y : RingCon R
h : (fun c => Setoid.r) x = (fun c => Setoid.r) y
⊢ x = y
[PROOFSTEP]
rcases x with ⟨⟨x, _⟩, _⟩
[GOAL]
case mk.mk
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c y : RingCon R
x : R → R → Prop
iseqv✝ : Equivalence x
add'✝ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w + y) (x_1 + z)
mul'✝ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w * y) (x_1 * z)
h :
  (fun c => Setoid.r) { toSetoid := { r := x, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ } = (fun c => Setoid.r) y
⊢ { toSetoid := { r := x, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ } = y
[PROOFSTEP]
rcases y with ⟨⟨y, _⟩, _⟩
[GOAL]
case mk.mk.mk.mk
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
x : R → R → Prop
iseqv✝¹ : Equivalence x
add'✝¹ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w + y) (x_1 + z)
mul'✝¹ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w * y) (x_1 * z)
y : R → R → Prop
iseqv✝ : Equivalence y
add'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w + y_1) (x + z)
mul'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w * y_1) (x * z)
h :
  (fun c => Setoid.r) { toSetoid := { r := x, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ } =
    (fun c => Setoid.r) { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ }
⊢ { toSetoid := { r := x, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ } =
    { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ }
[PROOFSTEP]
have : x = y := h
[GOAL]
case mk.mk.mk.mk
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
x : R → R → Prop
iseqv✝¹ : Equivalence x
add'✝¹ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w + y) (x_1 + z)
mul'✝¹ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w * y) (x_1 * z)
y : R → R → Prop
iseqv✝ : Equivalence y
add'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w + y_1) (x + z)
mul'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w * y_1) (x * z)
h :
  (fun c => Setoid.r) { toSetoid := { r := x, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ } =
    (fun c => Setoid.r) { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ }
this : x = y
⊢ { toSetoid := { r := x, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ } =
    { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ }
[PROOFSTEP]
subst x
[GOAL]
case mk.mk.mk.mk
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
y : R → R → Prop
iseqv✝¹ : Equivalence y
add'✝¹ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w + y_1) (x + z)
mul'✝¹ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w * y_1) (x * z)
iseqv✝ : Equivalence y
add'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w + y_1) (x + z)
mul'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w * y_1) (x * z)
h :
  (fun c => Setoid.r) { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ } =
    (fun c => Setoid.r) { toSetoid := { r := y, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ }
⊢ { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ } =
    { toSetoid := { r := y, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
d : (a b : R) → Decidable (↑c a b)
⊢ DecidableEq (RingCon.Quotient c)
[PROOFSTEP]
delta RingCon.Quotient
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
d : (a b : R) → Decidable (↑c a b)
⊢ DecidableEq (Quotient c.toSetoid)
[PROOFSTEP]
infer_instance
