-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_swap_mul_swap {x y z : α} (h : List.Nodup [x, y, z]) :
    support (swap x y * swap y z) = {x, y, z}

Proof state:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} ≤ (swap x y * swap y z).support

Tactic:
intro

Result:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ ∈ {x, y, z} → a✝ ∈ (swap x y * swap y z).support

Proof state:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ ∈ {x, y, z} → a✝ ∈ (swap x y * swap y z).support

Tactic:
simp only [mem_insert, mem_singleton]

Result:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ = x ∨ a✝ = y ∨ a✝ = z → a✝ ∈ (swap x y * swap y z).support

Proof state:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ (swap x y * swap y z).support ≤ {x, y, z}

Tactic:
convert support_mul_le (swap x y) (swap y z) using 1

Result:
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = (swap x y).support ⊔ (swap y z).support

Proof state:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ = x ∨ a✝ = y ∨ a✝ = z → a✝ ∈ (swap x y * swap y z).support

Tactic:
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]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)
⊢ (swap x y * swap y z).support = {x, y, z}

Tactic:
push_neg at h

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ (swap x y * swap y z).support = {x, y, z}

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ (swap x y * swap y z).support = {x, y, z}

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ (swap x y * swap y z).support ≤ {x, y, z}

case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} ≤ (swap x y * swap y z).support

Proof state:
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = (swap x y).support ⊔ (swap y z).support

Tactic:
rw [support_swap h.left.left, support_swap h.right.left]

Result:
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ⊔ {y, z}

Proof state:
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ⊔ {y, z}

Tactic:
simp [Finset.ext_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : [x, y, z].Nodup
⊢ (swap x y * swap y z).support = {x, y, z}

Tactic:
simp only [List.not_mem_nil, and_true, List.mem_cons, not_false_iff, List.nodup_cons,
  List.mem_singleton, and_self_iff, List.nodup_nil] at h

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)
⊢ (swap x y * swap y z).support = {x, y, z}