-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem eq_of_card_le_one_of_prod_eq {s : Finset α} (hc : #s ≤ 1) {f : α → β} {b : β}
    (h : ∏ x ∈ s, f x = b) : ∀ x ∈ s, f x = b

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
⊢ ∀ x ∈ s, f x = b

Tactic:
intro x hx

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
⊢ f x = b

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : ¬#s = 0
h1 : #s = 1
⊢ f x = b

Tactic:
rw [card_eq_one] at h1

Result:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : ¬#s = 0
h1 : ∃ a, s = {a}
⊢ f x = b

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : ¬#s = 0
h1 : ∃ a, s = {a}
⊢ f x = b

Tactic:
obtain ⟨x2, hx2⟩ := h1

Result:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : ¬#s = 0
x2 : α
hx2 : s = {x2}
⊢ f x = b

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : #s = 0
⊢ f x = b

Tactic:
exact False.elim (card_ne_zero_of_mem hx hc0)

Result:
no goals

Proof state:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬#s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : f x2 = b
⊢ f x2 = b

Tactic:
exact h

Result:
no goals

Proof state:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hc0 : ¬#s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
⊢ f x = b

Tactic:
simp_rw [hx2] at h

Result:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬#s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : ∏ x ∈ {x2}, f x = b
⊢ f x = b

Proof state:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬#s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : ∏ x ∈ {x2}, f x = b
⊢ f x = b

Tactic:
rw [hx]

Result:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬#s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : ∏ x ∈ {x2}, f x = b
⊢ f x2 = b

Proof state:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : ¬#s = 0
x2 : α
hx2 : s = {x2}
⊢ f x = b

Tactic:
rw [hx2, mem_singleton] at hx

Result:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hc0 : ¬#s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
⊢ f x = b

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
⊢ f x = b

Tactic:
by_cases hc0 : #s = 0

Result:
case pos
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : #s = 0
⊢ f x = b

case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : ¬#s = 0
⊢ f x = b

Proof state:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬#s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : ∏ x ∈ {x2}, f x = b
⊢ f x2 = b

Tactic:
rw [prod_singleton] at h

Result:
case neg.intro
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬#s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : f x2 = b
⊢ f x2 = b

Proof state:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : ¬#s = 0
⊢ f x = b

Tactic:
have h1 : #s = 1 := le_antisymm hc (Nat.one_le_of_lt (Nat.pos_of_ne_zero hc0))

Result:
case neg
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
hc : #s ≤ 1
f : α → β
b : β
h : ∏ x ∈ s, f x = b
x : α
hx : x ∈ s
hc0 : ¬#s = 0
h1 : #s = 1
⊢ f x = b