ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
⊢ ∏ x in s, f x = f a * f b
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
⊢ ∏ x in s, f x = f a * f b
haveI := Classical.decEq α
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
⊢ ∏ x in s, f x = f a * f b
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
⊢ ∏ x in s, f x = f a * f b
let s' := ({a, b} : Finset α)
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
⊢ ∏ x in s, f x = f a * f b
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
⊢ ∏ x in s, f x = f a * f b
have hu : s' ⊆ s := by
  refine' insert_subset.mpr _
  apply And.intro ha
  apply singleton_subset_iff.mpr hb
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
hf : ∀ (c : α), c ∈ s → ¬c ∈ s' → f c = 1
⊢ ∏ x in s, f x = f a * f b
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
⊢ ∏ x in s, f x = f a * f b
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
  apply mem_insert.mpr
  rw [mem_singleton]
  exact hab
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
hf : ∀ (c : α), c ∈ s → ¬c ∈ s' → f c = 1
⊢ ∏ x in s', f x = f a * f b
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
hf : ∀ (c : α), c ∈ s → ¬c ∈ s' → f c = 1
⊢ ∏ x in s, f x = f a * f b
rw [← prod_subset hu hf]
no goals
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
hf : ∀ (c : α), c ∈ s → ¬c ∈ s' → f c = 1
⊢ ∏ x in s', f x = f a * f b
exact Finset.prod_pair hn
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
⊢ a ∈ s ∧ {b} ⊆ s
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
⊢ s' ⊆ s
refine' insert_subset.mpr _
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
⊢ {b} ⊆ s
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
⊢ a ∈ s ∧ {b} ⊆ s
apply And.intro ha
no goals
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
⊢ {b} ⊆ s
apply singleton_subset_iff.mpr hb
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
⊢ ∀ (c : α), c ∈ s → ¬c ∈ s' → f c = 1
intro c hc hcs
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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
apply h₀ c hc
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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)
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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
apply not_or.mp
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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)
intro hab
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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'
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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
apply hcs
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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}
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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'
apply mem_insert.mpr
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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}
rw [mem_singleton]
no goals
ι : Type ?u.373499
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ (c : α), 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
exact hab