-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem isThreeCycle_swap_mul_swap_same {a b c : α} (ab : a ≠ b) (ac : a ≠ c) (bc : b ≠ c) :
    IsThreeCycle (swap a b * swap a c)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x ∈ {a, b, c}
⊢ x ∈ (swap a b * swap a c).support

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ x ∈ (swap a b * swap a c).support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ x ∈ (swap a b * swap a c).support

Tactic:
rw [mem_support]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ (swap a b * swap a c) x ≠ x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ (swap a b * swap a c) x ≠ x

Tactic:
simp only [Perm.coe_mul, Function.comp_apply, Ne]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ ¬(swap a b) ((swap a c) x) = x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : (swap a b * swap a c).support = {a, b, c}
⊢ (swap a b * swap a c).IsThreeCycle

Tactic:
rw [← card_support_eq_three_iff, h]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : (swap a b * swap a c).support = {a, b, c}
⊢ {a, b, c}.card = 3

Proof state:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b c : α
bc : b ≠ c
x : α
ab : x ≠ b
ac : x ≠ c
⊢ ¬(swap x b) ((swap x c) x) = x

Tactic:
rw [swap_apply_left, swap_apply_of_ne_of_ne ac.symm bc.symm]

Result:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b c : α
bc : b ≠ c
x : α
ab : x ≠ b
ac : x ≠ c
⊢ ¬c = x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ ∀ x ∈ (swap a b).support ⊔ (swap a c).support, x ∈ {a, b, c}

Tactic:
simp [ab, ac, bc]

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
x : α
ac : a ≠ x
bc : b ≠ x
⊢ ¬b = x

Tactic:
exact bc

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b c : α
bc : b ≠ c
x : α
ab : x ≠ b
ac : x ≠ c
⊢ ¬c = x

Tactic:
exact ac.symm

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a c : α
ac : a ≠ c
x : α
ab : a ≠ x
bc : x ≠ c
⊢ ¬(swap a x) ((swap a c) x) = x

Tactic:
rw [swap_apply_of_ne_of_ne ab.symm bc, swap_apply_right]

Result:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a c : α
ac : a ≠ c
x : α
ab : a ≠ x
bc : x ≠ c
⊢ ¬a = x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ (swap a b * swap a c).IsThreeCycle

Tactic:
suffices h : support (swap a b * swap a c) = {a, b, c} by
  rw [← card_support_eq_three_iff, h]
  simp [ab, ac, bc]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ (swap a b * swap a c).support = {a, b, c}

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ ¬(swap a b) ((swap a c) x) = x

Tactic:
obtain rfl | rfl | rfl := hx

Result:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b c : α
bc : b ≠ c
x : α
ab : x ≠ b
ac : x ≠ c
⊢ ¬(swap x b) ((swap x c) x) = x

case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a c : α
ac : a ≠ c
x : α
ab : a ≠ x
bc : x ≠ c
⊢ ¬(swap a x) ((swap a c) x) = x

case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
x : α
ac : a ≠ x
bc : b ≠ x
⊢ ¬(swap a b) ((swap a x) x) = x

Proof state:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a c : α
ac : a ≠ c
x : α
ab : a ≠ x
bc : x ≠ c
⊢ ¬a = x

Tactic:
exact ab

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
x : α
ac : a ≠ x
bc : b ≠ x
⊢ ¬(swap a b) ((swap a x) x) = x

Tactic:
rw [swap_apply_right, swap_apply_left]

Result:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
x : α
ac : a ≠ x
bc : b ≠ x
⊢ ¬b = x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ (swap a b * swap a c).support = {a, b, c}

Tactic:
apply le_antisymm ((support_mul_le _ _).trans fun x => _) fun x hx => ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ ∀ x ∈ (swap a b).support ⊔ (swap a c).support, x ∈ {a, b, c}

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x ∈ {a, b, c}
⊢ x ∈ (swap a b * swap a c).support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : (swap a b * swap a c).support = {a, b, c}
⊢ {a, b, c}.card = 3

Tactic:
simp [ab, ac, bc]

Result:
no goals