mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Strict
strictConvex_univ : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : SMul 𝕜 E], StrictConvex 𝕜 Set.univ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RioSlice : (α : Type u_1) → (α → Type u_2) → [Ord α] → Type (max u_2 u_1)
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.noZeroDivisors : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R], NoZeroDivisors R
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
Equiv.divLeft₀_apply : ∀ {G₀ : Type u_1} [inst : CommGroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x : G₀), (Equiv.divLeft₀ a ha) x = a / x
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.equivYoneda'_inv_hom : ∀ (S : CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u)),
  (CategoryTheory.equivYoneda' S).inv.hom = (CategoryTheory.equivYoneda S.obj ⋯).inv
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.withLoopChecking.go : {m : Type → Type} → [MonadLiftT Lean.MetaM m] → Lean.Elab.Tactic.MkSimpContextResult → Bool → m Unit
-- Init.Data.List.Basic
List.findSome?_cons : ∀ {α : Type u} {β : Type v} {a : α} {as : List α} {f : α → Option β},
  List.findSome? f (a :: as) =
    match f a with
    | some b => some b
    | none => List.findSome? f as
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.instAddCommMonoid.eq_1 : ∀ {α : Type u_1} {f : α → α},
  IterateAddAct.instAddCommMonoid =
    { add := fun m n => { val := m.val + n.val }, add_assoc := ⋯, zero := { val := 0 }, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun n a => { val := n * a.val }, nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.vertex.congr_simp : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X]
  [inst_3 : IsOrderedRing S] [inst_4 : DecidableEq X] (x x_1 : X), x = x_1 → stdSimplex.vertex x = stdSimplex.vertex x_1
-- Mathlib.RingTheory.AdicCompletion.Algebra
Ideal.Quotient.factorPow.congr_simp : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided] {m n : ℕ} (le : n ≤ m),
  Ideal.Quotient.factorPow I le = Ideal.Quotient.factorPow I le
-- Mathlib.Data.Nat.ModEq
/-- The natural number less than `n*m` congruent to `a` mod `n` and `b` mod `m`  -/
Nat.chineseRemainder : {m n : ℕ} → n.Coprime m → (a b : ℕ) → { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] }
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (self : CategoryTheory.PreOneHypercover S)
  ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂),
  CategoryTheory.CategoryStruct.comp (self.p₁ j) (self.f i₁) =
    CategoryTheory.CategoryStruct.comp (self.p₂ j) (self.f i₂)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.fromLeftNeg_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg), ↑(S.fromLeftNeg x) + ↑x = 0
-- Mathlib.Data.Set.Card
Set.ncard_eq_one : ∀ {α : Type u_1} {s : Set α}, s.ncard = 1 ↔ ∃ a, s = {a}
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.instIsZeroApply : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : Nontrivial ↥(LieModule.genWeightSpace M 0)],
  IsZeroApply (LieModule.Weight R L M) L R
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEmbedding.restrict_map : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ : MeasureTheory.Measure α) (s : Set β),
      (MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
-- Mathlib.Data.Nat.Factors
/-- `primeFactorsList` can be constructed inductively by extracting `minFac`, for sufficiently
large `n`.  -/
Nat.primeFactorsList_add_two : ∀ (n : ℕ), (n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.comul_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.Bicategory.whiskerLeft t CategoryTheory.Bicategory.Comonad.comul) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Comonad.comul t)
        (CategoryTheory.Bicategory.associator t t t).hom)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The fork `biprod.fstKernelFork` is indeed a limit.  -/
CategoryTheory.Limits.biprod.isKernelFstKernelFork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.biprod.fstKernelFork X Y)
-- Lean.Expr
Lean.instBEqLiteral.beq : Lean.Literal → Lean.Literal → Bool
-- Lean.Meta.Tactic.Induction
Lean.Meta.InductionSubgoal : Type
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.norm_mul_le : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : FreeGroup α), (x * y).norm ≤ x.norm + y.norm
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Presheaf.restrictedULiftYoneda.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ),
  CategoryTheory.Presheaf.restrictedULiftYoneda A =
    CategoryTheory.uliftYoneda.{w, v₂, u₂}.comp
      ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ ℰᵒᵖ (Type (max w v₂))).obj A.op)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.as_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f],
  (CategoryTheory.Limits.Image.monoFactorisation f).m = CategoryTheory.Limits.image.ι f
-- Lean.Data.LBool
Lean.instInhabitedLBool : Inhabited Lean.LBool
-- Batteries.Lean.IO.Process
/-- Pipe `input` into stdin of the spawned process,
then return `(exitCode, stdout, stdErr)` upon completion.
 -/
