-- Mathlib/Algebra/BigOperators/Group/Finset/Sigma.lean
theorem prod_comm' {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ}
    (h : ∀ x y, x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} :
    (∏ x ∈ s, ∏ y ∈ t x, f x y) = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
⊢ ∀ (z : γ × α), (z ∈ s.biUnion fun x => map (Embedding.sectR x α) (t x)) ↔ z.1 ∈ s ∧ z.2 ∈ t z.1

Tactic:
rintro ⟨x, y⟩

Result:
case mk
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
x : γ
y : α
⊢ ((x, y) ∈ s.biUnion fun x => map (Embedding.sectR x α) (t x)) ↔ (x, y).1 ∈ s ∧ (x, y).2 ∈ t (x, y).1

Proof state:
case mk
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
x : γ
y : α
⊢ ((x, y) ∈ s.biUnion fun x => map (Embedding.sectR x α) (t x)) ↔ (x, y).1 ∈ s ∧ (x, y).2 ∈ t (x, y).1

Tactic:
simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
  exists_eq_right, ← and_assoc]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
⊢ ∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Tactic:
classical
  have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔
    z.1 ∈ s ∧ z.2 ∈ t z.1 := by
    rintro ⟨x, y⟩
    simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
      exists_eq_right, ← and_assoc]
  exact
    (prod_finset_product' _ _ _ this).symm.trans
      ((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
⊢ ∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Tactic:
have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔
  z.1 ∈ s ∧ z.2 ∈ t z.1 := by
  rintro ⟨x, y⟩
  simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
    exists_eq_right, ← and_assoc]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
this : ∀ (z : γ × α), (z ∈ s.biUnion fun x => map (Embedding.sectR x α) (t x)) ↔ z.1 ∈ s ∧ z.2 ∈ t z.1
⊢ ∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
this : ∀ (z : γ × α), (z ∈ s.biUnion fun x => map (Embedding.sectR x α) (t x)) ↔ z.1 ∈ s ∧ z.2 ∈ t z.1
⊢ ∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Tactic:
exact
  (prod_finset_product' _ _ _ this).symm.trans
    ((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))

Result:
no goals