R✝ : Type u₁
inst✝⁴ : Semiring R✝
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R✝ → R✝ → Prop
R : Type u₁
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ RingQuot.neg r { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (-a) }
R✝ : Type u₁
inst✝⁴ : Semiring R✝
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R✝ → R✝ → Prop
R : Type u₁
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ -{ toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (-a) }
show neg r _ = _
R✝ : Type u₁
inst✝⁴ : Semiring R✝
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R✝ → R✝ → Prop
R : Type u₁
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ (match { toQuot := Quot.mk (Rel r) a } with
    | { toQuot := a } => { toQuot := Quot.map (fun a => -a) (_ : ∀ ⦃a b : R⦄, Rel r a b → Rel r (-a) (-b)) a }) =
    { toQuot := Quot.mk (Rel r) (-a) }
R✝ : Type u₁
inst✝⁴ : Semiring R✝
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R✝ → R✝ → Prop
R : Type u₁
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ RingQuot.neg r { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (-a) }
rw [neg_def]
no goals
R✝ : Type u₁
inst✝⁴ : Semiring R✝
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R✝ → R✝ → Prop
R : Type u₁
inst✝ : Ring R
r : R → R → Prop
a : R
⊢ (match { toQuot := Quot.mk (Rel r) a } with
    | { toQuot := a } => { toQuot := Quot.map (fun a => -a) (_ : ∀ ⦃a b : R⦄, Rel r a b → Rel r (-a) (-b)) a }) =
    { toQuot := Quot.mk (Rel r) (-a) }
rfl