-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
/-- The product over a sum can be written as a sum over the product of sets, `Finset.Pi`.
  `Finset.prod_univ_sum` is an alternative statement when the product is over `univ`. -/
lemma prod_sum (s : Finset ι) (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) :
    ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f x.1 (p x.1 x.2)

Proof state:
case empty
ι : Type u_1
α : Type u_3
κ : ι → Type u_6
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
⊢ ∏ a ∈ ∅, ∑ b ∈ t a, f a b = ∑ p ∈ ∅.pi t, ∏ x ∈ ∅.attach, f (↑x) (p ↑x ⋯)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
κ : ι → Type u_6
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝² : x ∈ t a
y : κ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left✝¹ : p₂ ∈ s.pi t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left✝ : p₃ ∈ s.pi t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
⊢ Pi.cons s a x p₂ a ⋯ = Pi.cons s a y p₃ a ⋯

Tactic:
rw [eq₂, eq₃, eq]

Result:
no goals

Proof state:
case insert
ι : Type u_1
α : Type u_3
κ : ι → Type u_6
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ 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 (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝ : 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 a s).attach, f (↑x) (i ↑x ⋯)

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

Result:
case insert
ι : Type u_1
α : Type u_3
κ : ι → Type u_6
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ 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 (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
⊢ 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 a s).attach, f (↑x) (i ↑x ⋯)

Proof state:
ι : Type u_1
α : Type u_3
κ : ι → Type u_6
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝¹ : x ∈ t a
y : κ a
a✝ : y ∈ t a
h : x ≠ y
⊢ ∀ (a_1 : (a' : ι) → a' ∈ insert a s → κ a'),
    (∃ a_2 ∈ s.pi t, Pi.cons s a x a_2 = a_1) →
      ∀ (b : (a' : ι) → a' ∈ insert a s → κ a'), (∃ a_3 ∈ s.pi t, Pi.cons s a y a_3 = b) → a_1 ≠ b

Tactic:
rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq

Result:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_3
κ : ι → Type u_6
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝² : x ∈ t a
y : κ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left✝¹ : p₂ ∈ s.pi t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left✝ : p₃ ∈ s.pi t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
⊢ False

Proof state:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_3
κ : ι → Type u_6
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝² : x ∈ t a
y : κ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left✝¹ : p₂ ∈ s.pi t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left✝ : p₃ ∈ s.pi t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
this : x = y
⊢ False

Tactic:
exact h this

Result:
no goals