mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorIso_inv_app_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : Cᴹᵒᵖ × Cᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.tensorIso C).inv.app X).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.2.unmop X.1.unmop)
-- Mathlib.Data.Quot
Quotient.eq_iff_equiv : ∀ {α : Sort u_1} {r : Setoid α} {x y : α}, ⟦x⟧ = ⟦y⟧ ↔ x ≈ y
-- Mathlib.Order.CompleteLattice.Defs
OrderDual.instCompleteLattice : {α : Type u_1} → [CompleteLattice α] → CompleteLattice αᵒᵈ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceToUpper : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Mono f]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget C)],
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.const_apply' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] (a : α) (b : β),
  (BoundedContinuousFunction.const α b) a = b
-- Mathlib.Data.Finset.Max
Finset.max_pair : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), {a, b}.max = max ↑a ↑b
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_smulₛₗ : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type v} {β : Type w} [inst : SMul R α]
  [inst_1 : SMul S β] (f : α → β) (σ : R → S) (r : R),
  (∀ (a : α), f (r • a) = σ r • f a) → ∀ (M : Matrix m n α), (r • M).map f = σ r • M.map f
-- Mathlib.Algebra.Module.Submodule.Defs
/-- Reinterpret a `Submodule` as a `SubMulAction`.  -/
Submodule.toSubMulAction : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → SubMulAction R M
-- Init.System.ST
instMonadAttachST : {σ : Type} → MonadAttach (ST σ)
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The unit isomorphism of `equivalence`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso : {A : Type u_1} →
  {A' : Type u_2} →
    {B : Type u_3} →
      {B' : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] →
                {eA : A ≌ A'} →
                  {eB : B ≌ B'} →
                    {e' : A' ≌ B'} →
                      {F : CategoryTheory.Functor A B'} →
                        {G : CategoryTheory.Functor B A} →
                          (eB.functor.comp e'.inverse ≅ G.comp eA.functor) →
                            (eA.functor ≅ F.comp e'.inverse) →
                              (CategoryTheory.Functor.id A ≅ (F.comp eB.inverse).comp G)
-- Mathlib.LinearAlgebra.Dimension.Localization
IsDomain.hasRankNullity : ∀ {R : Type uR} [inst : CommRing R] [IsDomain R], HasRankNullity.{w, uR} R
-- Mathlib.Condensed.Light.TopCatAdjunction
LightCondSet.toTopCatMap_hom_apply : ∀ {X Y : LightCondSet} (f : X ⟶ Y) (a : X.obj.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))),
  (TopCat.Hom.hom (LightCondSet.toTopCatMap f)) a =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op (LightProfinite.of PUnit.{u + 1})))) a
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Homeomorph.setCongr.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} (h : s = t),
  Homeomorph.setCongr h = { toEquiv := Equiv.setCongr h, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivAt_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (x : M × M'),
  HasMFDerivAt% Prod.snd x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
-- Lean.Server.References
Lean.Server.References.mk.inj : ∀ {ileans : Lean.Server.ILeanMap} {workers : Lean.Server.WorkerRefMap} {ileans_1 : Lean.Server.ILeanMap}
  {workers_1 : Lean.Server.WorkerRefMap},
  { ileans := ileans, workers := workers } = { ileans := ileans_1, workers := workers_1 } →
    ileans = ileans_1 ∧ workers = workers_1
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsColimit.isZero_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C}
  {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Limits.IsZero F → CategoryTheory.Limits.IsZero c.pt
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.instCoeFun : {α : Type u_2} → {ι : Type u_3} → CoeFun (Combinatorics.Line α ι) fun x => α → ι → α
-- Mathlib.Algebra.Category.Grp.AB
AddCommGrpCat.HasLimit.lift.eq_1 : ∀ {J : Type w} (f : J → AddCommGrpCat) (s : CategoryTheory.Limits.Fan f),
  AddCommGrpCat.HasLimit.lift f s =
    AddCommGrpCat.ofHom
      { toFun := fun x j => (CategoryTheory.ConcreteCategory.hom (s.π.app { as := j })) x, map_zero' := ⋯,
        map_add' := ⋯ }
-- Std.Sat.AIG.RelabelNat
/-- The map returned by `ofAIG` fulfills the `Inv1` property.
 -/
Std.Sat.AIG.RelabelNat.State.ofAIG.Inv1 : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (aig : Std.Sat.AIG α),
  ∃ n, Std.Sat.AIG.RelabelNat.State.Inv1 n (Std.Sat.AIG.RelabelNat.State.ofAIG aig)
-- Init.Data.Fin.Lemmas
Fin.castLT_castSucc : ∀ {n : ℕ} (a : Fin n) (h : ↑a < n), a.castSucc.castLT h = a
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaPairingExt : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  {x y : (CategoryTheory.yonedaPairing C).obj X}, (∀ (Y : Cᵒᵖ), x.app Y = y.app Y) → x = y
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R},
  q.totalDegree < p.totalDegree → (p + q).totalDegree = p.totalDegree
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.sdiff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → ∀ (X : Set α), M.Indep (I \ X)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- An arbitrary isomorphism from `Multiplicative (ZMod n)` to any cyclic group
of `Nat.card` equal to `n`.
See `zmodMulEquivOfGenerator` for a version which takes an explicit generator.  -/
zmodCyclicMulEquiv : {G : Type u_2} → [inst : Group G] → IsCyclic G → Multiplicative (ZMod (Nat.card G)) ≃* G
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `F' : D ⥤ H` is a left Kan extension of `F : C ⥤ H` along `L : C ⥤ D`, the colimit over `F'`
is isomorphic to the colimit over `F`.  -/
CategoryTheory.Functor.colimitIsoOfIsLeftKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : F ⟶ L.comp F') →
                    [F'.IsLeftKanExtension α] →
                      [inst_4 : CategoryTheory.Limits.HasColimit F] →
                        [inst_5 : CategoryTheory.Limits.HasColimit F'] →
                          CategoryTheory.Limits.colimit F' ≅ CategoryTheory.Limits.colimit F
-- Mathlib.Data.Nat.Count
Nat.exists_of_count_lt_count : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {a b : ℕ}, Nat.count p a < Nat.count p b → ∃ x ∈ Set.Ico a b, p x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, k ∈ m₂ → (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.Scheme.SpecToEquivOfField.eq_1 : ∀ (K : Type u) [inst : Field K] (X : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.SpecToEquivOfField K X =
    {
      toFun := fun f =>
        ⟨f (IsLocalRing.closedPoint ↑(CommRingCat.of K)),
          AlgebraicGeometry.Scheme.descResidueField (AlgebraicGeometry.Scheme.stalkClosedPointTo f)⟩,
      invFun := fun xf =>
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map xf.snd) (X.fromSpecResidueField xf.fst),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.imageSieve_eq_imageSieve : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vC, uD} D]
  (G : CategoryTheory.Functor C D) {U V : C} (f : G.obj U ⟶ G.obj V),
  G.imageSieve f = CategoryTheory.Presheaf.imageSieve (CategoryTheory.yonedaMap G V) f
-- Std.Do.SPred.SPred
/-- Conjunction of a list of stateful predicates. A state satisfies `conjunction env` if it satisfies
all predicates in `env`.
 -/
Std.Do.SPred.conjunction : {σs : List (Type u)} → List (Std.Do.SPred σs) → Std.Do.SPred σs
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.totalSpaceMk_isInducing : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  (b : B), Topology.IsInducing (Bundle.TotalSpace.mk b)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.cyclesMap 0 = 0
-- Mathlib.RingTheory.WittVector.WittPolynomial
/-- `wittPolynomial p R n` is the `n`-th Witt polynomial
with respect to a prime `p` with coefficients in a commutative ring `R`.
It is defined as:

`∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …]`.  -/
Witt.termW : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.ETransform
/-- The **Dyson e-transform**.
Turns `(s, t)` into `(s ∪ e +ᵥ t, t ∩ -e +ᵥ s)`. This reduces the sum of the two sets.  -/
Finset.addDysonETransform : {α : Type u_1} → [DecidableEq α] → [AddCommGroup α] → α → Finset α × Finset α → Finset α × Finset α
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `i` is an isomorphism such that `i.hom ≫ kernel.ι f = l`, then `l` is a kernel of `f`.  -/
CategoryTheory.Limits.kernel.isoKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            {Z : C} →
              (l : Z ⟶ X) →
                (i : Z ≅ CategoryTheory.Limits.kernel f) →
                  (h : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.kernel.ι f) = l) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι l ⋯)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
IsOpen.nullMeasurableSet : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  {μ : MeasureTheory.Measure α}, IsOpen s → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.hasForgetToFinPartOrd : CategoryTheory.HasForget₂ FinBoolAlg FinPartOrd
-- Mathlib.Data.List.Cycle
Cycle.chain_coe_cons : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) (l : List α), Cycle.Chain r ↑(a :: l) ↔ List.IsChain r (a :: (l ++ [a]))
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbit_vadd_subset : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] (m : M) (a : α),
  AddAction.orbit M (m +ᵥ a) ⊆ AddAction.orbit M a
-- Mathlib.Algebra.Category.Grp.Limits
/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)  -/
AddCommGrpCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections] →
        CategoryTheory.Limits.IsLimit (AddCommGrpCat.limitCone F)
