case inl
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
h : ∃ i, i ∈ s ∧ f i
⊢ (∏ i in s, if f i then a else 1) = a

case inr
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
h : ¬∃ i, i ∈ s ∧ f i
⊢ (∏ i in s, if f i then a else 1) = 1
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
⊢ (∏ i in s, if f i then a else 1) = if ∃ i, i ∈ s ∧ f i then a else 1
split_ifs with h
case inl.intro.intro
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
i : α
hi : i ∈ s
hfi : f i
⊢ (∏ i in s, if f i then a else 1) = a
case inl
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
h : ∃ i, i ∈ s ∧ f i
⊢ (∏ i in s, if f i then a else 1) = a
obtain ⟨i, hi, hfi⟩ := h
case inl.intro.intro
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
i : α
hi : i ∈ s
hfi : f i
⊢ ∀ (b : α), b ∈ s → b ≠ i → (if f b then a else 1) = 1
case inl.intro.intro
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
i : α
hi : i ∈ s
hfi : f i
⊢ (∏ i in s, if f i then a else 1) = a
rw [prod_eq_single_of_mem _ hi, if_pos hfi]
no goals
case inl.intro.intro
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
i : α
hi : i ∈ s
hfi : f i
⊢ ∀ (b : α), b ∈ s → b ≠ i → (if f b then a else 1) = 1
exact fun j hj h => if_neg fun hfj => (hf hj hi h).le_bot ⟨hfj, hfi⟩
case inr
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
h : ∀ (i : α), i ∈ s → ¬f i
⊢ (∏ i in s, if f i then a else 1) = 1
case inr
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
h : ¬∃ i, i ∈ s ∧ f i
⊢ (∏ i in s, if f i then a else 1) = 1
push_neg  at h
case inr
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
h : ∀ (i : α), i ∈ s → ¬f i
⊢ ∀ (x : α), x ∈ s → (if f x then a else 1) = 1
case inr
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
h : ∀ (i : α), i ∈ s → ¬f i
⊢ (∏ i in s, if f i then a else 1) = 1
rw [prod_eq_one]
no goals
case inr
ι : Type ?u.798449
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
f : α → Prop
inst✝ : DecidablePred f
hf : Set.PairwiseDisjoint (↑s) f
a : β
h : ∀ (i : α), i ∈ s → ¬f i
⊢ ∀ (x : α), x ∈ s → (if f x then a else 1) = 1
exact fun i hi => if_neg (h i hi)