Theorem: Equiv.permWithCycleType_nonempty_iff (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (permWithCycleType α m).Nonempty ↔ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (permWithCycleType α m).Nonempty → Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) → (permWithCycleType α m).Nonempty

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (permWithCycleType α m).Nonempty → Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
h : (permWithCycleType α m).Nonempty
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
h : (permWithCycleType α m).Nonempty
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
obtain ⟨g, hg⟩ := h
State after:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g ∈ permWithCycleType α m
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

State before:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g ∈ permWithCycleType α m
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
simp only [Equiv.permWithCycleType, Set.toFinset_univ, Finset.mem_filter,
  Finset.mem_univ, true_and_iff] at hg
State after:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

State before:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
constructor
State after:
case mp.intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ Multiset.sum m ≤ Fintype.card α

case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a

State before:
case mp.intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ Multiset.sum m ≤ Fintype.card α

case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a
Tactic:
rw [← hg, Equiv.Perm.sum_cycleType]
State after:
case mp.intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ (Perm.support g).card ≤ Fintype.card α

case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a

State before:
case mp.intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ (Perm.support g).card ≤ Fintype.card α

case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a
Tactic:
exact (Equiv.Perm.support g).card_le_univ
State after:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a

State before:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a
Tactic:
intro a
State after:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
a : ℕ
⊢ a ∈ m → 2 ≤ a

State before:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
a : ℕ
⊢ a ∈ m → 2 ≤ a
Tactic:
rw [← hg]
State after:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
a : ℕ
⊢ a ∈ Perm.cycleType g → 2 ≤ a

State before:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
a : ℕ
⊢ a ∈ Perm.cycleType g → 2 ≤ a
Tactic:
exact Equiv.Perm.two_le_of_mem_cycleType
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) → (permWithCycleType α m).Nonempty
Tactic:
rintro ⟨hc, h2c⟩
State after:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ (permWithCycleType α m).Nonempty

State before:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ (permWithCycleType α m).Nonempty
Tactic:
have hc' : m.toList.sum ≤ Fintype.card α := by
  simp only [Multiset.sum_toList]
  exact hc
State after:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
⊢ (permWithCycleType α m).Nonempty

State before:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
⊢ (permWithCycleType α m).Nonempty
Tactic:
obtain ⟨p, hp_length, hp_nodup, hp_disj⟩ := List.exists_pw_disjoint_with_card hc'
State after:
case mpr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ (permWithCycleType α m).Nonempty

State before:
case mpr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ (permWithCycleType α m).Nonempty
Tactic:
use List.prod (List.map (fun l => List.formPerm l) p)
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ List.prod (List.map (fun l => List.formPerm l) p) ∈ permWithCycleType α m

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ List.prod (List.map (fun l => List.formPerm l) p) ∈ permWithCycleType α m
Tactic:
simp only [Equiv.permWithCycleType, Finset.mem_filter, Set.toFinset_univ,
  Finset.mem_univ, true_and_iff]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ Perm.cycleType (List.prod (List.map (fun l => List.formPerm l) p)) = m

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ Perm.cycleType (List.prod (List.map (fun l => List.formPerm l) p)) = m
Tactic:
have hp2 : ∀ x ∈ p, 2 ≤ x.length :=
  by
  intro x hx
  apply h2c x.length
  rw [← Multiset.mem_toList, ← hp_length, List.mem_map]
  exact ⟨x, hx, rfl⟩
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ Perm.cycleType (List.prod (List.map (fun l => List.formPerm l) p)) = m

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ Perm.cycleType (List.prod (List.map (fun l => List.formPerm l) p)) = m
Tactic:
rw [Equiv.Perm.cycleType_eq _ rfl]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ↑(List.map (Finset.card ∘ Perm.support) (List.map (fun l => List.formPerm l) p)) = m

case h.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ∀ σ ∈ List.map (fun l => List.formPerm l) p, Perm.IsCycle σ

