awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ Insert.insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ Insert.insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
insert :
  f a b * ∏ x ∈ s.attach, f (↑x : ι) (g (↑x : ι) ⋯) =
    f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) a ⋯) : ι)
        (Pi.cons (δ := κ) s a b g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) a ⋯) : ι) ⋯) *
      ∏ x ∈ s.attach,
        f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) (↑x : ι) ⋯) : ι)
          (Pi.cons (δ := κ) s a b g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) (↑x : ι) ⋯) : ι) ⋯)
insert₁ :
  Set.InjOn (β := ↥(Insert.insert a s))
    (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) (↑x : ι) ⋯) (↑s.attach : Set ↥s)
insert₂ :
  Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) a ⋯ ∉
    image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) (↑x : ι) ⋯) s.attach
⊢ f a b * ∏ x ∈ s.attach, f (↑x : ι) (g (↑x : ι) ⋯) =
    ∏ x ∈ (Insert.insert a s).attach, f (↑x : ι) (Pi.cons (δ := κ) s a b g (↑x : ι) ⋯)

Tactic:
rw [attach_insert, prod_insert, prod_image]

Premises used: Finset.prod_insert, Finset.attach_insert, Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ Insert.insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ Insert.insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
insert :
  f a b * ∏ x ∈ s.attach, f (↑x : ι) (g (↑x : ι) ⋯) =
    f a b * ∏ x ∈ s.attach, f (↑x : ι) (Pi.cons (δ := κ) s a b g (↑x : ι) ⋯)
⊢ f a b * ∏ x ∈ s.attach, f (↑x : ι) (g (↑x : ι) ⋯) =
    f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) a ⋯) : ι)
        (Pi.cons (δ := κ) s a b g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) a ⋯) : ι) ⋯) *
      ∏ x ∈ s.attach,
        f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) (↑x : ι) ⋯) : ι)
          (Pi.cons (δ := κ) s a b g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert a s) (↑x : ι) ⋯) : ι) ⋯)

Tactic:
simp only [Pi.cons_same]

Premises used: Finset.Pi.cons_same
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ Insert.insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ Insert.insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
insert :
  ∀ (v : ι) (hv : v ∈ s),
    f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) (g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) ⋯) =
      f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι)
        (Pi.cons (δ := κ) s a b g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) ⋯)
⊢ f a b * ∏ x ∈ s.attach, f (↑x : ι) (g (↑x : ι) ⋯) =
    f a b * ∏ x ∈ s.attach, f (↑x : ι) (Pi.cons (δ := κ) s a b g (↑x : ι) ⋯)

Tactic:
congr with ⟨v, hv⟩
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ Insert.insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ Insert.insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
v : ι
hv : v ∈ s
insert :
  g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) ⋯ =
    Pi.cons (δ := κ) s a b g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) ⋯
⊢ f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) (g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) ⋯) =
    f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι)
      (Pi.cons (δ := κ) s a b g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) ⋯)

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
hv : a ∈ s
⊢ False

Tactic:
ha hv
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
hv : a ∈ s
⊢ False

Tactic:
exact ha hv
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
v : ι
hv : v ∈ s
⊢ g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) ⋯ =
    Pi.cons (δ := κ) s a b g (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) v hv) : ι) ⋯

Tactic:
exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm

Premises used: Finset.Pi.cons_ne, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
⊢ Set.InjOn (β := ↥(insert a s)) (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert a s) (↑x : ι) ⋯)
    (↑s.attach : Set ↥s)

Tactic:
fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj

Premises used: Function.comp, Subtype.mk.inj, Set.InjOn, Subtype.ext
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
⊢ Set.InjOn (β := ↥(insert a s)) (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert a s) (↑x : ι) ⋯)
    (↑s.attach : Set ↥s)

Tactic:
exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj

