Theorem: Finset.equiv_univ (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
α' : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype α'
inst✝ : DecidableEq α'
e : α ≃ α'
⊢ image (⇑e) univ = univ
Tactic:
ext x
State after:
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
α' : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype α'
inst✝ : DecidableEq α'
e : α ≃ α'
x : α'
⊢ x ∈ image (⇑e) univ ↔ x ∈ univ

State before:
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
α' : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype α'
inst✝ : DecidableEq α'
e : α ≃ α'
x : α'
⊢ x ∈ image (⇑e) univ ↔ x ∈ univ
Tactic:
simp
State after:
no goals