-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_dite_eq [DecidableEq α] (s : Finset α) (a : α) (b : ∀ x : α, a = x → β) :
    ∏ x ∈ s, (if h : a = x then b x h else 1) = ite (a ∈ s) (b a rfl) 1

Proof state:
case pos.h₀
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : a = b_1 then b b_1 h else 1) = 1

Tactic:
intros _ _ h

Result:
case pos.h₀
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h✝ : a ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ (if h : a = b✝ then b b✝ h else 1) = 1

Proof state:
case neg.hnc
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
a✝ : a ∈ s
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∈ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯

Tactic:
rw [Finset.prod_eq_single a, dif_pos rfl]

Result:
case pos.h₀
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : a = b_1 then b b_1 h else 1) = 1

case pos.h₁
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Proof state:
case pos.h₀
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h✝ : a ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ (if h : a = b✝ then b b✝ h else 1) = 1

Tactic:
rw [dif_neg]

Result:
case pos.h₀.hnc
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h✝ : a ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ ¬a = b✝

Proof state:
case pos.h₁
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
⊢ ∀ x ∈ s, (if h : a = x then b x h else 1) = 1

Tactic:
intros

Result:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
x✝ : α
a✝ : x✝ ∈ s
⊢ (if h : a = x✝ then b x✝ h else 1) = 1

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
x✝ : α
a✝ : x✝ ∈ s
⊢ (if h : a = x✝ then b x✝ h else 1) = 1

Tactic:
rw [dif_neg]

Result:
case neg.hnc
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
x✝ : α
a✝ : x✝ ∈ s
⊢ ¬a = x✝

Proof state:
case pos.h₀.hnc
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h✝ : a ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ ¬a = b✝

Tactic:
exact h.symm

Result:
no goals

Proof state:
case neg.hnc
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
x✝ : α
a✝ : x✝ ∈ s
⊢ ¬a = x✝

Tactic:
rintro rfl

Result:
case neg.hnc
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
a✝ : a ∈ s
⊢ False

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1

Tactic:
split_ifs with h

Result:
case pos
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∈ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯

case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = 1

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = 1

Tactic:
rw [Finset.prod_eq_one]

Result:
case neg
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → a = x → β
h : a ∉ s
⊢ ∀ x ∈ s, (if h : a = x then b x h else 1) = 1