no goals
ι : Type ?u.302040
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : Fintype α
inst✝ : CommMonoid β
s t : Finset α
h : IsCompl s t
f : α → β
⊢ ∏ x in disjUnion s t (_ : Disjoint s t), f x = ∏ i : α, f i
classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl
ι : Type ?u.302040
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : Fintype α
inst✝ : CommMonoid β
s t : Finset α
h : IsCompl s t
f : α → β
⊢ ∏ x in ⊤, f x = ∏ i : α, f i
ι : Type ?u.302040
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : Fintype α
inst✝ : CommMonoid β
s t : Finset α
h : IsCompl s t
f : α → β
⊢ ∏ x in disjUnion s t (_ : Disjoint s t), f x = ∏ i : α, f i
rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]
no goals
ι : Type ?u.302040
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : Fintype α
inst✝ : CommMonoid β
s t : Finset α
h : IsCompl s t
f : α → β
⊢ ∏ x in ⊤, f x = ∏ i : α, f i
rfl