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

State before:
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
⊢ f = g
Tactic:
refine funext <| fun x ↦ ?_
State after:
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
⊢ f x = g x

State before:
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
⊢ f x = g x
Tactic:
obtain (hx | hx) := em (x ∈ f.support)
State after:
case inl
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∈ f.support
⊢ f x = g x

case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∉ f.support
⊢ f x = g x

State before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∉ f.support
⊢ f x = g x
Tactic:
have hx' := hx
State after:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx hx' : x ∉ f.support
⊢ f x = g x

State before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx hx' : x ∉ f.support
⊢ f x = g x
Tactic:
rw [h] at hx'
State after:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∉ f.support
hx' : x ∉ g.support
⊢ f x = g x

State before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∉ f.support
hx' : x ∉ g.support
⊢ f x = g x
Tactic:
rw [mem_support_iff, not_not] at hx hx'
State after:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : f x = x
hx' : g x = x
⊢ f x = g x

State before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : f x = x
hx' : g x = x
⊢ f x = g x
Tactic:
rw [hx, hx']
State after:
no goals

State before:
case inl
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∈ f.support
⊢ f x = g x
Tactic:
rw [h' x hx]
State after:
no goals