-- 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 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:
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

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

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

Result:
case insert.e_a.e_f.h.mk
ι : 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
⊢ f (↑⟨v, hv⟩) (g ↑⟨v, hv⟩ ⋯) = f (↑⟨v, hv⟩) (Pi.cons s a b g ↑⟨v, hv⟩ ⋯)

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

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

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₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ ⟨a, ⋯⟩ ∉ image (fun x => ⟨↑x, ⋯⟩) s.attach

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

Result:
no goals

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

Tactic:
congr

Result:
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⟩ ⋯

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))
⊢ ∑ 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:
refine sum_congr rfl fun b _ => ?_

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
⊢ 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:
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))
⊢ ∏ 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:
rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]

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