ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 (List.drop j ω) = List.drop j (cs.rightInvSeq ω)
<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 (List.take j ω) = List.take j (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>ω : List B<VAR>t : W<VAR>ht : t ∈ cs.rightInvSeq ω<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>ω : List B<VAR>t : W<VAR>ht : t ∈ cs.leftInvSeq ω<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>ω : List B<VAR>j : ℕ<GOAL>cs.wordProd ω * (cs.rightInvSeq ω).getD j 1 = cs.wordProd (ω.eraseIdx 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.leftInvSeq ω).getD j 1 * cs.wordProd ω = cs.wordProd (ω.eraseIdx 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>hω : cs.IsReduced ω<VAR>t : W<VAR>ht : t ∈ cs.rightInvSeq ω<GOAL>cs.IsRightInversion (cs.wordProd ω) t
<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>hω : cs.IsReduced ω<VAR>t : W<VAR>ht : t ∈ cs.leftInvSeq ω<GOAL>cs.IsLeftInversion (cs.wordProd ω) t
<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 ω).prod = (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.leftInvSeq ω).prod = (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<VAR>rω : cs.IsReduced ω<GOAL>(cs.rightInvSeq ω).Nodup
<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>rω : cs.IsReduced ω<GOAL>(cs.leftInvSeq ω).Nodup
<VAR>f : Type u₀ → Type u₁<VAR>g : Type (max u₀ v₀) → Type v₁<VAR>ULiftable f g<VAR>α : Type u₀<VAR>x : g (ULift.{v₀, u₀} α)<GOAL>ULiftable.up (ULiftable.down x) = x
<VAR>f : Type u₀ → Type u₁<VAR>g : Type (max u₀ v₀) → Type v₁<VAR>ULiftable f g<VAR>α : Type u₀<VAR>x : f α<GOAL>ULiftable.down (ULiftable.up x) = x
<VAR>G : Type u_1<VAR>Group G<VAR>g₁ g₂ : G<GOAL>⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
<VAR>G : Type u_1<VAR>Group G<VAR>g₁ g₂ : G<GOAL>⁅g₁, g₂⁆ = 1 ↔ Commute g₁ g₂
<VAR>G : Type u_1<VAR>Group G<VAR>g₁ g₂ : G<VAR>h : Commute g₁ g₂<GOAL>⁅g₁, g₂⁆ = 1
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>⁅g, 1⁆ = 1
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>⁅1, g⁆ = 1
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>⁅g, g⁆ = 1
<VAR>G : Type u_1<VAR>Group G<VAR>g₁ g₂ : G<GOAL>⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>F : Type u_3<VAR>Group G<VAR>Group G'<VAR>FunLike F G G'<VAR>MonoidHomClass F G G'<VAR>f : F<VAR>g₁ g₂ : G<GOAL>f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆
<VAR>G : Type u_1<VAR>Group G<VAR>g₁ g₂ g₃ : G<GOAL>g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<GOAL>⁅H₁, H₂⁆ = Subgroup.closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
<VAR>G : Type u_1<VAR>Group G<VAR>g₁ g₂ : G<VAR>H₁ H₂ : Subgroup G<VAR>h₁ : g₁ ∈ H₁<VAR>h₂ : g₂ ∈ H₂<GOAL>⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ H₃ : Subgroup G<GOAL>⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ K₁ K₂ : Subgroup G<VAR>h₁ : H₁ ≤ K₁<VAR>h₂ : H₂ ≤ K₂<GOAL>⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<GOAL>⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ Subgroup.centralizer ↑H₂
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ H₃ : Subgroup G<VAR>h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥<VAR>h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥<GOAL>⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<GOAL>⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<GOAL>⁅H₁, H₂⁆ = ⁅H₂, H₁⁆
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<VAR>H₁.Normal<VAR>H₂.Normal<GOAL>⁅H₁, H₂⁆ = Subgroup.normalClosure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<VAR>h : H₂.Normal<GOAL>⁅H₁, H₂⁆ ≤ H₂
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<VAR>H₁.Normal<GOAL>⁅H₁, H₂⁆ ≤ H₁
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ : Subgroup G<GOAL>⁅⊥, H₁⁆ = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ : Subgroup G<GOAL>⁅H₁, ⊥⁆ = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<VAR>H₁.Normal<VAR>H₂.Normal<GOAL>⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H₁ H₂ : Subgroup G<VAR>f : G →* G'<GOAL>Subgroup.map f ⁅H₁, H₂⁆ = ⁅Subgroup.map f H₁, Subgroup.map f H₂⁆
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H₁ H₂ : Subgroup G<VAR>f : G →* G'<VAR>K₁ K₂ : Subgroup G'<VAR>h₁ : K₁ ≤ Subgroup.map f H₁<VAR>h₂ : K₂ ≤ Subgroup.map f H₂<GOAL>⁅K₁, K₂⁆ ≤ Subgroup.map f ⁅H₁, H₂⁆
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H₁ H₂ : Subgroup G<VAR>K₁ K₂ : Subgroup G'<GOAL>⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
<VAR>η : Type u_4<VAR>Gs : η → Type u_5<VAR>(i : η) → Group (Gs i)<VAR>H K : (i : η) → Subgroup (Gs i)<GOAL>⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ ≤ Subgroup.pi Set.univ fun i => ⁅H i, K i⁆
<VAR>η : Type u_4<VAR>Finite η<VAR>Gs : η → Type u_5<VAR>(i : η) → Group (Gs i)<VAR>H K : (i : η) → Subgroup (Gs i)<GOAL>⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ = Subgroup.pi Set.univ fun i => ⁅H i, K i⁆
<VAR>G : Type u_1<VAR>Group G<GOAL>commutatorSet G = {g | ∃ g₁ g₂, ⁅g₁, g₂⁆ = g}
<VAR>G : Type u_1<VAR>Group G<GOAL>1 ∈ commutatorSet G
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<GOAL>g ∈ commutatorSet G ↔ ∃ g₁ g₂, ⁅g₁, g₂⁆ = g
<VAR>G : Type u_1<VAR>Group G<VAR>g₁ g₂ : G<GOAL>⁅g₁, g₂⁆ ∈ commutatorSet G
<VAR>G : Type u_1<VAR>LinearOrderedAddCommGroup G<VAR>Archimedean G<VAR>H : AddSubgroup G<VAR>a : G<VAR>ha : IsLeast {g | g ∈ H ∧ 0 < g} a<GOAL>H = AddSubgroup.closure {a}
<VAR>G : Type u_1<VAR>LinearOrderedAddCommGroup G<VAR>Archimedean G<VAR>H : AddSubgroup G<VAR>hbot : H ≠ ⊥<VAR>a : G<VAR>h₀ : 0 < a<VAR>hd : Disjoint (↑H) (Set.Ioo 0 a)<GOAL>∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
<VAR>G : Type u_1<VAR>LinearOrderedAddCommGroup G<VAR>Archimedean G<VAR>H : AddSubgroup G<VAR>a : G<VAR>h₀ : 0 < a<VAR>hd : Disjoint (↑H) (Set.Ioo 0 a)<GOAL>∃ b, H = AddSubgroup.closure {b}
<VAR>H : AddSubgroup ℤ<GOAL>∃ a, H = AddSubgroup.closure {a}
<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module ℤ M<VAR>Module.Finite ℤ M<VAR>hM : Module.IsTorsion ℤ M<GOAL>Finite M
<VAR>G : Type u<VAR>AddCommGroup G<VAR>hG : AddGroup.FG G<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))
<VAR>G : Type u<VAR>AddCommGroup G<VAR>Finite G<GOAL>∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>Finite G<GOAL>∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃+ ⨁ (i : ι), ZMod (n i))
<VAR>G : Type u<VAR>AddCommGroup G<VAR>hG' : AddGroup.FG G<VAR>hG : AddMonoid.IsTorsion G<GOAL>Finite G
<VAR>G : Type u<VAR>CommGroup G<VAR>Group.FG G<VAR>hG : Monoid.IsTorsion G<GOAL>Finite G
<VAR>G : Type u_1<VAR>Group G<GOAL>derivedSeries G 0 = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<GOAL>derivedSeries G (n + 1) = ⁅derivedSeries G n, derivedSeries G n⁆
<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<GOAL>(derivedSeries G n).Normal
<VAR>G : Type u_1<VAR>Group G<GOAL>derivedSeries G 1 = commutator G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>n : ℕ<GOAL>Subgroup.map f (derivedSeries G n) ≤ derivedSeries G' n
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>n : ℕ<GOAL>derivedSeries G' n ≤ Subgroup.map f (derivedSeries G n)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>n : ℕ<GOAL>Subgroup.map f (derivedSeries G n) = derivedSeries G' n
<VAR>G : Type u_1<VAR>Group G<VAR>self : IsSolvable G<GOAL>∃ n, derivedSeries G n = ⊥
<VAR>G : Type u_1<VAR>Group G<GOAL>IsSolvable G ↔ ∃ n, derivedSeries G n = ⊥
<VAR>G : Type u_3<VAR>hG : Group G<VAR>h : ∀ (a b : G), a * b = b * a<GOAL>IsSolvable G
<VAR>G : Type u_1<VAR>Group G<VAR>h : ⊤ = ⊥<GOAL>IsSolvable G
<VAR>G : Type u_1<VAR>Group G<VAR>G' : Type u_3<VAR>G'' : Type u_4<VAR>Group G'<VAR>Group G''<VAR>f : G' →* G<VAR>g : G →* G''<VAR>hfg : g.ker ≤ f.range<VAR>hG' : IsSolvable G'<VAR>hG'' : IsSolvable G''<GOAL>IsSolvable G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>hf : Function.Injective ⇑f<VAR>IsSolvable G'<GOAL>IsSolvable G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>IsSolvable G<GOAL>IsSolvable G'
<VAR>G : Type u_1<VAR>Group G<VAR>IsSimpleGroup G<VAR>n : ℕ<GOAL>derivedSeries G n.succ = commutator G
<VAR>G : Type u_1<VAR>Group G<VAR>IsSimpleGroup G<GOAL>(∀ (a b : G), a * b = b * a) ↔ IsSolvable G
<VAR>G : Type u_1<VAR>Group G<VAR>g : G<VAR>h1 : g ≠ 1<VAR>h2 : ∀ (n : ℕ), g ∈ derivedSeries G n<GOAL>¬IsSolvable G
<GOAL>¬IsSolvable (Equiv.Perm (Fin 5))
<VAR>X : Type u_3<VAR>hX : 5 ≤ Cardinal.mk X<GOAL>¬IsSolvable (Equiv.Perm X)
<VAR>α β : Type u<VAR>f : β → α → β<VAR>xs : FreeMonoid α<GOAL>(Monoid.Foldl.ofFreeMonoid f) xs = MulOpposite.op (flip (List.foldl f) (FreeMonoid.toList xs))
<VAR>α β : Type u<VAR>f : α → β → β<VAR>xs : FreeMonoid α<GOAL>∀ (a : β), (Monoid.Foldr.ofFreeMonoid f) xs a = flip (List.foldr f) (FreeMonoid.toList xs) a
<VAR>m : Type u → Type u<VAR>Monad m<VAR>α β : Type u<VAR>LawfulMonad m<VAR>f : β → α → m β<VAR>xs : FreeMonoid α<GOAL>(Monoid.foldlM.ofFreeMonoid f) xs = MulOpposite.op (flip (List.foldlM f) (FreeMonoid.toList xs))
<VAR>m : Type u → Type u<VAR>Monad m<VAR>α β : Type u<VAR>LawfulMonad m<VAR>f : α → β → m β<VAR>xs : FreeMonoid α<GOAL>∀ (a : CategoryTheory.KleisliCat.mk m β), (Monoid.foldrM.ofFreeMonoid f) xs a = flip (List.foldrM f) (FreeMonoid.toList xs) a
<VAR>α β : Type u<VAR>f : α → β<VAR>xs : List α<GOAL>f <$> xs = FreeMonoid.toList ((FreeMonoid.map f) (FreeMonoid.ofList xs))
<VAR>α β : Type u<VAR>f : β → α → β<VAR>xs : FreeMonoid α<VAR>a : β<GOAL>MulOpposite.unop ((Monoid.Foldl.ofFreeMonoid f) xs) a = List.foldl f a (FreeMonoid.toList xs)
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>Monoid α<VAR>Monoid β<VAR>f : α →* β<VAR>g : γ → α<VAR>x : t γ<GOAL>f (Traversable.foldMap g x) = Traversable.foldMap (⇑f ∘ g) x
<VAR>α β : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>Monoid β<VAR>f : FreeMonoid α →* β<VAR>x : t α<GOAL>f (Traversable.foldMap FreeMonoid.of x) = Traversable.foldMap (⇑f ∘ FreeMonoid.of) x
<VAR>α β : Type u<VAR>f : α → β → α<GOAL>⇑(Monoid.Foldl.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.Foldl.mk ∘ flip f
<VAR>α β : Type u<VAR>f : β → α → α<GOAL>⇑(Monoid.Foldr.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.Foldr.mk ∘ f
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β → m α<GOAL>⇑(Monoid.foldlM.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.foldlM.mk ∘ flip f
<VAR>α β : Type u<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>f : β → α → m α<GOAL>⇑(Monoid.foldrM.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.foldrM.mk ∘ f
<VAR>α : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>xs : t α<GOAL>Traversable.toList xs = FreeMonoid.toList (Traversable.foldMap FreeMonoid.of xs)
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>Monoid γ<VAR>f : α → β<VAR>g : β → γ<VAR>xs : t α<GOAL>Traversable.foldMap g (f <$> xs) = Traversable.foldMap (g ∘ f) xs
<VAR>α β : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>f : α → β → α<VAR>xs : t β<VAR>x : α<GOAL>Traversable.foldl f x xs = List.foldl f x (Traversable.toList xs)
<VAR>α β : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>f : α → β → β<VAR>xs : t α<VAR>x : β<GOAL>Traversable.foldr f x xs = List.foldr f x (Traversable.toList xs)
<VAR>α β : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>f : α → β<VAR>xs : t α<GOAL>Traversable.toList (f <$> xs) = f <$> Traversable.toList xs
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>g : β → γ<VAR>f : α → γ → α<VAR>a : α<VAR>l : t β<GOAL>Traversable.foldl f a (g <$> l) = Traversable.foldl (fun x y => f x (g y)) a l
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>g : β → γ<VAR>f : γ → α → α<VAR>a : α<VAR>l : t β<GOAL>Traversable.foldr f a (g <$> l) = Traversable.foldr (f ∘ g) a l
<VAR>α : Type u<VAR>xs : List α<GOAL>Traversable.toList xs = xs
<VAR>α : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>xs : t α<GOAL>Traversable.length xs = (Traversable.toList xs).length
<VAR>α β : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β → m α<VAR>x : α<VAR>xs : t β<GOAL>Traversable.foldlm f x xs = List.foldlM f x (Traversable.toList xs)
<VAR>α β : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β → m β<VAR>x : β<VAR>xs : t α<GOAL>Traversable.foldrm f x xs = List.foldrM f x (Traversable.toList xs)
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>g : β → γ<VAR>f : α → γ → m α<VAR>a : α<VAR>l : t β<GOAL>Traversable.foldlm f a (g <$> l) = Traversable.foldlm (fun x y => f x (g y)) a l
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>g : β → γ<VAR>f : γ → α → m α<VAR>a : α<VAR>l : t β<GOAL>Traversable.foldrm f a (g <$> l) = Traversable.foldrm (f ∘ g) a l
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>a b : N ⋊[φ] G<GOAL>a * b = { left := a.left * (φ a.right) b.left, right := a.right * b.right }
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>a b : N ⋊[φ] G<GOAL>(a * b).left = a.left * (φ a.right) b.left
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>a b : N ⋊[φ] G<GOAL>(a * b).right = a.right * b.right
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<GOAL>SemidirectProduct.left 1 = 1
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<GOAL>SemidirectProduct.right 1 = 1
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>a : N ⋊[φ] G<GOAL>a⁻¹.left = (φ a.right⁻¹) a.left⁻¹
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>a : N ⋊[φ] G<GOAL>a⁻¹.right = a.right⁻¹
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>n : N<GOAL>(SemidirectProduct.inl n).left = n
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>n : N<GOAL>(SemidirectProduct.inl n).right = 1
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<GOAL>Function.Injective ⇑SemidirectProduct.inl
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>n₁ n₂ : N<GOAL>SemidirectProduct.inl n₁ = SemidirectProduct.inl n₂ ↔ n₁ = n₂
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>g : G<GOAL>(SemidirectProduct.inr g).left = 1
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>g : G<GOAL>(SemidirectProduct.inr g).right = g
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<GOAL>Function.Injective ⇑SemidirectProduct.inr
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>g₁ g₂ : G<GOAL>SemidirectProduct.inr g₁ = SemidirectProduct.inr g₂ ↔ g₁ = g₂
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>g : G<VAR>n : N<GOAL>SemidirectProduct.inl ((φ g) n) = SemidirectProduct.inr g * SemidirectProduct.inl n * SemidirectProduct.inr g⁻¹
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>g : G<VAR>n : N<GOAL>SemidirectProduct.inl ((φ g)⁻¹ n) = SemidirectProduct.inr g⁻¹ * SemidirectProduct.inl n * SemidirectProduct.inr g
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>g : G<VAR>n : N<GOAL>{ left := n, right := g } = SemidirectProduct.inl n * SemidirectProduct.inr g
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>x : N ⋊[φ] G<GOAL>SemidirectProduct.inl x.left * SemidirectProduct.inr x.right = x
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<GOAL>⇑SemidirectProduct.rightHom = SemidirectProduct.right
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<GOAL>SemidirectProduct.rightHom.comp SemidirectProduct.inl = 1
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<GOAL>SemidirectProduct.rightHom.comp SemidirectProduct.inr = MonoidHom.id G
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>n : N<GOAL>SemidirectProduct.rightHom (SemidirectProduct.inl n) = 1
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>g : G<GOAL>SemidirectProduct.rightHom (SemidirectProduct.inr g) = g
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<GOAL>Function.Surjective ⇑SemidirectProduct.rightHom
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<GOAL>SemidirectProduct.inl.range = SemidirectProduct.rightHom.ker
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>Group N<VAR>Group G<VAR>Group H<VAR>φ : G →* MulAut N<VAR>f₁ : N →* H<VAR>f₂ : G →* H<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁<VAR>n : N<GOAL>(SemidirectProduct.lift f₁ f₂ h) (SemidirectProduct.inl n) = f₁ n
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>Group N<VAR>Group G<VAR>Group H<VAR>φ : G →* MulAut N<VAR>f₁ : N →* H<VAR>f₂ : G →* H<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁<GOAL>(SemidirectProduct.lift f₁ f₂ h).comp SemidirectProduct.inl = f₁
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>Group N<VAR>Group G<VAR>Group H<VAR>φ : G →* MulAut N<VAR>f₁ : N →* H<VAR>f₂ : G →* H<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁<VAR>g : G<GOAL>(SemidirectProduct.lift f₁ f₂ h) (SemidirectProduct.inr g) = f₂ g
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>Group N<VAR>Group G<VAR>Group H<VAR>φ : G →* MulAut N<VAR>f₁ : N →* H<VAR>f₂ : G →* H<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁<GOAL>(SemidirectProduct.lift f₁ f₂ h).comp SemidirectProduct.inr = f₂
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>Group N<VAR>Group G<VAR>Group H<VAR>φ : G →* MulAut N<VAR>F : N ⋊[φ] G →* H<GOAL>F = SemidirectProduct.lift (F.comp SemidirectProduct.inl) (F.comp SemidirectProduct.inr) ⋯
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>Group N<VAR>Group G<VAR>Group H<VAR>φ : G →* MulAut N<VAR>f g : N ⋊[φ] G →* H<VAR>hl : f.comp SemidirectProduct.inl = g.comp SemidirectProduct.inl<VAR>hr : f.comp SemidirectProduct.inr = g.comp SemidirectProduct.inr<GOAL>f = g
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>N₁ : Type u_4<VAR>G₁ : Type u_5<VAR>Group N₁<VAR>Group G₁<VAR>φ₁ : G₁ →* MulAut N₁<VAR>f₁ : N →* N₁<VAR>f₂ : G →* G₁<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁<VAR>g : N ⋊[φ] G<GOAL>((SemidirectProduct.map f₁ f₂ h) g).left = f₁ g.left
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>N₁ : Type u_4<VAR>G₁ : Type u_5<VAR>Group N₁<VAR>Group G₁<VAR>φ₁ : G₁ →* MulAut N₁<VAR>f₁ : N →* N₁<VAR>f₂ : G →* G₁<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁<VAR>g : N ⋊[φ] G<GOAL>((SemidirectProduct.map f₁ f₂ h) g).right = f₂ g.right
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>N₁ : Type u_4<VAR>G₁ : Type u_5<VAR>Group N₁<VAR>Group G₁<VAR>φ₁ : G₁ →* MulAut N₁<VAR>f₁ : N →* N₁<VAR>f₂ : G →* G₁<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁<GOAL>SemidirectProduct.rightHom.comp (SemidirectProduct.map f₁ f₂ h) = f₂.comp SemidirectProduct.rightHom
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>N₁ : Type u_4<VAR>G₁ : Type u_5<VAR>Group N₁<VAR>Group G₁<VAR>φ₁ : G₁ →* MulAut N₁<VAR>f₁ : N →* N₁<VAR>f₂ : G →* G₁<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁<VAR>n : N<GOAL>(SemidirectProduct.map f₁ f₂ h) (SemidirectProduct.inl n) = SemidirectProduct.inl (f₁ n)
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>N₁ : Type u_4<VAR>G₁ : Type u_5<VAR>Group N₁<VAR>Group G₁<VAR>φ₁ : G₁ →* MulAut N₁<VAR>f₁ : N →* N₁<VAR>f₂ : G →* G₁<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁<GOAL>(SemidirectProduct.map f₁ f₂ h).comp SemidirectProduct.inl = SemidirectProduct.inl.comp f₁
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>N₁ : Type u_4<VAR>G₁ : Type u_5<VAR>Group N₁<VAR>Group G₁<VAR>φ₁ : G₁ →* MulAut N₁<VAR>f₁ : N →* N₁<VAR>f₂ : G →* G₁<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁<VAR>g : G<GOAL>(SemidirectProduct.map f₁ f₂ h) (SemidirectProduct.inr g) = SemidirectProduct.inr (f₂ g)
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>Group N<VAR>Group G<VAR>φ : G →* MulAut N<VAR>N₁ : Type u_4<VAR>G₁ : Type u_5<VAR>Group N₁<VAR>Group G₁<VAR>φ₁ : G₁ →* MulAut N₁<VAR>f₁ : N →* N₁<VAR>f₂ : G →* G₁<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (φ₁ (f₂ g))).comp f₁<GOAL>(SemidirectProduct.map f₁ f₂ h).comp SemidirectProduct.inr = SemidirectProduct.inr.comp f₂
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>self : S.LocalizationMap N<VAR>y : ↥S<GOAL>IsAddUnit ((↑self.toAddMonoidHom).toFun ↑y)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>self : S.LocalizationMap N<VAR>z : N<GOAL>∃ x, z + (↑self.toAddMonoidHom).toFun ↑x.2 = (↑self.toAddMonoidHom).toFun x.1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>self : S.LocalizationMap N<VAR>x y : M<GOAL>(↑self.toAddMonoidHom).toFun x = (↑self.toAddMonoidHom).toFun y → ∃ c, ↑c + x = ↑c + y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>self : S.LocalizationMap N<VAR>y : ↥S<GOAL>IsUnit ((↑self.toMonoidHom).toFun ↑y)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>self : S.LocalizationMap N<VAR>x y : M<GOAL>(↑self.toMonoidHom).toFun x = (↑self.toMonoidHom).toFun y → ∃ c, ↑c * x = ↑c * y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>self : S.LocalizationMap N<VAR>z : N<GOAL>∃ x, z * (↑self.toMonoidHom).toFun ↑x.2 = (↑self.toMonoidHom).toFun x.1
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<GOAL>AddLocalization.r S = AddLocalization.r' S
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<GOAL>Localization.r S = Localization.r' S
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>x y : M × ↥S<GOAL>(Localization.r S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)