α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a : (a : α) → a ∈ univ → δ a) (ha : a ∈ pi univ t), (fun x x_1 a => x a (_ : a ∈ univ)) a ha ∈ Fintype.piFinset t
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∏ x in pi univ t, f x = ∏ x in Fintype.piFinset t, f fun a x_1 => x a
refine prod_bij (fun x _ a => x a (mem_univ _)) ?_ (by simp)
  (by simp (config := { contextual := true }) [Function.funext_iff]) fun x hx =>
  ⟨fun a _ => x a, by simp_all⟩
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ (fun x x_1 a => x a (_ : a ∈ univ)) a ha ∈ Fintype.piFinset t
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a : (a : α) → a ∈ univ → δ a) (ha : a ∈ pi univ t), (fun x x_1 a => x a (_ : a ∈ univ)) a ha ∈ Fintype.piFinset t
intro a ha
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ ∃ a_1, (∀ (a : α) (h : a ∈ univ), a_1 a h ∈ t a) ∧ (fun a => a_1 a (_ : a ∈ univ)) = fun a_2 => a a_2 (_ : a_2 ∈ univ)
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ (fun x x_1 a => x a (_ : a ∈ univ)) a ha ∈ Fintype.piFinset t
simp only [Fintype.piFinset, mem_map, mem_pi, Function.Embedding.coeFn_mk]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ ∃ a_1, (∀ (a : α) (h : a ∈ univ), a_1 a h ∈ t a) ∧ (fun a => a_1 a (_ : a ∈ univ)) = fun a_2 => a a_2 (_ : a_2 ∈ univ)
exact ⟨a, by simpa using ha, by simp⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a : (a : α) → a ∈ univ → δ a) (ha : a ∈ pi univ t),
    f a = f fun a_1 x => (fun x x_1 a => x a (_ : a ∈ univ)) a ha a_1
simp
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a₁ a₂ : (a : α) → a ∈ univ → δ a) (ha₁ : a₁ ∈ pi univ t) (ha₂ : a₂ ∈ pi univ t),
    (fun x x_1 a => x a (_ : a ∈ univ)) a₁ ha₁ = (fun x x_1 a => x a (_ : a ∈ univ)) a₂ ha₂ → a₁ = a₂
simp (config := { contextual := true }) [Function.funext_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
x : (a : α) → δ a
hx : x ∈ Fintype.piFinset t
⊢ ∃ ha, x = (fun x x_1 a => x a (_ : a ∈ univ)) (fun a x_1 => x a) ha
simp_all
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ ∀ (a_1 : α) (h : a_1 ∈ univ), a a_1 h ∈ t a_1
simpa using ha
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.15155
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_3
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ (fun a_1 => a a_1 (_ : a_1 ∈ univ)) = fun a_1 => a a_1 (_ : a_1 ∈ univ)
simp