mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instCoeDerivationContMDiffMapModelWithCornersSelfSomeENatTop : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] →
                        [inst_7 : ContMDiffMul I (↑⊤) G] →
                          Coe (LeftInvariantDerivation I G)
                            (Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
                              (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤))
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The scalar action via `Mul.toSMul` is transformed by the same map as the elements
of the matrix, when `f` preserves multiplication.  -/
Matrix.map_smul' : ∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : Mul α] [inst_1 : Mul β] (f : α → β) (r : α) (A : Matrix n n α),
  (∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) → (r • A).map f = f r • A.map f
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.toMeasure_injective : ∀ {α : Type u_2}, Function.Injective MeasureTheory.LevyProkhorov.toMeasure
-- Mathlib.Geometry.Manifold.Immersion
/-- `f : M → N` is a `C^n` immersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
around `x` and `f x`, respectively such that in these charts, `f` looks like `u ↦ (u, 0)`.
Additionally, we demand that `f` map `φ.source` into `ψ.source`.

NB. We don't know the particular atlases used for `M` and `N`, so asking for `φ` and `ψ` to be
in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficient.

This definition has a fixed parameter `F`, which is a choice of complement of `E` in `E'`:
being an immersion at `x` includes a choice of linear isomorphism between `E × F` and `E'`.
While the particular choice of complement is often not important, choosing a complement is useful
in some settings, such as proving that embedded submanifolds are locally given either by an
immersion or a submersion.
Unless you have a particular reason, prefer to use `IsImmersionAt` instead.
 -/
Manifold.IsImmersionAtOfComplement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        (F : Type u_5) →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              ModelWithCorners 𝕜 E H →
                                ModelWithCorners 𝕜 E'' G →
                                  {M : Type u_11} →
                                    [inst : TopologicalSpace M] →
                                      [ChartedSpace H M] →
                                        {N : Type u_13} →
                                          [inst : TopologicalSpace N] →
                                            [ChartedSpace G N] → WithTop ℕ∞ → (M → N) → M → Prop
-- Mathlib.Computability.TuringMachine.Computable
/-- A proof that the identity map on α is computable.  -/
Turing.idComputable : {α αΓ : Type} → [Fintype αΓ] → (ea : α → List αΓ) → Turing.TM2Computable ea ea id
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableWithinAt_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E},
  t ∈ nhds x → (DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x)
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- An element `x` is a conjugate root of some element `algebraMap R S r` in the image of the base ring
if and only if `x = algebraMap R S r`.
 -/
isConjRoot_iff_eq_algebraMap : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] [IsDomain S] {r : K}
  {x : S}, IsConjRoot K ((algebraMap K S) r) x ↔ x = (algebraMap K S) r
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.addRight.eq_1 : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Add X] [inst_2 : SeparatelyContinuousAdd X] (x : X),
  ContinuousMap.addRight x = { toFun := fun x_1 => x_1 + x, continuous_toFun := ⋯ }
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.graph.instSubsingleton : ∀ {n : ℕ}, Subsingleton (FirstOrder.Language.graph.Relations n)
-- Mathlib.Algebra.Group.AddChar
AddChar.toAddMonoidHomEquiv_symm_zero : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M], AddChar.toAddMonoidHomEquiv.symm 0 = 0
-- Init.Data.String.Iterate
/-- Creates an iterator over the valid positions within `s`, starting at `p`.
 -/
