ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : (a : α) → β a → Type u_3<VAR>(x : α) → (y : β x) → Preorder (γ x y)<VAR>f : (x : α) → (y : β x) → γ x y<VAR>x : Sigma β<GOAL>(Pi.monotoneUncurry α β γ) f x = Sigma.uncurry f x
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : (a : α) → β a → Type u_3<VAR>(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)<GOAL>OmegaCompletePartialOrder.Continuous (Pi.monotoneCurry α β γ)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : (a : α) → β a → Type u_3<VAR>(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)<GOAL>OmegaCompletePartialOrder.Continuous (Pi.monotoneUncurry α β γ)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : (a : α) → β a → Type u_3<VAR>(x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)<VAR>f : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y<VAR>hc : OmegaCompletePartialOrder.Continuous f<GOAL>OmegaCompletePartialOrder.Continuous ((Pi.monotoneUncurry α β γ).comp (f.comp (Pi.monotoneCurry α β γ)))
<VAR>B : Type u_1<VAR>self : CoxeterMatrix B<GOAL>self.M.IsSymm
<VAR>B : Type u_1<VAR>self : CoxeterMatrix B<VAR>i : B<GOAL>self.M i i = 1
<VAR>B : Type u_1<VAR>self : CoxeterMatrix B<VAR>i i' : B<GOAL>i ≠ i' → self.M i i' ≠ 1
<VAR>B : Type u_1<VAR>M : CoxeterMatrix B<VAR>i i' : B<GOAL>M.M i i' = M.M i' i
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>M : CoxeterMatrix B<VAR>i i' : B'<GOAL>(CoxeterMatrix.reindex e M).M i i' = M.M (e.symm i) (e.symm i')
<VAR>α : Type u<VAR>DecidableEq α<VAR>Finite α<VAR>P : Equiv.Perm α → Prop<VAR>f : Equiv.Perm α<GOAL>P 1 → (∀ (f : Equiv.Perm α) (x y : α), x ≠ y → P f → P (Equiv.swap x y * f)) → P f
<VAR>α : Type u<VAR>DecidableEq α<VAR>Finite α<GOAL>Submonoid.closure {σ | σ.IsSwap} = ⊤
<VAR>α : Type u<VAR>DecidableEq α<VAR>Finite α<GOAL>Subgroup.closure {σ | σ.IsSwap} = ⊤
<VAR>n : ℕ<GOAL>Submonoid.closure (Set.range fun i => Equiv.swap i.castSucc i.succ) = ⊤
<VAR>α : Type u<VAR>DecidableEq α<VAR>Finite α<VAR>P : Equiv.Perm α → Prop<VAR>f : Equiv.Perm α<GOAL>P 1 → (∀ (f : Equiv.Perm α) (x y : α), x ≠ y → P f → P (f * Equiv.swap x y)) → P f
<VAR>α : Type u<VAR>DecidableEq α<VAR>w x y z : α<VAR>hwx : w ≠ x<VAR>hyz : y ≠ z<GOAL>IsConj (Equiv.swap w x) (Equiv.swap y z)
<VAR>n : ℕ<VAR>a : (_ : Fin n) × Fin n<GOAL>a ∈ Equiv.Perm.finPairsLT n ↔ a.snd < a.fst
<VAR>n : ℕ<GOAL>Equiv.Perm.signAux 1 = 1
<VAR>n : ℕ<VAR>f : Equiv.Perm (Fin n)<GOAL>Set.InjOn f.signBijAux ↑(Equiv.Perm.finPairsLT n)
<VAR>n : ℕ<VAR>f : Equiv.Perm (Fin n)<VAR>a : (_ : Fin n) × Fin n<GOAL>a ∈ Equiv.Perm.finPairsLT n → ∃ b ∈ Equiv.Perm.finPairsLT n, f.signBijAux b = a
<VAR>n : ℕ<VAR>f : Equiv.Perm (Fin n)<VAR>a : (_ : Fin n) × Fin n<GOAL>a ∈ Equiv.Perm.finPairsLT n → f.signBijAux a ∈ Equiv.Perm.finPairsLT n
<VAR>n : ℕ<VAR>f : Equiv.Perm (Fin n)<GOAL>f⁻¹.signAux = f.signAux
<VAR>n : ℕ<VAR>f g : Equiv.Perm (Fin n)<GOAL>(f * g).signAux = f.signAux * g.signAux
<VAR>n : ℕ<GOAL>(Equiv.swap 0 1).signAux = -1
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>(Equiv.swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1
<VAR>n : ℕ<VAR>x y : Fin n<VAR>_hxy : x ≠ y<GOAL>(Equiv.swap x y).signAux = -1
<VAR>α : Type u<VAR>DecidableEq α<VAR>n : ℕ<VAR>l : List α<VAR>f : Equiv.Perm α<VAR>e : α ≃ Fin n<VAR>_h : ∀ (x : α), f x ≠ x → x ∈ l<GOAL>Equiv.Perm.signAux ((e.symm.trans f).trans e) = Equiv.Perm.signAux2 l f
<VAR>α : Type u<VAR>DecidableEq α<VAR>Finite α<VAR>f g : Equiv.Perm α<VAR>s : Multiset α<VAR>hs : ∀ (x : α), x ∈ s<GOAL>(f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y => (Equiv.swap x y).signAux3 hs = -1
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Finite α<VAR>DecidableEq β<VAR>Finite β<VAR>f : Equiv.Perm α<VAR>e : α ≃ β<VAR>s : Multiset α<VAR>t : Multiset β<VAR>hs : ∀ (x : α), x ∈ s<VAR>ht : ∀ (x : β), x ∈ t<GOAL>Equiv.Perm.signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<GOAL>Equiv.Perm.sign (f * g) = Equiv.Perm.sign f * Equiv.Perm.sign g
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<GOAL>Equiv.Perm.sign (Equiv.trans f g) = Equiv.Perm.sign g * Equiv.Perm.sign f
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<GOAL>Equiv.Perm.sign 1 = 1
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<GOAL>Equiv.Perm.sign (Equiv.refl α) = 1
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>Equiv.Perm.sign f⁻¹ = Equiv.Perm.sign f
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>e : Equiv.Perm α<GOAL>Equiv.Perm.sign (Equiv.symm e) = Equiv.Perm.sign e
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>x y : α<VAR>h : x ≠ y<GOAL>Equiv.Perm.sign (Equiv.swap x y) = -1
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>x y : α<GOAL>Equiv.Perm.sign (Equiv.swap x y) = if x = y then 1 else -1
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>h : f.IsSwap<GOAL>Equiv.Perm.sign f = -1
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>f : Equiv.Perm α<VAR>e : α ≃ β<GOAL>Equiv.Perm.sign ((e.symm.trans f).trans e) = Equiv.Perm.sign f
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>f : Equiv.Perm β<VAR>e : α ≃ β<GOAL>Equiv.Perm.sign ((e.trans f).trans e.symm) = Equiv.Perm.sign f
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>l : List (Equiv.Perm α)<VAR>hl : ∀ g ∈ l, g.IsSwap<GOAL>Equiv.Perm.sign l.prod = (-1) ^ l.length
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>|↑(Equiv.Perm.sign f)| = 1
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>Nontrivial α<GOAL>Function.Surjective ⇑Equiv.Perm.sign
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Equiv.Perm α →* ℤˣ<VAR>hs : Function.Surjective ⇑s<GOAL>s = Equiv.Perm.sign
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>h₁ : ∀ (x : α), p x ↔ p (f x)<VAR>h₂ : ∀ (x : α), f x ≠ x → p x<GOAL>Equiv.Perm.sign (f.subtypePerm h₁) = Equiv.Perm.sign f
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>f : Equiv.Perm α<VAR>g : Equiv.Perm β<VAR>e : α ≃ β<VAR>h : ∀ (x : α), e (f x) = g (e x)<GOAL>Equiv.Perm.sign f = Equiv.Perm.sign g
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>f : Equiv.Perm α<VAR>g : Equiv.Perm β<VAR>i : (x : α) → f x ≠ x → β<VAR>h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)<VAR>hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂<VAR>hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y<GOAL>Equiv.Perm.sign f = Equiv.Perm.sign g
<VAR>β : Type v<VAR>α : Type u_1<VAR>DecidableEq α<VAR>σ : α → Equiv.Perm β<VAR>l : List α<VAR>hl : l.Nodup<VAR>mem_l : ∀ (a : α), a ∈ l<GOAL>(List.map (fun a => Equiv.Perm.prodExtendRight a (σ a)) l).prod = Equiv.prodCongrRight σ
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>a : α<VAR>σ : Equiv.Perm β<GOAL>Equiv.Perm.sign (Equiv.Perm.prodExtendRight a σ) = Equiv.Perm.sign σ
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>σ : α → Equiv.Perm β<GOAL>Equiv.Perm.sign (Equiv.prodCongrRight σ) = ∏ k : α, Equiv.Perm.sign (σ k)
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>σ : α → Equiv.Perm β<GOAL>Equiv.Perm.sign (Equiv.prodCongrLeft σ) = ∏ k : α, Equiv.Perm.sign (σ k)
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>e : α ≃ β<VAR>p : Equiv.Perm α<GOAL>Equiv.Perm.sign (e.permCongr p) = Equiv.Perm.sign p
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>σa : Equiv.Perm α<VAR>σb : Equiv.Perm β<GOAL>Equiv.Perm.sign (σa.sumCongr σb) = Equiv.Perm.sign σa * Equiv.Perm.sign σb
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>ep : Equiv.Perm { a // p a }<VAR>en : Equiv.Perm { a // ¬p a }<GOAL>Equiv.Perm.sign (ep.subtypeCongr en) = Equiv.Perm.sign ep * Equiv.Perm.sign en
<VAR>α : Type u<VAR>DecidableEq α<VAR>β : Type v<VAR>Fintype α<VAR>DecidableEq β<VAR>Fintype β<VAR>e : Equiv.Perm α<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<GOAL>Equiv.Perm.sign (e.extendDomain f) = Equiv.Perm.sign e
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : Equiv.Perm (Subtype p)<GOAL>Equiv.Perm.sign (Equiv.Perm.ofSubtype f) = Equiv.Perm.sign f
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>f.SameCycle x x
<VAR>α : Type u_2<VAR>x y : α<VAR>h : x = y<VAR>f : Equiv.Perm α<GOAL>f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f.SameCycle x y → f.SameCycle y x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f.SameCycle x y ↔ f.SameCycle y x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y z : α<GOAL>f.SameCycle x y → f.SameCycle y z → f.SameCycle x z
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<GOAL>Equivalence f.SameCycle
<VAR>α : Type u_2<VAR>x y : α<GOAL>Equiv.Perm.SameCycle 1 x y ↔ x = y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f⁻¹.SameCycle x y ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>f g : Equiv.Perm α<VAR>x y : α<GOAL>(g * f * g⁻¹).SameCycle x y ↔ f.SameCycle (g⁻¹ x) (g⁻¹ y)
<VAR>α : Type u_2<VAR>f g : Equiv.Perm α<VAR>x y : α<GOAL>f.SameCycle x y → (g * f * g⁻¹).SameCycle (g x) (g y)
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f.SameCycle x y → (f x = x ↔ f y = y)
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>h : f.SameCycle x y<VAR>hx : Function.IsFixedPt (⇑f) x<GOAL>x = y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>h : f.SameCycle x y<VAR>hy : Function.IsFixedPt (⇑f) y<GOAL>x = y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f.SameCycle (f x) y ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f.SameCycle x (f y) ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f.SameCycle (f⁻¹ x) y ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f.SameCycle x (f⁻¹ y) ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>n : ℤ<GOAL>f.SameCycle ((f ^ n) x) y ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>n : ℤ<GOAL>f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>n : ℕ<GOAL>f.SameCycle ((f ^ n) x) y ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>n : ℕ<GOAL>f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>n : ℕ<GOAL>(f ^ n).SameCycle x y → f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>n : ℤ<GOAL>(f ^ n).SameCycle x y → f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>p : α → Prop<VAR>h : ∀ (x : α), p x ↔ p (f x)<VAR>x y : { x // p x }<GOAL>(f.subtypePerm h).SameCycle x y ↔ f.SameCycle ↑x ↑y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>g : Equiv.Perm α<VAR>x y : α<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<GOAL>(g.extendDomain f).SameCycle ↑(f x) ↑(f y) ↔ g.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>Finite α<GOAL>f.SameCycle x y → ∃ i < orderOf f, (f ^ i) x = y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>Finite α<VAR>h : f.SameCycle x y<GOAL>∃ i, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>h : f.IsCycle<GOAL>f ≠ 1
<VAR>α : Type u_2<GOAL>¬Equiv.Perm.IsCycle 1
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>hf : f.IsCycle<VAR>hx : f x ≠ x<VAR>hy : f y ≠ y<GOAL>f.SameCycle x y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f.IsCycle → f x ≠ x → f y ≠ y → ∃ i, (f ^ i) x = y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<GOAL>f⁻¹.IsCycle
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<GOAL>f⁻¹.IsCycle ↔ f.IsCycle
<VAR>α : Type u_2<VAR>f g : Equiv.Perm α<GOAL>f.IsCycle → (g * f * g⁻¹).IsCycle
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>g : Equiv.Perm α<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<GOAL>g.IsCycle → (g.extendDomain f).IsCycle
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x : α<VAR>hx : f x ≠ x<GOAL>f.IsCycle ↔ ∀ {y : α}, f.SameCycle x y ↔ f y ≠ y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>Finite α<VAR>hf : f.IsCycle<VAR>hx : f x ≠ x<VAR>hy : f y ≠ y<GOAL>∃ i, (f ^ i) x = y
<VAR>α : Type u_2<VAR>x y : α<VAR>DecidableEq α<VAR>hxy : x ≠ y<GOAL>(Equiv.swap x y).IsCycle
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableEq α<GOAL>f.IsSwap → f.IsCycle
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableEq α<VAR>Fintype α<VAR>h : f.IsCycle<GOAL>2 ≤ f.support.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>hσ : σ.IsCycle<VAR>n : ℕ<GOAL>hσ.zpowersEquivSupport ⟨σ ^ n, ⋯⟩ = ⟨(σ ^ n) (Classical.choose hσ), ⋯⟩
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>hσ : σ.IsCycle<VAR>n : ℕ<GOAL>hσ.zpowersEquivSupport.symm ⟨(σ ^ n) (Classical.choose hσ), ⋯⟩ = ⟨σ ^ n, ⋯⟩
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableEq α<VAR>Fintype α<VAR>hf : f.IsCycle<GOAL>orderOf f = f.support.card
<VAR>α : Type u_4<VAR>DecidableEq α<VAR>n : ℕ<VAR>b x : α<VAR>f : Equiv.Perm α<GOAL>(Equiv.swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((Equiv.swap x (f x) * f) ^ i) (f x) = b
<VAR>α : Type u_4<VAR>DecidableEq α<VAR>n : ℤ<VAR>b x : α<VAR>f : Equiv.Perm α<GOAL>(Equiv.swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((Equiv.swap x (f x) * f) ^ i) (f x) = b
<VAR>α : Type u_4<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hfx : f x ≠ x<VAR>hffx : f (f x) = x<GOAL>f = Equiv.swap x (f x)
<VAR>α : Type u_4<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x<VAR>hffx : f (f x) ≠ x<GOAL>(Equiv.swap x (f x) * f).IsCycle
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<GOAL>Equiv.Perm.sign f = -(-1) ^ f.support.card
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableEq α<VAR>Fintype α<VAR>n : ℕ<VAR>h1 : (f ^ n).IsCycle<VAR>h2 : f.support ⊆ (f ^ n).support<GOAL>f.IsCycle
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableEq α<VAR>Fintype α<VAR>n : ℤ<VAR>h1 : (f ^ n).IsCycle<VAR>h2 : f.support ⊆ (f ^ n).support<GOAL>f.IsCycle
<VAR>β : Type u_3<VAR>l : List (Equiv.Perm β)<VAR>h1 : ∀ f ∈ l, f.IsCycle<VAR>h2 : List.Pairwise Equiv.Perm.Disjoint l<GOAL>l.Nodup
<VAR>α : Type u_2<VAR>f g : Equiv.Perm α<VAR>DecidableEq α<VAR>Fintype α<VAR>hf : f.IsCycle<VAR>hg : g.IsCycle<VAR>h : f.support ⊆ g.support<VAR>h' : ∀ x ∈ f.support, f x = g x<GOAL>f = g
<VAR>α : Type u_2<VAR>f g : Equiv.Perm α<VAR>x : α<VAR>DecidableEq α<VAR>Fintype α<VAR>hf : f.IsCycle<VAR>hg : g.IsCycle<VAR>h : ∀ x ∈ f.support ∩ g.support, f x = g x<VAR>hx : f x = g x<VAR>hx' : x ∈ f.support<GOAL>f = g
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableEq α<VAR>Fintype α<VAR>hf : f.IsCycle<VAR>n : ℕ<GOAL>(f ^ n).support = f.support ↔ ¬orderOf f ∣ n
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableEq α<VAR>Fintype α<VAR>hf : f.IsCycle<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : n < orderOf f<GOAL>(f ^ n).support = f.support
<VAR>β : Type u_3<VAR>Finite β<VAR>f : Equiv.Perm β<VAR>hf : f.IsCycle<VAR>n : ℕ<GOAL>(f ^ n).IsCycle ↔ n.Coprime (orderOf f)
<VAR>β : Type u_3<VAR>Finite β<VAR>f : Equiv.Perm β<VAR>hf : f.IsCycle<VAR>n : ℕ<GOAL>f ^ n = 1 ↔ ∃ x, f x ≠ x ∧ (f ^ n) x = x
<VAR>β : Type u_3<VAR>Finite β<VAR>f : Equiv.Perm β<VAR>hf : f.IsCycle<VAR>n : ℕ<VAR>x : β<VAR>hx : f x ≠ x<GOAL>f ^ n = 1 ↔ (f ^ n) x = x
<VAR>β : Type u_3<VAR>Finite β<VAR>f : Equiv.Perm β<VAR>hf : f.IsCycle<VAR>n : ℕ<GOAL>f ^ n = 1 ↔ ∀ (x : β), f x ≠ x → (f ^ n) x = x
<VAR>β : Type u_3<VAR>Finite β<VAR>f : Equiv.Perm β<VAR>hf : f.IsCycle<VAR>a b : ℕ<GOAL>f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x
<VAR>β : Type u_3<VAR>Finite β<VAR>f : Equiv.Perm β<VAR>hf : f.IsCycle<VAR>hf' : Nat.Prime (orderOf f)<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hn' : n < orderOf f<GOAL>(f ^ n).IsCycle
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<GOAL>IsConj σ τ
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<GOAL>IsConj σ τ ↔ σ.support.card = τ.support.card
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<GOAL>f.IsCycleOn ∅
<VAR>α : Type u_2<VAR>s : Set α<GOAL>Equiv.Perm.IsCycleOn 1 s ↔ s.Subsingleton
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>a : α<GOAL>f.IsCycleOn {a} ↔ f a = a
<VAR>α : Type u_2<VAR>Subsingleton α<VAR>f : Equiv.Perm α<VAR>s : Set α<GOAL>f.IsCycleOn s
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<GOAL>f⁻¹.IsCycleOn s ↔ f.IsCycleOn s
<VAR>α : Type u_2<VAR>f g : Equiv.Perm α<VAR>s : Set α<VAR>h : f.IsCycleOn s<GOAL>(g * f * g⁻¹).IsCycleOn (⇑g '' s)
<VAR>α : Type u_2<VAR>a b : α<VAR>DecidableEq α<VAR>hab : a ≠ b<GOAL>(Equiv.swap a b).IsCycleOn {a, b}
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>a : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<VAR>ha : a ∈ s<GOAL>f a ≠ a
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<GOAL>f.IsCycleOn {x | f x ≠ x}
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<GOAL>f.IsCycle ↔ ∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬Function.IsFixedPt (⇑f) x → x ∈ s
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>x : α<VAR>hf : f.IsCycleOn s<GOAL>f x ∈ s ↔ x ∈ s
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<GOAL>(f.subtypePerm ⋯).IsCycle
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>hf : f.IsCycleOn s<GOAL>(f.subtypePerm ⋯).IsCycleOn Set.univ
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>a : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>(f ^ n) a = a ↔ s.card ∣ n
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>a : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>n : ℤ<GOAL>(f ^ n) a = a ↔ ↑s.card ∣ n
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>a : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>m n : ℕ<GOAL>(f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD s.card]
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>a : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>m n : ℤ<GOAL>(f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD ↑s.card]
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>a : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<GOAL>(f ^ s.card) a = a
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>a b : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>∃ n < s.card, (f ^ n) a = b
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>a b : α<VAR>hs : s.Finite<VAR>hf : f.IsCycleOn s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>∃ n, (f ^ n) a = b
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>h : f.IsCycleOn s<VAR>ha : a ∈ s<GOAL>(Set.range fun n => (f ^ n) a) = s
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>a : α<VAR>h : f.IsCycleOn s<VAR>ha : a ∈ s<GOAL>(Set.range fun n => (f ^ n) a) = s
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>n : ℕ<VAR>hf : (f ^ n).IsCycleOn s<VAR>h : Set.BijOn (⇑f) s s<GOAL>f.IsCycleOn s
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>n : ℤ<VAR>hf : (f ^ n).IsCycleOn s<VAR>h : Set.BijOn (⇑f) s s<GOAL>f.IsCycleOn s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>g : Equiv.Perm α<VAR>s : Set α<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>h : g.IsCycleOn s<GOAL>(g.extendDomain f).IsCycleOn (Subtype.val ∘ ⇑f '' s)
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>hs : f.IsCycleOn s<GOAL>s.Countable
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<GOAL>l.formPerm.IsCycleOn {a | a ∈ l}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<GOAL>∃ f, f.IsCycleOn ↑s ∧ f.support ⊆ s
<VAR>α : Type u_2<VAR>s : Set α<VAR>hs : s.Countable<GOAL>∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>hf : f.IsCycleOn s<GOAL>s ×ˢ s = ⋃ n, (fun a => (a, (f ^ n) a)) '' s
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<GOAL>(↑(Finset.range s.card)).PairwiseDisjoint fun k => Finset.map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<GOAL>s ×ˢ s = (Finset.range s.card).disjiUnion (fun k => Finset.map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) ⋯
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Semiring α<VAR>AddCommMonoid β<VAR>Module α β<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>hσ : σ.IsCycleOn ↑s<VAR>f : ι → α<VAR>g : ι → β<GOAL>(∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ Finset.range s.card, ∑ i ∈ s, f i • g ((σ ^ k) i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Semiring α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>hσ : σ.IsCycleOn ↑s<VAR>f g : ι → α<GOAL>(∑ i ∈ s, f i) * ∑ i ∈ s, g i = ∑ k ∈ Finset.range s.card, ∑ i ∈ s, f i * g ((σ ^ k) i)
<VAR>α : Type u_1<VAR>x : Option α<GOAL>Option.traverse pure x = x
<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α : Type u_1<VAR>β γ : Type u<VAR>f : β → F γ<VAR>g : α → G β<VAR>x : Option α<GOAL>Option.traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) x = Functor.Comp.mk (Option.traverse f <$> Option.traverse g x)
<VAR>α β : Type u_1<VAR>f : α → β<VAR>x : Option α<GOAL>Option.traverse (pure ∘ f) x = pure (f <$> x)
<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>LawfulApplicative F<VAR>α : Type u_1<VAR>β : Type u<VAR>f : α → F β<VAR>x : Option α<GOAL>(fun {α} => η.app α) (Option.traverse f x) = Option.traverse ((fun {α} => η.app α) ∘ f) x
<VAR>α : Type u_1<VAR>xs : List α<GOAL>List.traverse pure xs = xs
<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α : Type u_1<VAR>β γ : Type u<VAR>f : β → F γ<VAR>g : α → G β<VAR>x : List α<GOAL>List.traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) x = Functor.Comp.mk (List.traverse f <$> List.traverse g x)
<VAR>α β : Type u_1<VAR>f : α → β<VAR>x : List α<GOAL>List.traverse (pure ∘ f) x = pure (f <$> x)
<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>LawfulApplicative F<VAR>η : ApplicativeTransformation F G<VAR>α : Type u_1<VAR>β : Type u<VAR>f : α → F β<VAR>x : List α<GOAL>(fun {α} => η.app α) (List.traverse f x) = List.traverse ((fun {α} => η.app α) ∘ f) x
<VAR>F : Type u → Type u<VAR>Applicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<GOAL>traverse f [] = pure []
<VAR>F : Type u → Type u<VAR>Applicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>a : α'<VAR>l : List α'<GOAL>traverse f (a :: l) = Seq.seq ((fun x x_1 => x :: x_1) <$> f a) fun x => traverse f l
<VAR>F : Type u → Type u<VAR>Applicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>LawfulApplicative F<VAR>as bs : List α'<GOAL>traverse f (as ++ bs) = Seq.seq ((fun x x_1 => x ++ x_1) <$> traverse f as) fun x => traverse f bs
<VAR>α' β' : Type u<VAR>f : α' → Set β'<VAR>l : List α'<VAR>n : List β'<GOAL>n ∈ traverse f l ↔ List.Forall₂ (fun b a => b ∈ f a) n l
<VAR>σ : Type u<VAR>G : Type u → Type u<VAR>Applicative G<VAR>α β γ : Type u<VAR>g : α → β<VAR>f : β → G γ<VAR>x : σ ⊕ α<GOAL>Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x
<VAR>σ α : Type u_1<VAR>x : σ ⊕ α<GOAL>Sum.traverse pure x = x
<VAR>σ : Type u<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α β γ : Type u<VAR>f : β → F γ<VAR>g : α → G β<VAR>x : σ ⊕ α<GOAL>Sum.traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) x = Functor.Comp.mk (Sum.traverse f <$> Sum.traverse g x)
<VAR>σ α β : Type u<VAR>f : α → β<VAR>x : σ ⊕ α<GOAL>Sum.traverse (pure ∘ f) x = pure (f <$> x)
<VAR>σ : Type u<VAR>G : Type u → Type u<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α : Type u_1<VAR>β γ : Type u<VAR>g : α → G β<VAR>f : β → γ<VAR>x : σ ⊕ α<GOAL>(fun x => f <$> x) <$> Sum.traverse g x = Sum.traverse (fun x => f <$> g x) x
<VAR>σ : Type u<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>LawfulApplicative F<VAR>η : ApplicativeTransformation F G<VAR>α : Type u_1<VAR>β : Type u<VAR>f : α → F β<VAR>x : σ ⊕ α<GOAL>(fun {α} => η.app α) (Sum.traverse f x) = Sum.traverse ((fun {α} => η.app α) ∘ f) x
<VAR>α : Type u<VAR>L : List (α × Bool)<GOAL>FreeAddGroup.Red L L