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

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

case support.a
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.toPerm = g.toPerm
x : α
⊢ x ∈ f.support ↔ x ∈ g.support

State before:
case support.a
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.toPerm = g.toPerm
x : α
⊢ x ∈ f.support ↔ x ∈ g.support
Tactic:
rw [mem_support_iff, mem_support_iff, ← toPerm_eq_coe, h, toPerm_eq_coe]
State after:
no goals

State before:
case toPerm.H
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.toPerm = g.toPerm
x : α
⊢ f.toPerm x = g.toPerm x
Tactic:
rw [h]
State after:
no goals