-- 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:
ι : 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 ∈ 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))

Tactic:
intro x _ y _ h

Result:
ι : 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
⊢ Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))

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 ⋯)
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₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
v : ι
hv : v ∈ s
⊢ a ≠ ↑⟨v, hv⟩

Tactic:
rintro rfl

Result:
ι : 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₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
hv : a ∈ s
⊢ False

Proof state:
case insert.e_a.e_f.h.mk.e_a
ι : 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₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
v : ι
hv : v ∈ s
⊢ g ↑⟨v, hv⟩ ⋯ = Pi.cons s a b g ↑⟨v, hv⟩ ⋯

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

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
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
⊢ ∑ 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:
refine sum_congr rfl fun g _ => ?_

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₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ f a b * ∏ x ∈ s.attach, f (↑x) (g ↑x ⋯) = ∏ x ∈ (insert a s).attach, f (↑x) (Pi.cons s a b g ↑x ⋯)

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
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 ⋯)

Tactic:
rw [sum_image h₂, mul_sum]

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₂
⊢ ∑ 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 ⋯)

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 : Pi.cons s a x p₂ a ⋯ = Pi.cons s a y p₃ a ⋯
⊢ False

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

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✝
this : x = y
⊢ False

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 ⋯)
⊢ ∏ a ∈ insert a✝ s✝, ∑ b ∈ t a, f a b = ∑ p ∈ (insert a✝ s✝).pi t, ∏ x ∈ (insert a✝ s✝).attach, f (↑x) (p ↑x ⋯)

Tactic:
rename_i a s

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 ⋯)
⊢ ∏ a ∈ insert a s, ∑ b ∈ t a, f a b = ∑ p ∈ (insert a s).pi t, ∏ x ∈ (insert a s).attach, f (↑x) (p ↑x ⋯)