-- Mathlib.Topology.ShrinkingLemma
/-- Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk"
to a new closed cover so that each of the new closed sets is contained in the corresponding
original open set. See also `exists_iUnion_eq_closure_subset` for a stronger statement.  -/
exists_iUnion_eq_closed_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} [NormalSpace X],
  (∀ (i : ι), IsOpen (u i)) →
    (∀ (x : X), {i | x ∈ u i}.Finite) →
      ⋃ i, u i = Set.univ → ∃ v, Set.iUnion v = Set.univ ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_C : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : CommSemiring R]
  (r : R), (MvPowerSeries.rename f) (MvPowerSeries.C r) = MvPowerSeries.C r
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- We can turn any limit cone over a pair into a bilimit bicone.  -/
CategoryTheory.Limits.biconeIsBilimitOfColimitCoconeOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {J : Type u_1} →
        [Fintype J] →
          {f : J → C} →
            {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} →
              (ht : CategoryTheory.Limits.IsColimit t) → (CategoryTheory.Limits.Bicone.ofColimitCocone ht).IsBilimit
-- Mathlib.Data.List.Sym
List.mem_of_mem_of_mem_sym : ∀ {α : Type u_1} {n : ℕ} {xs : List α} {a : α} {z : Sym α n}, a ∈ z → z ∈ List.sym n xs → a ∈ xs
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_sub : ∀ {α : Type u_1} [inst : Sub α] (a b : αˢʸᵐ), SymAlg.unsym (a - b) = SymAlg.unsym a - SymAlg.unsym b
-- Lean.Util.Recognizers
Lean.Expr.listLit? : Lean.Expr → Option (Lean.Expr × List Lean.Expr)
-- Mathlib.ModelTheory.Semantics
/-- A sentence can be evaluated as true or false in a structure.  -/
FirstOrder.Language.«term_⊨_» : Lean.TrailingParserDescr
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instBool : Lean.Elab.ConfigEval.EvalTerm Bool
-- Mathlib.Data.NNRat.Floor
NNRat.floor_coe : ∀ (q : ℚ≥0), ⌊↑q⌋₊ = ⌊q⌋₊
-- Mathlib.Geometry.Manifold.Complex
/-- A holomorphic function on a compact connected complex manifold is constant.  -/
MDifferentiable.apply_eq_of_compactSpace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {H : Type u_3} [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
  {M : Type u_4} [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I 1 M] [CompactSpace M]
  [PreconnectedSpace M] {f : M → F}, MDiff f → ∀ (a b : M), f a = f b
-- Mathlib.Algebra.GroupWithZero.Invertible
Invertible.ne_zero : ∀ {α : Type u} [inst : MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a], a ≠ 0
-- Init.GrindInstances.Ring.UInt
USize.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Ioo' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Finset.Ioo a b ↔ x < b ∧ a < x
-- Aesop.Builder.Basic
Aesop.PhaseSpec.safe.injEq : ∀ (info info_1 : Aesop.SafeRuleInfo), (Aesop.PhaseSpec.safe info = Aesop.PhaseSpec.safe info_1) = (info = info_1)
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.All.balRight : ∀ {α : Type u_1} {p : α → Prop} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.All p l → p v → RBTree.RBNode.All p r → RBTree.RBNode.All p (l.balRight v r)
-- Mathlib.CategoryTheory.Generator.Abelian
CategoryTheory.Abelian.has_injective_coseparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.EnoughInjectives C] (G : C),
  CategoryTheory.IsSeparator G → ∃ G, CategoryTheory.Injective G ∧ CategoryTheory.IsCoseparator G
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- Part of proving $A_5$ is simple. Shows that the square of any element of $A_5$ with a 3-cycle in
its cycle decomposition is a 3-cycle, so the normal closure of the original element must be
$A_5$.  -/
Equiv.Perm.isThreeCycle_sq_of_three_mem_cycleType_five : ∀ {g : Equiv.Perm (Fin 5)}, 3 ∈ g.cycleType → (g * g).IsThreeCycle
-- Mathlib.Order.CompleteBooleanAlgebra
/-- A frame, aka complete Heyting algebra, is a complete lattice whose `⊓` distributes over `⨆`.  -/
Order.Frame : Type u_1 → Type u_1
-- Init.Conv
/-- * `arg i` traverses into the `i`'th argument of the target. For example if the
  target is `f a b c d` then `arg 1` traverses to `a` and `arg 3` traverses to `c`.
  The index may be negative; `arg -1` traverses into the last argument,
  `arg -2` into the second-to-last argument, and so on.
