case mp
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
⊢ ↑(scalar n) r = ↑(scalar n) s → r = s

case mpr
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
⊢ r = s → ↑(scalar n) r = ↑(scalar n) s
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
⊢ ↑(scalar n) r = ↑(scalar n) s ↔ r = s
constructor
case mp
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
h : ↑(scalar n) r = ↑(scalar n) s
⊢ r = s
case mp
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
⊢ ↑(scalar n) r = ↑(scalar n) s → r = s
intro h
case mp
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
h : ↑(scalar n) r = ↑(scalar n) s
inhabited_h : Inhabited n
⊢ r = s
case mp
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
h : ↑(scalar n) r = ↑(scalar n) s
⊢ r = s
inhabit n
no goals
case mp
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
h : ↑(scalar n) r = ↑(scalar n) s
inhabited_h : Inhabited n
⊢ r = s
rw [← scalar_apply_eq r (Inhabited.default (α := n)),
    ← scalar_apply_eq s (Inhabited.default (α := n)), h]
case mpr
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r : α
⊢ ↑(scalar n) r = ↑(scalar n) r
case mpr
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r s : α
⊢ r = s → ↑(scalar n) r = ↑(scalar n) s
rintro rfl
no goals
case mpr
l : Type ?u.458991
m : Type ?u.458994
n : Type u_1
o : Type ?u.459000
m' : o → Type ?u.459005
n' : o → Type ?u.459010
R : Type ?u.459013
S : Type ?u.459016
α : Type v
β : Type w
γ : Type ?u.459023
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
r : α
⊢ ↑(scalar n) r = ↑(scalar n) r
rfl