case inl
G : Type ?u.38544
M : Type u_1
N : Type ?u.38550
α : Sort ?u.38553
β : Sort ?u.38556
ι : Sort ?u.38559
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : p
⊢ (∏ᶠ (i : p), f i) = f h

case inr
G : Type ?u.38544
M : Type u_1
N : Type ?u.38550
α : Sort ?u.38553
β : Sort ?u.38556
ι : Sort ?u.38559
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
⊢ (∏ᶠ (i : p), f i) = 1
G : Type ?u.38544
M : Type u_1
N : Type ?u.38550
α : Sort ?u.38553
β : Sort ?u.38556
ι : Sort ?u.38559
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
⊢ (∏ᶠ (i : p), f i) = if h : p then f h else 1
split_ifs with h
case inl
G : Type ?u.38544
M : Type u_1
N : Type ?u.38550
α : Sort ?u.38553
β : Sort ?u.38556
ι : Sort ?u.38559
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : p
this : Unique p
⊢ (∏ᶠ (i : p), f i) = f h
case inl
G : Type ?u.38544
M : Type u_1
N : Type ?u.38550
α : Sort ?u.38553
β : Sort ?u.38556
ι : Sort ?u.38559
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : p
⊢ (∏ᶠ (i : p), f i) = f h
haveI : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
no goals
case inl
G : Type ?u.38544
M : Type u_1
N : Type ?u.38550
α : Sort ?u.38553
β : Sort ?u.38556
ι : Sort ?u.38559
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : p
this : Unique p
⊢ (∏ᶠ (i : p), f i) = f h
exact finprod_unique f
case inr
G : Type ?u.38544
M : Type u_1
N : Type ?u.38550
α : Sort ?u.38553
β : Sort ?u.38556
ι : Sort ?u.38559
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
this : IsEmpty p
⊢ (∏ᶠ (i : p), f i) = 1
case inr
G : Type ?u.38544
M : Type u_1
N : Type ?u.38550
α : Sort ?u.38553
β : Sort ?u.38556
ι : Sort ?u.38559
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
⊢ (∏ᶠ (i : p), f i) = 1
haveI : IsEmpty p := ⟨h⟩
no goals
case inr
G : Type ?u.38544
M : Type u_1
N : Type ?u.38550
α : Sort ?u.38553
β : Sort ?u.38556
ι : Sort ?u.38559
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
p : Prop
inst✝ : Decidable p
f : p → M
h : ¬p
this : IsEmpty p
⊢ (∏ᶠ (i : p), f i) = 1
exact finprod_of_isEmpty f