String.positionsFrom : (s : String) → s.Pos → Std.Iter { p // p ≠ s.endPos }
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x) (n : ℤ),
  a = Lean.Grind.CommRing.Expr.intCast n →
    (match a with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.intCast n => h_2 n
      | Lean.Grind.CommRing.Expr.natCast n => h_3 n
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | x => h_5 x) ≍
      h_2 n
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₄.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₀ app₀_1 : f.obj' 0 _proof_361✝ ⟶ g.obj' 0 _proof_361✝) (e_app₀ : app₀ = app₀_1)
  (app₁ app₁_1 : f.obj' 1 _proof_362✝ ⟶ g.obj' 1 _proof_362✝) (e_app₁ : app₁ = app₁_1)
  (app₂ app₂_1 : f.obj' 2 _proof_363✝ ⟶ g.obj' 2 _proof_363✝) (e_app₂ : app₂ = app₂_1)
  (app₃ app₃_1 : f.obj' 3 _proof_364✝ ⟶ g.obj' 3 _proof_364✝) (e_app₃ : app₃ = app₃_1)
  (app₄ app₄_1 : f.obj' 4 _proof_365✝ ⟶ g.obj' 4 _proof_365✝) (e_app₄ : app₄ = app₄_1)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝) app₁ =
      CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂ =
      CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_363✝))
  (w₂ :
    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃ =
      CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_364✝))
  (w₃ :
    CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄ =
      CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_365✝)),
  CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃ =
    CategoryTheory.ComposableArrows.homMk₄ app₀_1 app₁_1 app₂_1 app₃_1 app₄_1 ⋯ ⋯ ⋯ ⋯
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_apply_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P), ((signedDist v) p) q = inner ℝ (NormedSpace.normalize v) (q -ᵥ p)
-- Mathlib.Topology.Homotopy.HSpaces
HSpace.mk : {X : Type u} →
  [inst : TopologicalSpace X] →
    (hmul : C(X × X, X)) →
      (e : X) →
        hmul (e, e) = e →
          (hmul.comp ((ContinuousMap.const X e).prodMk (ContinuousMap.id X))).HomotopyRel (ContinuousMap.id X) {e} →
            (hmul.comp ((ContinuousMap.id X).prodMk (ContinuousMap.const X e))).HomotopyRel (ContinuousMap.id X) {e} →
              HSpace X
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.mk : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      (toDiagram : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) →
        (top : J) →
          toDiagram.IsTerminal top →
            (∀ (j : J) (hj : toDiagram.IsTerminal j), j = top) →
              CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- Convert a `PreAbstractSimplicialComplex` satisfying `IsAbstract` to an
`AbstractSimplicialComplex`.  -/
PreAbstractSimplicialComplex.toAbstractSimplicialComplex : (ι : Type u_1) → (K : PreAbstractSimplicialComplex ι) → (∀ (v : ι), {v} ∈ K.faces) → AbstractSimplicialComplex ι
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coe_fst_eventuallyEq_proj' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z},
  proj x ∈ e.baseSet → Prod.fst ∘ ↑e =ᶠ[nhds x] proj
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.refl.injEq : ∀ (s s_1 : Lean.Grind.AC.Seq),
  (Lean.Meta.Grind.AC.EqCnstrProof.refl s = Lean.Meta.Grind.AC.EqCnstrProof.refl s_1) = (s = s_1)
-- Mathlib.Order.Max
instNoTopOrderOfNoMaxOrder : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α], NoTopOrder α
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.withConstants_relMap_sumInl : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] {α : Type w'} [inst_1 : (L.withConstants α).Structure M]
  [(L.lhomWithConstants α).IsExpansionOn M] {n : ℕ} {R : L.Relations n} {x : Fin n → M},
  FirstOrder.Language.Structure.RelMap (Sum.inl R) x = FirstOrder.Language.Structure.RelMap R x
-- Init.Data.Order.Lemmas
Std.instMaxEqOrOfIsLinearOrderOfLawfulOrderSup : ∀ {α : Type u} [inst : LE α] [inst_1 : Max α] [Std.IsLinearOrder α] [Std.LawfulOrderSup α], Std.MaxEqOr α
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.smul_X_eq_monomial : ∀ {R : Type u_1} [inst : Semiring R] {a : R} {n : ℕ} [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  a • SkewPolynomial.X ^ n = (SkewPolynomial.monomial n) a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {k k' fallback : α} {f : β k → β k},
  (m.modify k f).getKeyD k' fallback = if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β},
  (t.insert k v).minKey! = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.Order.Sublattice
Sublattice.top_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L : Sublattice β),
  ⊤.prod L = Sublattice.comap LatticeHom.snd L
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.ιMapObj.congr_simp : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p] (i : I) (j : J) (hij : p i = j),
  X.ιMapObj p i j hij = X.ιMapObj p i j hij
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_one : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : MulZeroOneClass α] [inst_1 : DecidableEq n]
  (A : Matrix l m α), Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A 1 = Matrix.blockDiagonal fun x => A
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.toListModel_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option β → Option β},
      (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.Const.alter m a f)).buckets).Perm
        (Std.Internal.List.Const.alterKey a f (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density of `A` containing `0` is `1` if and only if `A` is the naturals.  -/
schnirelmannDensity_eq_one_iff_of_zero_mem : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], 0 ∈ A → (schnirelmannDensity A = 1 ↔ A = Set.univ)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a : α}, m.contains a = false → m[a]! = default
-- Lean.HeadIndex
Lean.instBEqHeadIndex : BEq Lean.HeadIndex
-- Mathlib.Order.Filter.CountablyGenerated
Filter.CountableFilterBasis.toFilterBasis : {α : Type u_6} → Filter.CountableFilterBasis α → FilterBasis α
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatTrans_app : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF RF' : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] (τ : F ⟶ F') (X : C),
  CategoryTheory.CategoryStruct.comp (α.app X) ((RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X)) =
    CategoryTheory.CategoryStruct.comp (τ.app X) (α'.app X)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The morphism `⦋1⦌ ⟶ ⦋n⦌` that picks out the arrow `i ⟶ i+1` in `Fin (n+1)`.  -/
SimplexCategory.mkOfSucc : {n : ℕ} → Fin n → ({ len := 1 } ⟶ { len := n })
-- Mathlib.RingTheory.Extension.Generators
/-- The kernel of a presentation.  -/
Algebra.Generators.ker : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Generators R S ι) → Ideal P.Ring
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.fiberEquivGroup_self : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e : ↑(f ⁻¹' {x})),
  (hf.fiberEquivGroup e) e = 1
-- Mathlib.Condensed.Discrete.Characterization
CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone : ∀ (X : CondensedSet)
  (h :
    (S : Profinite) → CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.obj).mapCocone S.asLimitCone.op)),
  CondensedSet.LocallyConstant.functor.essImage X
