case refine'_1
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β), single (g a) 0 = 0

case refine'_2
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = single (g a) b₁ + single (g a) b₂

case refine'_3
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
⊢ (sum v fun a b => sum (single (f a) b) fun a => single (g a)) = mapDomain (g ∘ f) v
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
⊢ mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)
refine' ((sum_sum_index _ _).trans _).symm
case refine'_3
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
x✝¹ : α
x✝ : x✝¹ ∈ v.support
⊢ single (g (f x✝¹)) 0 = 0
case refine'_3
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
⊢ (sum v fun a b => sum (single (f a) b) fun a => single (g a)) = mapDomain (g ∘ f) v
refine' sum_congr fun _ _ => sum_single_index _
case refine'_1
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ single (g a✝) 0 = 0
case refine'_1
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β), single (g a) 0 = 0
intro
no goals
case refine'_1
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ single (g a✝) 0 = 0
exact single_zero _
case refine'_2
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ ∀ (b₁ b₂ : M), single (g a✝) (b₁ + b₂) = single (g a✝) b₁ + single (g a✝) b₂
case refine'_2
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = single (g a) b₁ + single (g a) b₂
intro
no goals
case refine'_2
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ ∀ (b₁ b₂ : M), single (g a✝) (b₁ + b₂) = single (g a✝) b₁ + single (g a✝) b₂
exact single_add _
no goals
case refine'_3
α : Type u_3
β : Type u_4
γ : Type u_1
ι : Type ?u.162151
M : Type u_2
M' : Type ?u.162157
N : Type ?u.162160
P : Type ?u.162163
G : Type ?u.162166
H : Type ?u.162169
R : Type ?u.162172
S : Type ?u.162175
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
g : β → γ
x✝¹ : α
x✝ : x✝¹ ∈ v.support
⊢ single (g (f x✝¹)) 0 = 0
exact single_zero _