α : Type u_1
β : Type ?u.44418
γ : Type ?u.44421
ι : Type ?u.44424
M : Type u_2
M' : Type ?u.44430
N : Type ?u.44433
P : Type ?u.44436
G : Type ?u.44439
H : Type ?u.44442
R : Type ?u.44445
S : Type ?u.44448
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a a' : α
b : M
⊢ single a (if a' = a then b else 0) = if a' = a then single a' b else 0
α : Type u_1
β : Type ?u.44418
γ : Type ?u.44421
ι : Type ?u.44424
M : Type u_2
M' : Type ?u.44430
N : Type ?u.44433
P : Type ?u.44436
G : Type ?u.44439
H : Type ?u.44442
R : Type ?u.44445
S : Type ?u.44448
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a a' : α
b : M
⊢ single a (↑(single a' b) a) = ↑(single a' (single a' b)) a
rw [single_apply, single_apply]
case h
α : Type u_1
β : Type ?u.44418
γ : Type ?u.44421
ι : Type ?u.44424
M : Type u_2
M' : Type ?u.44430
N : Type ?u.44433
P : Type ?u.44436
G : Type ?u.44439
H : Type ?u.44442
R : Type ?u.44445
S : Type ?u.44448
inst✝ : Zero M
a✝¹ a'✝ : α
b✝ : M
a a' : α
b : M
a✝ : α
⊢ ↑(single a (if a' = a then b else 0)) a✝ = ↑(if a' = a then single a' b else 0) a✝
α : Type u_1
β : Type ?u.44418
γ : Type ?u.44421
ι : Type ?u.44424
M : Type u_2
M' : Type ?u.44430
N : Type ?u.44433
P : Type ?u.44436
G : Type ?u.44439
H : Type ?u.44442
R : Type ?u.44445
S : Type ?u.44448
inst✝ : Zero M
a✝ a'✝ : α
b✝ : M
a a' : α
b : M
⊢ single a (if a' = a then b else 0) = if a' = a then single a' b else 0
ext
case h.inl
α : Type u_1
β : Type ?u.44418
γ : Type ?u.44421
ι : Type ?u.44424
M : Type u_2
M' : Type ?u.44430
N : Type ?u.44433
P : Type ?u.44436
G : Type ?u.44439
H : Type ?u.44442
R : Type ?u.44445
S : Type ?u.44448
inst✝ : Zero M
a✝¹ a'✝ : α
b✝ : M
a a' : α
b : M
a✝ : α
h : a' = a
⊢ ↑(single a b) a✝ = ↑(single a' b) a✝

case h.inr
α : Type u_1
β : Type ?u.44418
γ : Type ?u.44421
ι : Type ?u.44424
M : Type u_2
M' : Type ?u.44430
N : Type ?u.44433
P : Type ?u.44436
G : Type ?u.44439
H : Type ?u.44442
R : Type ?u.44445
S : Type ?u.44448
inst✝ : Zero M
a✝¹ a'✝ : α
b✝ : M
a a' : α
b : M
a✝ : α
h : ¬a' = a
⊢ ↑(single a 0) a✝ = ↑0 a✝
case h
α : Type u_1
β : Type ?u.44418
γ : Type ?u.44421
ι : Type ?u.44424
M : Type u_2
M' : Type ?u.44430
N : Type ?u.44433
P : Type ?u.44436
G : Type ?u.44439
H : Type ?u.44442
R : Type ?u.44445
S : Type ?u.44448
inst✝ : Zero M
a✝¹ a'✝ : α
b✝ : M
a a' : α
b : M
a✝ : α
⊢ ↑(single a (if a' = a then b else 0)) a✝ = ↑(if a' = a then single a' b else 0) a✝
split_ifs with h
no goals
case h.inl
α : Type u_1
β : Type ?u.44418
γ : Type ?u.44421
ι : Type ?u.44424
M : Type u_2
M' : Type ?u.44430
N : Type ?u.44433
P : Type ?u.44436
G : Type ?u.44439
H : Type ?u.44442
R : Type ?u.44445
S : Type ?u.44448
inst✝ : Zero M
a✝¹ a'✝ : α
b✝ : M
a a' : α
b : M
a✝ : α
h : a' = a
⊢ ↑(single a b) a✝ = ↑(single a' b) a✝
rw [h]
no goals
case h.inr
α : Type u_1
β : Type ?u.44418
γ : Type ?u.44421
ι : Type ?u.44424
M : Type u_2
M' : Type ?u.44430
N : Type ?u.44433
P : Type ?u.44436
G : Type ?u.44439
H : Type ?u.44442
R : Type ?u.44445
S : Type ?u.44448
inst✝ : Zero M
a✝¹ a'✝ : α
b✝ : M
a a' : α
b : M
a✝ : α
h : ¬a' = a
⊢ ↑(single a 0) a✝ = ↑0 a✝
rw [zero_apply, single_apply, ite_self]