-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_eq_mul {s : Finset α} {f : α → β} (a b : α) (hn : a ≠ b)
    (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) (ha : a ∉ s → f a = 1) (hb : b ∉ s → f b = 1) :
    ∏ x ∈ s, f x = f a * f b

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
by_cases h₁ : a ∈ s <;> by_cases h₂ : b ∈ s

Result:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∈ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [ha h₁, one_mul]

Result:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f b

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = 1

Tactic:
exact
  _root_.trans
    (prod_congr rfl fun c hc =>
      h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, ne_of_mem_of_not_mem hc h₂⟩)
    prod_const_one

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
haveI := Classical.decEq α

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
⊢ ∏ x ∈ s, f x = f a * f b

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f b

Tactic:
apply prod_eq_single_of_mem b h₂

Result:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [ha h₁, hb h₂, mul_one]

Result:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = 1

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∈ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
exact prod_eq_mul_of_mem a b h₁ h₂ hn h₀

Result:
no goals

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [hb h₂, mul_one]

Result:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1

Tactic:
exact fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩

Result:
no goals

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a

Tactic:
apply prod_eq_single_of_mem a h₁

Result:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∀ b ∈ s, b ≠ a → f b = 1

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq α
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∀ b ∈ s, b ≠ a → f b = 1

Tactic:
exact fun c hc hca => h₀ c hc ⟨hca, ne_of_mem_of_not_mem hc h₂⟩

Result:
no goals