ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
⊢ f x = b
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
⊢ ∀ (x : α), x ∈ s → f x = b
intro x hx
case pos
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : card s = 0
⊢ f x = b

case neg
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : ¬card s = 0
⊢ f x = b
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
⊢ f x = b
by_cases hc0 : s.card = 0
no goals
case pos
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : card s = 0
⊢ f x = b
exact False.elim (card_ne_zero_of_mem hx hc0)
case neg
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : ¬card s = 0
h1 : card s = 1
⊢ f x = b
case neg
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : ¬card s = 0
⊢ f x = b
have h1 : s.card = 1 := le_antisymm hc (Nat.one_le_of_lt (Nat.pos_of_ne_zero hc0))
case neg
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : ¬card s = 0
h1 : ∃ a, s = {a}
⊢ f x = b
case neg
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : ¬card s = 0
h1 : card s = 1
⊢ f x = b
rw [card_eq_one] at h1
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : ¬card s = 0
x2 : α
hx2 : s = {x2}
⊢ f x = b
case neg
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : ¬card s = 0
h1 : ∃ a, s = {a}
⊢ f x = b
cases' h1 with x2 hx2
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hc0 : ¬card s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
⊢ f x = b
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hx : x ∈ s
hc0 : ¬card s = 0
x2 : α
hx2 : s = {x2}
⊢ f x = b
rw [hx2, mem_singleton] at hx
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬card s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : ∏ x in {x2}, f x = b
⊢ f x = b
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
h : ∏ x in s, f x = b
x : α
hc0 : ¬card s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
⊢ f x = b
simp_rw [hx2] at h
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬card s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : ∏ x in {x2}, f x = b
⊢ f x2 = b
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬card s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : ∏ x in {x2}, f x = b
⊢ f x = b
rw [hx]
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬card s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : f x2 = b
⊢ f x2 = b
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬card s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : ∏ x in {x2}, f x = b
⊢ f x2 = b
rw [prod_singleton] at h
no goals
case neg.intro
ι : Type ?u.793618
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
hc : card s ≤ 1
f : α → β
b : β
x : α
hc0 : ¬card s = 0
x2 : α
hx : x = x2
hx2 : s = {x2}
h : f x2 = b
⊢ f x2 = b
exact h