-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_ite_one (s : Finset α) (p : α → Prop) [DecidablePred p]
    (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) :
    ∏ i ∈ s, ite (p i) a 1 = ite (∃ i ∈ s, p i) a 1

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
⊢ (∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1

Tactic:
split_ifs with h

Result:
case pos
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
h : ∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = a

case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
h : ¬∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1

Proof state:
case pos.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
i : α
hi : i ∈ s
hpi : p i
⊢ (∏ i ∈ s, if p i then a else 1) = a

Tactic:
rw [prod_eq_single_of_mem _ hi, if_pos hpi]

Result:
case pos.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
i : α
hi : i ∈ s
hpi : p i
⊢ ∀ b ∈ s, b ≠ i → (if p b then a else 1) = 1

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
h : ∀ i ∈ s, ¬p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1

Tactic:
rw [prod_eq_one]

Result:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
h : ∀ i ∈ s, ¬p i
⊢ ∀ x ∈ s, (if p x then a else 1) = 1

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
h : ∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = a

Tactic:
obtain ⟨i, hi, hpi⟩ := h

Result:
case pos.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
i : α
hi : i ∈ s
hpi : p i
⊢ (∏ i ∈ s, if p i then a else 1) = a

Proof state:
case pos.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
i : α
hi : i ∈ s
hpi : p i
⊢ ∀ b ∈ s, b ≠ i → (if p b then a else 1) = 1

Tactic:
exact fun j hj hji ↦ if_neg fun hpj ↦ hji <| h _ hj _ hi hpj hpi

Result:
no goals

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
h : ∀ i ∈ s, ¬p i
⊢ ∀ x ∈ s, (if p x then a else 1) = 1

Tactic:
exact fun i hi => if_neg (h i hi)

Result:
no goals

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
h : ¬∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1

Tactic:
push_neg at h

Result:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : β
h : ∀ i ∈ s, ¬p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1