mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Functor.mapExtAddHom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (e : CategoryTheory.Abelian.Ext X Y n),
  (F.mapExtAddHom X Y n) e = CategoryTheory.Abelian.Ext.mapExactFunctor F e
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_id_mop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
  (CategoryTheory.CategoryStruct.id { unmop := X }).unmop = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.mapHomologicalComplexIso.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.Category.{v', u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F G : CochainComplex C ℤ} (φ : F ⟶ G)
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)],
  CochainComplex.mappingCone.mapHomologicalComplexIso φ H =
    HomologicalComplex.Hom.isoOfComponents (CochainComplex.mappingCone.mapHomologicalComplexXIso φ H) ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (t.insertManyIfNewUnit l)[k]? = if k ∈ t ∨ l.contains k = true then some () else none
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infDist.eq_1 : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α) (s : Set α), Metric.infDist x s = (Metric.infEDist x s).toReal
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.eq_of_mem_ball : ∀ {X : Type u_1} [inst : MetricSpace X] (D : Delone.DeloneSet X) {r : NNReal},
  r ≤ D.packingRadius / 2 → ∀ {x y z : X}, x ∈ D → y ∈ D → x ∈ Metric.ball z ↑r → y ∈ Metric.ball z ↑r → x = y
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.whiskerVertical_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] {T : CategoryTheory.Functor C₁ D₁} {L : CategoryTheory.Functor C₁ C₂}
  {R : CategoryTheory.Functor D₁ D₂} {B : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T L R B)
  {L' : CategoryTheory.Functor C₁ C₂} {R' : CategoryTheory.Functor D₁ D₂} (α : L ⟶ L') (β : R' ⟶ R) (X : C₁),
  (w.whiskerVertical α β).app X =
    CategoryTheory.CategoryStruct.comp (β.app (T.obj X))
      (CategoryTheory.CategoryStruct.comp (w.natTrans.app X) (B.map (α.app X)))
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmoothOfRelativeDimension_localizationPreserves : ∀ (n : ℕ),
  RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension n
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.inl__obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C), (CategoryTheory.Sum.inl_ C D).obj X = Sum.inl X
-- Mathlib.Order.UpperLower.Closure
UpperSet.sdiff_eq_left : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {t : Set α}, s.sdiff t = s ↔ Disjoint (↑s) t
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_enorm_rpow : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] (f : α → ε)
  (p q : ℝ), 0 < q → MeasureTheory.eLpNorm' (fun x => ‖f x‖ₑ ^ q) p μ = MeasureTheory.eLpNorm' f (p * q) μ ^ q
-- Mathlib.Order.ScottContinuity
ScottContinuous.monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, ScottContinuous f → Monotone f
-- Mathlib.RingTheory.Flat.TorsionFree
/-- Scalar multiplication `m ↦ r • m` by a nonzerodivisor `r` is injective on a flat module.  -/
Module.Flat.isSMulRegular_of_nonZeroDivisors : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {r : R},
  r ∈ nonZeroDivisors R → ∀ [Module.Flat R M], IsSMulRegular M r
-- Mathlib.Geometry.Euclidean.Volume.Measure
InnerProductSpace.euclideanHausdorffMeasure_eq_volume : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MeasurableSpace V]
  [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V],
  MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V) = MeasureTheory.volume
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y Z : T}
  [inst_2 : P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [inst_3 : Q.RespectsIso]
  (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g))
  (hfg : autoParam (fg = CategoryTheory.CategoryStruct.comp f g) CategoryTheory.MorphismProperty.Over.mapComp._auto_1)
  (X_1 : P.Over Q X),
  ((CategoryTheory.MorphismProperty.Over.mapComp Q hf hg fg hfg).hom.app X_1).left =
    CategoryTheory.CategoryStruct.id X_1.left
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.invertTrans.go : Lean.Expr → Bool → Option Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Category.CoalgCat.Basic
CategoryTheory.Iso.toCoalgEquiv_refl : ∀ {R : Type u} [inst : CommRing R] {X : CoalgCat R},
  (CategoryTheory.Iso.refl X).toCoalgEquiv = CoalgEquiv.refl R ↑X.toModuleCat
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Extend an ordered partition of `n` entries, by adding a new singleton part to the left.  -/
OrderedFinpartition.extendLeft : {n : ℕ} → OrderedFinpartition n → OrderedFinpartition (n + 1)
-- Init.Data.Int.Order
Int.neg_le_neg_iff : ∀ {a b : ℤ}, -a ≤ -b ↔ b ≤ a
-- Mathlib.Algebra.Torsor.Defs
/-- Point reflection in `x` as a permutation.  -/
Equiv.pointReflection : {G : Type u_3} → {P : Type u_4} → [inst : AddGroup G] → [AddTorsor G P] → P → Equiv.Perm P
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.localInverse_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  HasStrictFDerivAt.localInverse f f' a hf = ↑(HasStrictFDerivAt.toOpenPartialHomeomorph f hf).symm
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
summable_subtype_iff_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {s : Set β},
  Summable (f ∘ Subtype.val) ↔ Summable (s.indicator f)
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- constructor for `Cofix F`  -/
MvQPF.Cofix.mk : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → F (α ::: MvQPF.Cofix F α) → MvQPF.Cofix F α
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux_subset : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) {E₁ E₂ : Set α},
  E₁ ⊆ E₂ → thickenedIndicatorAux δ E₁ ≤ thickenedIndicatorAux δ E₂
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instLocallyConvexSpaceReal : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞}, LocallyConvexSpace ℝ (TestFunction Ω F n)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.comp_id : ∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {E : Type u_9} {F : Type u_10} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (f : E →SWOT[σ₁₂] F),
  (ContinuousLinearMapWOT.id 𝕜₂ F).comp f = f
