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

Tactic:
simp only [disjoint_iff_ne, mem_image]

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
⊢ ∀ (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

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, ⋯⟩) (Pi.cons s a b g ↑⟨a, ⋯⟩ ⋯) * ∏ x ∈ s.attach, f (↑⟨↑x, ⋯⟩) (Pi.cons s a b g ↑⟨↑x, ⋯⟩ ⋯)

Tactic:
simp only [Pi.cons_same]

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 ⋯) = f a b * ∏ x ∈ 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₂
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 ⋯)

Tactic:
rw [attach_insert, prod_insert, prod_image]

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 ⋯) =
    f (↑⟨a, ⋯⟩) (Pi.cons s a b g ↑⟨a, ⋯⟩ ⋯) * ∏ x ∈ s.attach, f (↑⟨↑x, ⋯⟩) (Pi.cons s a b g ↑⟨↑x, ⋯⟩ ⋯)

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

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

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✝
⊢ False

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]

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

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
hv : a ∈ s
⊢ False

Tactic:
exact ha hv

Result:
no goals