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

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ support (swap a b * swap a c) = {a, b, c}
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ IsThreeCycle (swap a b * swap a c)
suffices h : support (swap a b * swap a c) = {a, b, c}
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ ∀ (x : α), x ∈ support (swap a b) ⊔ support (swap a c) → 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 ∈ support (swap a b * swap a c)
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ support (swap a b * swap a c) = {a, b, c}
apply le_antisymm ((support_mul_le _ _).trans fun x => _) fun x hx => ?_
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : support (swap a b * swap a c) = {a, b, c}
⊢ Finset.card {a, b, c} = 3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : support (swap a b * swap a c) = {a, b, c}
⊢ IsThreeCycle (swap a b * swap a c)
rw [← card_support_eq_three_iff, h]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : support (swap a b * swap a c) = {a, b, c}
⊢ Finset.card {a, b, c} = 3
simp [ab, ac, bc]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ ∀ (x : α), x ∈ support (swap a b) ⊔ support (swap a c) → x ∈ {a, b, c}
simp [ab, ac, bc]
α : 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 ∈ support (swap a b * swap a 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 ∈ support (swap a b * swap a c)
simp only [Finset.mem_insert, Finset.mem_singleton] at hx
α : 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
α : 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 ∈ support (swap a b * swap a c)
rw [mem_support]
α : 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
α : 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
simp only [Perm.coe_mul, Function.comp_apply, Ne.def]
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
α : 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
obtain rfl | rfl | rfl := hx
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b c : α
bc : b ≠ c
x : α
ab : x ≠ b
ac : x ≠ c
⊢ ¬c = x
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
rw [swap_apply_left, swap_apply_of_ne_of_ne ac.symm bc.symm]
no goals
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b c : α
bc : b ≠ c
x : α
ab : x ≠ b
ac : x ≠ c
⊢ ¬c = x
exact ac.symm
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a c : α
ac : a ≠ c
x : α
ab : a ≠ x
bc : x ≠ c
⊢ ¬a = 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
rw [swap_apply_of_ne_of_ne ab.symm bc, swap_apply_right]
no goals
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a c : α
ac : a ≠ c
x : α
ab : a ≠ x
bc : x ≠ c
⊢ ¬a = x
exact ab
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
x : α
ac : a ≠ x
bc : b ≠ x
⊢ ¬b = 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
rw [swap_apply_right, swap_apply_left]
no goals
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
x : α
ac : a ≠ x
bc : b ≠ x
⊢ ¬b = x
exact bc