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

State before:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ (fintype fun x => x = i) = 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 => x = i) Finset.univ)
      (_ : ∀ (a : ι), a ∈ Finset.filter (fun x => x = i) Finset.univ ↔ a = i) =
    Fintype.subtype {i} (_ : ∀ (a : ι), a ∈ {i} ↔ a = i)

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