IO.Process.runCmdWithInput' : String → Array String → optParam String "" → optParam Bool true → IO IO.Process.Output
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- A weak rank function for a pairing is a function from the type (II) simplices
to a partially ordered type which maps an ancestrality relation between
simplices of the same dimension to a strict inequality.  -/
SSet.Subcomplex.Pairing.WeakRankFunction : {X : SSet} → {A : X.Subcomplex} → A.Pairing → (α : Type v) → [PartialOrder α] → Type (max u v)
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
/-- `πQ` is a cokernel.  -/
CategoryTheory.Triangulated.AbelianSubcategory.isColimitCokernelCofork : {C : Type u_1} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
              [inst_5 : CategoryTheory.Pretriangulated C] →
                [inst_6 : CategoryTheory.Category.{v_2, u_2} A] →
                  {ι : CategoryTheory.Functor A C} →
                    (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)),
                        n < 0 → f = 0) →
                      {X₁ X₂ : A} →
                        {f₁ : X₁ ⟶ X₂} →
                          {X₃ : C} →
                            {f₂ : ι.obj X₂ ⟶ X₃} →
                              {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)} →
                                (hT :
                                    CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈
                                      CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                  {K Q : A} →
                                    {α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} →
                                      {β : X₃ ⟶ ι.obj Q} →
                                        {γ :
                                            ι.obj Q ⟶
                                              (CategoryTheory.shiftFunctor C 1).obj
                                                ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))} →
                                          CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles →
                                            [inst_7 : ι.Full] →
                                              [inst_8 : CategoryTheory.Preadditive A] →
                                                [inst_9 : ι.Faithful] →
                                                  CategoryTheory.Limits.IsColimit
                                                    (CategoryTheory.Limits.CokernelCofork.ofπ
                                                      (CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β) ⋯)
-- Mathlib.Topology.UnitInterval
/-- Helper definition for `convexComb_assoc`, giving one of the coefficients appearing
when we reassociate a convex combination.
 -/
Set.Icc.convexComb_assoc_coeff₁ : ↑unitInterval → ↑unitInterval → ↑unitInterval
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.one_hadamard_eq_diagonal_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroOneClass α] {A : Matrix n n α} {d : n → α},
  Matrix.hadamard 1 A = Matrix.diagonal d ↔ A.diag = d
-- Init.Data.FloatArray.Basic
FloatArray.isEmpty : FloatArray → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_eq_getD_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {fallback : α},
  Std.Internal.List.minKeyD l fallback = (Std.Internal.List.minKey? l).getD fallback
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) (y : Bᵒᵖ),
  ((CategoryTheory.Bicategory.yoneda.obj x).obj y).str = CategoryTheory.Bicategory.homCategory (Opposite.unop y) x
-- Mathlib.CategoryTheory.Square
/-- The map `Square C → Square Cᵒᵖ` which switches `X₁` and `X₃`, but
does not move `X₂` and `X₃`.  -/
CategoryTheory.Square.op : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → CategoryTheory.Square Cᵒᵖ
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsHaarMeasure.nnreal_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] {c : NNReal}, c ≠ 0 → (c • μ).IsHaarMeasure
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_nonpos : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0}, ↑q ≤ 0 ↔ q ≤ 0
-- Mathlib.Order.Hom.Basic
/-- Order homomorphisms are equivalent to relation homomorphisms between `LE` relations.  -/
OrderHom.equivRelHom : (α : Type u_2) →
  (β : Type u_3) →
    [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) ≃ ((fun x1 x2 => x1 ≤ x2) →r fun x1 x2 => x1 ≤ x2)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.lift_symm_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] (f : FreeMonoid α →* M), FreeMonoid.lift.symm f = ⇑f ∘ FreeMonoid.of
-- Mathlib.Topology.Constructions.SumProd
Filter.Eventually.prod_inr_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : Y → Prop} {y : Y},
  (∀ᶠ (x : Y) in nhds y, p x) → ∀ (x : X), ∀ᶠ (x : X × Y) in nhds (x, y), p x.2
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.linearIndependent_cols_of_isUnit : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} [inst_1 : Fintype m] {A : Matrix m m R}
  [inst_2 : DecidableEq m], IsUnit A → LinearIndependent R A.col
