-- Mathlib/Data/Fintype/Pi.lean
theorem mem_piFinset {t : ∀ a, Finset (δ a)} {f : ∀ a, δ a} : f ∈ piFinset t ↔ ∀ a, f a ∈ t a

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t ↔ ∀ (a : α), f a ∈ t a

Tactic:
constructor

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

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

Proof state:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t

Tactic:
simp only [piFinset, mem_map, forall_prop_of_true, exists_prop, mem_univ, mem_pi]

Result:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → ∃ a, (∀ (a_1 : α), a a_1 ⋯ ∈ t a_1) ∧ { toFun := fun f a => f a ⋯, inj' := ⋯ } a = f

Proof state:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ ∀ (x : (a : α) → a ∈ univ → δ a),
    (∀ (a : α), x a ⋯ ∈ t a) → { toFun := fun f a => f a ⋯, inj' := ⋯ } x = f → ∀ (a : α), f a ∈ t a

Tactic:
rintro g hg hgf a

Result:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a => f a ⋯, inj' := ⋯ } g = f
a : α
⊢ f a ∈ t a

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

Tactic:
simp only [piFinset, mem_map, and_imp, forall_prop_of_true, exists_prop, mem_univ, exists_imp,
  mem_pi]

Result:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ ∀ (x : (a : α) → a ∈ univ → δ a),
    (∀ (a : α), x a ⋯ ∈ t a) → { toFun := fun f a => f a ⋯, inj' := ⋯ } x = f → ∀ (a : α), f a ∈ t a

Proof state:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a => f a ⋯, inj' := ⋯ } g = f
a : α
⊢ { toFun := fun f a => f a ⋯, inj' := ⋯ } g a ∈ t a

Tactic:
exact hg a

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → ∃ a, (∀ (a_1 : α), a a_1 ⋯ ∈ t a_1) ∧ { toFun := fun f a => f a ⋯, inj' := ⋯ } a = f

Tactic:
exact fun hf => ⟨fun a _ => f a, hf, rfl⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a => f a ⋯, inj' := ⋯ } g = f
a : α
⊢ f a ∈ t a

Tactic:
rw [← hgf]

Result:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a => f a ⋯, inj' := ⋯ } g = f
a : α
⊢ { toFun := fun f a => f a ⋯, inj' := ⋯ } g a ∈ t a