-- Mathlib.RingTheory.WittVector.Verschiebung
_private.Mathlib.RingTheory.WittVector.Verschiebung.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to
the matrix `J`.  -/
skewAdjointMatricesSubmodule : {R : Type u_1} →
  {n : Type u_11} → [inst : CommRing R] → [Fintype n] → Matrix n n R → [DecidableEq n] → Submodule R (Matrix n n R)
-- Mathlib.LinearAlgebra.PiTensorProduct.Generators
PiTensorProduct.equivPiTensorComplSingletonTensor_tprod : ∀ (R : Type u_1) {ι : Type u_2} [inst : DecidableEq ι] (M : ι → Type u_3) [inst_1 : CommSemiring R]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)] (i₀ : ι) (m : (i : ι) → M i),
  (PiTensorProduct.equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), m i) =
    ((PiTensorProduct.tprod R) fun j => m ↑j) ⊗ₜ[R] m i₀
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Composing two partial equivs, by restricting to the maximal domain where their composition
is well defined.
Within the `Manifold` namespace, there is the notation `e ≫ f` for this.
 -/
PartialEquiv.trans : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → PartialEquiv α β → PartialEquiv β γ → PartialEquiv α γ
-- Mathlib.Order.Defs.Unbundled
IsRelLowerSet.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α) (P : α → Prop),
  IsRelLowerSet s P = ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ s
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker.eq_1 : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] (f : F), RingHom.ker f = Ideal.comap f ⊥
-- Lean.Meta.IndPredBelow
/-- Given a pattern `p`, return an array of variables that bind `p` completely (i.e. variables and
named patterns).
 -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.collectDirectVarsInPattern : Lean.Meta.Match.Pattern → Array Lean.FVarId
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.tilted_mul_apply_cgf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} [MeasureTheory.SFinite μ]
  (s : Set Ω),
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
    (μ.tilted fun x => t * X x) s =
      ∫⁻ (a : Ω) in s, ENNReal.ofReal (Real.exp (t * X a - ProbabilityTheory.cgf X μ t)) ∂μ
-- Init.Data.Option.Lemmas
Option.map_comp_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ), Option.map g ∘ Option.map f = Option.map (g ∘ f)
-- Mathlib.CategoryTheory.Limits.Skeleton
CategoryTheory.Limits.hasColimitsOfSize_skeleton : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} C],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} (CategoryTheory.Skeleton C)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The oriented angle at `p₂` between the line segments to `p₁` and `p₃`, modulo `2 * π`. If
either of those points equals `p₂`, this is 0. See `EuclideanGeometry.angle` for the
corresponding unoriented angle definition.  -/
EuclideanGeometry.«term∡» : Lean.ParserDescr
-- Mathlib.Probability.Moments.CovarianceBilinDual
StrongDual.toLpₗ_of_not_memLp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal}
  {𝕜 : Type u_2} [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedSpace 𝕜 E],
  ¬MeasureTheory.MemLp id p μ → ∀ (L : StrongDual 𝕜 E), (StrongDual.toLpₗ μ p) L = 0
