no goals
α : Type u_2
β : Type ?u.325058
γ : Type ?u.325061
ι : Type ?u.325064
M : Type u_1
M' : Type ?u.325070
N : Type ?u.325073
P : Type ?u.325076
G : Type ?u.325079
H : Type ?u.325082
R : Type ?u.325085
S : Type ?u.325088
inst✝ : Zero M
a : α
m : M
⊢ some (single (Option.some a) m) = single a m
classical
  ext b
  simp [single_apply]
case h
α : Type u_2
β : Type ?u.325058
γ : Type ?u.325061
ι : Type ?u.325064
M : Type u_1
M' : Type ?u.325070
N : Type ?u.325073
P : Type ?u.325076
G : Type ?u.325079
H : Type ?u.325082
R : Type ?u.325085
S : Type ?u.325088
inst✝ : Zero M
a : α
m : M
b : α
⊢ ↑(some (single (Option.some a) m)) b = ↑(single a m) b
α : Type u_2
β : Type ?u.325058
γ : Type ?u.325061
ι : Type ?u.325064
M : Type u_1
M' : Type ?u.325070
N : Type ?u.325073
P : Type ?u.325076
G : Type ?u.325079
H : Type ?u.325082
R : Type ?u.325085
S : Type ?u.325088
inst✝ : Zero M
a : α
m : M
⊢ some (single (Option.some a) m) = single a m
ext b
no goals
case h
α : Type u_2
β : Type ?u.325058
γ : Type ?u.325061
ι : Type ?u.325064
M : Type u_1
M' : Type ?u.325070
N : Type ?u.325073
P : Type ?u.325076
G : Type ?u.325079
H : Type ?u.325082
R : Type ?u.325085
S : Type ?u.325088
inst✝ : Zero M
a : α
m : M
b : α
⊢ ↑(some (single (Option.some a) m)) b = ↑(single a m) b
simp [single_apply]