Theorem: Finset.map_id (Hfzfa.lean)

State before:
atoms : Type ?u.52518
α : Type u_1
x : Finset α
⊢ Finset.map
      { toFun := fun z => z,
        inj' := (_ : ∀ (a b : α), (fun z => z) a = (fun z => z) b → (fun z => z) a = (fun z => z) b) }
      x =
    x
Tactic:
ext y
State after:
case a
atoms : Type ?u.52518
α : Type u_1
x : Finset α
y : α
⊢ y ∈
      Finset.map
        { toFun := fun z => z,
          inj' := (_ : ∀ (a b : α), (fun z => z) a = (fun z => z) b → (fun z => z) a = (fun z => z) b) }
        x ↔
    y ∈ x

State before:
case a
atoms : Type ?u.52518
α : Type u_1
x : Finset α
y : α
⊢ y ∈
      Finset.map
        { toFun := fun z => z,
          inj' := (_ : ∀ (a b : α), (fun z => z) a = (fun z => z) b → (fun z => z) a = (fun z => z) b) }
        x ↔
    y ∈ x
Tactic:
simp
State after:
no goals