awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.1 ≤ y.1
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0

Tactic:
simp [apply_eq_zero_of_not_le hxy]

Premises used: IncidenceAlgebra.apply_eq_zero_of_not_le
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.2 ≤ y.2
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0

Tactic:
simp [apply_eq_zero_of_not_le hxy]

Premises used: IncidenceAlgebra.apply_eq_zero_of_not_le
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕜 β
a₁ a₂ : α
b₁ b₂ : β
⊢ (f.prod g : (a : α × β) → α × β → 𝕜) (a₁, b₁) (a₂, b₂) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a₁ a₂ : 𝕜) ((g : (a : β) → β → 𝕜) b₁ b₂ : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕜 β
x y : α × β
⊢ (f.prod g : (a : α × β) → α × β → 𝕜) x y =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableLE (α × β)
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((f₁ : (a : α) → α → 𝕜) a₁ a₂ : 𝕜) ((g₁ : (a : β) → β → 𝕜) b₁ b₂ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) ((f₂ : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) ((g₂ : (a : β) → β → 𝕜) b₂ b₃ : 𝕜) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((f₁ : (a : α) → α → 𝕜) a₁ a₂ : 𝕜) ((f₂ : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) ((g₁ : (a : β) → β → 𝕜) b₁ b₂ : 𝕜) ((g₂ : (a : β) → β → 𝕜) b₂ b₃ : 𝕜)
h₁ :
  ∀ (x y : α × β),
    x ≤ y →
      Eq.{u_2 + 1} (α := 𝕜) ((f₁.prod g₁ * f₂.prod g₂ : (a : α × β) → α × β → 𝕜) x y : 𝕜)
        (((f₁ * f₂).prod (g₁ * g₂) : (a : α × β) → α × β → 𝕜) x y : 𝕜)
⊢ f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)

Tactic:
ext x y
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableLE (α × β)
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((f₁ : (a : α) → α → 𝕜) a₁ a₂ : 𝕜) ((g₁ : (a : β) → β → 𝕜) b₁ b₂ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) ((f₂ : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) ((g₂ : (a : β) → β → 𝕜) b₂ b₃ : 𝕜) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((f₁ : (a : α) → α → 𝕜) a₁ a₂ : 𝕜) ((f₂ : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) ((g₁ : (a : β) → β → 𝕜) b₁ b₂ : 𝕜) ((g₂ : (a : β) → β → 𝕜) b₂ b₃ : 𝕜)
x y : α × β
h_1 : x ≤ y
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f₁.prod g₁ * f₂.prod g₂ : (a : α × β) → α × β → 𝕜) x y : 𝕜)
    (((f₁ * f₂).prod (g₁ * g₂) : (a : α × β) → α × β → 𝕜) x y : 𝕜)

Tactic:
simp [Icc_prod_def, sum_mul_sum, h, sum_product]

Premises used: Finset.Icc_prod_def, Finset.sum_product, Finset.sum_mul_sum
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : DecidableEq α
inst_4 : DecidableEq β
h :
  ∀ (x y : α × β),
    x ≤ y →
      Eq.{u_2 + 1} (α := 𝕜) ((IncidenceAlgebra.prod 1 1 : (a : α × β) → α × β → 𝕜) x y : 𝕜)
        ((1 : (a : α × β) → α × β → 𝕜) x y : 𝕜)
⊢ Eq (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod 1 1) 1

Tactic:
ext x y
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : DecidableEq α
inst_4 : DecidableEq β
x y : α × β
h : x ≤ y
⊢ Eq.{u_2 + 1} (α := 𝕜) ((IncidenceAlgebra.prod 1 1 : (a : α × β) → α × β → 𝕜) x y : 𝕜)
    ((1 : (a : α × β) → α × β → 𝕜) x y : 𝕜)

Tactic:
simp [Prod.ext_iff, ← ite_and, and_comm]

Premises used: Prod.ext_iff, and_comm, ite_and
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : DecidableLE α
inst_4 : DecidableLE β
h :
  ∀ (x y : α × β) (hxy : x ≤ y),
    Eq.{u_2 + 1} (α := 𝕜) ((IncidenceAlgebra.prod (zeta 𝕜) (zeta 𝕜) : (a : α × β) → α × β → 𝕜) x y : 𝕜)
      ((zeta 𝕜 : (a : α × β) → α × β → 𝕜) x y : 𝕜)
⊢ Eq (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod (zeta 𝕜) (zeta 𝕜)) (zeta 𝕜)

Tactic:
ext x y hxy
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : DecidableLE α
inst_4 : DecidableLE β
x y : α × β
hxy : x ≤ y
⊢ Eq.{u_2 + 1} (α := 𝕜) ((IncidenceAlgebra.prod (zeta 𝕜) (zeta 𝕜) : (a : α × β) → α × β → 𝕜) x y : 𝕜)
    ((zeta 𝕜 : (a : α × β) → α × β → 𝕜) x y : 𝕜)

Tactic:
simp [hxy, hxy.1, hxy.2]

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : CommRing 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableLE (α × β)
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
⊢ f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)

Tactic:
prod_mul_prod' _ _ _ _ fun _ _ _ _ _ _ ↦ mul_mul_mul_comm ..

Premises used: mul_mul_mul_comm, IncidenceAlgebra.prod_mul_prod', DFunLike.coe
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableEq α
inst_6 : DecidableEq β
inst_7 : DecidableLE α
inst_8 : DecidableLE β
⊢ Eq (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod (mu 𝕜) (mu 𝕜)) (mu 𝕜)

Tactic:
left_inv_eq_right_inv ?_ zeta_mul_mu

Premises used: left_inv_eq_right_inv, IncidenceAlgebra.zeta_mul_mu
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableEq α
inst_6 : DecidableEq β
inst_7 : DecidableLE α
inst_8 : DecidableLE β
refine : HMul.hMul (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod (mu 𝕜) (mu 𝕜)) (zeta 𝕜) = 1
⊢ Eq (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod (mu 𝕜) (mu 𝕜)) (mu 𝕜)

Tactic:
refine left_inv_eq_right_inv ?_ zeta_mul_mu

Premises used: left_inv_eq_right_inv
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableEq α
inst_6 : DecidableEq β
inst_7 : DecidableLE α
inst_8 : DecidableLE β
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 α) : (a : α) → α → 𝕜) a₁ a₂ : 𝕜)
          (((mu 𝕜 : IncidenceAlgebra 𝕜 β) : (a : β) → β → 𝕜) b₁ b₂ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) ((zeta 𝕜 : (a : β) → β → 𝕜) b₂ b₃ : 𝕜) =
      HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 α) : (a : α) → α → 𝕜) a₁ a₂ : 𝕜)
          ((zeta 𝕜 : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 β) : (a : β) → β → 𝕜) b₁ b₂ : 𝕜)
          ((zeta 𝕜 : (a : β) → β → 𝕜) b₂ b₃ : 𝕜)
