[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
x✝¹ x✝ : (a : α) → a ∈ univ → δ a
⊢ (fun f a => f a (_ : a ∈ univ)) x✝¹ = (fun f a => f a (_ : a ∈ univ)) x✝ → x✝¹ = x✝
[PROOFSTEP]
simp (config := { contextual := true }) [Function.funext_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t ↔ ∀ (a : α), f a ∈ t a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t → ∀ (a : α), f a ∈ t a
[PROOFSTEP]
simp only [piFinset, mem_map, and_imp, forall_prop_of_true, exists_prop, mem_univ, exists_imp, mem_pi]
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ ∀ (x : (a : α) → a ∈ univ → δ a),
    (∀ (a : α), x a (_ : a ∈ univ) ∈ t a) →
      ↑{ toFun := fun f a => f a (_ : a ∈ univ),
                inj' :=
                  (_ :
                    ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                      ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
            x =
          f →
        ∀ (a : α), f a ∈ t a
[PROOFSTEP]
rintro g hg hgf a
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a (_ : a ∈ univ) ∈ t a
hgf :
  ↑{ toFun := fun f a => f a (_ : a ∈ univ),
          inj' :=
            (_ :
              ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
      g =
    f
a : α
⊢ f a ∈ t a
[PROOFSTEP]
rw [← hgf]
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a (_ : a ∈ univ) ∈ t a
hgf :
  ↑{ toFun := fun f a => f a (_ : a ∈ univ),
          inj' :=
            (_ :
              ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
      g =
    f
a : α
⊢ ↑{ toFun := fun f a => f a (_ : a ∈ univ),
          inj' :=
            (_ :
              ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
      g a ∈
    t a
[PROOFSTEP]
exact hg a
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t
[PROOFSTEP]
simp only [piFinset, mem_map, forall_prop_of_true, exists_prop, mem_univ, mem_pi]
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) →
    ∃ a,
      (∀ (a_1 : α), a a_1 (_ : a_1 ∈ univ) ∈ t a_1) ∧
        ↑{ toFun := fun f a => f a (_ : a ∈ univ),
                inj' :=
                  (_ :
                    ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                      ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
            a =
          f
[PROOFSTEP]
exact fun hf => ⟨fun a _ => f a, hf, rfl⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ x ∈ Set.pi Set.univ fun a => ↑(t a)
[PROOFSTEP]
rw [Set.mem_univ_pi]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)
[PROOFSTEP]
exact Fintype.mem_piFinset
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_2
inst✝ : Nonempty α
x✝ : (a : α) → δ a
⊢ ¬x✝ ∈ piFinset fun x => ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
f x✝ : (a : α) → δ a
⊢ (x✝ ∈ piFinset fun i => {f i}) ↔ x✝ ∈ {f}
[PROOFSTEP]
simp only [Function.funext_iff, Fintype.mem_piFinset, mem_singleton]
[GOAL]
α✝ : Type u_1
α : Type u_2
β : α → Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ ∀ (x : (a : α) → β a), x ∈ Fintype.piFinset fun x => univ
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
α : Type ?u.21193
β : Type ?u.21196
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Fintype (α ↪ β)
[PROOFSTEP]
classical. exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
[GOAL]
α✝ : Type u_1
α : Type ?u.21193
β : Type ?u.21196
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Fintype (α ↪ β)
[PROOFSTEP]
exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
[GOAL]
α✝ : Type u_1
α : Type u_2
β : α → Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ (pi univ fun a => univ) = univ
[PROOFSTEP]
ext
[GOAL]
case a
α✝ : Type u_1
α : Type u_2
β : α → Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
a✝ : (a : α) → a ∈ univ → β a
⊢ (a✝ ∈ pi univ fun a => univ) ↔ a✝ ∈ univ
[PROOFSTEP]
simp
