case pos
α : Type u_1
β : Type ?u.287003
γ : Type ?u.287006
ι : Type ?u.287009
M : Type u_2
M' : Type ?u.287015
N : Type ?u.287018
P : Type ?u.287021
G : Type ?u.287024
H : Type ?u.287027
R : Type ?u.287030
S : Type ?u.287033
inst✝ : AddZeroClass M
a : α
b₁ b₂ : M
a' : α
h : a = a'
⊢ ↑(single a (b₁ + b₂)) a' = ↑(single a b₁ + single a b₂) a'

case neg
α : Type u_1
β : Type ?u.287003
γ : Type ?u.287006
ι : Type ?u.287009
M : Type u_2
M' : Type ?u.287015
N : Type ?u.287018
P : Type ?u.287021
G : Type ?u.287024
H : Type ?u.287027
R : Type ?u.287030
S : Type ?u.287033
inst✝ : AddZeroClass M
a : α
b₁ b₂ : M
a' : α
h : ¬a = a'
⊢ ↑(single a (b₁ + b₂)) a' = ↑(single a b₁ + single a b₂) a'
α : Type u_1
β : Type ?u.287003
γ : Type ?u.287006
ι : Type ?u.287009
M : Type u_2
M' : Type ?u.287015
N : Type ?u.287018
P : Type ?u.287021
G : Type ?u.287024
H : Type ?u.287027
R : Type ?u.287030
S : Type ?u.287033
inst✝ : AddZeroClass M
a : α
b₁ b₂ : M
a' : α
⊢ ↑(single a (b₁ + b₂)) a' = ↑(single a b₁ + single a b₂) a'
by_cases h : a = a'
no goals
case pos
α : Type u_1
β : Type ?u.287003
γ : Type ?u.287006
ι : Type ?u.287009
M : Type u_2
M' : Type ?u.287015
N : Type ?u.287018
P : Type ?u.287021
G : Type ?u.287024
H : Type ?u.287027
R : Type ?u.287030
S : Type ?u.287033
inst✝ : AddZeroClass M
a : α
b₁ b₂ : M
a' : α
h : a = a'
⊢ ↑(single a (b₁ + b₂)) a' = ↑(single a b₁ + single a b₂) a'
rw [h, add_apply, single_eq_same, single_eq_same, single_eq_same]
no goals
case neg
α : Type u_1
β : Type ?u.287003
γ : Type ?u.287006
ι : Type ?u.287009
M : Type u_2
M' : Type ?u.287015
N : Type ?u.287018
P : Type ?u.287021
G : Type ?u.287024
H : Type ?u.287027
R : Type ?u.287030
S : Type ?u.287033
inst✝ : AddZeroClass M
a : α
b₁ b₂ : M
a' : α
h : ¬a = a'
⊢ ↑(single a (b₁ + b₂)) a' = ↑(single a b₁ + single a b₂) a'
rw [add_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, zero_add]