α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ (∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x) ↔ ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ Perm.Disjoint (formPerm l) (formPerm l') ↔ Disjoint l l'
rw [disjoint_iff_eq_or_eq, List.Disjoint]
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ (∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x) → ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False

case mpr
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ (∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False) → ∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ (∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x) ↔ ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
constructor
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ False
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ (∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x) → ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
rintro h x hx hx'
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
x : α
hx : x ∈ l
hx' : x ∈ l'
h : ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
⊢ False
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ False
specialize h x
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
x : α
hx : x ∈ l
hx' : x ∈ l'
h : length l ≤ 1 ∨ length l' ≤ 1
⊢ False
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
x : α
hx : x ∈ l
hx' : x ∈ l'
h : ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
⊢ False
rw [formPerm_apply_mem_eq_self_iff _ hl _ hx, formPerm_apply_mem_eq_self_iff _ hl' _ hx'] at h
no goals
case mp
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
x : α
hx : x ∈ l
hx' : x ∈ l'
h : length l ≤ 1 ∨ length l' ≤ 1
⊢ False
rcases h with (hl | hl') <;> linarith
case mpr
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
case mpr
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
⊢ (∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False) → ∀ (x : α), ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
intro h x
case pos
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x

case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
case mpr
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
by_cases hx : x ∈ l
case pos
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x

case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : ¬x ∈ l'
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x

case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
case pos
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x

case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
by_cases hx' : x ∈ l'
no goals
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : ¬x ∈ l'
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x

case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
all_goals have := formPerm_eq_self_of_not_mem _ _ ‹_›; tauto
no goals
case pos
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
exact (h hx hx').elim
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
this : ↑(formPerm l) x = x
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
have := formPerm_eq_self_of_not_mem _ _ ‹_›
no goals
case neg
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
hl' : Nodup l'
hn : 2 ≤ length l
hn' : 2 ≤ length l'
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : ¬x ∈ l
this : ↑(formPerm l) x = x
⊢ ↑(formPerm l) x = x ∨ ↑(formPerm l') x = x
tauto