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

State before:
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
⊢ f = g
Tactic:
apply coe_inj
State after:
case h
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
⊢ f.toPerm = g.toPerm

State before:
case h
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
⊢ f.toPerm = g.toPerm
Tactic:
ext x
State after:
case h.H
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
x : α
⊢ f.toPerm x = g.toPerm x

State before:
case h.H
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
x : α
⊢ f.toPerm x = g.toPerm x
Tactic:
exact h x
State after:
no goals