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

State before:
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : f = g
⊢ f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
Tactic:
simp [h]
State after:
no goals