α : Type u_1
β : Type u_2
ι : Type ?u.465098
G : Type ?u.465101
M : Type u_3
N : Type ?u.465107
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ (∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose h)) = ∏ᶠ (a : α), g a
α : Type u_1
β : Type u_2
ι : Type ?u.465098
G : Type ?u.465101
M : Type u_3
N : Type ?u.465107
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ (∏ᶠ (b : β), if h : b ∈ range f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a
simp_rw [← finprod_eq_dif]
α : Type u_1
β : Type u_2
ι : Type ?u.465098
G : Type ?u.465101
M : Type u_3
N : Type ?u.465107
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ ∀ (a : α), (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
α : Type u_1
β : Type u_2
ι : Type ?u.465098
G : Type ?u.465101
M : Type u_3
N : Type ?u.465107
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ (∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose h)) = ∏ᶠ (a : α), g a
rw [finprod_dmem, finprod_mem_range hf, finprod_congr fun a => _]
α : Type u_1
β : Type u_2
ι : Type ?u.465098
G : Type ?u.465101
M : Type u_3
N : Type ?u.465107
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a✝ b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
a : α
⊢ (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
α : Type u_1
β : Type u_2
ι : Type ?u.465098
G : Type ?u.465101
M : Type u_3
N : Type ?u.465107
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
⊢ ∀ (a : α), (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
intro a
no goals
α : Type u_1
β : Type u_2
ι : Type ?u.465098
G : Type ?u.465101
M : Type u_3
N : Type ?u.465107
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a✝ b : α
s t : Set α
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x => x ∈ range f
g : α → M
a : α
⊢ (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]