-- Mathlib/Data/Fintype/Pi.lean
lemma piFinset_update_eq_filter_piFinset_mem (s : ∀ i, Finset (δ i)) (i : α) {t : Finset (δ i)}
    (hts : t ⊆ s i) : piFinset (Function.update s i t) = {f ∈ piFinset s | f i ∈ t}

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
⊢ piFinset (update s i t) = filter (fun f => f i ∈ t) (piFinset s)

Tactic:
ext f

Result:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
⊢ f ∈ piFinset (update s i t) ↔ f ∈ filter (fun f => f i ∈ t) (piFinset s)

Proof state:
case h.refine_2.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
f : (a : α) → δ a
j : α
t : Finset (δ j)
hts : t ⊆ s j
h : (∀ (a : α), f a ∈ s a) ∧ f j ∈ t
⊢ f j ∈ update s j t j

Tactic:
simpa using h.2

Result:
no goals

Proof state:
case h.refine_1.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : ∀ (a : α), f a ∈ update s i t a
this : f i ∈ t
j : α
hji : j ≠ i
⊢ f j ∈ s j

Tactic:
simpa [hji] using h j

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : ∀ (a : α), f a ∈ update s i t a
⊢ ?m.20508

Tactic:
simpa using h i

Result:
no goals

Proof state:
case h.refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : ∀ (a : α), f a ∈ update s i t a
⊢ (∀ (a : α), f a ∈ s a) ∧ f i ∈ t

Tactic:
have := by simpa using h i

Result:
case h.refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : ∀ (a : α), f a ∈ update s i t a
this : f i ∈ t
⊢ (∀ (a : α), f a ∈ s a) ∧ f i ∈ t

Proof state:
case h.refine_2.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : (∀ (a : α), f a ∈ s a) ∧ f i ∈ t
j : α
hji : j ≠ i
⊢ f j ∈ update s i t j

Tactic:
simpa [hji] using h.1 j

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ update s i t a) ↔ (∀ (a : α), f a ∈ s a) ∧ f i ∈ t

Tactic:
refine ⟨fun h ↦ ?_, fun h j ↦ ?_⟩

Result:
case h.refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : ∀ (a : α), f a ∈ update s i t a
⊢ (∀ (a : α), f a ∈ s a) ∧ f i ∈ t

case h.refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : (∀ (a : α), f a ∈ s a) ∧ f i ∈ t
j : α
⊢ f j ∈ update s i t j

Proof state:
case h.refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : (∀ (a : α), f a ∈ s a) ∧ f i ∈ t
j : α
⊢ f j ∈ update s i t j

Tactic:
obtain rfl | hji := eq_or_ne j i

Result:
case h.refine_2.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
f : (a : α) → δ a
j : α
t : Finset (δ j)
hts : t ⊆ s j
h : (∀ (a : α), f a ∈ s a) ∧ f j ∈ t
⊢ f j ∈ update s j t j

case h.refine_2.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : (∀ (a : α), f a ∈ s a) ∧ f i ∈ t
j : α
hji : j ≠ i
⊢ f j ∈ update s i t j

Proof state:
case h.refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : ∀ (a : α), f a ∈ update s i t a
this : f i ∈ t
j : α
⊢ f j ∈ s j

Tactic:
obtain rfl | hji := eq_or_ne j i

Result:
case h.refine_1.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
f : (a : α) → δ a
j : α
t : Finset (δ j)
hts : t ⊆ s j
h : ∀ (a : α), f a ∈ update s j t a
this : f j ∈ t
⊢ f j ∈ s j

case h.refine_1.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : ∀ (a : α), f a ∈ update s i t a
this : f i ∈ t
j : α
hji : j ≠ i
⊢ f j ∈ s j

Proof state:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
⊢ f ∈ piFinset (update s i t) ↔ f ∈ filter (fun f => f i ∈ t) (piFinset s)

Tactic:
simp only [mem_piFinset, mem_filter]

Result:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ update s i t a) ↔ (∀ (a : α), f a ∈ s a) ∧ f i ∈ t

Proof state:
case h.refine_1.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
f : (a : α) → δ a
j : α
t : Finset (δ j)
hts : t ⊆ s j
h : ∀ (a : α), f a ∈ update s j t a
this : f j ∈ t
⊢ f j ∈ s j

Tactic:
exact hts this

Result:
no goals

Proof state:
case h.refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : ∀ (a : α), f a ∈ update s i t a
this : f i ∈ t
⊢ (∀ (a : α), f a ∈ s a) ∧ f i ∈ t

Tactic:
refine ⟨fun j ↦ ?_, this⟩

Result:
case h.refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
f : (a : α) → δ a
h : ∀ (a : α), f a ∈ update s i t a
this : f i ∈ t
j : α
⊢ f j ∈ s j