α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ ∀ (x_1 : Finset α), x_1 ∈ powerset s → ∀ (y : Finset α), y ∈ powerset s → insert x x_1 = insert x y → x_1 = y

α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ Disjoint (powerset s) (image (insert x) (powerset s))
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ ∏ a in powerset (insert x s), f a = (∏ a in powerset s, f a) * ∏ t in powerset s, f (insert x t)
rw [powerset_insert, Finset.prod_union, Finset.prod_image]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ powerset s
heq : insert x t₁ = insert x t₂
⊢ t₁ = t₂
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ ∀ (x_1 : Finset α), x_1 ∈ powerset s → ∀ (y : Finset α), y ∈ powerset s → insert x x_1 = insert x y → x_1 = y
intro t₁ h₁ t₂ h₂ heq
no goals
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ powerset s
heq : insert x t₁ = insert x t₂
⊢ t₁ = t₂
rw [← Finset.erase_insert (not_mem_of_mem_powerset_of_not_mem h₁ h), ←
  Finset.erase_insert (not_mem_of_mem_powerset_of_not_mem h₂ h), heq]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ ∀ (a : Finset α), a ∈ powerset s → ∀ (b : Finset α), b ∈ image (insert x) (powerset s) → a ≠ b
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ Disjoint (powerset s) (image (insert x) (powerset s))
rw [Finset.disjoint_iff_ne]
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ image (insert x) (powerset s)
⊢ t₁ ≠ t₂
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
⊢ ∀ (a : Finset α), a ∈ powerset s → ∀ (b : Finset α), b ∈ image (insert x) (powerset s) → a ≠ b
intro t₁ h₁ t₂ h₂
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ image (insert x) (powerset s)
t₃ : Finset α
_h₃ : t₃ ∈ powerset s
H₃₂ : insert x t₃ = t₂
⊢ t₁ ≠ t₂
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ image (insert x) (powerset s)
⊢ t₁ ≠ t₂
rcases Finset.mem_image.1 h₂ with ⟨t₃, _h₃, H₃₂⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ image (insert x) (powerset s)
t₃ : Finset α
_h₃ : t₃ ∈ powerset s
H₃₂ : insert x t₃ = t₂
⊢ t₁ ≠ insert x t₃
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ image (insert x) (powerset s)
t₃ : Finset α
_h₃ : t₃ ∈ powerset s
H₃₂ : insert x t₃ = t₂
⊢ t₁ ≠ t₂
rw [← H₃₂]
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : Finset α
x : α
h : ¬x ∈ s
f : Finset α → β
t₁ : Finset α
h₁ : t₁ ∈ powerset s
t₂ : Finset α
h₂ : t₂ ∈ image (insert x) (powerset s)
t₃ : Finset α
_h₃ : t₃ ∈ powerset s
H₃₂ : insert x t₃ = t₂
⊢ t₁ ≠ insert x t₃
exact ne_insert_of_not_mem _ _ (not_mem_of_mem_powerset_of_not_mem h₁ h)