Premises used: Function.comp, Subtype.mk.inj, Subtype.ext
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
h₁ :
  ∀ x ∈ t a,
    ∀ y ∈ t a,
      x ≠ y →
        Disjoint (α := Finset ((a' : ι) → (h : a' ∈ insert a s) → κ a'))
          (image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t)) (image (Pi.cons (δ := κ) s a y) (s.pi (β := κ) t))
b : κ a
h : b ∈ t a
h₂ :
  ∀ p₁ ∈ s.pi (β := κ) t,
    ∀ p₂ ∈ s.pi (β := κ) t,
      Eq (α := (a' : ι) → (h : a' ∈ insert a s) → κ a') (Pi.cons (δ := κ) s a b p₁) (Pi.cons (δ := κ) s a b p₂) →
        p₁ = p₂
g : (a : ι) → a ∈ s → κ a
h_1 : g ∈ s.pi (β := κ) t
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert a s) a ⋯ ∉
    image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert a s) (↑x : ι) ⋯) s.attach

Tactic:
simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha

Premises used: Finset.mem_image, Finset.mem_attach, Subtype.exists, exists_eq_right, exists_prop, Subtype.mk.injEq, true_and
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
empty :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ ∅, ∑ b ∈ t a, f a b) (∑ p ∈ pi (β := κ) ∅ t, ∏ x ∈ attach ∅, f (↑x : ι) (p (↑x : ι) ⋯))
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b)
        (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))),
    Eq.{u_4 + 1} (α := R) (∏ a ∈ Insert.insert a s, ∑ b ∈ t a, f a b)
      (∑ p ∈ (Insert.insert a s).pi (β := κ) t, ∏ x ∈ (Insert.insert a s).attach, f (↑x : ι) (p (↑x : ι) ⋯))
⊢ Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha

Premises used: Finset.mul_sum, Finset.prod_insert, Finset.mem_image, Finset.attach_insert, Finset.mem_attach, Function.comp, Subtype.exists, exists_eq_right, Finset.Pi.cons_ne, Insert.insert, exists_prop, Subtype.mk.inj, Subtype.mk.injEq, Finset.Pi.cons_same, Eq.symm, Finset.sum_congr, rfl, true_and, Finset.sum_mul, Finset.prod_image, Subtype.ext
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
empty :
  Eq.{u_4 + 1} (α := R) (∏ a ∈ ∅, ∑ b ∈ t a, f a b) (∑ p ∈ pi (β := κ) ∅ t, ∏ x ∈ attach ∅, f (↑x : ι) (p (↑x : ι) ⋯))
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b)
        (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))),
    Eq.{u_4 + 1} (α := R) (∏ a ∈ Insert.insert a s, ∑ b ∈ t a, f a b)
      (∑ p ∈ (Insert.insert a s).pi (β := κ) t, ∏ x ∈ (Insert.insert a s).attach, f (↑x : ι) (p (↑x : ι) ⋯))
⊢ Eq.{u_4 + 1} (α := R) (∏ a ∈ s, ∑ b ∈ t a, f a b) (∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha

Premises used: Finset.mul_sum, Finset.prod_insert, Finset.mem_image, Finset.attach_insert, Finset.mem_attach, Function.comp, Subtype.exists, exists_eq_right, Finset.Pi.cons_ne, Insert.insert, exists_prop, Subtype.mk.inj, Subtype.mk.injEq, Finset.Pi.cons_same, Eq.symm, Finset.sum_congr, rfl, true_and, Finset.sum_mul, Finset.prod_image, Subtype.ext
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
κ : ι → Type u_5
inst_2 : Fintype ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
⊢ Eq.{u_4 + 1} (α := R) (∏ i : ι, ∑ j ∈ t i, f i j) (∑ x ∈ piFinset (δ := κ) t, ∏ i : ι, f i (x i))

Tactic:
simp only [prod_attach_univ, prod_sum, Finset.sum_univ_pi]

Premises used: Finset.prod_attach_univ, Finset.sum_univ_pi, Finset.prod_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
inst_2 : Fintype ι
s : Finset κ
g : ι → κ → R
rw rw₁ : Eq.{u_4 + 1} (α := R) (∏ i : ι, ∑ j ∈ s, g i j) (∏ i : ι, ∑ j ∈ s, g i j)
⊢ Eq.{u_4 + 1} (α := R) (∑ f ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s, ∏ i : ι, g i (f i))
    (∏ i : ι, ∑ j ∈ s, g i j)

Tactic:
rw [← prod_univ_sum]

Premises used: Finset.prod_univ_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
κ : Type u_2
R : Type u_4
inst : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
⊢ Eq.{u_4 + 1} (α := R) (∏ i : Fin n, ∑ j ∈ s, f j)
    (∑ x ∈ piFinset (δ := fun (_i : Fin n) ↦ κ) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (x i))

Tactic:
@prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d

Premises used: Finset.prod_univ_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
κ : Type u_2
R : Type u_4
inst : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
h : HPow.hPow (α := R) (∑ a ∈ s, f a) n = ∏ i : Fin n, ∑ j ∈ s, f j
⊢ HPow.hPow (α := R) (∑ a ∈ s, f a) n =
    ∑ p ∈ piFinset (δ := fun (_i : Fin n) ↦ κ) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)

