α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)
⊢ support (swap x y * swap y z) = {x, y, z}
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : List.Nodup [x, y, z]
⊢ support (swap x y * swap y z) = {x, y, z}
simp only [List.not_mem_nil, and_true_iff, List.mem_cons, not_false_iff, List.nodup_cons,
  List.mem_singleton, and_self_iff, List.nodup_nil] at h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ support (swap x y * swap y z) = {x, y, z}
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)
⊢ support (swap x y * swap y z) = {x, y, z}
push_neg  at h
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ support (swap x y * swap y z) ≤ {x, y, z}

case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} ≤ support (swap x y * swap y z)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ support (swap x y * swap y z) = {x, y, z}
apply le_antisymm
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = support (swap x y) ⊔ support (swap y z)
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ support (swap x y * swap y z) ≤ {x, y, z}
convert support_mul_le (swap x y) (swap y z) using 1
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ⊔ {y, z}
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = support (swap x y) ⊔ support (swap y z)
rw [support_swap h.left.left, support_swap h.right.left]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ∪ {y, z}
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ⊔ {y, z}
simp only [sup_eq_union]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = insert x ({y} ∪ {z})
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ∪ {y, z}
simp only [mem_singleton, mem_insert, union_insert, insert_union, mem_union, true_or, or_true,
  insert_eq_of_mem]
no goals
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = insert x ({y} ∪ {z})
rfl
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ ∈ {x, y, z} → a✝ ∈ support (swap x y * swap y z)
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} ≤ support (swap x y * swap y z)
intro
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ = x ∨ a✝ = y ∨ a✝ = z → a✝ ∈ support (swap x y * swap y z)
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ ∈ {x, y, z} → a✝ ∈ support (swap x y * swap y z)
simp only [mem_insert, mem_singleton]
no goals
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ = x ∨ a✝ = y ∨ a✝ = z → a✝ ∈ support (swap x y * swap y z)
rintro (rfl | rfl | rfl | _) <;>
  simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm,
    h.left.right.left.symm, h.right.left.symm]