awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Finset ι
t : Finset κ
f : ι → R
g : κ → R
simp_rw : Eq.{u_4 + 1} (α := R) (∑ i ∈ s, f i * ∑ j ∈ t, g j) (∑ i ∈ s, ∑ j ∈ t, f i * g j)
⊢ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ j ∈ t, g j) = ∑ i ∈ s, ∑ j ∈ t, f i * g j

Tactic:
simp_rw [sum_mul, ← mul_sum]

Premises used: Finset.mul_sum, Finset.sum_mul
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_4
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype ι
inst_2 : Fintype κ
f : ι → R
g : κ → R
⊢ HMul.hMul (α := R) (∑ i : ι, f i) (∑ j : κ, g j) = ∑ i : ι, ∑ j : κ, f i * g j

Tactic:
Finset.sum_mul_sum _ _ _ _

Premises used: Finset.sum_mul_sum
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Finset ι
f : ι → R
b_1 : R
h : ∀ i ∈ s, Commute b_1 (f i)
b : R
hb : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) b
obtain :
  ∀ (i : ι) (hi : i ∈ s.val) (hb : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) (f i)),
    Commute b_1 (f i)
⊢ Commute b_1 b

Tactic:
obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hb

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Finset ι
f : ι → R
b : R
h : ∀ i ∈ s, Commute b (f i)
i : ι
hi : i ∈ s.val
hb : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) (f i)
⊢ Commute b (f i)

Tactic:
h _ hi
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Finset ι
f : ι → R
b : R
h : ∀ i ∈ s, Commute b (f i)
i : ι
hi : i ∈ s.val
hb : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) (f i)
⊢ Commute b (f i)

Tactic:
exact h _ hi
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Finset ι
f : ι → R
b : R
h : ∀ i ∈ s, Commute (f i) b
⊢ Commute (∑ i ∈ s, f i) b

Tactic:
((Commute.sum_right _ _ _) fun _i hi => (h _ hi).symm).symm

Premises used: Commute.symm, Commute.sum_right
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
R : Type u_4
inst : NonUnitalNonAssocSemiring R
m n : ℕ
f g : ℕ → R
⊢ HMul.hMul (α := R) (∑ i ∈ range (m + 1), f i) (∑ i ∈ range (n + 1), g i) =
    HMul.hMul (α := R) (∑ i ∈ range m, f i) (∑ i ∈ range n, g i) + f m * ∑ i ∈ range n, g i +
        (∑ i ∈ range m, f i) * g n +
      f m * g n

Tactic:
simp only [add_mul, mul_add, add_assoc, sum_range_succ]

Premises used: add_mul, add_assoc, mul_add, Finset.sum_range_succ
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
s : Finset ι
inst : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
y : R
hy : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) y
rcases :
  ∀ (x : ι) (hx : x ∈ s.val) (hy : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) (f x)),
    a ∣ f x
⊢ a ∣ y

Tactic:
rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
s : Finset ι
inst : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
x : ι
hx : x ∈ s.val
hy : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) (f x)
⊢ a ∣ f x

Tactic:
h x hx
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
s : Finset ι
inst : NonUnitalSemiring R
f : ι → R
a : R
h : ∀ i ∈ s, a ∣ f i
x : ι
hx : x ∈ s.val
hy : Membership.mem (γ := Multiset R) (Multiset.map (fun (i : ι) ↦ f i) s.val) (f x)
⊢ a ∣ f x

Tactic:
exact h x hx
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : NonAssocSemiring R
inst_1 : DecidableEq ι
s : Finset ι
f : ι → R
i : ι
⊢ (∑ j ∈ s, f j * if i = j then 1 else 0) = if i ∈ s then f i else 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : NonAssocSemiring R
inst_1 : DecidableEq ι
s : Finset ι
f : ι → R
i : ι
⊢ ∑ j ∈ s, (if i = j then 1 else 0) * f j = if i ∈ s then f i else 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) = ∏ i ∈ s, f i

Tactic:
simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi, ← h1, right_distrib]

Premises used: Finset.prod_eq_mul_prod_diff_singleton_of_mem, right_distrib
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
e_a : Eq.{u_4 + 1} (α := R) (∏ i ∈ s \ {i}, g i) (∏ i ∈ s \ {i}, f i)
e_a₁ : Eq.{u_4 + 1} (α := R) (∏ i ∈ s \ {i}, h i) (∏ i ∈ s \ {i}, f i)
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
congr 2
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
e_a : ∀ x ∈ s \ {i}, g x = f x
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s \ {i}, g i) (∏ i ∈ s \ {i}, f i)