case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.Pairwise Perm.Disjoint (List.map (fun l => List.formPerm l) p)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ List.sum (Multiset.toList m) ≤ Fintype.card α
Tactic:
simp only [Multiset.sum_toList]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ Multiset.sum m ≤ Fintype.card α

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ Multiset.sum m ≤ Fintype.card α
Tactic:
exact hc
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ ∀ x ∈ p, 2 ≤ List.length x
Tactic:
intro x hx
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ 2 ≤ List.length x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ 2 ≤ List.length x
Tactic:
apply h2c x.length
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ List.length x ∈ m

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ List.length x ∈ m
Tactic:
rw [← Multiset.mem_toList, ← hp_length, List.mem_map]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ ∃ a ∈ p, List.length a = List.length x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ ∃ a ∈ p, List.length a = List.length x
Tactic:
exact ⟨x, hx, rfl⟩
State after:
no goals

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ↑(List.map (Finset.card ∘ Perm.support) (List.map (fun l => List.formPerm l) p)) = m
Tactic:
rw [← Multiset.coe_toList m]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ↑(List.map (Finset.card ∘ Perm.support) (List.map (fun l => List.formPerm l) p)) = ↑(Multiset.toList m)

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ↑(List.map (Finset.card ∘ Perm.support) (List.map (fun l => List.formPerm l) p)) = ↑(Multiset.toList m)
Tactic:
apply congr_arg
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.map (Finset.card ∘ Perm.support) (List.map (fun l => List.formPerm l) p) = Multiset.toList m

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.map (Finset.card ∘ Perm.support) (List.map (fun l => List.formPerm l) p) = Multiset.toList m
Tactic:
rw [List.map_map]
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.map ((Finset.card ∘ Perm.support) ∘ fun l => List.formPerm l) p = Multiset.toList m

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.map ((Finset.card ∘ Perm.support) ∘ fun l => List.formPerm l) p = Multiset.toList m
Tactic:
rw [← hp_length]
State after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.map ((Finset.card ∘ Perm.support) ∘ fun l => List.formPerm l) p = List.map List.length p

State before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.map ((Finset.card ∘ Perm.support) ∘ fun l => List.formPerm l) p = List.map List.length p
Tactic:
apply List.map_congr
State after:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ∀ x ∈ p, ((Finset.card ∘ Perm.support) ∘ fun l => List.formPerm l) x = List.length x

State before:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ∀ x ∈ p, ((Finset.card ∘ Perm.support) ∘ fun l => List.formPerm l) x = List.length x
Tactic:
intro x hx
State after:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ ((Finset.card ∘ Perm.support) ∘ fun l => List.formPerm l) x = List.length x

State before:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ ((Finset.card ∘ Perm.support) ∘ fun l => List.formPerm l) x = List.length x
Tactic:
simp only [Function.comp_apply]
State after:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ (Perm.support (List.formPerm x)).card = List.length x

State before:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ (Perm.support (List.formPerm x)).card = List.length x
Tactic:
rw [List.support_formPerm_of_nodup x (hp_nodup x hx)]
State after:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ (List.toFinset x).card = List.length x

case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ ∀ (x_1 : α), x ≠ [x_1]

State before:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ (List.toFinset x).card = List.length x
Tactic:
rw [List.toFinset_card_of_nodup (hp_nodup x hx)]
State after:
no goals

State before:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ ∀ (x_1 : α), x ≠ [x_1]
Tactic:
intro a h
State after:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
a : α
h : x = [a]
⊢ False

State before:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
a : α
h : x = [a]
⊢ False
Tactic:
apply Nat.not_succ_le_self 1
State after:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
a : α
h : x = [a]
⊢ Nat.succ 1 ≤ 1

State before:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
a : α
h : x = [a]
⊢ Nat.succ 1 ≤ 1
Tactic:
conv_rhs => rw [← List.length_singleton a]; rw [← h]
State after:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
a : α
h : x = [a]
⊢ Nat.succ 1 ≤ List.length x