-- Lean.Parser.Syntax
Lean.Parser.Command.optNamedName : Lean.Parser.Parser
-- Mathlib.Condensed.Functors
/-- Dot notation for the value of `stoneanToCondensed`.  -/
Stonean.toCondensed : Stonean → CondensedSet
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
/-- If `f` is monotone on `[a, b]`, then `f'` is the limit of `G n` a.e. on `[a, b]`, where each
`G n` is `AEStronglyMeasurable` and the liminf of the lower Lebesgue integral of `‖G n ·‖ₑ` is at
most `f b - f a`.  -/
MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le : ∀ {f : ℝ → ℝ} {a b : ℝ},
  a ≤ b →
    MonotoneOn f (Set.Icc a b) →
      ∃ G,
        (∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b),
            Filter.Tendsto (fun n => G n x) Filter.atTop (nhds (deriv f x))) ∧
          (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (G n) (MeasureTheory.volume.restrict (Set.Icc a b))) ∧
            Filter.liminf (fun n => ∫⁻ (x : ℝ) in Set.Icc a b, ‖G n x‖ₑ) Filter.atTop ≤ ENNReal.ofReal (f b - f a)
-- Mathlib.CategoryTheory.Limits.Pi
/-- A cocone over `F : J ⥤ Π i, C i` has as its components cocones over each of the `F ⋙ Pi.eval C i`.
 -/
CategoryTheory.pi.coconeCompEval : {I : Type v₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type v₁} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          {F : CategoryTheory.Functor J ((i : I) → C i)} →
            CategoryTheory.Limits.Cocone F →
              (i : I) → CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Pi.eval C i))
-- Init.Prelude
/-- Creates an info-less `nullKind` node with the given children, if any.  -/
Lean.mkNullNode : optParam (Array Lean.Syntax) #[] → Lean.Syntax
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mem_trivChange_source : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i j : ι) (p : B × F), p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {s : Set (α × β)},
  MeasurableSet s → (μ.compProd κ) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.LocallyQuasiFinite.of_fiberToSpecResidueField : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (∀ (x : ↥Y), AlgebraicGeometry.LocallyQuasiFinite (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f x)) →
    AlgebraicGeometry.LocallyQuasiFinite f
-- Mathlib.Data.List.TakeDrop
_private.Mathlib.Data.List.TakeDrop.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.sigmaEquiv_apply : ∀ {I : Type u_5} (A : Type u_6) (X : I → Type u_7) [inst : TopologicalSpace A]
  [inst_1 : (i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)),
  (ContinuousMap.sigmaEquiv A X) f = ContinuousMap.sigma f
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : AddZeroClass α] [inst_4 : AddZeroClass β] [inst_5 : AddZeroClass γ] (f : β →+o γ) (g : α →+o β),
  f.comp g = { toAddMonoidHom := f.comp ↑g, monotone' := ⋯ }
-- Mathlib.Order.TypeTags
WithTop.coe : {α : Type u_1} → Coe α (WithTop α)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.getPowFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m Lean.Expr
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `zero_le`. -/
zero_le' : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Zero α] [IsBotZeroClass α] {a : α}, 0 ≤ a
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_neg : ∀ (a b : ℤ), a.tmod (-b) = a.tmod b
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop_eq_wf : ∀ {α : Type u} {n : Type u → Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_5 : Monad n]
  [LawfulMonad n] {γ : Type u} {LargeEnough : α → Prop} {hl : ∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b}
  {upperBound next : α} {hn : LargeEnough next} {acc : γ} (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxc.Iterator α) Id Pl)
  (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (Pl out c))),
  Std.Rxc.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl upperBound acc next hn f =
    Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next hn f
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycleOn_inv : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α}, f⁻¹.IsCycleOn s ↔ f.IsCycleOn s
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instInv : {K : Type u} → [inst : CommRing K] → [IsDomain K] → Inv (RatFunc K)
-- Mathlib.Order.Notation
/-- Set / lattice complement 

Conventions for notations in identifiers:

 * The recommended spelling of `ᶜ` in identifiers is `compl`. -/
«term_ᶜ» : Lean.TrailingParserDescr
-- Mathlib.Data.List.TakeDrop
List.takeD_eq_take : ∀ {α : Type u} {n : ℕ} {l : List α} (a : α), n ≤ l.length → List.takeD n l a = List.take n l
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.insert k).contains k = true
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vec3_dotProduct : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Mul α] (v w : Fin 3 → α), v ⬝ᵥ w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7}
  [inst_3 : CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [inst_4 : CategoryTheory.Category.{v_8, u_8} E']
  (X : CategoryTheory.Functor E E')
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X_1 : C₁) (X_2 : C₂)
  {X_3 Y : C₃} (f : X_3 ⟶ Y),
  ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).obj X_1).obj X_2).map f = X.map (((F.obj X_1).obj X_2).map f)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Negating the first vector passed to `oangle` does not change twice the angle.  -/
