ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃* P<GOAL>f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃+ P<GOAL>f.addEquivOfLocalizations (f.ofAddEquivOfLocalizations k) = k
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃+ P<VAR>x : N<GOAL>(f.addEquivOfLocalizations (f.ofAddEquivOfLocalizations k)) x = k x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>k : N ≃* P<VAR>x : N<GOAL>(f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k)) x = k x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<GOAL>f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<GOAL>f.ofAddEquivOfLocalizations (AddEquiv.refl N) = f
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : N ≃+ P<VAR>j : P ≃+ Q<GOAL>(f.ofAddEquivOfLocalizations (k.trans j)).toMap = j.toAddMonoidHom.comp (f.ofAddEquivOfLocalizations k).toMap
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : N ≃* P<VAR>j : P ≃* Q<GOAL>(f.ofMulEquivOfLocalizations (k.trans j)).toMap = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMap
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>k : P ≃+ M<VAR>H : AddSubmonoid.map k.toAddMonoidHom T = S<VAR>x : P<GOAL>(f.ofAddEquivOfDom H).toMap x = f.toMap (k x)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>k : P ≃* M<VAR>H : Submonoid.map k.toMonoidHom T = S<VAR>x : P<GOAL>(f.ofMulEquivOfDom H).toMap x = f.toMap (k x)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>k : P ≃+ M<VAR>H : AddSubmonoid.map k.toAddMonoidHom T = S<GOAL>(f.ofAddEquivOfDom H).toMap = f.toMap.comp k.toAddMonoidHom
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>k : P ≃* M<VAR>H : Submonoid.map k.toMonoidHom T = S<GOAL>(f.ofMulEquivOfDom H).toMap = f.toMap.comp k.toMonoidHom
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>k : P ≃+ M<VAR>H : AddSubmonoid.map k.toAddMonoidHom T = S<VAR>x : M<GOAL>(f.ofAddEquivOfDom H).toMap (k.symm x) = f.toMap x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>k : P ≃* M<VAR>H : Submonoid.map k.toMonoidHom T = S<VAR>x : M<GOAL>(f.ofMulEquivOfDom H).toMap (k.symm x) = f.toMap x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>k : M ≃+ P<VAR>H : AddSubmonoid.map k.symm.toAddMonoidHom T = S<VAR>x : M<GOAL>(f.ofAddEquivOfDom H).toMap (k x) = f.toMap x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>k : M ≃* P<VAR>H : Submonoid.map k.symm.toMonoidHom T = S<VAR>x : M<GOAL>(f.ofMulEquivOfDom H).toMap (k x) = f.toMap x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<GOAL>f.ofAddEquivOfDom ⋯ = f
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<GOAL>f.ofMulEquivOfDom ⋯ = f
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃+ P<VAR>H : AddSubmonoid.map j.toAddMonoidHom S = T<VAR>x : N<GOAL>(f.addEquivOfAddEquiv k H) x = (f.map ⋯ k) x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃* P<VAR>H : Submonoid.map j.toMonoidHom S = T<VAR>x : N<GOAL>(f.mulEquivOfMulEquiv k H) x = (f.map ⋯ k) x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃* P<VAR>H : Submonoid.map j.toMonoidHom S = T<GOAL>(f.mulEquivOfMulEquiv k H).toMonoidHom = f.map ⋯ k
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃+ P<VAR>H : AddSubmonoid.map j.toAddMonoidHom S = T<GOAL>(f.addEquivOfAddEquiv k H).toAddMonoidHom = f.map ⋯ k
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃+ P<VAR>H : AddSubmonoid.map j.toAddMonoidHom S = T<VAR>x : M<GOAL>(f.addEquivOfAddEquiv k H) (f.toMap x) = k.toMap (j x)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃* P<VAR>H : Submonoid.map j.toMonoidHom S = T<VAR>x : M<GOAL>(f.mulEquivOfMulEquiv k H) (f.toMap x) = k.toMap (j x)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃+ P<VAR>H : AddSubmonoid.map j.toAddMonoidHom S = T<VAR>x : M<VAR>y : ↥S<GOAL>(f.addEquivOfAddEquiv k H) (f.mk' x y) = k.mk' (j x) ⟨j ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃* P<VAR>H : Submonoid.map j.toMonoidHom S = T<VAR>x : M<VAR>y : ↥S<GOAL>(f.mulEquivOfMulEquiv k H) (f.mk' x y) = k.mk' (j x) ⟨j ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃+ P<VAR>H : AddSubmonoid.map j.toAddMonoidHom S = T<VAR>x : M<GOAL>(f.ofAddEquivOfLocalizations (f.addEquivOfAddEquiv k H)).toMap x = k.toMap (j x)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃* P<VAR>H : Submonoid.map j.toMonoidHom S = T<VAR>x : M<GOAL>(f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMap x = k.toMap (j x)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>P : Type u_3<VAR>CommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃* P<VAR>H : Submonoid.map j.toMonoidHom S = T<GOAL>(f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)).toMap = k.toMap.comp j.toMonoidHom
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>P : Type u_3<VAR>AddCommMonoid P<VAR>f : S.LocalizationMap N<VAR>T : AddSubmonoid P<VAR>Q : Type u_4<VAR>AddCommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>j : M ≃+ P<VAR>H : AddSubmonoid.map j.toAddMonoidHom S = T<GOAL>(f.ofAddEquivOfLocalizations (f.addEquivOfAddEquiv k H)).toMap = k.toMap.comp j.toAddMonoidHom
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>x : M<GOAL>Localization.mk x 1 = (Localization.monoidOf S).toMap x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>x : M<GOAL>AddLocalization.mk x 0 = (AddLocalization.addMonoidOf S).toMap x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>x : M<VAR>y : ↥S<GOAL>AddLocalization.mk x y = (AddLocalization.addMonoidOf S).mk' x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>x : M<VAR>y : ↥S<GOAL>Localization.mk x y = (Localization.monoidOf S).mk' x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<GOAL>Localization.mk = (Localization.monoidOf S).mk'
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<GOAL>AddLocalization.mk = (AddLocalization.addMonoidOf S).mk'
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>p : Sort u<VAR>f : M → ↥S → p<VAR>H : ∀ {a c : M} {b d : ↥S}, (AddLocalization.r S) (a, b) (c, d) → f a b = f c d<VAR>a : M<VAR>b : ↥S<GOAL>((AddLocalization.addMonoidOf S).mk' a b).liftOn f H = f a b
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>p : Sort u<VAR>f : M → ↥S → p<VAR>H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d<VAR>a : M<VAR>b : ↥S<GOAL>((Localization.monoidOf S).mk' a b).liftOn f H = f a b
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>p : Sort u_4<VAR>f : M → ↥S → M → ↥S → p<VAR>H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (AddLocalization.r S) (a, b) (a', b') → (AddLocalization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d'<VAR>a c : M<VAR>b d : ↥S<GOAL>((AddLocalization.addMonoidOf S).mk' a b).liftOn₂ ((AddLocalization.addMonoidOf S).mk' c d) f H = f a b c d
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>p : Sort u_4<VAR>f : M → ↥S → M → ↥S → p<VAR>H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (Localization.r S) (a, b) (a', b') → (Localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d'<VAR>a c : M<VAR>b d : ↥S<GOAL>((Localization.monoidOf S).mk' a b).liftOn₂ ((Localization.monoidOf S).mk' c d) f H = f a b c d
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : Localization S<GOAL>(Localization.mulEquivOfQuotient f) x = ((Localization.monoidOf S).lift ⋯) x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : AddLocalization S<GOAL>(AddLocalization.addEquivOfQuotient f) x = ((AddLocalization.addMonoidOf S).lift ⋯) x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(AddLocalization.addEquivOfQuotient f) ((AddLocalization.addMonoidOf S).mk' x y) = f.mk' x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(Localization.mulEquivOfQuotient f) ((Localization.monoidOf S).mk' x y) = f.mk' x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(Localization.mulEquivOfQuotient f) (Localization.mk x y) = f.mk' x y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(AddLocalization.addEquivOfQuotient f) (AddLocalization.mk x y) = f.mk' x y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<GOAL>(AddLocalization.addEquivOfQuotient f) ((AddLocalization.addMonoidOf S).toMap x) = f.toMap x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<GOAL>(Localization.mulEquivOfQuotient f) ((Localization.monoidOf S).toMap x) = f.toMap x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(AddLocalization.addEquivOfQuotient f).symm (f.mk' x y) = (AddLocalization.addMonoidOf S).mk' x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(Localization.mulEquivOfQuotient f).symm (f.mk' x y) = (Localization.monoidOf S).mk' x y
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(AddLocalization.addEquivOfQuotient f).symm (f.mk' x y) = AddLocalization.mk x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<GOAL>(Localization.mulEquivOfQuotient f).symm (f.mk' x y) = Localization.mk x y
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<GOAL>(Localization.mulEquivOfQuotient f).symm (f.toMap x) = (Localization.monoidOf S).toMap x
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<VAR>x : M<GOAL>(AddLocalization.addEquivOfQuotient f).symm (f.toMap x) = (AddLocalization.addMonoidOf S).toMap x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>x : M<GOAL>Localization.mk = Submonoid.LocalizationMap.mk' (Localization.Away.monoidOf x)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>x : M<GOAL>AddLocalization.mk = AddSubmonoid.LocalizationMap.mk' (AddLocalization.Away.addMonoidOf x)
<VAR>α : Type u_1<VAR>CancelCommMonoid α<VAR>s : Submonoid α<VAR>b : ↥s<GOAL>Function.Injective fun a => Localization.mk a b
<VAR>α : Type u_1<VAR>AddCancelCommMonoid α<VAR>s : AddSubmonoid α<VAR>b : ↥s<GOAL>Function.Injective fun a => AddLocalization.mk a b
<VAR>α : Type u_1<VAR>CancelCommMonoid α<VAR>s : Submonoid α<VAR>a₁ b₁ : α<VAR>a₂ b₂ : ↥s<GOAL>Localization.mk a₁ a₂ = Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
<VAR>α : Type u_1<VAR>AddCancelCommMonoid α<VAR>s : AddSubmonoid α<VAR>a₁ b₁ : α<VAR>a₂ b₂ : ↥s<GOAL>AddLocalization.mk a₁ a₂ = AddLocalization.mk b₁ b₂ ↔ ↑b₂ + a₁ = ↑a₂ + b₁
<VAR>f : Type u₀ → Type u₁<VAR>self : EquivFunctor f<VAR>α : Type u₀<GOAL>EquivFunctor.map (Equiv.refl α) = id
<VAR>f : Type u₀ → Type u₁<VAR>self : EquivFunctor f<VAR>α β γ : Type u₀<VAR>k : α ≃ β<VAR>h : β ≃ γ<GOAL>EquivFunctor.map (k.trans h) = EquivFunctor.map h ∘ EquivFunctor.map k
<VAR>f : Type u₀ → Type u₁<VAR>EquivFunctor f<VAR>α β : Type u₀<VAR>e : α ≃ β<VAR>x : f α<GOAL>(EquivFunctor.mapEquiv f e) x = EquivFunctor.map e x
<VAR>f : Type u₀ → Type u₁<VAR>EquivFunctor f<VAR>α β : Type u₀<VAR>e : α ≃ β<VAR>y : f β<GOAL>(EquivFunctor.mapEquiv f e).symm y = EquivFunctor.map e.symm y
<VAR>f : Type u₀ → Type u₁<VAR>EquivFunctor f<VAR>α : Type u₀<GOAL>EquivFunctor.mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
<VAR>f : Type u₀ → Type u₁<VAR>EquivFunctor f<VAR>α β : Type u₀<VAR>e : α ≃ β<GOAL>(EquivFunctor.mapEquiv f e).symm = EquivFunctor.mapEquiv f e.symm
<VAR>f : Type u₀ → Type u₁<VAR>EquivFunctor f<VAR>α β γ : Type u₀<VAR>ab : α ≃ β<VAR>bc : β ≃ γ<GOAL>(EquivFunctor.mapEquiv f ab).trans (EquivFunctor.mapEquiv f bc) = EquivFunctor.mapEquiv f (ab.trans bc)
<VAR>f : Type u₀ → Type u₁<VAR>Applicative f<VAR>LawfulApplicative f<VAR>α β : Type u₀<VAR>h : ∀ (γ : Type u₀), Function.Injective pure<GOAL>Function.Injective (EquivFunctor.mapEquiv f)
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>self : LawfulBitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α α' β β' γ γ' : Type u<VAR>f : β → F γ<VAR>f' : β' → F γ'<VAR>g : α → G β<VAR>g' : α' → G β'<VAR>x : t α α'<GOAL>bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x = Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>self : LawfulBitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α α' β β' : Type u<VAR>f : α → F β<VAR>f' : α' → F β'<VAR>x : t α α'<GOAL>(fun {α} => η.app α) (bitraverse f f' x) = bitraverse ((fun {α} => η.app α) ∘ f) ((fun {α} => η.app α) ∘ f') x
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>self : LawfulBitraversable t<VAR>α β : Type u<VAR>x : t α β<GOAL>bitraverse pure pure x = pure x
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>self : LawfulBitraversable t<VAR>α α' β β' : Type u<VAR>f : α → β<VAR>f' : α' → β'<VAR>x : t α α'<GOAL>bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>σ.cycleType = Multiset.map (Finset.card ∘ Equiv.Perm.support) σ.cycleFactorsFinset.val
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>s : Finset (Equiv.Perm α)<VAR>h1 : ∀ f ∈ s, f.IsCycle<VAR>h2 : (↑s).Pairwise Equiv.Perm.Disjoint<VAR>h0 : s.noncommProd id ⋯ = σ<GOAL>σ.cycleType = Multiset.map (Finset.card ∘ Equiv.Perm.support) s.val
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>l : List (Equiv.Perm α)<VAR>h0 : l.prod = σ<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Equiv.Perm.Disjoint l<GOAL>σ.cycleType = ↑(List.map (Finset.card ∘ Equiv.Perm.support) l)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>σ.cycleType = 0 ↔ σ = 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<GOAL>Equiv.Perm.cycleType 1 = 0
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>Multiset.card σ.cycleType = 0 ↔ σ = 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>0 < Multiset.card σ.cycleType ↔ σ ≠ 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>n : ℕ<VAR>h : n ∈ σ.cycleType<GOAL>2 ≤ n
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>n : ℕ<VAR>h : n ∈ σ.cycleType<GOAL>1 < n
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>hσ : σ.IsCycle<GOAL>σ.cycleType = ↑[σ.support.card]
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>Multiset.card σ.cycleType = 1 ↔ σ.IsCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<VAR>h : σ.Disjoint τ<GOAL>(σ * τ).cycleType = σ.cycleType + τ.cycleType
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>σ⁻¹.cycleType = σ.cycleType
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<GOAL>(τ * σ * τ⁻¹).cycleType = σ.cycleType
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>σ.cycleType.sum = σ.support.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>Equiv.Perm.sign σ = (Multiset.map (fun n => -(-1) ^ n) σ.cycleType).prod
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<GOAL>Equiv.Perm.sign f = (-1) ^ (f.cycleType.sum + Multiset.card f.cycleType)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>σ.cycleType.lcm = orderOf σ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>n : ℕ<VAR>h : n ∈ σ.cycleType<GOAL>n ∣ orderOf σ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>orderOf (f.cycleOf x) ∣ orderOf f
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>hσ : σ ^ 2 = 1<GOAL>2 ∣ σ.support.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>hσ : Nat.Prime (orderOf σ)<GOAL>∃ n, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>h1 : Nat.Prime (orderOf σ)<VAR>h2 : σ.support.card < 2 * orderOf σ<GOAL>σ.IsCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f g : Equiv.Perm α<VAR>hf : f ∈ g.cycleFactorsFinset<GOAL>f.cycleType ≤ g.cycleType
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f g : Equiv.Perm α<VAR>hf : f ∈ g.cycleFactorsFinset<GOAL>(g * f⁻¹).cycleType = g.cycleType - f.cycleType
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<VAR>h : σ.cycleType = τ.cycleType<GOAL>IsConj σ τ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<GOAL>IsConj σ τ ↔ σ.cycleType = τ.cycleType
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>β : Type u_2<VAR>Fintype β<VAR>DecidableEq β<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g : Equiv.Perm α<GOAL>(g.extendDomain f).cycleType = g.cycleType
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>g : Equiv.Perm (Subtype p)<GOAL>(Equiv.Perm.ofSubtype g).cycleType = g.cycleType
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>n : ℕ<VAR>σ : Equiv.Perm α<GOAL>n ∈ σ.cycleType ↔ ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>n : ℕ<VAR>σ : Equiv.Perm α<VAR>h : n ∈ σ.cycleType<GOAL>n ≤ σ.support.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>n : ℕ<VAR>g : Equiv.Perm α<VAR>hn2 : Fintype.card α < n + 2<VAR>hng : n ∈ g.cycleType<GOAL>g.cycleType = {n}
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>σ : Equiv.Perm α<VAR>hσ : σ ^ p ^ n = 1<GOAL>σ.supportᶜ.card ≡ Fintype.card α [MOD p]
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Function.End α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hf : f ^ p ^ n = 1<GOAL>Fintype.card α ≡ Fintype.card ↑(Function.fixedPoints f) [MOD p]
<VAR>α : Type u_1<VAR>Fintype α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hα : ¬p ∣ Fintype.card α<VAR>σ : Equiv.Perm α<VAR>hσ : σ ^ p ^ n = 1<GOAL>∃ a, σ a = a
<VAR>α : Type u_1<VAR>Fintype α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hα : p ∣ Fintype.card α<VAR>σ : Equiv.Perm α<VAR>hσ : σ ^ p ^ n = 1<VAR>a : α<VAR>ha : σ a = a<GOAL>∃ b, σ b = b ∧ b ≠ a
<VAR>α : Type u_1<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>h1 : Nat.Prime (orderOf σ)<VAR>h2 : Fintype.card α < 2 * orderOf σ<GOAL>σ.IsCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>h1 : Nat.Prime (Fintype.card α)<VAR>h2 : orderOf σ = Fintype.card α<GOAL>σ.IsCycle
<VAR>G : Type u_2<VAR>Group G<VAR>n : ℕ<VAR>v : Mathlib.Vector G n<GOAL>v ∈ Equiv.Perm.vectorsProdEqOne G n ↔ v.toList.prod = 1
<VAR>G : Type u_2<VAR>Group G<GOAL>Equiv.Perm.vectorsProdEqOne G 0 = {Mathlib.Vector.nil}
<VAR>G : Type u_2<VAR>Group G<GOAL>Equiv.Perm.vectorsProdEqOne G 1 = {1 ::ᵥ Mathlib.Vector.nil}
<VAR>G : Type u_2<VAR>Group G<VAR>n : ℕ<VAR>v : Mathlib.Vector G n<GOAL>↑((Equiv.Perm.VectorsProdEqOne.vectorEquiv G n) v) = v.toList.prod⁻¹ ::ᵥ v
<VAR>G : Type u_2<VAR>Group G<VAR>n : ℕ<VAR>v : ↑(Equiv.Perm.vectorsProdEqOne G (n + 1))<GOAL>(Equiv.Perm.VectorsProdEqOne.vectorEquiv G n).symm v = (↑v).tail
<VAR>G : Type u_2<VAR>Group G<VAR>n : ℕ<VAR>Fintype G<GOAL>Fintype.card ↑(Equiv.Perm.vectorsProdEqOne G n) = Fintype.card G ^ (n - 1)
<VAR>G : Type u_2<VAR>Group G<VAR>n : ℕ<VAR>v : ↑(Equiv.Perm.vectorsProdEqOne G n)<GOAL>Equiv.Perm.VectorsProdEqOne.rotate v 0 = v