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

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

Tactic:
have hu : s' ⊆ s := by
  refine insert_subset_iff.mpr ?_
  apply And.intro ha
  apply singleton_subset_iff.mpr hb

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

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

Tactic:
exact Finset.prod_pair hn

Result:
no goals

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

Tactic:
have hf : ∀ c ∈ s, c ∉ s' → f c = 1 := by
  intro c hc hcs
  apply h₀ c hc
  apply not_or.mp
  intro hab
  apply hcs
  rw [mem_insert, mem_singleton]
  exact hab

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

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
⊢ c ≠ a ∧ c ≠ b

Tactic:
apply not_or.mp

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
⊢ ¬(c = a ∨ c = b)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
hab : c = a ∨ c = b
⊢ False

Tactic:
apply hcs

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
hab : c = a ∨ c = b
⊢ c ∈ s'

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

Tactic:
let s' := ({a, b} : Finset α)

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

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

Tactic:
apply And.intro ha

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

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

Tactic:
refine insert_subset_iff.mpr ?_

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

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
hab : c = a ∨ c = b
⊢ c ∈ s'

Tactic:
rw [mem_insert, mem_singleton]

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
hab : c = a ∨ c = b
⊢ c = a ∨ c = b

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
⊢ ¬(c = a ∨ c = b)

Tactic:
intro hab

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
hab : c = a ∨ c = b
⊢ False

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

Tactic:
intro c hc hcs

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
⊢ f c = 1

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

Tactic:
apply singleton_subset_iff.mpr hb

Result:
no goals

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

Tactic:
rw [← prod_subset hu hf]

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

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

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
hab : c = a ∨ c = b
⊢ c = a ∨ c = b

Tactic:
exact hab

Result:
no goals