ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
ha : ¬a ∈ s → f a = 1
hb : ¬b ∈ s → f b = 1
this : DecidableEq α
⊢ ∏ x in s, f x = f a * f b
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
ha : ¬a ∈ s → f a = 1
hb : ¬b ∈ s → f b = 1
⊢ ∏ x in s, f x = f a * f b
haveI := Classical.decEq α
case pos
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a * f b

case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a * f b

case pos
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a * f b

case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a * f b
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
ha : ¬a ∈ s → f a = 1
hb : ¬b ∈ s → f b = 1
this : DecidableEq α
⊢ ∏ x in s, f x = f a * f b
by_cases h₁ : a ∈ s <;> by_cases h₂ : b ∈ s
no goals
case pos
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a * f b
exact prod_eq_mul_of_mem a b h₁ h₂ hn h₀
case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a
case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a * f b
rw [hb h₂, mul_one]
case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 : α), b ∈ s → b ≠ a → f b = 1
case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a
apply prod_eq_single_of_mem a h₁
no goals
case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 : α), b ∈ s → b ≠ a → f b = 1
exact fun c hc hca => h₀ c hc ⟨hca, ne_of_mem_of_not_mem hc h₂⟩
case pos
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f b
case pos
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a * f b
rw [ha h₁, one_mul]
case pos
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 : α), b_1 ∈ s → b_1 ≠ b → f b_1 = 1
case pos
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f b
apply prod_eq_single_of_mem b h₂
no goals
case pos
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 : α), b_1 ∈ s → b_1 ≠ b → f b_1 = 1
exact fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩
case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = 1
case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = f a * f b
rw [ha h₁, hb h₂, mul_one]
no goals
case neg
ι : Type ?u.375985
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
hn : a ≠ b
h₀ : ∀ (c : α), 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 in s, f x = 1
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