G : Type ?u.40810
M : Type u_1
N : Type ?u.40816
α : Sort u_2
β : Sort ?u.40822
ι : Sort ?u.40825
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (if h : Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down)) then ∏ i in Finite.toFinset h, f i.down else 1)
G : Type ?u.40810
M : Type u_1
N : Type ?u.40816
α : Sort u_2
β : Sort ?u.40822
ι : Sort ?u.40825
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (∏ᶠ (i : α), f i)
rw [finprod]
case inl
G : Type ?u.40810
M : Type u_1
N : Type ?u.40816
α : Sort u_2
β : Sort ?u.40822
ι : Sort ?u.40825
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
⊢ p (∏ i in Finite.toFinset h✝, f i.down)

case inr
G : Type ?u.40810
M : Type u_1
N : Type ?u.40816
α : Sort u_2
β : Sort ?u.40822
ι : Sort ?u.40825
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : ¬Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
⊢ p 1
G : Type ?u.40810
M : Type u_1
N : Type ?u.40816
α : Sort u_2
β : Sort ?u.40822
ι : Sort ?u.40825
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (if h : Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down)) then ∏ i in Finite.toFinset h, f i.down else 1)
split_ifs
no goals
case inl
G : Type ?u.40810
M : Type u_1
N : Type ?u.40816
α : Sort u_2
β : Sort ?u.40822
ι : Sort ?u.40825
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
⊢ p (∏ i in Finite.toFinset h✝, f i.down)

case inr
G : Type ?u.40810
M : Type u_1
N : Type ?u.40816
α : Sort u_2
β : Sort ?u.40822
ι : Sort ?u.40825
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : ¬Set.Finite (mulSupport ((fun i => f i) ∘ PLift.down))
⊢ p 1
exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]