ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∏ x in Set.toFinset s, f x = Finset.prod univ g

ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∀ (x : β), x ∈ univ → ¬x ∈ Set.toFinset s → f x = 1
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ Finset.prod univ f = Finset.prod univ g
rw [← @Finset.prod_subset _ _ s.toFinset Finset.univ f _ (by simp)]
no goals
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ Set.toFinset s ⊆ univ
simp
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∏ a : Subtype ?m.385802, f ↑a = Finset.prod univ g

case h
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∀ (x : β), x ∈ Set.toFinset s ↔ ?m.385802 x

ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ β → Prop

ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ Fintype (Subtype ?m.385802)
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∏ x in Set.toFinset s, f x = Finset.prod univ g
rw [Finset.prod_subtype]
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∀ (x : { x // x ∈ s }), x ∈ univ → f ↑x = g x
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∏ a : Subtype ?m.385802, f ↑a = Finset.prod univ g
apply Finset.prod_congr rfl
no goals
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∀ (x : { x // x ∈ s }), x ∈ univ → f ↑x = g x
exact fun ⟨x, h⟩ _ => w x h
no goals
case h
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∀ (x : β), x ∈ Set.toFinset s ↔ x ∈ s
simp
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
x : β
a✝ : x ∈ univ
h : ¬x ∈ Set.toFinset s
⊢ f x = 1
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
⊢ ∀ (x : β), x ∈ univ → ¬x ∈ Set.toFinset s → f x = 1
rintro x _ h
no goals
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
x : β
a✝ : x ∈ univ
h : ¬x ∈ Set.toFinset s
⊢ f x = 1
exact w' x (by simpa using h)
no goals
ι : Type ?u.384746
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g✝ : α✝ → β✝
inst✝³ : CommMonoid β✝
α : Type u_1
inst✝² : CommMonoid α
β : Type u_2
inst✝¹ : Fintype β
s : Set β
inst✝ : DecidablePred fun x => x ∈ s
f : β → α
g : ↑s → α
w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }
w' : ∀ (x : β), ¬x ∈ s → f x = 1
x : β
a✝ : x ∈ univ
h : ¬x ∈ Set.toFinset s
⊢ ¬x ∈ s
simpa using h