⊢ HMul.hMul (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod (mu 𝕜) (mu 𝕜)) (zeta 𝕜) = 1

Tactic:
rw [← zeta_prod_zeta, prod_mul_prod', mu_mul_zeta, mu_mul_zeta, one_prod_one]

Premises used: IncidenceAlgebra.one_prod_one, IncidenceAlgebra.mu_mul_zeta, IncidenceAlgebra.prod_mul_prod', IncidenceAlgebra.zeta_prod_zeta
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableEq α
inst_6 : DecidableEq β
inst_7 : DecidableLE α
inst_8 : DecidableLE β
x x_1 x_2 : α
x_3 x_4 x_5 : β
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 β) : (a : β) → β → 𝕜) x_3 x_4 : 𝕜)
      ((zeta 𝕜 : (a : α) → α → 𝕜) x_1 x_2 : 𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x_1 x_2 : 𝕜)
      (((mu 𝕜 : IncidenceAlgebra 𝕜 β) : (a : β) → β → 𝕜) x_3 x_4 : 𝕜)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableEq α
inst_6 : DecidableEq β
inst_7 : DecidableLE α
inst_8 : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 α) : (a : α) → α → 𝕜) a₁ a₂ : 𝕜)
          (((mu 𝕜 : IncidenceAlgebra 𝕜 β) : (a : β) → β → 𝕜) b₁ b₂ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) ((zeta 𝕜 : (a : β) → β → 𝕜) b₂ b₃ : 𝕜) =
      HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 α) : (a : α) → α → 𝕜) a₁ a₂ : 𝕜)
          ((zeta 𝕜 : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 β) : (a : β) → β → 𝕜) b₁ b₂ : 𝕜)
          ((zeta 𝕜 : (a : β) → β → 𝕜) b₂ b₃ : 𝕜)