Tactic:
apply prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
e_a : ∀ x ∈ s \ {i}, h x = f x
⊢ Eq.{u_4 + 1} (α := R) (∏ i ∈ s \ {i}, h i) (∏ i ∈ s \ {i}, f i)

Tactic:
apply prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∀ x ∈ s \ {i}, g x = f x

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∀ x ∈ s \ {i}, h x = f x

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = f i * ∏ i ∈ s \ {i}, f i
simp_rw₁ : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = (g i + h i) * ∏ i ∈ s \ {i}, f i
simp_rw₂ : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) = ∏ i ∈ s, f i

Tactic:
classical
    simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi, ← h1, right_distrib]
    congr 2 <;> apply prod_congr rfl <;> simpa

Premises used: Finset.prod_congr, right_distrib, rfl
-- 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
⊢ Eq.{u_4 + 1} (α := R) (∏ a ∈ ∅, ∑ b ∈ t a, f a b) (∑ p ∈ pi (β := κ) ∅ t, ∏ x ∈ attach ∅, f (↑x : ι) (p (↑x : ι) ⋯))

Tactic:
simp
-- 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 : ι) ⋯))
x : κ a
_ :
  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))
⊢ 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))

Tactic:
_
-- 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 : ι) ⋯))
x : κ a
h : x ∈ t a
y : κ 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))
⊢ 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))

Tactic:
_
-- 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 : ι) ⋯))
x : κ a
h_1 : x ∈ t a
y : κ a
h_2 : y ∈ t a
h : x ≠ y
simp :
  ∀ (a_1 : (a' : ι) → (h : a' ∈ insert a s) → κ a'),
    (∃ a_2 ∈ s.pi (β := κ) t, Pi.cons (δ := κ) s a x a_2 = a_1) →
      ∀ (b : (a' : ι) → (h : a' ∈ insert a s) → κ a'),
        (∃ a_3 ∈ s.pi (β := κ) t, Pi.cons (δ := κ) s a y a_3 = b) → a_1 ≠ b
⊢ 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))

Tactic:
simp only [disjoint_iff_ne, mem_image]

Premises used: Finset.mem_image, Finset.disjoint_iff_ne
-- 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 : ι) ⋯))
x : κ a
h_1 : x ∈ t a
y : κ a
h_2 : y ∈ t a
h : x ≠ y
a_1 : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left : p₂ ∈ s.pi (β := κ) t
eq₂ : Pi.cons (δ := κ) s a x p₂ = a_1
b : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left_1 : p₃ ∈ s.pi (β := κ) t
eq₃ : Pi.cons (δ := κ) s a y p₃ = b
eq : a_1 = b
rw : a_1 a ⋯ = Pi.cons (δ := κ) s a y p₃ a ⋯
rw₁ : a_1 a ⋯ = b a ⋯
rw₂ rw₃ : b a ⋯ = b a ⋯
⊢ Pi.cons (δ := κ) s a x p₂ a ⋯ = Pi.cons (δ := κ) s a y p₃ a ⋯

Tactic:
rw [eq₂, eq₃, eq]
-- 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 : ι) ⋯))
x : κ a
h_1 : x ∈ t a
y : κ a
h_2 : y ∈ t a
h : x ≠ y
a_1 : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left : p₂ ∈ s.pi (β := κ) t
eq₂ : Pi.cons (δ := κ) s a x p₂ = a_1
b : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left_1 : p₃ ∈ s.pi (β := κ) t
eq₃ : Pi.cons (δ := κ) s a y p₃ = b
eq : a_1 = b
⊢ Pi.cons (δ := κ) s a x p₂ a ⋯ = Pi.cons (δ := κ) s a y p₃ a ⋯

Tactic:
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]
-- 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 : ι) ⋯))
x : κ a
h_1 : x ∈ t a
y : κ a
h_2 : y ∈ t a
h : x ≠ y
a_1 : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left : p₂ ∈ s.pi (β := κ) t
eq₂ : Pi.cons (δ := κ) s a x p₂ = a_1
b : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left_1 : p₃ ∈ s.pi (β := κ) t
eq₃ : Pi.cons (δ := κ) s a y p₃ = b
eq : a_1 = b
this : Pi.cons (δ := κ) s a x p₂ a ⋯ = Pi.cons (δ := κ) s a y p₃ a ⋯
⊢ x = y

Tactic:
rw [Pi.cons_same, Pi.cons_same] at this

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 : ι) ⋯))
x : κ a
h_1 : x ∈ t a
y : κ a
h_2 : y ∈ t a
h : x ≠ y
a_1 : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left : p₂ ∈ s.pi (β := κ) t
eq₂ : Pi.cons (δ := κ) s a x p₂ = a_1
b : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left_1 : p₃ ∈ s.pi (β := κ) t
eq₃ : Pi.cons (δ := κ) s a y p₃ = b
eq : a_1 = b
this : x = y
⊢ False

