case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t → ∀ (a : α), f a ∈ t a

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t ↔ ∀ (a : α), f a ∈ t a
constructor
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
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
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t → ∀ (a : α), f a ∈ t a
simp only [piFinset, mem_map, and_imp, forall_prop_of_true, exists_prop, mem_univ, exists_imp,
  mem_pi]
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
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
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
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
rintro g hg hgf a
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
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
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
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
rw [← hgf]
no goals
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
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
exact hg a
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
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
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t
simp only [piFinset, mem_map, forall_prop_of_true, exists_prop, mem_univ, mem_pi]
no goals
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
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
exact fun hf => ⟨fun a _ => f a, hf, rfl⟩