case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
⊢ ↑f x = ↑g x
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
⊢ f = g
ext x
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : x ∈ support g
⊢ ↑f x = ↑g x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : ¬x ∈ support g
⊢ ↑f x = ↑g x
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
⊢ ↑f x = ↑g x
by_cases hx : x ∈ g.support
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : x ∈ support g
⊢ ↑f x = ↑g x
exact h' x hx
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : ¬x ∈ support g
⊢ ¬x ∈ support f
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : ¬x ∈ support g
⊢ ↑f x = ↑g x
rw [not_mem_support.mp hx, ← not_mem_support]
no goals
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : ¬x ∈ support g
⊢ ¬x ∈ support f
exact fun H => hx (h H)