Theorem: Subtype.fintype_subtypeEq' (ForML/PiEquiv.lean)

State before:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ (fintype fun x => i = x) = Fintype.subtypeEq' i
Tactic:
rw [fintype, Fintype.subtypeEq']
State after:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ Fintype.subtype (Finset.filter (fun x => i = x) Finset.univ)
      (_ : ∀ (a : ι), a ∈ Finset.filter (fun x => i = x) Finset.univ ↔ i = a) =
    Fintype.subtype {i} (_ : ∀ (a : ι), a ∈ {i} ↔ i = a)

State before:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ Fintype.subtype (Finset.filter (fun x => i = x) Finset.univ)
      (_ : ∀ (a : ι), a ∈ Finset.filter (fun x => i = x) Finset.univ ↔ i = a) =
    Fintype.subtype {i} (_ : ∀ (a : ι), a ∈ {i} ↔ i = a)
Tactic:
simp [Finset.filter_eq]
State after:
no goals