Tactic:
exact fun _ _ _ _ _ _ ↦ Commute.mul_mul_mul_comm (by simp : _ = _) _ _

Premises used: Commute.mul_mul_mul_comm
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableEq α
inst_6 : DecidableEq β
inst_7 : DecidableLE α
inst_8 : DecidableLE β
inst_9 : BoundedOrder α
inst_10 : BoundedOrder β
⊢ eulerChar 𝕜 (α × β) = eulerChar 𝕜 α * eulerChar 𝕜 β

Tactic:
simp [eulerChar, ← mu_prod_mu]

Premises used: IncidenceAlgebra.eulerChar, IncidenceAlgebra.mu_prod_mu
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
pos :
  ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
    Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
neg :
  ∀ (ha : a ∉ ⋃ i ∈ s, S i),
    Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0

Tactic:
by_cases ha : a ∈ ⋃ i ∈ s, S i
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a

Tactic:
have ha' := ha
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha ha' : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
⊢ ∃ i ∈ s, a ∈ S i

Tactic:
simp only [Set.mem_iUnion, exists_prop] at ha

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha' : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
ha : ∃ i ∈ s, a ∈ S i
pos :
  ∀ (i : ι) (hi : i ∈ s) (ha : a ∈ S i),
    Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0

Tactic:
obtain ⟨i, hi, ha⟩ := ha
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha' : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
i : ι
hi : i ∈ s
ha : a ∈ S i
⊢ HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a) = 0

Tactic:
simp [ha, ha']
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha' : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
i : ι
hi : i ∈ s
ha : a ∈ S i
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0

Tactic:
apply prod_eq_zero hi (by simp [ha, ha'])

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
neg :
  ∀ (i : ι) (hi : i ∈ s),
    Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0

Tactic:
obtain ⟨i, hi⟩ := hs
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
⊢ a ∉ S i

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
⊢ a ∉ S i

Tactic:
have ha : a ∉ S i := by aesop
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha_1 : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
ha : a ∉ S i
⊢ HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a) = 0

Tactic:
simp [*, -coe_biUnion]

Premises used: Finset.coe_biUnion
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha_1 : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
ha : a ∉ S i
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0

Tactic:
exact prod_eq_zero hi <| by simp [*, -coe_biUnion]

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
pos :
  ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
    Set.indicator (⋃ i ∈ s, S i) f a =
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
neg :
  ∀ (ha : a ∉ ⋃ i ∈ s, S i),
    Set.indicator (⋃ i ∈ s, S i) f a =
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
⊢ Set.indicator (⋃ i ∈ s, S i) f a =
    ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a

Tactic:
by_cases ha : a ∈ ⋃ i ∈ s, S i
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
neg :
  Eq.{u_3 + 1} (α := G) 0
    (∑ x ∈ s.powerset with x.Nonempty, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a))
⊢ Set.indicator (⋃ i ∈ s, S i) f a =
    ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a

Tactic:
simp only [ha, not_false_eq_true, Set.indicator_of_notMem, Int.reduceNeg, pow_succ, mul_neg,
      mul_one, neg_smul]

Premises used: neg_smul, pow_succ, Int.reduceNeg, Set.indicator_of_notMem, mul_one, not_false_eq_true, mul_neg
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
neg :
  Eq.{u_3 + 1} (α := G)
    (∑ x ∈ s.powerset with x.Nonempty, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a)) 0