-- Lean.Meta.Basic
/-- If `foApprox` is set to true, and some `aᵢ` is not a free variable,
then we use first-order unification
```
  ?m a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k
```
reduces to
```
  ?m a_1 ... a_i =?= f
  a_{i+1}        =?= b_1
  ...
  a_{i+k}        =?= b_k
```
 -/
Lean.Meta.Config.foApprox : Lean.Meta.Config → Bool
-- Mathlib.Data.Nat.Pairing
Nat.unpair_zero : Nat.unpair 0 = 0
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_eq_left : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → b ≤ a → b ≠ 0 → a * b = a
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPPiBinderTypes : Lean.Options → Bool
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.comm : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R] (r : R) (x : QuaternionAlgebra R c₁ c₂ c₃), ↑r * x = x * ↑r
-- Init.Data.List.ControlImpl
List.flatMapMTR.loop : {m : Type u → Type v} → [Monad m] → {α : Type w} → {β : Type u} → (α → m (List β)) → List α → List (List β) → m (List β)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Cycle.formPerm_eq_formPerm_iff : ∀ {α : Type u_2} [inst : DecidableEq α] {s s' : Cycle α} {hs : s.Nodup} {hs' : s'.Nodup},
  s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.Subsingleton ∧ s'.Subsingleton
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.uliftFunctor_obj : ∀ (R : Type u) [inst : Ring R] (X : ModuleCat R),
  (ModuleCat.uliftFunctor.{v', v, u} R).obj X = ModuleCat.of R (ULift.{v', v} ↑X)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mem_sub : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α} {a : α}, a ∈ s - t ↔ ∃ x ∈ s, ∃ y ∈ t, x - y = a
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.card_mapSubgroup : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {G' : Type u_3} [inst_1 : Group G'] (e : G ≃* G'),
  Nat.card ↥(e.mapSubgroup H) = Nat.card ↥H
-- Mathlib.Order.Filter.IsBounded
Filter.isCoboundedUnder_ge_mul_of_nonneg : ∀ {α : Type u_1} {ι : Type u_4} [inst : LinearOrder α] [inst_1 : Mul α] [inst_2 : Zero α] [PosMulMono α] [MulPosMono α]
  {f : Filter ι} [f.NeBot] {u v : ι → α},
  0 ≤ᶠ[f] u →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
      0 ≤ᶠ[f] v →
        Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f v → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f (u * v)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.mkOfSucc_homToOrderHom_one : ∀ {n : ℕ} (i : Fin n), (SimplexCategory.Hom.toOrderHom (SimplexCategory.mkOfSucc i)) 1 = i.succ
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mk.inj : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : NonUnitalNonAssocSemiring A} {inst_2 : Module R A}
  {toNonUnitalSubsemiring : NonUnitalSubsemiring A}
  {smul_mem' : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier}
  {toNonUnitalSubsemiring_1 : NonUnitalSubsemiring A}
  {smul_mem'_1 : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring_1.carrier → c • x ∈ toNonUnitalSubsemiring_1.carrier},
  { toNonUnitalSubsemiring := toNonUnitalSubsemiring, smul_mem' := smul_mem' } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, smul_mem' := smul_mem'_1 } →
    toNonUnitalSubsemiring = toNonUnitalSubsemiring_1
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_zero_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a.fdiv b = 0
-- Init.Prelude
/-- The number of distinct values representable by `UInt16`, that is, `2^16 = 65536`.  -/
UInt16.size : ℕ
-- Mathlib.Data.Num.Lemmas
Num.ppred.eq_1 : Num.zero.ppred = none
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_id_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct W Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct W Z] {Z_1 : C} (h : W ⨯ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) g) h)
-- Mathlib.Algebra.Homology.Homotopy
/-- An additive functor takes homotopies to homotopies.  -/
CategoryTheory.Functor.mapHomotopy : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            {W : Type u_2} →
              [inst_2 : CategoryTheory.Category.{v_1, u_2} W] →
                [inst_3 : CategoryTheory.Preadditive W] →
                  (F : CategoryTheory.Functor V W) →
                    [inst_4 : F.Additive] →
                      {f g : C ⟶ D} →
                        Homotopy f g → Homotopy ((F.mapHomologicalComplex c).map f) ((F.mapHomologicalComplex c).map g)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullback_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y Z T : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T),
  CategoryTheory.CategoryStruct.comp (J.overMapPullbackComp A f (CategoryTheory.CategoryStruct.comp g h)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (J.overMapPullbackComp A g h).inv (J.overMapPullback A f))
        (CategoryTheory.CategoryStruct.comp
          ((J.overMapPullback A h).associator (J.overMapPullback A g) (J.overMapPullback A f)).hom
          (CategoryTheory.CategoryStruct.comp ((J.overMapPullback A h).whiskerLeft (J.overMapPullbackComp A f g).hom)
            (J.overMapPullbackComp A (CategoryTheory.CategoryStruct.comp f g) h).hom))) =
    (J.overMapPullbackCongr A ⋯).hom
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- If an initial object `0` exists in a CCC, then `0 ⨯ A ≅ 0`.  -/
CategoryTheory.mulZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A : C} →
        [CategoryTheory.Closed A] →
          [CategoryTheory.BraidedCategory C] →
            {I : C} → CategoryTheory.Limits.IsInitial I → (CategoryTheory.MonoidalCategoryStruct.tensorObj I A ≅ I)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial.eq_2 : ∀ (n n_1 : ℕ), n.ascFactorial n_1.succ = (n + n_1) * n.ascFactorial n_1
