ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>x y : AddAction.orbitRel.Quotient G α<GOAL>x.orbit = y.orbit ↔ x = y
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>x y : MulAction.orbitRel.Quotient G α<GOAL>x.orbit = y.orbit ↔ x = y
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>H : AddSubgroup G<VAR>a b : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>⟦a⟧ = ⟦b⟧
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>H : Subgroup G<VAR>a b : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>⟦a⟧ = ⟦b⟧
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>H : Subgroup G<VAR>a b : α<VAR>h : Quotient.mk'' a = Quotient.mk'' b<GOAL>Quotient.mk'' a = Quotient.mk'' b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>H : AddSubgroup G<VAR>a b : α<VAR>h : Quotient.mk'' a = Quotient.mk'' b<GOAL>Quotient.mk'' a = Quotient.mk'' b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>x : AddAction.orbitRel.Quotient G α<GOAL>x.orbit.Nonempty
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>x : MulAction.orbitRel.Quotient G α<GOAL>x.orbit.Nonempty
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>x : MulAction.orbitRel.Quotient G α<GOAL>Set.MapsTo (fun x => g • x) x.orbit x.orbit
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>x : AddAction.orbitRel.Quotient G α<GOAL>Set.MapsTo (fun x => g +ᵥ x) x.orbit x.orbit
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>x : MulAction.orbitRel.Quotient G α<VAR>a : ↑x.orbit<GOAL>↑(g • a) = g • ↑a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>x : AddAction.orbitRel.Quotient G α<VAR>a : ↑x.orbit<GOAL>↑(g +ᵥ a) = g +ᵥ ↑a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>H : AddSubgroup G<VAR>x : AddAction.orbitRel.Quotient G α<VAR>a b : ↑x.orbit<GOAL>↑a ∈ AddAction.orbit ↥H ↑b ↔ a ∈ AddAction.orbit (↥H) b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>H : Subgroup G<VAR>x : MulAction.orbitRel.Quotient G α<VAR>a b : ↑x.orbit<GOAL>↑a ∈ MulAction.orbit ↥H ↑b ↔ a ∈ MulAction.orbit (↥H) b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>H : AddSubgroup G<VAR>x : AddAction.orbitRel.Quotient G α<VAR>a b : ↑x.orbit<GOAL>⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>H : Subgroup G<VAR>x : MulAction.orbitRel.Quotient G α<VAR>a b : ↑x.orbit<GOAL>⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>H : AddSubgroup G<VAR>x : AddAction.orbitRel.Quotient G α<VAR>a b : ↑x.orbit<VAR>c : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>↑a ∈ AddAction.orbit (↥H) c ↔ ↑b ∈ AddAction.orbit (↥H) c
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>H : Subgroup G<VAR>x : MulAction.orbitRel.Quotient G α<VAR>a b : ↑x.orbit<VAR>c : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>↑a ∈ MulAction.orbit (↥H) c ↔ ↑b ∈ MulAction.orbit (↥H) c
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MulAction G β<GOAL>MulAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (MulAction.orbitRel G α)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>AddAction G β<GOAL>AddAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (AddAction.orbitRel G α)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MulAction G β<GOAL>MulAction.orbitRel G (α × β) ≤ Setoid.comap Prod.snd (MulAction.orbitRel G β)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>AddAction G β<GOAL>AddAction.orbitRel G (α × β) ≤ Setoid.comap Prod.snd (AddAction.orbitRel G β)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a : α<VAR>g : G<GOAL>g ∈ MulAction.stabilizer G a ↔ g • a = a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a : α<VAR>g : G<GOAL>g ∈ AddAction.stabilizer G a ↔ g +ᵥ a = a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>AddAction G β<VAR>VAdd α β<VAR>VAddAssocClass G α β<VAR>a : α<VAR>b : β<GOAL>AddAction.stabilizer G a ≤ AddAction.stabilizer G (a +ᵥ b)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MulAction G β<VAR>SMul α β<VAR>IsScalarTower G α β<VAR>a : α<VAR>b : β<GOAL>MulAction.stabilizer G a ≤ MulAction.stabilizer G (a • b)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup G<VAR>AddAction G β<VAR>VAdd α β<VAR>VAddCommClass G α β<VAR>a : α<VAR>b : β<GOAL>AddAction.stabilizer G b ≤ AddAction.stabilizer G (a +ᵥ b)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group G<VAR>MulAction G β<VAR>SMul α β<VAR>SMulCommClass G α β<VAR>a : α<VAR>b : β<GOAL>MulAction.stabilizer G b ≤ MulAction.stabilizer G (a • b)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>AddAction G β<VAR>VAdd α β<VAR>VAddAssocClass G α β<VAR>a : α<VAR>b : β<VAR>h : Function.Injective fun x => x +ᵥ b<GOAL>AddAction.stabilizer G (a +ᵥ b) = AddAction.stabilizer G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MulAction G β<VAR>SMul α β<VAR>IsScalarTower G α β<VAR>a : α<VAR>b : β<VAR>h : Function.Injective fun x => x • b<GOAL>MulAction.stabilizer G (a • b) = MulAction.stabilizer G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group G<VAR>MulAction G β<VAR>Group α<VAR>MulAction α β<VAR>SMulCommClass G α β<VAR>a : α<VAR>b : β<GOAL>MulAction.stabilizer G (a • b) = MulAction.stabilizer G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup G<VAR>AddAction G β<VAR>AddGroup α<VAR>AddAction α β<VAR>VAddCommClass G α β<VAR>a : α<VAR>b : β<GOAL>AddAction.stabilizer G (a +ᵥ b) = AddAction.stabilizer G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>Group α<VAR>IsScalarTower G α α<VAR>a b : α<GOAL>MulAction.stabilizer G (a * b) = MulAction.stabilizer G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>AddGroup α<VAR>VAddAssocClass G α α<VAR>a b : α<GOAL>AddAction.stabilizer G (a + b) = AddAction.stabilizer G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>Group α<VAR>SMulCommClass G α α<VAR>a b : α<GOAL>MulAction.stabilizer G (a * b) = MulAction.stabilizer G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>AddGroup α<VAR>VAddCommClass G α α<VAR>a b : α<GOAL>AddAction.stabilizer G (a + b) = AddAction.stabilizer G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>a : α<GOAL>MulAction.stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MulAction.stabilizer G a)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>a : α<GOAL>AddAction.stabilizer G (g +ᵥ a) = AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (AddAction.stabilizer G a)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>S : Set α<VAR>a b : α<GOAL>Equiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) S ↔ (a ∈ S ↔ b ∈ S)
<VAR>G : Type u_1<VAR>Group G<VAR>α : Type u_2<VAR>MulAction G α<VAR>s : Set α<VAR>H : Subgroup G<GOAL>H ≤ MulAction.stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s
<VAR>G : Type u_1<VAR>Group G<VAR>α : Type u_2<VAR>MulAction G α<VAR>s : Set α<VAR>hs : s.Finite<VAR>g : G<GOAL>g ∈ MulAction.stabilizer G s ↔ g • s ⊆ s
<VAR>G : Type u_1<VAR>Group G<VAR>α : Type u_2<VAR>MulAction G α<VAR>s : Set α<VAR>hs : s.Finite<VAR>g : G<GOAL>g ∈ MulAction.stabilizer G s ↔ s ⊆ g • s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype ↥(Equiv.Perm.sumCongrHom α β).range<VAR>Fintype (Equiv.Perm α × Equiv.Perm β)<GOAL>Fintype.card ↥(Equiv.Perm.sumCongrHom α β).range = Fintype.card (Equiv.Perm α × Equiv.Perm β)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>Fintype ↥(Equiv.Perm.sigmaCongrRightHom β).range<VAR>Fintype ((a : α) → Equiv.Perm (β a))<GOAL>Fintype.card ↥(Equiv.Perm.sigmaCongrRightHom β).range = Fintype.card ((a : α) → Equiv.Perm (β a))
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>Fintype ↥(Equiv.Perm.subtypeCongrHom p).range<VAR>Fintype (Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a })<GOAL>Fintype.card ↥(Equiv.Perm.subtypeCongrHom p).range = Fintype.card (Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a })
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>a b : X<GOAL>MulAction.orbit G a = MulAction.orbit G b ∨ Disjoint (MulAction.orbit G a) (MulAction.orbit G b)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<GOAL>(Set.range fun x => MulAction.orbit G x).PairwiseDisjoint id
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<GOAL>Setoid.IsPartition (Set.range fun a => MulAction.orbit G a)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>SMul G X<VAR>B : Set X<GOAL>MulAction.IsBlock G B ↔ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>SMul G X<VAR>B : Set X<GOAL>MulAction.IsBlock G B ↔ ∀ (g g' : G), g • B ∩ g' • B ≠ ∅ → g • B = g' • B
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>SMul G X<VAR>B : Set X<VAR>hfB : MulAction.IsFixedBlock G B<GOAL>MulAction.IsBlock G B
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>SMul G X<GOAL>MulAction.IsBlock G ⊥
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>SMul G X<VAR>a : X<GOAL>MulAction.IsBlock G {a}
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>SMul G X<VAR>B : Set X<VAR>hB : B.Subsingleton<GOAL>MulAction.IsBlock G B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<VAR>hB : MulAction.IsBlock G B<VAR>g : G<GOAL>g • B = B ∨ Disjoint (g • B) B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<GOAL>MulAction.IsBlock G B ↔ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<GOAL>MulAction.IsBlock G B ↔ ∀ (g : G), g • B ∩ B ≠ ∅ → g • B = B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<GOAL>MulAction.IsBlock G B ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<VAR>hB : MulAction.IsBlock G B<VAR>a : X<VAR>g : G<GOAL>a ∈ B → g • a ∈ B → g • B = B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<GOAL>MulAction.IsBlock G B ↔ ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ⊆ B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<VAR>hfB : MulAction.IsInvariantBlock G B<GOAL>MulAction.IsFixedBlock G B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<VAR>hfB : MulAction.IsInvariantBlock G B<GOAL>MulAction.IsBlock G B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>a : X<GOAL>MulAction.IsFixedBlock G (MulAction.orbit G a)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>a : X<GOAL>MulAction.IsBlock G (MulAction.orbit G a)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<GOAL>MulAction.IsFixedBlock G ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<GOAL>MulAction.IsBlock G ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>H : Subgroup G<VAR>B : Set X<VAR>hfB : MulAction.IsBlock G B<GOAL>MulAction.IsBlock (↥H) B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>Group H<VAR>MulAction H Y<VAR>φ : H → G<VAR>j : Y →ₑ[φ] X<VAR>B : Set X<VAR>hB : MulAction.IsBlock G B<GOAL>MulAction.IsBlock H (⇑j ⁻¹' B)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>Group H<VAR>MulAction H Y<VAR>φ : G →* H<VAR>j : X →ₑ[⇑φ] Y<VAR>hφ : Function.Surjective ⇑φ<VAR>hj : Function.Injective ⇑j<VAR>B : Set X<VAR>hB : MulAction.IsBlock G B<GOAL>MulAction.IsBlock H (⇑j '' B)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>C : SubMulAction G X<VAR>B : Set X<VAR>hB : MulAction.IsBlock G B<GOAL>MulAction.IsBlock G (Subtype.val ⁻¹' B)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>C : SubMulAction G X<VAR>B : Set ↥C<GOAL>MulAction.IsBlock G B ↔ MulAction.IsBlock G (Subtype.val '' B)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<GOAL>MulAction.IsBlock G B ↔ MulAction.IsBlock (↥⊤) B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B₁ B₂ : Set X<VAR>h₁ : MulAction.IsBlock G B₁<VAR>h₂ : MulAction.IsBlock G B₂<GOAL>MulAction.IsBlock G (B₁ ∩ B₂)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>ι : Type u_3<VAR>B : ι → Set X<VAR>hB : ∀ (i : ι), MulAction.IsBlock G (B i)<GOAL>MulAction.IsBlock G (⋂ i, B i)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<VAR>H : Subgroup G<VAR>hB : MulAction.IsBlock (↥H) B<VAR>g : G<GOAL>MulAction.IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)) (g • B)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<VAR>g : G<VAR>hB : MulAction.IsBlock G B<GOAL>MulAction.IsBlock G (g • B)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>hGX : MulAction.IsPretransitive G X<VAR>B : Set X<VAR>hB : MulAction.IsBlock G B<VAR>hBe : B.Nonempty<GOAL>MulAction.IsBlockSystem G (Set.range fun g => g • B)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a : X<VAR>g : G<GOAL>g • MulAction.orbit (↥N) a = MulAction.orbit (↥N) (g • a)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>N : Subgroup G<VAR>N.Normal<VAR>a : X<GOAL>MulAction.IsBlock G (MulAction.orbit (↥N) a)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>N : Subgroup G<VAR>N.Normal<GOAL>MulAction.IsBlockSystem G (Set.range fun a => MulAction.orbit (↥N) a)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>H : Subgroup G<VAR>a : X<VAR>hH : MulAction.stabilizer G a ≤ H<GOAL>MulAction.IsBlock G (MulAction.orbit (↥H) a)
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>B : Set X<VAR>hB : MulAction.IsBlock G B<VAR>a : X<VAR>ha : a ∈ B<GOAL>MulAction.stabilizer G a ≤ MulAction.stabilizer G B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>htGX : MulAction.IsPretransitive G X<VAR>B : Set X<VAR>hB : MulAction.IsBlock G B<VAR>a : X<VAR>ha : a ∈ B<GOAL>MulAction.orbit (↥(MulAction.stabilizer G B)) a = B
<VAR>G : Type u_1<VAR>Group G<VAR>X : Type u_2<VAR>MulAction G X<VAR>a : X<VAR>H : Subgroup G<VAR>hH : MulAction.stabilizer G a ≤ H<GOAL>MulAction.stabilizer G (MulAction.orbit (↥H) a) = H
<VAR>α : Type u<VAR>u : (Function.End α)ˣ<GOAL>⇑(Equiv.symm (Equiv.Perm.equivUnitsEnd.symm u)) = ↑u⁻¹
<VAR>α : Type u<VAR>e : Equiv.Perm α<GOAL>∀ (a : α), ↑(Equiv.Perm.equivUnitsEnd e)⁻¹ a = (Equiv.symm e).toFun a
<VAR>α : Type u<VAR>e : Equiv.Perm α<GOAL>∀ (a : α), ↑(Equiv.Perm.equivUnitsEnd e) a = e.toFun a
<VAR>α : Type u<VAR>u : (Function.End α)ˣ<GOAL>⇑(Equiv.Perm.equivUnitsEnd.symm u) = ↑u
<VAR>α : Type u<VAR>G : Type u_1<VAR>Group G<VAR>f : G →* Function.End α<GOAL>∀ (a : G), ⇑(Equiv.symm (f.toHomPerm a)) = ↑(f.toHomUnits a)⁻¹
<VAR>α : Type u<VAR>G : Type u_1<VAR>Group G<VAR>f : G →* Function.End α<GOAL>∀ (a : G), ⇑(f.toHomPerm a) = f a
<VAR>α : Type u<VAR>f g : Equiv.Perm α<VAR>x : α<GOAL>(f * g) x = f (g x)
<VAR>α : Type u<VAR>x : α<GOAL>1 x = x
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>f⁻¹ (f x) = x
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>f (f⁻¹ x) = x
<VAR>α : Type u<GOAL>1 = Equiv.refl α
<VAR>α : Type u<VAR>f g : Equiv.Perm α<GOAL>f * g = Equiv.trans g f
<VAR>α : Type u<VAR>f : Equiv.Perm α<GOAL>f⁻¹ = Equiv.symm f
<VAR>α : Type u<VAR>f g : Equiv.Perm α<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>n : ℕ<GOAL>⇑(f ^ n) = (⇑f)^[n]
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>n : ℕ<GOAL>(⇑f)^[n] = ⇑(f ^ n)
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>x = f⁻¹ y ↔ f x = y
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f⁻¹ x = y ↔ x = f y
<VAR>α : Type u_1<VAR>σ : Equiv.Perm α<VAR>m n : ℤ<VAR>x : α<GOAL>(σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>s : Set α<GOAL>⇑f⁻¹ '' s = ⇑f ⁻¹' s
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>s : Set α<GOAL>⇑f⁻¹ ⁻¹' s = ⇑f '' s
<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>e.trans 1 = e
<VAR>α : Type u<VAR>e : Equiv.Perm α<GOAL>e * Equiv.refl α = e
<VAR>α : Type u<GOAL>Equiv.symm 1 = 1
<VAR>α : Type u<GOAL>(Equiv.refl α)⁻¹ = 1
<VAR>α : Type u_1<VAR>β : Sort u_2<VAR>e : α ≃ β<GOAL>Equiv.trans 1 e = e
<VAR>α : Type u<VAR>e : Equiv.Perm α<GOAL>Equiv.refl α * e = e
<VAR>α : Type u<VAR>e : Equiv.Perm α<GOAL>Equiv.trans e⁻¹ e = 1
<VAR>α : Type u<VAR>e : Equiv.Perm α<GOAL>e * Equiv.symm e = 1
<VAR>α : Type u<VAR>e : Equiv.Perm α<GOAL>Equiv.trans e e⁻¹ = 1
<VAR>α : Type u<VAR>e : Equiv.Perm α<GOAL>Equiv.symm e * e = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Equiv.Perm α<VAR>f : Equiv.Perm β<VAR>g : Equiv.Perm α<VAR>h : Equiv.Perm β<GOAL>e.sumCongr f * g.sumCongr h = (e * g).sumCongr (f * h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Equiv.Perm α<VAR>f : Equiv.Perm β<GOAL>(e.sumCongr f)⁻¹ = e⁻¹.sumCongr f⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Equiv.Perm.sumCongr 1 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : Equiv.Perm α × Equiv.Perm β<GOAL>(Equiv.Perm.sumCongrHom α β) a = a.1.sumCongr a.2
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.Injective ⇑(Equiv.Perm.sumCongrHom α β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>i j : α<GOAL>(Equiv.swap i j).sumCongr 1 = Equiv.swap (Sum.inl i) (Sum.inl j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>i j : β<GOAL>Equiv.Perm.sumCongr 1 (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>F G : (a : α) → Equiv.Perm (β a)<GOAL>Equiv.Perm.sigmaCongrRight F * Equiv.Perm.sigmaCongrRight G = Equiv.Perm.sigmaCongrRight (F * G)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>F : (a : α) → Equiv.Perm (β a)<GOAL>(Equiv.Perm.sigmaCongrRight F)⁻¹ = Equiv.Perm.sigmaCongrRight fun a => (F a)⁻¹
<VAR>α : Type u_1<VAR>β : α → Type u_2<GOAL>Equiv.Perm.sigmaCongrRight 1 = 1
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>F : (a : α) → Equiv.Perm (β a)<GOAL>(Equiv.Perm.sigmaCongrRightHom β) F = Equiv.Perm.sigmaCongrRight F
<VAR>α : Type u_1<VAR>β : α → Type u_2<GOAL>Function.Injective ⇑(Equiv.Perm.sigmaCongrRightHom β)
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>pair : Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a }<GOAL>(Equiv.Perm.subtypeCongrHom p) pair = pair.1.subtypeCongr pair.2
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Function.Injective ⇑(Equiv.Perm.subtypeCongrHom p)
<VAR>α : Type u<VAR>e p : Equiv.Perm α<GOAL>(Equiv.permCongr e) p = e * p * e⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<GOAL>Equiv.Perm.extendDomain 1 f = 1
<VAR>α : Type u<VAR>β : Type v<VAR>e : Equiv.Perm α<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<GOAL>(e.extendDomain f)⁻¹ = e⁻¹.extendDomain f
<VAR>α : Type u<VAR>β : Type v<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>e e' : Equiv.Perm α<GOAL>e.extendDomain f * e'.extendDomain f = (e * e').extendDomain f
<VAR>α : Type u<VAR>β : Type v<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>e : Equiv.Perm α<GOAL>(Equiv.Perm.extendDomainHom f) e = e.extendDomain f
<VAR>α : Type u<VAR>β : Type v<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<GOAL>Function.Injective ⇑(Equiv.Perm.extendDomainHom f)
<VAR>α : Type u<VAR>β : Type v<VAR>p : β → Prop<VAR>DecidablePred p<VAR>e : Equiv.Perm α<VAR>f : α ≃ Subtype p<GOAL>e.extendDomain f = 1 ↔ e = 1
<VAR>α : Type u<VAR>β : Type v<VAR>e : Equiv.Perm α<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>n : ℕ<GOAL>(e ^ n).extendDomain f = e.extendDomain f ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>e : Equiv.Perm α<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>n : ℤ<GOAL>(e ^ n).extendDomain f = e.extendDomain f ^ n
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Equiv.Perm α<VAR>h : ∀ (x : α), p x ↔ p (f x)<VAR>x : { x // p x }<GOAL>(f.subtypePerm h) x = ⟨f ↑x, ⋯⟩
<VAR>α : Type u<VAR>p : α → Prop<VAR>h : ∀ (x : α), p x ↔ p x := ⋯<GOAL>Equiv.Perm.subtypePerm 1 h = 1
<VAR>α : Type u<VAR>p : α → Prop<VAR>f g : Equiv.Perm α<VAR>hf : ∀ (x : α), p x ↔ p (f x)<VAR>hg : ∀ (x : α), p x ↔ p (g x)<GOAL>f.subtypePerm hf * g.subtypePerm hg = (f * g).subtypePerm ⋯
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Equiv.Perm α<GOAL>(∀ (x : α), p x ↔ p (f x)) ↔ ∀ (x : α), p x ↔ p (f⁻¹ x)
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Equiv.Perm α<VAR>hf : ∀ (x : α), p x ↔ p (f⁻¹ x)<GOAL>f⁻¹.subtypePerm hf = (f.subtypePerm ⋯)⁻¹
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Equiv.Perm α<VAR>hf : ∀ (x : α), p x ↔ p (f x)<GOAL>(f.subtypePerm hf)⁻¹ = f⁻¹.subtypePerm ⋯
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Equiv.Perm α<VAR>hf : ∀ (x : α), p x ↔ p (f x)<VAR>n : ℕ<VAR>x : α<GOAL>p x ↔ p ((f ^ n) x)
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Equiv.Perm α<VAR>n : ℕ<VAR>hf : ∀ (x : α), p x ↔ p (f x)<GOAL>f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Equiv.Perm α<VAR>hf : ∀ (x : α), p x ↔ p (f x)<VAR>n : ℤ<VAR>x : α<GOAL>p x ↔ p ((f ^ n) x)
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Equiv.Perm α<VAR>n : ℤ<VAR>hf : ∀ (x : α), p x ↔ p (f x)<GOAL>f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : Equiv.Perm α<VAR>h₁ : ∀ (x : α), p x ↔ p (f x)<VAR>h₂ : ∀ (x : α), f x ≠ x → p x<GOAL>Equiv.Perm.ofSubtype (f.subtypePerm h₁) = f
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>f : Equiv.Perm (Subtype p)<VAR>ha : p a<GOAL>(Equiv.Perm.ofSubtype f) a = ↑(f ⟨a, ha⟩)
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : Equiv.Perm (Subtype p)<VAR>x : Subtype p<GOAL>(Equiv.Perm.ofSubtype f) ↑x = ↑(f x)
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>f : Equiv.Perm (Subtype p)<VAR>ha : ¬p a<GOAL>(Equiv.Perm.ofSubtype f) a = a
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : Equiv.Perm (Subtype p)<VAR>x : α<GOAL>p x ↔ p ((Equiv.Perm.ofSubtype f) x)
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : Equiv.Perm (Subtype p)<GOAL>(Equiv.Perm.ofSubtype f).subtypePerm ⋯ = f
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : Equiv.Perm (Subtype p)<GOAL>↑((Equiv.Perm.subtypeEquivSubtypePerm p) f) = Equiv.Perm.ofSubtype f
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : { f // ∀ (a : α), ¬p a → f a = a }<GOAL>(Equiv.Perm.subtypeEquivSubtypePerm p).symm f = (↑f).subtypePerm ⋯
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>f : Equiv.Perm (Subtype p)<VAR>h : p a<GOAL>↑((Equiv.Perm.subtypeEquivSubtypePerm p).toFun f) a = ↑(f ⟨a, h⟩)
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>f : Equiv.Perm (Subtype p)<VAR>h : ¬p a<GOAL>↑((Equiv.Perm.subtypeEquivSubtypePerm p).toFun f) a = a
<VAR>α : Type u<VAR>DecidableEq α<VAR>x y : α<GOAL>(Equiv.swap x y)⁻¹ = Equiv.swap x y
<VAR>α : Type u<VAR>DecidableEq α<VAR>i j : α<GOAL>Equiv.swap i j * Equiv.swap i j = 1
<VAR>α : Type u<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>Equiv.swap x y * f = f * Equiv.swap (f⁻¹ x) (f⁻¹ y)
<VAR>α : Type u<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>f * Equiv.swap x y = Equiv.swap (f x) (f y) * f
<VAR>α : Type u<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>x y : α<GOAL>Equiv.swap (f x) (f y) = f * Equiv.swap x y * f⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>MulAction (Equiv.Perm α) β<VAR>i j : α<VAR>x : β<GOAL>Equiv.swap i j • Equiv.swap i j • x = x
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>MulAction (Equiv.Perm α) β<VAR>i j : α<GOAL>Function.Involutive fun x => Equiv.swap i j • x
<VAR>α : Type u<VAR>DecidableEq α<VAR>i j : α<VAR>σ : Equiv.Perm α<GOAL>Equiv.swap i j * (Equiv.swap i j * σ) = σ
<VAR>α : Type u<VAR>DecidableEq α<VAR>i j : α<VAR>σ : Equiv.Perm α<GOAL>σ * Equiv.swap i j * Equiv.swap i j = σ
<VAR>α : Type u<VAR>DecidableEq α<VAR>i j : α<GOAL>Function.Involutive fun x => Equiv.swap i j * x
<VAR>α : Type u<VAR>DecidableEq α<VAR>i j : α<GOAL>Function.Involutive fun x => x * Equiv.swap i j
<VAR>α : Type u<VAR>DecidableEq α<VAR>i j : α<GOAL>Equiv.swap i j = 1 ↔ i = j