-- Init.Data.Fin.Basic
_private.Init.Data.Fin.Basic.0.Fin.mlt : ∀ {n b a : ℕ}, a < n → b % n < n
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.add.inj : ∀ {a a_1 a_2 a_3 : Mathlib.Tactic.Linarith.CompSource}, a.add a_1 = a_2.add a_3 → a = a_2 ∧ a_1 = a_3
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_emod_unique : ∀ {a b r q : ℤ}, 0 < b → (a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b)
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasDerivAtFilter_sub_const_iff`. -/
HasDerivAtFilter.sub_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} (c : F),
  HasDerivAtFilter f f' L → HasDerivAtFilter (fun x => f x - c) f' L
-- Mathlib.Analysis.Complex.Order
Complex.eq_re_of_ofReal_le : ∀ {r : ℝ} {z : ℂ}, ↑r ≤ z → z = ↑z.re
-- Mathlib.AlgebraicGeometry.Properties
/-- To show that a statement `P` holds for all open subsets of all schemes, it suffices to show that
1. In any scheme `X`, if `P` holds for an open cover of `U`, then `P` holds for `U`.
2. For an open immersion `f : X ⟶ Y`, if `P` holds for the entire space of `X`, then `P` holds for
  the image of `f`.
3. `P` holds for the entire space of an affine scheme.
 -/
AlgebraicGeometry.reduce_to_affine_global : ∀ (P : {X : AlgebraicGeometry.Scheme} → X.Opens → Prop) {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  (∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U) →
    (∀ (X Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
        ∃ U V, U = ⊤ ∧ V = AlgebraicGeometry.Scheme.Hom.opensRange f ∧ (P U → P V)) →
      (∀ (R : CommRingCat), P ⊤) → P U
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Construct an object of the category `(Δ ↓ F)` from a cone on `F`. This is part of an
equivalence, see `Cone.equivCostructuredArrow`.  -/
CategoryTheory.Limits.Cone.toCostructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          CategoryTheory.Functor (CategoryTheory.Limits.Cone F)
            (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F)
-- Mathlib.Topology.LocallyFinsupp
/-- Simplifier lemma: Functions with locally finite support within `U` evaluate to zero outside of `U`.
 -/
Function.locallyFinsuppWithin.apply_eq_zero_of_notMem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] {z : X}
  (D : Function.locallyFinsuppWithin U Y), z ∉ U → D z = 0
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.orthogonal_le_iff_orthogonal_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₀ K₁ : Submodule 𝕜 E} [K₀.HasOrthogonalProjection] [K₁.HasOrthogonalProjection], K₀ᗮ ≤ K₁ ↔ K₁ᗮ ≤ K₀
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_inj : ∀ {α : Type u} [inst : Monoid α] {a b : α} [inst_1 : Invertible a] [inst_2 : Invertible b], ⅟a = ⅟b ↔ a = b
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_MonadExcept : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u_1} {α : Type u} {x : m α} {h : ε → m α}
  [inst : MonadExceptOf ε m] [inst_1 : Std.Do.WP m ps] (Q : Std.Do.PostCond α ps),
  ⦃(Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q⦄ tryCatch x h ⦃Q⦄
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxcHasSize.eq_1 : ISize.instRxcHasSize = { size := fun lo hi => (hi.toInt + 1 - lo.toInt).toNat }
-- Init.Data.String.PosRaw
String.Pos.Raw.ne_zero_of_lt : ∀ {a b : String.Pos.Raw}, a < b → b ≠ 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) (a : B) {Z : F.obj a ⟶ G.obj a}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id a)) (α.app a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.naturality (CategoryTheory.CategoryStruct.id a)).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.mapId a).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (α.app a)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (α.app a)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).inv (α.app a)) h)))
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.bypass.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u : V}, SimpleGraph.Walk.nil.bypass = SimpleGraph.Walk.nil
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminators.mk : Lean.SMap (Bool × Array Lean.Name) Lean.Name → Lean.Meta.CustomEliminators
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- `P.Comma L R Q W` is the subcategory of `Comma L R` consisting of
objects `X : Comma L R` where `X.hom` satisfies `P`. The morphisms are given by
morphisms in `Comma L R` where the left one satisfies `Q` and the right one satisfies `W`.  -/
CategoryTheory.MorphismProperty.Comma : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            CategoryTheory.Functor A T →
              CategoryTheory.Functor B T →
                CategoryTheory.MorphismProperty T →
                  CategoryTheory.MorphismProperty A → CategoryTheory.MorphismProperty B → Type (max (max u_1 u_2) v_3)
-- Mathlib.Order.UpperLower.Closure
bddBelow_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow ↑(upperClosure s) ↔ BddBelow s
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.trunc'_trunc' : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] {n m : σ →₀ ℕ},
  n ≤ m →
    ∀ (φ : MvPowerSeries σ R), (MvPowerSeries.trunc' R n) ↑((MvPowerSeries.trunc' R m) φ) = (MvPowerSeries.trunc' R n) φ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.Supports.eq_def : ∀ (S : Finset Turing.PartrecToTM2.Λ') (x : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.Λ'.Supports S x =
    match x with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => Turing.PartrecToTM2.Λ'.Supports S q
    | Turing.PartrecToTM2.Λ'.push k s q => Turing.PartrecToTM2.Λ'.Supports S q
    | Turing.PartrecToTM2.Λ'.read q => ∀ (s : Option Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.Λ'.Supports S (q s)
    | Turing.PartrecToTM2.Λ'.clear p k q => Turing.PartrecToTM2.Λ'.Supports S q
    | q.copy => Turing.PartrecToTM2.Λ'.Supports S q
    | q.succ => Turing.PartrecToTM2.Λ'.Supports S q
    | q₁.pred q₂ => Turing.PartrecToTM2.Λ'.Supports S q₁ ∧ Turing.PartrecToTM2.Λ'.Supports S q₂
    | Turing.PartrecToTM2.Λ'.ret k => Turing.PartrecToTM2.contSupp k ⊆ S
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.prod_unique : ∀ {M : Type u_4} {ι : Type u_7} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : Unique ι] (f : ι → M),
  ∏ x, f x = f default
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, ¬p.Nil → p.dropLast.support = p.support.dropLast
-- Mathlib.Topology.Sheaves.Presheaf
/-- Pullback a presheaf on `Y` along a continuous map `f : X ⟶ Y`, obtaining a presheaf
on `X`.  -/
TopCat.Presheaf.pullback : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} → (X ⟶ Y) → CategoryTheory.Functor (TopCat.Presheaf C Y) (TopCat.Presheaf C X)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivWithinAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] {f : E → F} {f' : E →L[𝕜] F} {f₂ : G → G'} {f₂' : G →L[𝕜] G'} (p : E × G)
  {s : Set (E × G)},
  HasFDerivWithinAt f f' (Prod.fst '' s) p.1 →
    HasFDerivWithinAt f₂ f₂' (Prod.snd '' s) p.2 → HasFDerivWithinAt (Prod.map f f₂) (f'.prodMap f₂') s p
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.integrable_stoppedValue : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [inst_2 : LE E] {f : ℕ → Ω → E},
  MeasureTheory.Submartingale f 𝒢 μ →
    ∀ {τ : Ω → ℕ∞},
      MeasureTheory.IsStoppingTime 𝒢 τ →
        ∀ {N : ℕ}, (∀ (ω : Ω), τ ω ≤ ↑N) → MeasureTheory.Integrable (MeasureTheory.stoppedValue f τ) μ
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_ofSnowflaking_closedEBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  (d : ENNReal),
  ⇑Metric.Snowflaking.ofSnowflaking '' Metric.closedEBall x d =
    Metric.closedEBall (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.eq_restrictScalarsRange_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} {M' : Type u_5} {P' : Type u_6} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : SMul S R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] [inst_7 : Module S M] [inst_8 : Module S P] [inst_9 : IsScalarTower S R M]
  [inst_10 : IsScalarTower S R P] [inst_11 : AddCommMonoid M'] [inst_12 : Module S M'] [inst_13 : AddCommMonoid P']
  [inst_14 : Module S P'] (i : M' →ₗ[S] M) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (f : M →ₗ[R] P)
  (hf : ∀ (m : M'), f (i m) ∈ k.range) (m : M') (p : P'), p = (i.restrictScalarsRange k hk f hf) m ↔ k p = f (i m)
-- Mathlib.LinearAlgebra.Alternating.Curry
AlternatingMap.curryLeft_apply_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (x : M)
  (v : Fin n → M), (f.curryLeft x) v = f (Matrix.vecCons x v)
-- Mathlib.Order.Circular
/-- Strict betweenness is given by betweenness in one direction and non-betweenness in the other.

I.e., if `b` is between `a` and `c` but not between `c` and `a`, then we say `b` is strictly
between `a` and `c`.  -/
CircularPreorder.sbtw_iff_btw_not_btw : ∀ {α : Type u_1} [self : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
-- Mathlib.Analysis.MellinTransform
mellin.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s : ℂ),
  mellin f s = ∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (s - 1) • f t
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.locallyIntegrableOn : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X},
  MeasureTheory.LocallyIntegrable f μ → ∀ (s : Set X), MeasureTheory.LocallyIntegrableOn f s μ
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.toProd_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N], Function.Surjective ⇑Monoid.Coprod.toProd
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Exact membership in the set. This is useful primarily for stating
correctness properties; use `∈` for a version that actually uses the BST property
of the tree.

```
Emem 2 {1, 2, 3} = true
Emem 4 {1, 2, 3} = false
```  -/
Ordnode.Emem : {α : Type u_1} → α → Ordnode α → Prop