-- Mathlib.Algebra.Group.Defs
CancelCommMonoid.toCancelMonoid : (M : Type u) → [CancelCommMonoid M] → CancelMonoid M
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
HomologicalComplex.instProjectiveXObjSingle : ∀ {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : DecidableEq ι] (i j : ι) (P : C) [CategoryTheory.Projective P],
  CategoryTheory.Projective (((HomologicalComplex.single C c i).obj P).X j)
-- Mathlib.Algebra.Free
/-- The head of the element  -/
FreeSemigroup.head : {α : Type u} → FreeSemigroup α → α
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.continuousWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E}, HasFPowerSeriesWithinAt f p s x → ContinuousWithinAt f s x
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `div_lt_iff₀` for a version with multiplication on the other side.  -/
div_lt_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (b / c < a ↔ b < c * a)
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
Submodule.adjoint.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (g : Submodule 𝕜 (E × F)),
  g.adjoint =
    Submodule.map (↑(WithLp.linearEquiv 2 𝕜 (F × E)))
      (Submodule.map (↑((LinearEquiv.skewSwap 𝕜 F E).symm.trans (WithLp.linearEquiv 2 𝕜 (F × E)).symm)) g)ᗮ
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, panicking if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryGE! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a
-- Mathlib.Order.Category.Frm
Frm.inv_hom_apply : ∀ {X Y : Frm} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x