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

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

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

case inr
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∉ s
⊢ f x = g x

State before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∉ s
⊢ f x = g x
Tactic:
rw [(show f x = x by simpa using not_mem_mono hf hx),
  (show g x = x by simpa using not_mem_mono hg hx)]
State after:
no goals

State before:
case inl
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∈ s
⊢ f x = g x
Tactic:
exact h _ hx
State after:
no goals

State before:
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∉ s
⊢ f x = x
Tactic:
simpa using not_mem_mono hf hx
State after:
no goals

State before:
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∉ s
⊢ g x = x
Tactic:
simpa using not_mem_mono hg hx
State after:
no goals