α : Type u_2
β : Type ?u.49306
γ : Type ?u.49309
ι : Type ?u.49312
M : Type u_1
M' : Type ?u.49318
N : Type ?u.49321
P : Type ?u.49324
G : Type ?u.49327
H : Type ?u.49330
R : Type ?u.49333
S : Type ?u.49336
inst✝ : Zero M
a✝ a' : α
b : M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
this : ↑(single a b₁) a = ↑(single a b₂) a
⊢ b₁ = b₂
α : Type u_2
β : Type ?u.49306
γ : Type ?u.49309
ι : Type ?u.49312
M : Type u_1
M' : Type ?u.49318
N : Type ?u.49321
P : Type ?u.49324
G : Type ?u.49327
H : Type ?u.49330
R : Type ?u.49333
S : Type ?u.49336
inst✝ : Zero M
a✝ a' : α
b : M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ b₁ = b₂
have : (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a := by rw [eq]
no goals
α : Type u_2
β : Type ?u.49306
γ : Type ?u.49309
ι : Type ?u.49312
M : Type u_1
M' : Type ?u.49318
N : Type ?u.49321
P : Type ?u.49324
G : Type ?u.49327
H : Type ?u.49330
R : Type ?u.49333
S : Type ?u.49336
inst✝ : Zero M
a✝ a' : α
b : M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
this : ↑(single a b₁) a = ↑(single a b₂) a
⊢ b₁ = b₂
rwa [single_eq_same, single_eq_same] at this
no goals
α : Type u_2
β : Type ?u.49306
γ : Type ?u.49309
ι : Type ?u.49312
M : Type u_1
M' : Type ?u.49318
N : Type ?u.49321
P : Type ?u.49324
G : Type ?u.49327
H : Type ?u.49330
R : Type ?u.49333
S : Type ?u.49336
inst✝ : Zero M
a✝ a' : α
b : M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ ↑(single a b₁) a = ↑(single a b₂) a
rw [eq]