ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<GOAL>Subgroup.closure (Set.range cs.simple) = ⊤
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<GOAL>Submonoid.closure (Set.range cs.simple) = ⊤
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>simple : ∀ (i : B), p (cs.simple i)<VAR>one : p 1<VAR>mul : ∀ (w w' : W), p w → p w' → p (w * w')<GOAL>p w
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)<GOAL>p w
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)<GOAL>p w
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>G : Type u_5<VAR>Monoid G<VAR>φ₁ φ₂ : W →* G<VAR>h : ∀ (i : B), φ₁ (cs.simple i) = φ₂ (cs.simple i)<GOAL>φ₁ = φ₂
<VAR>B : Type u_1<VAR>M : CoxeterMatrix B<VAR>G : Type u_5<VAR>Group G<VAR>f : B → G<VAR>hf : M.IsLiftable f<VAR>r : FreeGroup B<VAR>hr : r ∈ M.relationsSet<GOAL>(FreeGroup.lift f) r = 1
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>a : PresentedGroup M.relationsSet<GOAL>cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm a) = a
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>G : Type u_5<VAR>Monoid G<VAR>f : B → G<VAR>hf : M.IsLiftable f<VAR>i : B<GOAL>(cs.lift ⟨f, hf⟩) (cs.simple i) = f i
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<GOAL>Function.Injective CoxeterSystem.simple
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<GOAL>cs.wordProd [] = 1
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<VAR>ω : List B<GOAL>cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.wordProd [i] = cs.simple i
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<VAR>ω : List B<GOAL>cs.wordProd (ω.concat i) = cs.wordProd ω * cs.simple i
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω ω' : List B<GOAL>cs.wordProd (ω ++ ω') = cs.wordProd ω * cs.wordProd ω'
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>cs.wordProd ω.reverse = (cs.wordProd ω)⁻¹
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<GOAL>Function.Surjective cs.wordProd
<VAR>B : Type u_1<VAR>i i' : B<VAR>m : ℕ<GOAL>CoxeterSystem.alternatingWord i i' (m + 1) = (CoxeterSystem.alternatingWord i' i m).concat i'
<VAR>B : Type u_1<VAR>i i' : B<VAR>m : ℕ<GOAL>CoxeterSystem.alternatingWord i i' (m + 1) = (if Even m then i' else i) :: CoxeterSystem.alternatingWord i i' m
<VAR>B : Type u_1<VAR>i i' : B<VAR>m : ℕ<GOAL>(CoxeterSystem.alternatingWord i i' m).length = m
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>m : ℕ<GOAL>cs.wordProd (CoxeterSystem.alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>m : ℕ<VAR>hm : m ≤ M.M i i' * 2<GOAL>cs.wordProd (CoxeterSystem.alternatingWord i i' m) = cs.wordProd (CoxeterSystem.alternatingWord i' i (M.M i i' * 2 - m))
<VAR>B : Type u_1<VAR>W : Type u_3<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<GOAL>cs.wordProd (CoxeterSystem.braidWord M i i') = cs.wordProd (CoxeterSystem.braidWord M i' i)
<VAR>β : Type u_3<VAR>Finite β<GOAL>Subgroup.closure {σ | σ.IsCycle} = ⊤
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = ⊤<VAR>x : α<GOAL>Subgroup.closure {σ, Equiv.swap x (σ x)} = ⊤
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>n : ℕ<VAR>σ : Equiv.Perm α<VAR>h0 : n.Coprime (Fintype.card α)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = Finset.univ<VAR>x : α<GOAL>Subgroup.closure {σ, Equiv.swap x ((σ ^ n) x)} = ⊤
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>σ τ : Equiv.Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = Finset.univ<VAR>h3 : τ.IsSwap<GOAL>Subgroup.closure {σ, τ} = ⊤
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>S : Set G<GOAL>(∀ g ∈ Subgroup.closure S, (MulAction.fixedBy α g)ᶜ.Finite) ↔ ∀ g ∈ S, (MulAction.fixedBy α g)ᶜ.Finite
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>x y : α<GOAL>(MulAction.fixedBy α (Equiv.swap x y))ᶜ.Finite
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>h : σ.IsSwap<GOAL>(MulAction.fixedBy α σ)ᶜ.Finite
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>a b c : α<VAR>C : Type u_3<VAR>SetLike C (Equiv.Perm α)<VAR>SubmonoidClass C (Equiv.Perm α)<VAR>M : C<VAR>hab : Equiv.swap a b ∈ M<VAR>hbc : Equiv.swap b c ∈ M<GOAL>Equiv.swap a c ∈ M
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>S : Set G<VAR>T : Set α<VAR>a : α<VAR>hS : ∀ g ∈ S, g⁻¹ ∈ S<VAR>subset : T ⊆ MulAction.orbit (↥(Subgroup.closure S)) a<VAR>not_mem : a ∉ T<VAR>nonempty : T.Nonempty<GOAL>∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>x y : α<GOAL>Equiv.swap x y ∈ Subgroup.closure S ↔ x ∈ MulAction.orbit (↥(Subgroup.closure S)) y
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>f : Equiv.Perm α<GOAL>f ∈ Subgroup.closure S ↔ (MulAction.fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), f x ∈ MulAction.orbit (↥(Subgroup.closure S)) x
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>f : Equiv.Perm α<GOAL>f ∈ Subgroup.closure {σ | σ.IsSwap} ↔ (MulAction.fixedBy α f)ᶜ.Finite
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Finite α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ σ ∈ S, σ.IsSwap<VAR>MulAction.IsPretransitive (↥(Subgroup.closure S)) α<GOAL>Subgroup.closure S = ⊤
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>DecidableEq α<VAR>Finite α<VAR>S : Set G<VAR>hS1 : ∀ σ ∈ S, ((MulAction.toPermHom G α) σ).IsSwap<VAR>hS2 : Subgroup.closure S = ⊤<VAR>h : MulAction.IsPretransitive G α<GOAL>Function.Surjective ⇑(MulAction.toPermHom G α)
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<GOAL>f.Disjoint g → g.Disjoint f
<VAR>α : Type u_1<GOAL>Symmetric Equiv.Perm.Disjoint
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<GOAL>f.Disjoint g ↔ g.Disjoint f
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<VAR>h : f.Disjoint g<GOAL>Commute f g
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<GOAL>Equiv.Perm.Disjoint 1 f
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<GOAL>f.Disjoint 1
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<GOAL>f.Disjoint g ↔ ∀ (x : α), f x = x ∨ g x = x
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<GOAL>f.Disjoint f ↔ f = 1
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<VAR>h : f.Disjoint g<GOAL>f⁻¹.Disjoint g
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<VAR>h : f.Disjoint g<GOAL>f.Disjoint g⁻¹
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<GOAL>f⁻¹.Disjoint g ↔ f.Disjoint g
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<GOAL>f.Disjoint g⁻¹ ↔ f.Disjoint g
<VAR>α : Type u_1<VAR>f g h : Equiv.Perm α<VAR>H1 : f.Disjoint h<VAR>H2 : g.Disjoint h<GOAL>(f * g).Disjoint h
<VAR>α : Type u_1<VAR>f g h : Equiv.Perm α<VAR>H1 : f.Disjoint g<VAR>H2 : f.Disjoint h<GOAL>f.Disjoint (g * h)
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<VAR>h : Equiv.Perm α<GOAL>(h * f * h⁻¹).Disjoint (h * g * h⁻¹) ↔ f.Disjoint g
<VAR>α : Type u_1<VAR>f g : Equiv.Perm α<VAR>H : f.Disjoint g<VAR>h : Equiv.Perm α<GOAL>(h * f * h⁻¹).Disjoint (h * g * h⁻¹)
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>l : List (Equiv.Perm α)<VAR>h : ∀ g ∈ l, f.Disjoint g<GOAL>f.Disjoint l.prod
<VAR>α : Type u_1<VAR>l₁ l₂ : List (Equiv.Perm α)<VAR>hl : List.Pairwise Equiv.Perm.Disjoint l₁<VAR>hp : l₁.Perm l₂<GOAL>l₁.prod = l₂.prod
<VAR>α : Type u_1<VAR>l : List (Equiv.Perm α)<VAR>h1 : 1 ∉ l<VAR>h2 : List.Pairwise Equiv.Perm.Disjoint l<GOAL>l.Nodup
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>x : α<VAR>hfx : f x = x<VAR>n : ℕ<GOAL>(f ^ n) x = x
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>x : α<VAR>hfx : f x = x<VAR>n : ℤ<GOAL>(f ^ n) x = x
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>x : α<VAR>hffx : f (f x) = x<VAR>n : ℕ<GOAL>(f ^ n) x = x ∨ (f ^ n) x = f x
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>x : α<VAR>hffx : f (f x) = x<VAR>i : ℤ<GOAL>(f ^ i) x = x ∨ (f ^ i) x = f x
<VAR>α : Type u_1<VAR>σ τ : Equiv.Perm α<VAR>hστ : σ.Disjoint τ<VAR>a : α<GOAL>(σ * τ) a = a ↔ σ a = a ∧ τ a = a
<VAR>α : Type u_1<VAR>σ τ : Equiv.Perm α<VAR>hστ : σ.Disjoint τ<GOAL>σ * τ = 1 ↔ σ = 1 ∧ τ = 1
<VAR>α : Type u_1<VAR>σ τ : Equiv.Perm α<VAR>hστ : σ.Disjoint τ<VAR>m n : ℤ<GOAL>(σ ^ m).Disjoint (τ ^ n)
<VAR>α : Type u_1<VAR>σ τ : Equiv.Perm α<VAR>hστ : σ.Disjoint τ<VAR>m n : ℕ<GOAL>(σ ^ m).Disjoint (τ ^ n)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x y : Subtype p<GOAL>Equiv.Perm.ofSubtype (Equiv.swap x y) = Equiv.swap ↑x ↑y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : Equiv.Perm (Subtype p)<VAR>h : f.IsSwap<GOAL>(Equiv.Perm.ofSubtype f).IsSwap
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>hy : (Equiv.swap x (f x) * f) y ≠ y<GOAL>f y ≠ y ∧ y ≠ x
<VAR>α : Type u_1<VAR>p : Equiv.Perm α<GOAL>{x | p⁻¹ x ≠ x} = {x | p x ≠ x}
<VAR>α : Type u_1<VAR>p : Equiv.Perm α<VAR>a : α<GOAL>p a ∈ {x | p x ≠ x} ↔ a ∈ {x | p x ≠ x}
<VAR>α : Type u_1<VAR>p : Equiv.Perm α<VAR>n : ℤ<GOAL>{x | (p ^ n) x ≠ x} ⊆ {x | p x ≠ x}
<VAR>α : Type u_1<VAR>p q : Equiv.Perm α<GOAL>{x | (p * q) x ≠ x} ⊆ {x | p x ≠ x} ∪ {x | q x ≠ x}
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>n : ℕ<VAR>x : α<GOAL>f ((f ^ n) x) = (f ^ n) x ↔ f x = x
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<VAR>n : ℤ<VAR>x : α<GOAL>f ((f ^ n) x) = (f ^ n) x ↔ f x = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>x ∈ f.support ↔ f x ≠ x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>x ∉ f.support ↔ f x = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>↑f.support = {x | f x ≠ x}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<GOAL>σ.support = ∅ ↔ σ = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<GOAL>Equiv.Perm.support 1 = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<GOAL>Equiv.Perm.support (Equiv.refl α) = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : f.support ⊆ g.support<VAR>h' : ∀ x ∈ g.support, f x = g x<GOAL>f = g
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<GOAL>(f * g).support ≤ f.support ⊔ g.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>l : List (Equiv.Perm α)<VAR>x : α<VAR>hx : x ∈ l.prod.support<GOAL>∃ f ∈ l, x ∈ f.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>n : ℕ<GOAL>(σ ^ n).support ≤ σ.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<GOAL>σ⁻¹.support = σ.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>f x ∈ f.support ↔ x ∈ f.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>n : ℕ<VAR>x : α<GOAL>(f ^ n) x ∈ f.support ↔ x ∈ f.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>n : ℤ<VAR>x : α<GOAL>(f ^ n) x ∈ f.support ↔ x ∈ f.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : ∀ x ∈ f.support ∩ g.support, f x = g x<VAR>k : ℕ<VAR>x : α<GOAL>x ∈ f.support ∩ g.support → (f ^ k) x = (g ^ k) x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<GOAL>f.Disjoint g ↔ Disjoint f.support g.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : f.Disjoint g<GOAL>Disjoint f.support g.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : f.Disjoint g<GOAL>(f * g).support = f.support ∪ g.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>l : List (Equiv.Perm α)<VAR>h : List.Pairwise Equiv.Perm.Disjoint l<GOAL>l.prod.support = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map Equiv.Perm.support l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>l : List (Equiv.Perm α)<GOAL>l.prod.support ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map Equiv.Perm.support l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>n : ℤ<GOAL>(σ ^ n).support ≤ σ.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>x y : α<VAR>h : x ≠ y<GOAL>(Equiv.swap x y).support = {x, y}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>x y : α<GOAL>(Equiv.swap x y).support = {x, y} ↔ x ≠ y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>x y z : α<VAR>h : [x, y, z].Nodup<GOAL>(Equiv.swap x y * Equiv.swap y z).support = {x, y, z}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f.support \ {x, y} ≤ (Equiv.swap x y * f).support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x : α<VAR>h : f (f x) ≠ x<GOAL>(Equiv.swap x (f x) * f).support = f.support \ {x}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>hy : y ∈ (Equiv.swap x (f x) * f).support<GOAL>y ∈ f.support ∧ y ≠ x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : f.Disjoint g<VAR>x : α<VAR>hx : x ∈ f.support<GOAL>x ∉ g.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>l : List (Equiv.Perm α)<VAR>h : f ∈ l<VAR>hl : List.Pairwise Equiv.Perm.Disjoint l<VAR>x : α<GOAL>x ∈ f.support → f x = l.prod x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f g x y : Equiv.Perm α<VAR>h : f.Disjoint g<VAR>hf : x.support ≤ f.support<VAR>hg : y.support ≤ g.support<GOAL>x.Disjoint y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>l : List (Equiv.Perm α)<VAR>h : f ∈ l<VAR>hl : List.Pairwise Equiv.Perm.Disjoint l<GOAL>f.support ≤ l.prod.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>β : Type u_2<VAR>DecidableEq β<VAR>Fintype β<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g : Equiv.Perm α<GOAL>(g.extendDomain f).support = Finset.map f.asEmbedding g.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>β : Type u_2<VAR>DecidableEq β<VAR>Fintype β<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g : Equiv.Perm α<GOAL>(g.extendDomain f).support.card = g.support.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>f.support.card = 0 ↔ f = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>h : f ≠ 1<GOAL>1 < f.support.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>f.support.card ≠ 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>f.support.card ≤ 1 ↔ f = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>h : f ≠ 1<GOAL>2 ≤ f.support.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x : α<VAR>hx : f x ≠ x<GOAL>(Equiv.swap x (f x) * f).support.card < f.support.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>(Equiv.swap x y).support.card = 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>f.support.card = 2 ↔ f.IsSwap
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : f.Disjoint g<GOAL>(f * g).support.card = f.support.card + g.support.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>l : List (Equiv.Perm α)<VAR>h : List.Pairwise Equiv.Perm.Disjoint l<GOAL>l.prod.support.card = (List.map (Finset.card ∘ Equiv.Perm.support) l).sum
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>f : Equiv.Perm α<VAR>h : ∀ (x : α), x ∈ s ↔ f x ∈ s<GOAL>(f.subtypePerm h).support = Finset.filter (fun x => decide (f ↑x ≠ ↑x) = true) s.attach
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>h : σ ≠ 1<GOAL>(Finset.filter (fun x => σ x = x) Finset.univ).card < Fintype.card α - 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<GOAL>(σ * τ * σ⁻¹).support = Finset.map (Equiv.toEmbedding σ) τ.support
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<GOAL>(σ * τ * σ⁻¹).support.card = τ.support.card
<VAR>G : Type u<VAR>Group G<VAR>self : IsFreeGroup G<GOAL>∃ ι, Nonempty (FreeGroupBasis ι G)
<VAR>ι : Type u_1<VAR>G : Type u_3<VAR>Group G<VAR>b : FreeGroupBasis ι G<VAR>i : ι<GOAL>b.repr (b i) = FreeGroup.of i
<VAR>X : Type u_5<VAR>x : X<GOAL>(FreeGroupBasis.ofFreeGroup X) x = FreeGroup.of x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>G : Type u_3<VAR>Group G<VAR>b : FreeGroupBasis ι G<VAR>e : ι ≃ ι'<VAR>x : ι'<GOAL>(b.reindex e) x = b (e.symm x)
<VAR>ι : Type u_1<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Group G<VAR>Group H<VAR>b : FreeGroupBasis ι G<VAR>e : G ≃* H<VAR>x : ι<GOAL>(b.map e) x = e (b x)
<VAR>ι : Type u_1<VAR>G : Type u_3<VAR>Group G<VAR>b : FreeGroupBasis ι G<GOAL>Function.Injective ⇑b
<VAR>ι : Type u_1<VAR>G : Type u_3<VAR>Group G<VAR>b : FreeGroupBasis ι G<GOAL>IsFreeGroup G
<VAR>ι : Type u_1<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Group G<VAR>Group H<VAR>b : FreeGroupBasis ι G<GOAL>∀ (a : ι → H) (a_1 : G), (b.lift a) a_1 = (FreeGroup.lift a) (b.repr a_1)
<VAR>ι : Type u_1<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Group G<VAR>Group H<VAR>b : FreeGroupBasis ι G<GOAL>∀ (a : G →* H) (a_1 : ι), b.lift.symm a a_1 = a (b.repr.symm (FreeGroup.of a_1))
<VAR>ι : Type u_1<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Group G<VAR>Group H<VAR>b : FreeGroupBasis ι G<VAR>f g : G →* H<VAR>h : ∀ (i : ι), f (b i) = g (b i)<GOAL>f = g
<VAR>G : Type u_2<VAR>Group G<VAR>IsFreeGroup G<GOAL>IsFreeGroup.mulEquiv G = ⋯.some.repr.symm
<VAR>G : Type u_1<VAR>Group G<VAR>IsFreeGroup G<GOAL>∀ (a : FreeGroup (IsFreeGroup.Generators G)), (IsFreeGroup.toFreeGroup G).symm a = (IsFreeGroup.mulEquiv G) a
<VAR>G : Type u_1<VAR>Group G<VAR>IsFreeGroup G<GOAL>∀ (a : G), (IsFreeGroup.toFreeGroup G) a = (IsFreeGroup.mulEquiv G).symm a
<VAR>G : Type u_1<VAR>Group G<VAR>IsFreeGroup G<VAR>H : Type u_2<VAR>Group H<VAR>f : IsFreeGroup.Generators G → H<VAR>a : IsFreeGroup.Generators G<GOAL>(IsFreeGroup.lift f) (IsFreeGroup.of a) = f a
<VAR>G : Type u_1<VAR>Group G<VAR>IsFreeGroup G<VAR>H : Type u_2<VAR>Group H<VAR>f : G →* H<VAR>a : IsFreeGroup.Generators G<GOAL>IsFreeGroup.lift.symm f a = f (IsFreeGroup.of a)
<VAR>G : Type u_1<VAR>Group G<VAR>IsFreeGroup G<VAR>H : Type u_2<VAR>Group H<VAR>f g : G →* H<VAR>h : ∀ (a : IsFreeGroup.Generators G), f (IsFreeGroup.of a) = g (IsFreeGroup.of a)<GOAL>f = g
<VAR>G : Type u_1<VAR>Group G<VAR>IsFreeGroup G<VAR>H : Type u_2<VAR>Group H<VAR>f : IsFreeGroup.Generators G → H<GOAL>∃! F, ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f a
<VAR>G : Type u<VAR>Group G<VAR>X : Type u<VAR>of : X → G<VAR>lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)<VAR>lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a<GOAL>IsFreeGroup G
<VAR>G : Type u<VAR>Group G<VAR>X : Type u<VAR>of : X → G<VAR>h : ∀ {H : Type u} [inst : Group H] (f : X → H), ∃! F, ∀ (a : X), F (of a) = f a<GOAL>IsFreeGroup G
<VAR>G : Type u_1<VAR>Group G<VAR>IsFreeGroup G<VAR>H : Type u_2<VAR>Group H<VAR>e : G ≃* H<GOAL>IsFreeGroup H
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>self : Sylow p G<GOAL>IsPGroup p ↥↑self
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>self : Sylow p G<VAR>Q : Subgroup G<GOAL>IsPGroup p ↥Q → ↑self ≤ Q → Q = ↑self
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P Q : Sylow p G<VAR>h : ↑P = ↑Q<GOAL>P = Q
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P Q : Sylow p G<GOAL>P = Q ↔ ↑P = ↑Q
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P : Sylow p G<VAR>K : Type u_2<VAR>Group K<VAR>ϕ : K →* G<VAR>hϕ : IsPGroup p ↥ϕ.ker<VAR>h : ↑P ≤ ϕ.range<GOAL>↑(P.comapOfKerIsPGroup ϕ hϕ h) = Subgroup.comap ϕ ↑P
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P : Sylow p G<VAR>K : Type u_2<VAR>Group K<VAR>ϕ : K →* G<VAR>hϕ : Function.Injective ⇑ϕ<VAR>h : ↑P ≤ ϕ.range<GOAL>↑(P.comapOfInjective ϕ hϕ h) = Subgroup.comap ϕ ↑P
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P : Sylow p G<VAR>N : Subgroup G<VAR>h : ↑P ≤ N<GOAL>↑(P.subtype h) = (↑P).subgroupOf N
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>N : Subgroup G<VAR>P Q : Sylow p G<VAR>hP : ↑P ≤ N<VAR>hQ : ↑Q ≤ N<VAR>h : P.subtype hP = Q.subtype hQ<GOAL>P = Q
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P : Subgroup G<VAR>hP : IsPGroup p ↥P<GOAL>∃ Q, P ≤ ↑Q
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>P : Sylow p H<VAR>f : H →* G<VAR>hf : IsPGroup p ↥f.ker<GOAL>∃ Q, Subgroup.comap f ↑Q = ↑P
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>P : Sylow p H<VAR>f : H →* G<VAR>hf : Function.Injective ⇑f<GOAL>∃ Q, Subgroup.comap f ↑Q = ↑P
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>P : Sylow p ↥H<GOAL>∃ Q, Subgroup.comap H.subtype ↑Q = ↑P
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>f : H →* G<VAR>hf : IsPGroup p ↥f.ker<VAR>Finite (Sylow p G)<GOAL>Finite (Sylow p H)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>f : H →* G<VAR>hf : Function.Injective ⇑f<VAR>Finite (Sylow p G)<GOAL>Finite (Sylow p H)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>α : Type u_2<VAR>Group α<VAR>MulDistribMulAction α G<VAR>g : α<VAR>P : Sylow p G<GOAL>↑(g • P) = g • ↑P
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>P : Sylow p G<GOAL>g • P = MulAut.conj g • P
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>P : Sylow p G<GOAL>↑(g • P) = MulAut.conj g • ↑P
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P : Sylow p G<VAR>H : Subgroup G<VAR>hP : ↑P ≤ H<VAR>h : ↥H<GOAL>↑(h • P) ≤ H
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P : Sylow p G<VAR>H : Subgroup G<VAR>hP : ↑P ≤ H<VAR>h : ↥H<GOAL>h • P.subtype hP = (h • P).subtype ⋯
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>P : Sylow p G<GOAL>g • P = P ↔ g ∈ (↑P).normalizer
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>P : Sylow p G<VAR>h : (↑P).Normal<GOAL>g • P = P
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>P : Sylow p G<GOAL>P ∈ MulAction.fixedPoints (↥H) (Sylow p G) ↔ H ≤ (↑P).normalizer
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P : Subgroup G<VAR>hP : IsPGroup p ↥P<VAR>Q : Sylow p G<GOAL>P ⊓ (↑Q).normalizer = P ⊓ ↑Q
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P : Subgroup G<VAR>hP : IsPGroup p ↥P<VAR>Q : Sylow p G<GOAL>Q ∈ MulAction.fixedPoints (↥P) (Sylow p G) ↔ P ≤ ↑Q
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<GOAL>Nat.card (Sylow p G) ≡ 1 [MOD p]
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hp : Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<GOAL>¬p ∣ Nat.card (Sylow p G)
<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>MulAction.orbit G P = ⊤
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>P : Sylow p G<GOAL>MulAction.stabilizer G P = (↑P).normalizer
<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<VAR>x g : G<VAR>hx : x ∈ Subgroup.centralizer ↑P<VAR>hy : g⁻¹ * x * g ∈ Subgroup.centralizer ↑P<GOAL>∃ n ∈ (↑P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
<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<VAR>_hP : (↑P).IsCommutative<VAR>x g : G<VAR>hx : x ∈ P<VAR>hy : g⁻¹ * x * g ∈ P<GOAL>∃ n ∈ (↑P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
<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) = Nat.card (G ⧸ (↑P).normalizer)
<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).normalizer.index