case inl
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : a ∈ s
⊢ (∏ x in s, if h : x = a then b x h else 1) = b a (_ : a = a)

case inr
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : ¬a ∈ s
⊢ (∏ x in s, if h : x = a then b x h else 1) = 1
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
⊢ (∏ x in s, if h : x = a then b x h else 1) = if a ∈ s then b a (_ : a = a) else 1
split_ifs with h
case inl.h₀
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : a ∈ s
⊢ ∀ (b_1 : α), b_1 ∈ s → b_1 ≠ a → (if h : b_1 = a then b b_1 h else 1) = 1

case inl.h₁
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : a ∈ s
⊢ ¬a ∈ s → (if h : a = a then b a h else 1) = 1
case inl
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : a ∈ s
⊢ (∏ x in s, if h : x = a then b x h else 1) = b a (_ : a = a)
rw [Finset.prod_eq_single a, dif_pos rfl]
case inl.h₀
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h✝ : a ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ (if h : b✝ = a then b b✝ h else 1) = 1
case inl.h₀
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : a ∈ s
⊢ ∀ (b_1 : α), b_1 ∈ s → b_1 ≠ a → (if h : b_1 = a then b b_1 h else 1) = 1
intros _ _ h
case inl.h₀.hnc
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h✝ : a ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ ¬b✝ = a
case inl.h₀
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h✝ : a ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ (if h : b✝ = a then b b✝ h else 1) = 1
rw [dif_neg]
no goals
case inl.h₀.hnc
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h✝ : a ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ ¬b✝ = a
exact h
no goals
case inl.h₁
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : a ∈ s
⊢ ¬a ∈ s → (if h : a = a then b a h else 1) = 1
simp [h]
case inr
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : ¬a ∈ s
⊢ ∀ (x : α), x ∈ s → (if h : x = a then b x h else 1) = 1
case inr
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : ¬a ∈ s
⊢ (∏ x in s, if h : x = a then b x h else 1) = 1
rw [Finset.prod_eq_one]
case inr
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : ¬a ∈ s
x✝ : α
a✝ : x✝ ∈ s
⊢ (if h : x✝ = a then b x✝ h else 1) = 1
case inr
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : ¬a ∈ s
⊢ ∀ (x : α), x ∈ s → (if h : x = a then b x h else 1) = 1
intros
case inr.hnc
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : ¬a ∈ s
x✝ : α
a✝ : x✝ ∈ s
⊢ ¬x✝ = a
case inr
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : ¬a ∈ s
x✝ : α
a✝ : x✝ ∈ s
⊢ (if h : x✝ = a then b x✝ h else 1) = 1
rw [dif_neg]
case inr.hnc
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
x✝ : α
a✝ : x✝ ∈ s
b : (x : α) → x = x✝ → β
h : ¬x✝ ∈ s
⊢ False
case inr.hnc
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : (x : α) → x = a → β
h : ¬a ∈ s
x✝ : α
a✝ : x✝ ∈ s
⊢ ¬x✝ = a
rintro rfl
no goals
case inr.hnc
ι : Type ?u.413230
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
x✝ : α
a✝ : x✝ ∈ s
b : (x : α) → x = x✝ → β
h : ¬x✝ ∈ s
⊢ False
contradiction