ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>P : Sylow p G<GOAL>Nat.card (Sylow p G) ∣ (↑P).index
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>(↑P).Normal<VAR>fP : (↑P).FiniteIndex<GOAL>¬p ∣ (↑P).index
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hp : Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>P : Sylow p G<VAR>hP : (↑P).relindex (↑P).normalizer ≠ 0<GOAL>¬p ∣ (↑P).index
<VAR>G : Type u_1<VAR>Group G<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>N.Normal<VAR>Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<GOAL>(Subgroup.map N.subtype ↑P).normalizer ⊔ N = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>N.Normal<VAR>Finite (Sylow p ↥N)<VAR>P : Sylow p G<VAR>hP : ↑P ≤ N<GOAL>(↑P).normalizer ⊔ N = ⊤
<VAR>G : Type u<VAR>Group G<VAR>s : Subgroup G<VAR>t : Set (G ⧸ s)<GOAL>Nat.card ↑(QuotientGroup.mk ⁻¹' t) = Nat.card ↥s * Nat.card ↑t
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>Finite ↑↑H<VAR>x : G<GOAL>↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H) ↔ x ∈ H.normalizer
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<GOAL>Nat.card (↥H.normalizer ⧸ Subgroup.comap H.normalizer.subtype H) ≡ Nat.card (G ⧸ H) [MOD p]
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<GOAL>Nat.card ↥H.normalizer ≡ Nat.card G [MOD p ^ (n + 1)]
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<GOAL>p ∣ Nat.card (↥H.normalizer ⧸ Subgroup.comap H.normalizer.subtype H)
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p n : ℕ<VAR>_hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<GOAL>p ^ (n + 1) ∣ Nat.card ↥H.normalizer
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ^ (n + 1) ∣ Nat.card G<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<GOAL>∃ K, Nat.card ↥K = p ^ (n + 1) ∧ H ≤ K
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p : ℕ<VAR>n m : ℕ<VAR>_hp : Fact (Nat.Prime p)<VAR>_hdvd : p ^ m ∣ Nat.card G<VAR>H : Subgroup G<VAR>_hH : Nat.card ↥H = p ^ n<VAR>_hnm : n ≤ m<GOAL>∃ K, Nat.card ↥K = p ^ m ∧ H ≤ K
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p : ℕ<VAR>n : ℕ<VAR>Fact (Nat.Prime p)<VAR>hdvd : p ^ n ∣ Nat.card G<GOAL>∃ K, Nat.card ↥K = p ^ n
<VAR>G : Type u<VAR>Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>hn : p ^ n ≤ Nat.card G<GOAL>∃ H, Nat.card ↥H = p ^ n
<VAR>G : Type u<VAR>Group G<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hn : p ^ n ≤ Nat.card ↥H<GOAL>∃ H' ≤ H, Nat.card ↥H' = p ^ n
<VAR>G : Type u<VAR>Group G<VAR>k p : ℕ<VAR>hp : Nat.Prime p<VAR>h : IsPGroup p G<VAR>H : Subgroup G<VAR>hk : k ≤ Nat.card ↥H<VAR>hk₀ : k ≠ 0<GOAL>∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ^ n ∣ Nat.card G<GOAL>p ^ n ∣ Nat.card ↥↑P
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ∣ Nat.card G<GOAL>p ∣ Nat.card ↥↑P
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<GOAL>(Nat.card ↥↑P).Coprime (↑P).index
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ∣ Nat.card G<GOAL>↑P ≠ ⊥
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<GOAL>Nat.card ↥↑P = p ^ (Nat.card G).factorization p
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p<GOAL>↑(Sylow.ofCard H card_eq) = H
<VAR>G : Type u<VAR>Group G<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>P : Sylow p G<VAR>h : (↑P).Normal<GOAL>(↑P).Characteristic
<VAR>G : Type u<VAR>Group G<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>P : Sylow p G<VAR>hn : (↑P).normalizer.Normal<GOAL>(↑P).Normal
<VAR>G : Type u<VAR>Group G<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>P : Sylow p G<GOAL>(↑P).normalizer.normalizer = (↑P).normalizer
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>P : Sylow p G<GOAL>(↑P).Normal
<VAR>G : Type u<VAR>Group G<VAR>hnc : NormalizerCondition G<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>P : Sylow p G<GOAL>(↑P).Normal
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>[].formPerm = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<GOAL>[x].formPerm = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<VAR>l : List α<GOAL>(x :: y :: l).formPerm = Equiv.swap x y * (y :: l).formPerm
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<GOAL>[x, y].formPerm = Equiv.swap x y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<VAR>x : α<GOAL>(List.zipWith Equiv.swap l l').prod x ≠ x → x ∈ l ∨ x ∈ l'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<GOAL>{x | (List.zipWith Equiv.swap l l').prod x ≠ x} ≤ ↑(l.toFinset ⊔ l'.toFinset)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>l l' : List α<GOAL>(List.zipWith Equiv.swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>{x | l.formPerm x ≠ x} ≤ ↑l.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>Fintype α<GOAL>l.formPerm.support ≤ l.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : l.formPerm x ≠ x<GOAL>x ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : x ∉ l<GOAL>l.formPerm x = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : x ∈ l<GOAL>l.formPerm x ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : l.formPerm x ∈ l<GOAL>x ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<GOAL>l.formPerm x ∈ l ↔ x ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<VAR>xs : List α<GOAL>(x :: (xs ++ [y])).formPerm y = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<VAR>xs : List α<GOAL>(x :: xs).formPerm ((x :: xs).getLast ⋯) = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<VAR>xs : List α<GOAL>(x :: xs).formPerm (x :: xs)[xs.length] = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<VAR>xs : List α<GOAL>(x :: xs).formPerm ((x :: xs).get ⟨xs.length, ⋯⟩) = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<VAR>xs : List α<GOAL>(x :: xs).formPerm ((x :: xs).nthLe xs.length ⋯) = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<VAR>xs : List α<VAR>h : (x :: y :: xs).Nodup<GOAL>(x :: y :: xs).formPerm x = y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>hl : 1 < l.length<GOAL>l.formPerm l[0] = l[1]
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>hl : 1 < l.length<GOAL>l.formPerm (l.get ⟨0, ⋯⟩) = l.get ⟨1, hl⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>hl : 1 < l.length<GOAL>l.formPerm (l.nthLe 0 ⋯) = l.nthLe 1 hl
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x y : α<GOAL>(y :: l).formPerm x = y ↔ x = (y :: l).getLast ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>h : xs.Nodup<VAR>n : ℕ<VAR>hn : n + 1 < xs.length<GOAL>xs.formPerm xs[n] = xs[n + 1]
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>h : xs.Nodup<VAR>n : ℕ<VAR>hn : n + 1 < xs.length<GOAL>xs.formPerm (xs.get ⟨n, ⋯⟩) = xs.get ⟨n + 1, hn⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>h : xs.Nodup<VAR>n : ℕ<VAR>hn : n + 1 < xs.length<GOAL>xs.formPerm (xs.nthLe n ⋯) = xs.nthLe (n + 1) hn
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>w : xs.Nodup<VAR>i : ℕ<VAR>h : i < xs.length<GOAL>xs.formPerm xs[i] = xs[(i + 1) % xs.length]
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>h : xs.Nodup<VAR>i : Fin xs.length<GOAL>xs.formPerm (xs.get i) = xs.get ⟨(↑i + 1) % xs.length, ⋯⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>h : xs.Nodup<VAR>n : ℕ<VAR>hn : n < xs.length<GOAL>xs.formPerm (xs.nthLe n hn) = xs.nthLe ((n + 1) % xs.length) ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>h' : ∀ (x : α), l ≠ [x]<GOAL>{x | l.formPerm x ≠ x} = ↑l.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>l : List α<VAR>h : l.Nodup<VAR>h' : ∀ (x : α), l ≠ [x]<GOAL>l.formPerm.support = l.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<GOAL>(l.rotate 1).formPerm = l.formPerm
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>n : ℕ<GOAL>(l.rotate n).formPerm = l.formPerm
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<VAR>hd : l.Nodup<VAR>h : l ~r l'<GOAL>l.formPerm = l'.formPerm
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a b : α<GOAL>(l ++ [a, b]).formPerm = (l ++ [a]).formPerm * Equiv.swap a b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.reverse.formPerm = l.formPerm⁻¹
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>w : l.Nodup<VAR>n i : ℕ<VAR>h : i < l.length<GOAL>(l.formPerm ^ n) l[i] = l[(i + n) % l.length]
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>n : ℕ<VAR>i : Fin l.length<GOAL>(l.formPerm ^ n) (l.get i) = l.get ⟨(↑i + n) % l.length, ⋯⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>n k : ℕ<VAR>hk : k < l.length<GOAL>(l.formPerm ^ n) (l.nthLe k hk) = l.nthLe ((k + n) % l.length) ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<VAR>l : List α<VAR>h : (x :: l).Nodup<VAR>n : ℕ<GOAL>((x :: l).formPerm ^ n) x = (x :: l).get ⟨n % (x :: l).length, ⋯⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<GOAL>(x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔ (x :: y :: l) ~r (x' :: y' :: l')
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.formPerm x = x ↔ l.length ≤ 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.formPerm x ≠ x ↔ 2 ≤ l.length
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<GOAL>l.formPerm = 1 ↔ l.length ≤ 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<VAR>hl : l.Nodup<VAR>hl' : l'.Nodup<GOAL>l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>hx : x ∈ l<VAR>n : ℤ<GOAL>(l.formPerm ^ n) x ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<GOAL>l.formPerm ^ l.length = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<VAR>hl : l.Nodup<VAR>hl' : l'.Nodup<VAR>hn : 2 ≤ l.length<VAR>hn' : 2 ≤ l'.length<GOAL>l.formPerm.Disjoint l'.formPerm ↔ l.Disjoint l'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>hn : 2 ≤ l.length<GOAL>l.formPerm.IsCycle
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>hn : 2 ≤ l.length<GOAL>List.Pairwise l.formPerm.SameCycle l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>hn : 2 ≤ l.length<VAR>x : { x // x ∈ l }<GOAL>l.attach.formPerm.cycleOf x = l.attach.formPerm
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>hn : 2 ≤ l.length<GOAL>l.attach.formPerm.cycleType = {l.length}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.formPerm x = l.next x hx
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<GOAL>(↑l).formPerm hl = l.formPerm
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>h : s.Subsingleton<GOAL>s.formPerm ⋯ = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>h : s.Nodup<VAR>hn : s.Nontrivial<GOAL>(s.formPerm h).IsCycle
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Cycle α<VAR>h : s.Nodup<VAR>hn : s.Nontrivial<GOAL>(s.formPerm h).support = s.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>h : s.Nodup<VAR>x : α<VAR>hx : x ∉ s<GOAL>(s.formPerm h) x = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>h : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>(s.formPerm h) x = s.next h x hx
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>h : s.Nodup<GOAL>s.reverse.formPerm ⋯ = (s.formPerm h)⁻¹
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s s' : Cycle α<VAR>hs : s.Nodup<VAR>hs' : s'.Nodup<GOAL>s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.Subsingleton ∧ s'.Subsingleton
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>x : α<GOAL>Equiv.Perm.toList 1 x = []
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<GOAL>p.toList x = [] ↔ x ∉ p.support
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<GOAL>(p.toList x).length = (p.cycleOf x).support.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x y : α<GOAL>p.toList x ≠ [y]
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<GOAL>2 ≤ (p.toList x).length ↔ x ∈ p.support
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<VAR>h : x ∈ p.support<GOAL>0 < (p.toList x).length
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<VAR>n : ℕ<VAR>hn : n < (p.toList x).length<GOAL>(p.toList x).get ⟨n, hn⟩ = (p ^ n) x
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<VAR>h : x ∈ p.support<GOAL>(p.toList x).get ⟨0, ⋯⟩ = x
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<VAR>n : ℕ<VAR>hn : n < (p.toList x).length<GOAL>(p.toList x).nthLe n hn = (p ^ n) x
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<VAR>h : x ∈ p.support<GOAL>(p.toList x).nthLe 0 ⋯ = x
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x y : α<GOAL>y ∈ p.toList x ↔ p.SameCycle x y ∧ x ∈ p.support
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<GOAL>(p.toList x).Nodup
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x y : α<VAR>hy : y ∈ p.toList x<GOAL>(p.toList x).next y hy = p y
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<VAR>k : ℕ<GOAL>p.toList ((p ^ k) x) = (p.toList x).rotate k
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>h : f.SameCycle x y<GOAL>f.toList x ~r f.toList y
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : Equiv.Perm α<VAR>x : α<VAR>n : ℕ<GOAL>(p ^ n) x ∈ p.toList x ↔ x ∈ p.support
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>x : α<GOAL>[].formPerm.toList x = []
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>x y : α<GOAL>[x].formPerm.toList y = []
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<GOAL>l.formPerm.toList (l.get ⟨0, ⋯⟩) = l
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>l : List α<VAR>hl : 2 ≤ l.length<VAR>hn : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.formPerm.toList x ~r l
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>(f.toList x).formPerm = f.cycleOf x
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x<GOAL>f.toCycle hf = ↑(f.toList x)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<GOAL>(f.toCycle hf).Nodup
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<GOAL>(f.toCycle hf).Nontrivial
<VAR>α : Type u_1<VAR>Finite α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<GOAL>∃! s, ∃ (h : s.Nodup), s.formPerm h = f
<VAR>α : Type u_1<VAR>Finite α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<GOAL>∃! s, (↑s).formPerm ⋯ = f
<VAR>α β γ : Type u<VAR>f : Type u → Type v<VAR>Functor f<VAR>LawfulFunctor f<VAR>m : α → β<VAR>g : β → γ<VAR>x : f α<GOAL>g <$> m <$> x = (g ∘ m) <$> x
<VAR>α : Type u<VAR>F : Type u → Type v<VAR>Applicative F<VAR>LawfulApplicative F<VAR>x : F α<GOAL>(Seq.seq (pure fun x => x) fun x_1 => x) = x
<VAR>α β γ : Type u<VAR>F : Type u → Type v<VAR>Applicative F<VAR>LawfulApplicative F<VAR>x : F (α → β)<VAR>f : γ → α<VAR>y : F γ<GOAL>(Seq.seq x fun x => f <$> y) = Seq.seq ((fun x => x ∘ f) <$> x) fun x => y
<VAR>α β γ : Type u<VAR>F : Type u → Type v<VAR>Applicative F<VAR>LawfulApplicative F<VAR>f : β → γ<VAR>x : F (α → β)<VAR>y : F α<GOAL>(f <$> Seq.seq x fun x => y) = Seq.seq ((fun x => f ∘ x) <$> x) fun x => y
<VAR>α β γ : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>x : m α<VAR>g : α → m β<VAR>f : β → γ<GOAL>f <$> (x >>= g) = do let a ← x f <$> g a
<VAR>α β γ : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>x : m α<VAR>g : β → m γ<VAR>f : α → β<GOAL>f <$> x >>= g = x >>= g ∘ f
<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u_1<VAR>β : Type u<VAR>f : α → m β<GOAL>f >=> pure = f
<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>α β : Type u<VAR>f : α → m β<GOAL>pure >=> f = f
<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u_1<VAR>β γ φ : Type u<VAR>f : α → m β<VAR>g : β → m γ<VAR>h : γ → m φ<GOAL>(f >=> g) >=> h = f >=> g >=> h
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>α β : Type u<VAR>f : α → β<VAR>a : m (m α)<GOAL>joinM (Functor.map f <$> a) = f <$> joinM a
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u<VAR>a : m (m (m α))<GOAL>joinM (joinM <$> a) = joinM (joinM a)
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u<VAR>a : m α<GOAL>joinM (pure <$> a) = a
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u<VAR>a : m α<GOAL>joinM (pure a) = a
<VAR>F : Type → Type v<VAR>Alternative F<VAR>h : Decidable True<GOAL>guard True = pure ()
<VAR>F : Type → Type v<VAR>Alternative F<VAR>h : Decidable False<GOAL>guard False = failure
<VAR>m : Type u → Type v<VAR>Applicative m<VAR>self : CommApplicative m<VAR>α β : Type u<VAR>a : m α<VAR>b : m β<GOAL>(Seq.seq (Prod.mk <$> a) fun x => b) = Seq.seq ((fun b a => (a, b)) <$> b) fun x => a
<VAR>m : Type u → Type v<VAR>h : Applicative m<VAR>CommApplicative m<VAR>α β γ : Type u<VAR>a : m α<VAR>b : m β<VAR>f : α → β → γ<GOAL>(Seq.seq (f <$> a) fun x => b) = Seq.seq (flip f <$> b) fun x => a
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.IsReflection (cs.simple i)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<GOAL>t ^ 2 = 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<GOAL>t * t = 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<GOAL>t⁻¹ = t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<GOAL>cs.IsReflection t⁻¹
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<GOAL>Odd (cs.length t)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.length (w * t) ≠ cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.length (t * w) ≠ cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.IsReflection (w * t * w⁻¹)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w t : W<GOAL>cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w t : W<GOAL>cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w t : W<GOAL>cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.IsRightInversion (w * t) t ↔ ¬cs.IsRightInversion w t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>¬cs.IsRightInversion (w * t) t ↔ cs.IsRightInversion w t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>¬cs.IsLeftInversion (t * w) t ↔ cs.IsLeftInversion w t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsRightInversion w (cs.simple i) ↔ cs.IsRightDescent w i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsLeftInversion w (cs.simple i) ↔ cs.IsLeftDescent w i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<GOAL>cs.rightInvSeq [] = []
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<GOAL>cs.leftInvSeq [] = []
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.rightInvSeq [i] = [cs.simple i]
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.leftInvSeq [i] = [cs.simple i]
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>i : B<GOAL>cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>i : B<GOAL>cs.leftInvSeq (ω.concat i) = (cs.leftInvSeq ω).concat (cs.wordProd ω * cs.simple i * (cs.wordProd ω)⁻¹)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>cs.rightInvSeq ω.reverse = (cs.leftInvSeq ω).reverse
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>cs.leftInvSeq ω.reverse = (cs.rightInvSeq ω).reverse
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>(cs.rightInvSeq ω).length = ω.length
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>(cs.leftInvSeq ω).length = ω.length
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>(cs.rightInvSeq ω).getD j 1 = (cs.wordProd (List.drop (j + 1) ω))⁻¹ * (Option.map cs.simple (ω.get? j)).getD 1 * cs.wordProd (List.drop (j + 1) ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>(cs.leftInvSeq ω).getD j 1 = cs.wordProd (List.take j ω) * (Option.map cs.simple (ω.get? j)).getD 1 * (cs.wordProd (List.take j ω))⁻¹
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>(cs.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>(cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 1