no goals
ι : Type ?u.324815
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
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 in s, ∏ y in t x, f x y = ∏ y in t', ∏ x in s' y, f x y
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))
ι : Type ?u.324815
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
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 ∈ Finset.biUnion s fun x => map (Function.Embedding.sectr x α) (t x)) ↔ z.fst ∈ s ∧ z.snd ∈ t z.fst
⊢ ∏ x in s, ∏ y in t x, f x y = ∏ y in t', ∏ x in s' y, f x y
ι : Type ?u.324815
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
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 in s, ∏ y in t x, f x y = ∏ y in t', ∏ x in s' y, f x y
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]
no goals
ι : Type ?u.324815
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
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 ∈ Finset.biUnion s fun x => map (Function.Embedding.sectr x α) (t x)) ↔ z.fst ∈ s ∧ z.snd ∈ t z.fst
⊢ ∏ x in s, ∏ y in t x, f x y = ∏ y in t', ∏ x in s' y, f x y
exact
  (prod_finset_product' _ _ _ this).symm.trans
    ((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))
case mk
ι : Type ?u.324815
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
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) ∈ Finset.biUnion s fun x => map (Function.Embedding.sectr x α) (t x)) ↔
    (x, y).fst ∈ s ∧ (x, y).snd ∈ t (x, y).fst
ι : Type ?u.324815
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
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 ∈ Finset.biUnion s fun x => map (Function.Embedding.sectr x α) (t x)) ↔ z.fst ∈ s ∧ z.snd ∈ t z.fst
rintro ⟨x, y⟩
no goals
case mk
ι : Type ?u.324815
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
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) ∈ Finset.biUnion s fun x => map (Function.Embedding.sectr x α) (t x)) ↔
    (x, y).fst ∈ s ∧ (x, y).snd ∈ t (x, y).fst
simp only [mem_biUnion, mem_map, Function.Embedding.sectr_apply, Prod.mk.injEq,
  exists_eq_right, ← and_assoc]