Orientation.two_zsmul_oangle_neg_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), 2 • o.oangle (-x) y = 2 • o.oangle x y
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If two groups `H` and `G` act on a topological space `X` such that `G` acts
properly and there exists a group homomorphism `H → G` which is a closed embedding compatible with
the actions, then `H` also acts properly on `X`.  -/
properVAdd_of_isClosedEmbedding : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] {H : Type u_3} [inst_4 : AddGroup H] [inst_5 : AddAction H X]
  [inst_6 : TopologicalSpace H] [ProperVAdd G X] (f : H →+ G),
  Topology.IsClosedEmbedding ⇑f → (∀ (h : H) (x : X), f h +ᵥ x = h +ᵥ x) → ProperVAdd H X
-- Mathlib.Data.Set.Lattice
Set.sInter_pair : ∀ {α : Type u_1} (s t : Set α), ⋂₀ {s, t} = s ∩ t
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.instInhabitedTrySuggestionEntry : Inhabited Lean.Elab.Tactic.Try.TrySuggestionEntry
-- Mathlib.Order.SymmDiff
/-- Notation for bihimp  -/
symmDiff.«term_⇔_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Any additive free group is isomorphic to "the" additive free group.  -/
IsFreeAddGroup.addEquiv_def : ∀ (G : Type u_2) [inst : AddGroup G] [inst_1 : IsFreeAddGroup G], IsFreeAddGroup.addEquiv G = ⋯.some.repr.symm
-- Mathlib.CategoryTheory.Discrete.Basic
/-- Promote an equation between the wrapped terms in `X Y : Discrete α` to a morphism `X ⟶ Y`
in the discrete category.  -/
CategoryTheory.Discrete.eqToHom : {α : Type u₁} → {X Y : CategoryTheory.Discrete α} → X.as = Y.as → (X ⟶ Y)
-- Mathlib.Data.Multiset.Functor
Multiset.id_traverse : ∀ {α : Type u_1} (x : Multiset α), Multiset.traverse pure x = pure x
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.image_compl : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X),
  ⇑h '' sᶜ = (⇑h '' s)ᶜ
-- Init.Data.BitVec.Lemmas
BitVec.or_assoc : ∀ {w : ℕ} (x y z : BitVec w), x ||| y ||| z = x ||| (y ||| z)
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {B : M →ₗ[R] M →ₗ[R] R} {x : M}, IsRegular ((B x) x) → (∀ (y : M), (B x) x ∣ 2 * (B x) y) → B.IsReflective x
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Limits.Cofork.IsColimit.homIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Cofork f g}
  (ht : CategoryTheory.Limits.IsColimit t) (Z : C),
  CategoryTheory.Limits.Cofork.IsColimit.homIso ht Z =
    { toFun := fun k => ⟨CategoryTheory.CategoryStruct.comp t.π k, ⋯⟩,
      invFun := fun h => ↑(CategoryTheory.Limits.Cofork.IsColimit.desc' ht ↑h ⋯), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → {F : CategoryTheory.Pseudofunctor B C} → Inhabited (F.StrongTrans F)
-- Init.Data.SInt.Basic
/-- Computes the absolute value of a 64-bit signed integer.

This function is equivalent to `if a < 0 then -a else a`, so in particular `Int64.minValue` will be
mapped to `Int64.minValue`.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.abs : Int64 → Int64
-- Mathlib.RingTheory.Ideal.Height
/-- For a local ring with finite Krull dimension, a prime ideal has height equal to the Krull
dimension if and only if it is the maximal ideal.  -/
Ideal.height_eq_ringKrullDim_iff : ∀ {R : Type u_1} [inst : CommRing R] [FiniteRingKrullDim R] [inst_2 : IsLocalRing R] {I : Ideal R} [I.IsPrime],
  ↑I.height = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.nestedPRBC : Lean.Elab.Term.Do.ToTerm.Kind
-- Mathlib.Algebra.Group.Subgroup.Finite
MonoidHom.fintypeMrange.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Fintype M] [inst_3 : DecidableEq N]
  (f : M →* N), f.fintypeMrange = Set.fintypeRange ⇑f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_eq_get! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)] {h : a ∈ t}, t.get a h = t.get! a