ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
⊢ ∏ i' in s', f i' = ∏ i in image (↑e.symm) s', f (↑e i)
ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
⊢ ∏ i' in s', f i' = ∏ i in s, f (↑e i)
rw [h]
ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
a : ι
ha : a ∈ image (↑e.symm) s'
⊢ (fun i _hi => ↑e i) a ha ∈ s'
ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
⊢ ∏ i' in s', f i' = ∏ i in image (↑e.symm) s', f (↑e i)
refine'
  Finset.prod_bij' (fun i' _hi' => e.symm i') (fun a ha => Finset.mem_image_of_mem _ ha)
    (fun a _ha => by simp_rw [e.apply_symm_apply]) (fun i _hi => e i) (fun a ha => _)
    (fun a _ha => e.apply_symm_apply a) fun a _ha => e.symm_apply_apply a
case intro.intro
ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
i' : ι'
hi' : i' ∈ s'
ha : ↑e.symm i' ∈ image (↑e.symm) s'
⊢ (fun i _hi => ↑e i) (↑e.symm i') ha ∈ s'
ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
a : ι
ha : a ∈ image (↑e.symm) s'
⊢ (fun i _hi => ↑e i) a ha ∈ s'
rcases Finset.mem_image.mp ha with ⟨i', hi', rfl⟩
case intro.intro
ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
i' : ι'
hi' : i' ∈ s'
ha : ↑e.symm i' ∈ image (↑e.symm) s'
⊢ ↑e (↑e.symm i') ∈ s'
case intro.intro
ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
i' : ι'
hi' : i' ∈ s'
ha : ↑e.symm i' ∈ image (↑e.symm) s'
⊢ (fun i _hi => ↑e i) (↑e.symm i') ha ∈ s'
dsimp only
no goals
case intro.intro
ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
i' : ι'
hi' : i' ∈ s'
ha : ↑e.symm i' ∈ image (↑e.symm) s'
⊢ ↑e (↑e.symm i') ∈ s'
rwa [e.apply_symm_apply]
no goals
ι : Type u_2
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι' : Type u_1
inst✝ : DecidableEq ι
e : ι ≃ ι'
f : ι' → β
s' : Finset ι'
s : Finset ι
h : s = image (↑e.symm) s'
a : ι'
_ha : a ∈ s'
⊢ f a = f (↑e ((fun i' _hi' => ↑e.symm i') a _ha))
simp_rw [e.apply_symm_apply]