⊢ Eq.{u_3 + 1} (α := G) 0
    (∑ x ∈ s.powerset with x.Nonempty, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a))

Tactic:
symm
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
neg : ∀ x ∈ {t ∈ s.powerset | t.Nonempty}, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a) = 0
⊢ Eq.{u_3 + 1} (α := G)
    (∑ x ∈ s.powerset with x.Nonempty, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a)) 0

Tactic:
apply sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
neg : ∀ x ⊆ s, x.Nonempty → HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a = 0
⊢ ∀ x ∈ {t ∈ s.powerset | t.Nonempty}, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a) = 0

Tactic:
simp only [Int.reduceNeg, neg_eq_zero, mem_filter, mem_powerset, and_imp]

Premises used: and_imp, Int.reduceNeg, neg_eq_zero, Finset.mem_powerset, Finset.mem_filter
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
neg : HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) 0 = 0
neg₁ : a ∉ ⋂ i ∈ t, S i
⊢ HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a = 0

Tactic:
rw [Set.indicator_of_notMem]

Premises used: Set.indicator_of_notMem
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) 0 = 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
neg : ∀ (ha : Membership.mem (γ := Set α) (⋂ i ∈ t, S i) a), Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
⊢ a ∉ ⋂ i ∈ t, S i

Tactic:
contrapose ha
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
ha : Membership.mem (γ := Set α) (⋂ i ∈ t, S i) a
⊢ ∀ (i : ι) (i_1 : i ∈ t), a ∈ S i

Tactic:
simp only [Set.mem_iInter] at ha

Premises used: Set.mem_iInter
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
ha : ∀ (i : ι) (i_1 : i ∈ t), a ∈ S i
neg : ∀ (i : ι) (hi : i ∈ t), Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a

Tactic:
rcases ht with ⟨i, hi⟩
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ha : ∀ (i : ι) (i_1 : i ∈ t), a ∈ S i
i : ι
hi : i ∈ t
neg : ∃ i ∈ s, a ∈ S i
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a

Tactic:
simp only [Set.mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ha : ∀ (i : ι) (i_1 : i ∈ t), a ∈ S i
i : ι
hi : i ∈ t
⊢ ∃ i ∈ s, a ∈ S i

Tactic:
⟨i, hts hi, ha _ hi⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ha : ∀ (i : ι) (i_1 : i ∈ t), a ∈ S i
i : ι
hi : i ∈ t
⊢ ∃ i ∈ s, a ∈ S i

Tactic:
exact ⟨i, hts hi, ha _ hi⟩
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
pos :
  Set.indicator (⋃ i ∈ s, S i) f a -
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a =
    0
⊢ Set.indicator (⋃ i ∈ s, S i) f a =
    ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
⊢ Set.indicator (⋃ i ∈ s, S i) f a -
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t.val, S i) f a =
    HAdd.hAdd (α := G) (∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)
      (∑ t ∈ s.powerset with ¬t.Nonempty, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)

Tactic:
simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ, ha]

Premises used: pow_succ, sub_eq_neg_add, Finset.filter_eq', Finset.sum_neg_distrib
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
rw rw₁ :
  Eq.{u_3 + 1} (α := G) (∑ x ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a)
    (∑ t ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)
⊢ HAdd.hAdd (α := G) (∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)
      (∑ t ∈ s.powerset with ¬t.Nonempty, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a) =
    ∑ t ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a

Tactic:
rw [sum_filter_add_sum_filter_not]

Premises used: Finset.sum_filter_add_sum_filter_not
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
simp :
  Eq.{u_3 + 1} (α := G) (∑ t ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)
    (∑ i ∈ s.powerset, (HPow.hPow (α := ℤ) (-1) #i * ∏ i ∈ i, (S i).indicator 1 a) • f a)
⊢ ∑ t ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a =
    HSMul.hSMul (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) 1 ((S i).indicator 1 a)) (f a)

Tactic:
simp only [Int.reduceNeg, prod_sub, prod_const_one, mul_one, sum_smul]

Premises used: Finset.sum_smul, Finset.prod_sub, Int.reduceNeg, Finset.prod_const_one, mul_one