* `arg @i` is the same as `arg i` but it counts all arguments instead of just the
  explicit arguments.
* `arg 0` traverses into the function. If the target is `f a b c d`, `arg 0` traverses into `f`.  -/
Lean.Parser.Tactic.Conv.arg : Lean.ParserDescr
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
/-- The quasi-isomorphism `(CochainComplex.singleFunctor C 0).obj X ⟶ R.cochainComplex`
in `CochainComplex C ℤ` when `R` is an injective resolution of `X`.  -/
CategoryTheory.InjectiveResolution.ι' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {X : C} →
          (R : CategoryTheory.InjectiveResolution X) → (CochainComplex.singleFunctor C 0).obj X ⟶ R.cochainComplex
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] (s : Finset β) (H : s.Nonempty) (f : β → α),
  s.inf' H f = (s.inf (WithTop.some ∘ f)).untop ⋯
-- Mathlib.RingTheory.Ideal.Nonunits
Submonoid.isUnit_iff_and : ∀ {α : Type u_2} {C : Type u_4} [inst : SetLike C α] [inst_1 : GroupWithZero α] [inst_2 : SubmonoidClass C α] {S : C}
  {a : ↥S}, IsUnit a ↔ ↑a ≠ 0 ∧ (↑a)⁻¹ ∈ S