State before:
case h.h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
a : α
h : x = [a]
⊢ Nat.succ 1 ≤ List.length x
Tactic:
exact hp2 x hx
State after:
no goals

State before:
case h.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ∀ σ ∈ List.map (fun l => List.formPerm l) p, Perm.IsCycle σ
Tactic:
intro g
State after:
case h.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
g : Perm α
⊢ g ∈ List.map (fun l => List.formPerm l) p → Perm.IsCycle g

State before:
case h.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
g : Perm α
⊢ g ∈ List.map (fun l => List.formPerm l) p → Perm.IsCycle g
Tactic:
rw [List.mem_map]
State after:
case h.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
g : Perm α
⊢ (∃ a ∈ p, List.formPerm a = g) → Perm.IsCycle g

State before:
case h.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
g : Perm α
⊢ (∃ a ∈ p, List.formPerm a = g) → Perm.IsCycle g
Tactic:
rintro ⟨x, hx, rfl⟩
State after:
case h.h1.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ Perm.IsCycle (List.formPerm x)

State before:
case h.h1.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
⊢ Perm.IsCycle (List.formPerm x)
Tactic:
have hx_nodup : x.Nodup := hp_nodup x hx
State after:
case h.h1.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
hx_nodup : List.Nodup x
⊢ Perm.IsCycle (List.formPerm x)

State before:
case h.h1.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
hx_nodup : List.Nodup x
⊢ Perm.IsCycle (List.formPerm x)
Tactic:
rw [← Cycle.formPerm_coe x hx_nodup]
State after:
case h.h1.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
hx_nodup : List.Nodup x
⊢ Perm.IsCycle (Cycle.formPerm (↑x) hx_nodup)

State before:
case h.h1.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
hx_nodup : List.Nodup x
⊢ Perm.IsCycle (Cycle.formPerm (↑x) hx_nodup)
Tactic:
apply Cycle.isCycle_formPerm
State after:
case h.h1.intro.intro.hn
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
hx_nodup : List.Nodup x
⊢ Cycle.Nontrivial ↑x

State before:
case h.h1.intro.intro.hn
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
hx_nodup : List.Nodup x
⊢ Cycle.Nontrivial ↑x
Tactic:
rw [Cycle.nontrivial_coe_nodup_iff hx_nodup]
State after:
case h.h1.intro.intro.hn
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
hx_nodup : List.Nodup x
⊢ 2 ≤ List.length x

State before:
case h.h1.intro.intro.hn
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
x : List α
hx : x ∈ p
hx_nodup : List.Nodup x
⊢ 2 ≤ List.length x
Tactic:
exact hp2 x hx
State after:
no goals

State before:
case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.Pairwise Perm.Disjoint (List.map (fun l => List.formPerm l) p)
Tactic:
rw [List.pairwise_map]
State after:
case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.Pairwise (fun a b => Perm.Disjoint (List.formPerm a) (List.formPerm b)) p

State before:
case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.Pairwise (fun a b => Perm.Disjoint (List.formPerm a) (List.formPerm b)) p
Tactic:
apply List.Pairwise.imp_of_mem _ hp_disj
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ∀ {a b : List α}, a ∈ p → b ∈ p → List.Disjoint a b → Perm.Disjoint (List.formPerm a) (List.formPerm b)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ∀ {a b : List α}, a ∈ p → b ∈ p → List.Disjoint a b → Perm.Disjoint (List.formPerm a) (List.formPerm b)
Tactic:
intro a b ha hb hab
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : List.Disjoint a b
⊢ Perm.Disjoint (List.formPerm a) (List.formPerm b)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : List.Disjoint a b
⊢ Perm.Disjoint (List.formPerm a) (List.formPerm b)
Tactic:
rw [List.formPerm_disjoint_iff (hp_nodup a ha) (hp_nodup b hb) (hp2 a ha) (hp2 b hb)]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : List.Disjoint a b
⊢ List.Disjoint a b

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : List.Disjoint a b
⊢ List.Disjoint a b
Tactic:
exact hab
State after:
no goals