Theorem: Finperm.restrict_univ (Bruhat/Finperm.lean)

State before:
α✝¹ : Type u_1
x y : α✝¹
f✝ g : Finperm α✝¹
α✝ : Type u_2
β : Type u_3
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq β
f : Finperm α✝
α : Type u_4
inst✝ : DecidableEq α
⊢ restrict Set.univ = ⊤
Tactic:
ext
State after:
case h
α✝¹ : Type u_1
x y : α✝¹
f✝ g : Finperm α✝¹
α✝ : Type u_2
β : Type u_3
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq β
f : Finperm α✝
α : Type u_4
inst✝ : DecidableEq α
x✝ : Finperm α
⊢ x✝ ∈ restrict Set.univ ↔ x✝ ∈ ⊤

State before:
case h
α✝¹ : Type u_1
x y : α✝¹
f✝ g : Finperm α✝¹
α✝ : Type u_2
β : Type u_3
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq β
f : Finperm α✝
α : Type u_4
inst✝ : DecidableEq α
x✝ : Finperm α
⊢ x✝ ∈ restrict Set.univ ↔ x✝ ∈ ⊤
Tactic:
simp
State after:
no goals