Tactic:
convert! @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d

Premises used: Finset.prod_univ_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
κ : Type u_2
R : Type u_4
inst : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
⊢ HPow.hPow (α := R) (∑ a ∈ s, f a) n = ∏ i : Fin n, ∑ j ∈ s, f j

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s, (f i + g i)) (∏ i ∈ s, ∑ p ∈ {True, False}, if p then f i else g i)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s, ∑ p ∈ {True, False}, if p then f i else g i)
    (∑ p ∈ s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False},
      ∏ a ∈ s.attach, if p (↑a : ι) ⋯ then f (↑a : ι) else g (↑a : ι))

Tactic:
prod_sum _ _ _

Premises used: Finset.prod_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ (a : (a : ι) → a ∈ s → Prop)
    (ha :
      Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop)) (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False})
        a),
    (fun (f : (a : ι) → a ∈ s → Prop)
            (x :
              Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop))
                (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False}) f) ↦
          {a ∈ s | ∃ (h : a ∈ s), f a h})
        a ha ∈
      s.powerset

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ (a : Finset ι) (ha : a ∈ s.powerset),
    Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop)) (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False})
      ((fun (t : Finset ι) (x : t ∈ s.powerset) (a : ι) (x_1 : a ∈ s) ↦ a ∈ t) a ha)

Tactic:
simp [Classical.em]

Premises used: Classical.em
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
simp_rw :
  ∀ (a : (a : ι) → a ∈ s → Prop)
    (ha : ∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) (x : ι)
    (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
⊢ ∀ (a : (a : ι) → a ∈ s → Prop)
    (ha :
      Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop)) (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False})
        a),
    (fun (t : Finset ι) (x : t ∈ s.powerset) (a : ι) (x_1 : a ∈ s) ↦ a ∈ t)
        ((fun (f : (a : ι) → a ∈ s → Prop)
              (x :
                Membership.mem (γ := Finset ((a : ι) → a ∈ s → Prop))
                  (s.pi (β := fun (a : ι) ↦ Prop) fun (x : ι) ↦ {True, False}) f) ↦
            {a ∈ s | ∃ (h : a ∈ s), f a h})
          a ha)
        ⋯ =
      a

Tactic:
simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]

Premises used: funext_iff, Finset.mem_insert, Finset.mem_pi, Finset.mem_filter, eq_iff_iff
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : DecidableEq ι
f g : ι → R
s : Finset ι
tauto tauto₁ tauto₂ tauto₃ tauto₄ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1
mp :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) → a x x_1
mpr :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s ∧ ∃ (h : x ∈ s), a x h
mp₁ mp₂ mp₃ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), x ∈ s → ∀ (w : x ∈ s), a x w → a x x_1
mpr₁ mpr₂ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s ∧ ∃ (h : x ∈ s), a x h
mpr₃ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → x ∈ s
mpr₄ mpr₅ mpr₆ mpr₇ mpr₈ mpr₉ :
  ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) →
      ∀ (x : ι) (x_1 : x ∈ s), a x x_1 → ∃ (h : x ∈ s), a x h
⊢ ∀ (a : (a : ι) → a ∈ s → Prop)
    (ha : ∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ Membership.mem (γ := Finset Prop) {False} (a a_1 h)) (x : ι)
    (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1

Tactic:
tauto