α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
⊢ IsThreeCycle σ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Finset.card (support σ) = 3 ↔ IsThreeCycle σ
refine' ⟨fun h => _, IsThreeCycle.card_support⟩
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : Perm.cycleType σ = 0
⊢ IsThreeCycle σ

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
⊢ IsThreeCycle σ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
⊢ IsThreeCycle σ
by_cases h0 : σ.cycleType = 0
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
⊢ IsThreeCycle σ
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
⊢ IsThreeCycle σ
obtain ⟨n, hn⟩ := exists_mem_of_ne_zero h0
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : erase (Perm.cycleType σ) n = 0
⊢ IsThreeCycle σ

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
⊢ IsThreeCycle σ
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
⊢ IsThreeCycle σ
by_cases h1 : σ.cycleType.erase n = 0
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
hm : m ∈ erase (Perm.cycleType σ) n
⊢ IsThreeCycle σ
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
⊢ IsThreeCycle σ
obtain ⟨m, hm⟩ := exists_mem_of_ne_zero h1
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
⊢ IsThreeCycle σ
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
hm : m ∈ erase (Perm.cycleType σ) n
⊢ IsThreeCycle σ
rw [← sum_cycleType, ← cons_erase hn, ← cons_erase hm, Multiset.sum_cons, Multiset.sum_cons] at h
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
this : ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False
⊢ IsThreeCycle σ
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
⊢ IsThreeCycle σ
have : ∀ {k}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False := by
  intros
  linarith
no goals
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
this : ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False
⊢ IsThreeCycle σ
cases this (two_le_of_mem_cycleType (mem_of_mem_erase hm)) (two_le_of_mem_cycleType hn) h
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : 0 = 3
h0 : Perm.cycleType σ = 0
⊢ IsThreeCycle σ
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : Perm.cycleType σ = 0
⊢ IsThreeCycle σ
rw [← sum_cycleType, h0, sum_zero] at h
no goals
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : 0 = 3
h0 : Perm.cycleType σ = 0
⊢ IsThreeCycle σ
exact (ne_of_lt zero_lt_three h).elim
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
h : n = 3
hn : n ∈ Perm.cycleType σ
h1 : erase (Perm.cycleType σ) n = 0
⊢ IsThreeCycle σ
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : Finset.card (support σ) = 3
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : erase (Perm.cycleType σ) n = 0
⊢ IsThreeCycle σ
rw [← sum_cycleType, ← cons_erase hn, h1, cons_zero, Multiset.sum_singleton] at h
no goals
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
h : n = 3
hn : n ∈ Perm.cycleType σ
h1 : erase (Perm.cycleType σ) n = 0
⊢ IsThreeCycle σ
rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
k✝ : ℕ
a✝² : 2 ≤ m
a✝¹ : 2 ≤ n
a✝ : n + (m + k✝) = 3
⊢ False
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
⊢ ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False
intros
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬Perm.cycleType σ = 0
n : ℕ
hn : n ∈ Perm.cycleType σ
h1 : ¬erase (Perm.cycleType σ) n = 0
m : ℕ
h : n + (m + sum (erase (erase (Perm.cycleType σ) n) m)) = 3
hm : m ∈ erase (Perm.cycleType σ) n
k✝ : ℕ
a✝² : 2 ≤ m
a✝¹ : 2 ≤ n
a✝ : n + (m + k✝) = 3
⊢ False
linarith