-- Mathlib.Algebra.Star.Basic
StarMemClass.mk : ∀ {S : Type u_1} {R : Type u_2} [inst : Star R] [inst_1 : SetLike S R],
  (∀ {s : S} {r : R}, r ∈ s → star r ∈ s) → StarMemClass S R
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.mk_le_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} {X : CategoryTheory.Subobject B} {f : A ⟶ B}
  [inst_1 : CategoryTheory.Mono f] (g : A ⟶ CategoryTheory.Subobject.underlying.obj X),
  CategoryTheory.CategoryStruct.comp g X.arrow = f → CategoryTheory.Subobject.mk f ≤ X
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_of_isEmpty : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, m.isEmpty = true → m.getKeyD a fallback = fallback
-- Mathlib.Logic.Equiv.Basic
/-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates.  -/
Equiv.subtypeSubtypeEquivSubtypeInter : {α : Type u} → (p q : α → Prop) → { x // q ↑x } ≃ { x // p x ∧ q x }
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.Γ_preservesLimits : CategoryTheory.Limits.PreservesLimits AlgebraicGeometry.AffineScheme.Γ.rightOp
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.leftUnitor_inv_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : SemimoduleCat R} (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv) m = 1 ⊗ₜ[R] m
-- Lean.Parser.Command
/-- `set_option opt val in e` is like `set_option opt val` but scoped to a single term.
It sets the option `opt` to the value `val` in the term `e`.
 -/
