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
inst✝ : Algebra S R
n : S
a : R
⊢ RingQuot.smul r n { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (n • 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
inst✝ : Algebra S R
n : S
a : R
⊢ n • { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (n • a) }
show smul 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
inst✝ : Algebra S R
n : S
a : R
⊢ (match { toQuot := Quot.mk (Rel r) a } with
    | { toQuot := a } =>
      { toQuot := Quot.map (fun a => n • a) (_ : ∀ ⦃a b : R⦄, Rel r a b → Rel r (n • a) (n • b)) a }) =
    { toQuot := Quot.mk (Rel r) (n • 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
inst✝ : Algebra S R
n : S
a : R
⊢ RingQuot.smul r n { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (n • a) }
rw [smul_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
inst✝ : Algebra S R
n : S
a : R
⊢ (match { toQuot := Quot.mk (Rel r) a } with
    | { toQuot := a } =>
      { toQuot := Quot.map (fun a => n • a) (_ : ∀ ⦃a b : R⦄, Rel r a b → Rel r (n • a) (n • b)) a }) =
    { toQuot := Quot.mk (Rel r) (n • a) }
rfl