Tactic:
h this
-- 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 : ι) ⋯))
x : κ a
h_1 : x ∈ t a
y : κ a
h_2 : y ∈ t a
h : x ≠ y
a_1 : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left : p₂ ∈ s.pi (β := κ) t
eq₂ : Pi.cons (δ := κ) s a x p₂ = a_1
b : (a' : ι) → (h : a' ∈ insert a s) → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left_1 : p₃ ∈ s.pi (β := κ) t
eq₃ : Pi.cons (δ := κ) s a y p₃ = b
eq : a_1 = b
this : x = y
⊢ False

Tactic:
exact h this
-- 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 : ι) ⋯))
⊢ ∀ 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))

Tactic:
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
-- 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))
insert :
  Eq.{u_4 + 1} (α := R) (∑ i ∈ t a, f a i * ∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
    (∑ x ∈ t a,
      ∑ i ∈ image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t),
        ∏ x ∈ (Insert.insert a s).attach, f (↑x : ι) (i (↑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 : ι) ⋯))

Tactic:
rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]

Premises used: Finset.prod_insert, Finset.sum_biUnion, Finset.pi_insert, Finset.sum_mul
-- 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))
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ t a, f a i * ∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
    (∑ x ∈ t a,
      ∑ i ∈ image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t), ∏ x ∈ (insert a s).attach, f (↑x : ι) (i (↑x : ι) ⋯))

Tactic:
sum_congr rfl fun b _ => ?_

Premises used: Finset.sum_congr, rfl
-- 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))
insert :
  ∀ b ∈ t a,
    f a b * ∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯) =
      ∑ i ∈ image (Pi.cons (δ := κ) s a b) (s.pi (β := κ) t),
        ∏ x ∈ (Insert.insert a s).attach, f (↑x : ι) (i (↑x : ι) ⋯)
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ t a, f a i * ∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯))
    (∑ x ∈ t a,
      ∑ i ∈ image (Pi.cons (δ := κ) s a x) (s.pi (β := κ) t),
        ∏ x ∈ (Insert.insert a s).attach, f (↑x : ι) (i (↑x : ι) ⋯))

Tactic:
refine sum_congr rfl fun b _ => ?_

Premises used: Finset.sum_congr, rfl
-- 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
⊢ ∀ 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₂

Tactic:
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
-- 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₂
insert :
  Eq.{u_4 + 1} (α := R) (∑ i ∈ s.pi (β := κ) t, f a b * ∏ x ∈ s.attach, f (↑x : ι) (i (↑x : ι) ⋯))
    (∑ x ∈ s.pi (β := κ) t, ∏ x_1 ∈ (Insert.insert a s).attach, f (↑x_1 : ι) (Pi.cons (δ := κ) s a b x (↑x_1 : ι) ⋯))
⊢ f a b * ∑ p ∈ s.pi (β := κ) t, ∏ x ∈ s.attach, f (↑x : ι) (p (↑x : ι) ⋯) =
    ∑ i ∈ image (Pi.cons (δ := κ) s a b) (s.pi (β := κ) t), ∏ x ∈ (Insert.insert a s).attach, f (↑x : ι) (i (↑x : ι) ⋯)

Tactic:
rw [sum_image h₂, mul_sum]

Premises used: Finset.mul_sum, Finset.sum_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 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₂
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ s.pi (β := κ) t, f a b * ∏ x ∈ s.attach, f (↑x : ι) (i (↑x : ι) ⋯))
    (∑ x ∈ s.pi (β := κ) t, ∏ x_1 ∈ (insert a s).attach, f (↑x_1 : ι) (Pi.cons (δ := κ) s a b x (↑x_1 : ι) ⋯))

Tactic:
sum_congr rfl fun g _ => ?_

Premises used: Finset.sum_congr, rfl
-- 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₂
insert :
  ∀ g ∈ s.pi (β := κ) t,
    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 : ι) ⋯)
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ s.pi (β := κ) t, f a b * ∏ x ∈ s.attach, f (↑x : ι) (i (↑x : ι) ⋯))
    (∑ x ∈ s.pi (β := κ) t, ∏ x_1 ∈ (Insert.insert a s).attach, f (↑x_1 : ι) (Pi.cons (δ := κ) s a b x (↑x_1 : ι) ⋯))

Tactic:
refine sum_congr rfl fun g _ => ?_

Premises used: Finset.sum_congr, rfl