Lean.Parser.Term.set_option : Lean.Parser.Parser
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.ext_iff : ∀ {E : Type u_3} [inst : Group E] {p q : GroupNorm E}, p = q ↔ ∀ (x : E), p x = q x
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiable_prod_module_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_17} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_18} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  (f : M → F₁ × F₂), MDiff f ↔ MDiff (Prod.fst ∘ f) ∧ MDiff (Prod.snd ∘ f)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.utf8DecodeChar?_append_eq_assemble₃ : ∀ {l : List UInt8} {b : ByteArray} (hl : l.length = 3),
  ByteArray.utf8DecodeChar?.parseFirstByte l[0] = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
    (l.toByteArray ++ b).utf8DecodeChar? 0 = ByteArray.utf8DecodeChar?.assemble₃ l[0] l[1] l[2]
-- Init.Data.List.BasicAux
List.get.eq_1 : ∀ {α : Type u} (a : α) (tail : List α) (isLt : 0 < (a :: tail).length), (a :: tail).get ⟨0, isLt⟩ = a
-- Mathlib.Order.Heyting.Basic
Prod.instHNot : {α : Type u_2} → {β : Type u_3} → [HNot α] → [HNot β] → HNot (α × β)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.mem_support_rotate_iff : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} [inst : DecidableEq V] (c : G.Walk v v) (u : V) (h : u ∈ c.support),
  w ∈ (c.rotate u h).support ↔ w ∈ c.support
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.isStrongGenerator_of_isDense : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsDense], (CategoryTheory.ObjectProperty.ofObj F.obj).IsStrongGenerator
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix : Bool →
  Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.DiseqCnstr → Lean.Meta.Grind.AC.DiseqCnstrProof
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedComponent_empty : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α}, ∅.ordConnectedComponent x = ∅
-- Mathlib.Logic.Pairwise
Pairwise.comp_of_injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop},
  Pairwise r → ∀ {f : β → α}, Function.Injective f → Pairwise (Function.onFun r f)
-- Mathlib.Algebra.Category.ModuleCat.Images
/-- The universal property for the image factorisation  -/
ModuleCat.image.lift : {R : Type u} →
  [inst : Ring R] →
    {G H : ModuleCat R} → {f : G ⟶ H} → (F' : CategoryTheory.Limits.MonoFactorisation f) → ModuleCat.image f ⟶ F'.I
-- Mathlib.GroupTheory.Schreier
/-- **Schreier's Lemma**: If `R : Finset G` and `H : AddSubgroup G` are complements
with `0 ∈ R`, and if `G` is generated by `S : Finset G`, then `H` is generated by the `Finset`
  `(R + S).image (fun g ↦ g - (hR.toRightFun g))`.  -/
AddSubgroup.closure_add_image_eq_top' : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [inst_1 : DecidableEq G] {R S : Finset G}
  (hR : AddSubgroup.IsComplement ↑H ↑R),
  0 ∈ R →
    AddSubgroup.closure ↑S = ⊤ → AddSubgroup.closure ↑(Finset.image (fun g => ⟨g + -↑(hR.toRightFun g), ⋯⟩) (R + S)) = ⊤