mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
contMDiffAt_hom_bundle : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {n : WithTop ℕ∞} {E₁ : B → Type u_6}
  {E₂ : B → Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_8} [inst_13 : NormedAddCommGroup EB]
  [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_9} [inst_15 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_10} [inst_18 : NormedAddCommGroup EM]
  [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_11} [inst_20 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M] [inst_23 : FiberBundle F₁ E₁]
  [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂] [inst_26 : VectorBundle 𝕜 F₂ E₂]
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  (f : M → Bundle.TotalSpace (F₁ →L[𝕜] F₂) fun b => E₁ b →L[𝕜] E₂ b) {x₀ : M},
  ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂))) n f x₀ ↔
    ContMDiffAt IM IB n (fun x => (f x).proj) x₀ ∧
      ContMDiffAt IM (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n
        (fun x => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
        x₀
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.projectRightAssign.eq_1 : ∀ (assign : ℕ → Bool) (idx : ℕ), Std.Sat.AIG.toCNF.projectRightAssign✝ assign idx = assign idx
-- Mathlib.Algebra.Homology.CommSq
/-- The short complex attached to the kernel fork of a commutative square.
(This is similar to `CommSq.shortComplex`, but with different signs.)  -/
CategoryTheory.CommSq.shortComplex' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X₁ X₂ X₃ X₄ : C} →
        [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] →
          {fst : X₁ ⟶ X₂} →
            {snd : X₁ ⟶ X₃} →
              {f : X₂ ⟶ X₄} → {g : X₃ ⟶ X₄} → CategoryTheory.CommSq fst snd f g → CategoryTheory.ShortComplex C
-- Mathlib.Topology.UniformSpace.Basic
instCompleteLatticeUniformSpace : {α : Type ua} → CompleteLattice (UniformSpace α)
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          {I : CategoryTheory.InjectiveResolution Z} →
            {Z' : C} →
              {I' : CategoryTheory.InjectiveResolution Z'} →
                {f : Z ⟶ Z'} →
                  (hom : I.cocomplex ⟶ I'.cocomplex) →
                    CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom.f 0) =
                        CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0) →
                      I.Hom I' f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `b₆` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.b₆ : {R : Type u} → [CommRing R] → WeierstrassCurve R → R
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectOutput.below : {α β : Type w} →
  {m : Type w → Type w'} →
    [inst : Std.Iterator α m β] →
      {motive : (a : Std.IterM m β) → (a_1 : β) → a.IsPlausibleIndirectOutput a_1 → Prop} →
        {a : Std.IterM m β} → {a_1 : β} → a.IsPlausibleIndirectOutput a_1 → Prop
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.coe_sup : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s t : TopologicalSpace.PositiveCompacts α), ↑(s ⊔ t) = ↑s ∪ ↑t
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
/-- The geometric realization of `Δ[1]` is isomorphic to `TopCat.I`.  -/
SSet.stdSimplex.toTopObjIsoI : SSet.toTop.obj (SSet.stdSimplex.obj { len := 1 }) ≅ TopCat.I
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_eq_getD_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), p.getVert n = p.support.getD n v
-- Lean.Elab.AssertExists
Lean.Elab.Command.instBEqAssertExists.beq : Lean.Elab.Command.AssertExists → Lean.Elab.Command.AssertExists → Bool
-- Mathlib.Data.Multiset.ZeroCons
Multiset.zero_ne_singleton : ∀ {α : Type u_1} (a : α), 0 ≠ {a}
-- Init.Data.SInt.IntToBitVec
Int32.toBitVec32_toISize : ∀ (n : Int32) (h : System.Platform.numBits = 32), n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- In the category `ModuleCat R`, if `x` and `y` are pseudoequal, then the range of the associated
morphisms is the same.  -/
CategoryTheory.Abelian.Pseudoelement.ModuleCat.eq_range_of_pseudoequal : ∀ {R : Type u_1} [inst : Ring R] {G : ModuleCat R} {x y : CategoryTheory.Over G},
  CategoryTheory.Abelian.PseudoEqual G x y → (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.partialApp.sizeOf_spec : sizeOf Lean.Meta.ReduceMatcherResult.partialApp = 1
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor X =
    CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor X
-- Mathlib.Data.Nat.Hyperoperation
_private.Mathlib.Data.Nat.Hyperoperation.0.hyperoperation.match_1.eq_1 : ∀ (motive : ℕ → ℕ → ℕ → Sort u_1) (x k : ℕ) (h_1 : (x k : ℕ) → motive 0 x k) (h_2 : (m : ℕ) → motive 1 m 0)
  (h_3 : (x : ℕ) → motive 2 x 0) (h_4 : (n x : ℕ) → motive n.succ.succ.succ x 0)
  (h_5 : (n m k : ℕ) → motive n.succ m k.succ),
  (match 0, x, k with
    | 0, x, k => h_1 x k
    | 1, m, 0 => h_2 m
    | 2, x, 0 => h_3 x
    | n.succ.succ.succ, x, 0 => h_4 n x
    | n.succ, m, k.succ => h_5 n m k) =
    h_1 x k
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.comap_verts : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G'.Subgraph),
  (SimpleGraph.Subgraph.comap f H).verts = ⇑f ⁻¹' H.verts
-- Mathlib.Topology.Algebra.GroupWithZero
/-- If `f → a` and `g → b` along a nontrivial filter, valued in a Hausdorff
`GroupWithZero` with continuous multiplication and `ContinuousInv₀`, and `b ≠ 0`,
then `f / g → 1` if and only if `a = b`.  -/
tendsto_div_nhds_one_iff_eq₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} {l : Filter α} [l.NeBot] [T2Space G₀] {a b : G₀},
  Filter.Tendsto f l (nhds a) →
    Filter.Tendsto g l (nhds b) → b ≠ 0 → (Filter.Tendsto (fun x => f x / g x) l (nhds 1) ↔ a = b)
-- Init.Data.List.Sublist
List.IsSuffix.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.length ≤ l₂.length
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The (extended-real-valued) variation of a function `f` on a set `s` inside a linear order is
the supremum of the sum of `edist (f (u (i+1))) (f (u i))` over all finite increasing
sequences `u` in `s`.  -/
eVariationOn : {α : Type u_1} → [LinearOrder α] → {E : Type u_2} → [PseudoEMetricSpace E] → (α → E) → Set α → ENNReal
-- Mathlib.Algebra.Group.Prod
MonoidHom.coprod_apply : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommMonoid P]
  (f : M →* P) (g : N →* P) (p : M × N), (f.coprod g) p = f p.1 * g p.2
-- Mathlib.NumberTheory.ADEInequality
/-- A multiset `{p,q,r}` of positive natural numbers
is a solution to `(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1` if and only if
it is `Admissible` which means it is one of:

* `A' q r := {1,q,r}`
* `D' r := {2,2,r}`
* `E6 := {2,3,3}`, or `E7 := {2,3,4}`, or `E8 := {2,3,5}`
 -/
ADEInequality.classification : ∀ (p q r : ℕ+), 1 < ADEInequality.sumInv {p, q, r} ↔ ADEInequality.Admissible {p, q, r}
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- Get the coequalizer object from the typeclass `IsSplitPair`.  -/
CategoryTheory.HasSplitCoequalizer.coequalizerOfSplit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (f g : X ⟶ Y) → [CategoryTheory.HasSplitCoequalizer f g] → C
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.jmp.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (args : Array (Lean.Compiler.LCNF.Arg pu)),
  sizeOf (Lean.Compiler.LCNF.Code.jmp fvarId args) = 1 + sizeOf fvarId + sizeOf args
-- Mathlib.Order.Hom.Bounded
/-- The function preserves the bottom element. The preferred spelling is `map_bot`.  -/
BotHom.map_bot' : ∀ {α : Type u_6} {β : Type u_7} [inst : Bot α] [inst_1 : Bot β] (self : BotHom α β), self.toFun ⊥ = ⊥
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.symm_homotopyHomInvId : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D),
  f.symm.homotopyHomInvId = f.homotopyInvHomId
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- If `e₁` and `e₂` are complementary embeddings into a complex shape `c`,
indices `i₁` and `i₂` are at the boundary if `c.Rel (e₁.f i₁) (e₂.f i₂)`.  -/
ComplexShape.Embedding.AreComplementary.Boundary : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} →
            {e₁ : c₁.Embedding c} → {e₂ : c₂.Embedding c} → e₁.AreComplementary e₂ → ι₁ → ι₂ → Prop
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Iio_succ_eq_Iic_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : SuccOrder α] {b : α},
  ¬IsMax b → Finset.Iio (Order.succ b) = Finset.Iic b
-- Lean.Server.AsyncList
_private.Lean.Server.AsyncList.0.Lean.AsyncList.getFinishedPrefixWithConsistentLatency.sleepWithCancellation : List (Lean.Server.ServerTask Unit) → UInt32 → BaseIO Unit
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.PlausibleStep.yield : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {it' : Std.IterM m β} {out : β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    it.internalState.remaining = 0 →
      Std.Iterators.Types.Drop.PlausibleStep it (Std.IterStep.yield (Std.IterM.drop 0 it') out)
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.comap_nhds_neBot : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  IsDenseInducing i → ∀ (b : β), (Filter.comap i (nhds b)).NeBot
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_pi_congr_prop : ∀ {ι ι' : Prop} {f : ι → Type v} {g : ι' → Type v} (e : ι ↔ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g ⋯)) → Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι') → g i)
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_eq_zero_iff : ∀ {n : Int32}, n.toNatClampNeg = 0 ↔ n ≤ 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- A functor that preserves and reflects initial objects induces an equivalence on `IsInitial`.  -/
CategoryTheory.Limits.IsInitial.isInitialIffObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] →
            [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) G] →
              (X : C) → CategoryTheory.Limits.IsInitial X ≃ CategoryTheory.Limits.IsInitial (G.obj X)
-- Mathlib.Order.Minimal
maximal_and_iff_left_of_imp : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α],
  (∀ ⦃x : α⦄, P x → Q x) → (Maximal (fun x => Q x ∧ P x) x ↔ Q x ∧ Maximal P x)
-- Mathlib.LinearAlgebra.TensorAlgebra.Grading
/-- The tensor algebra is graded by the powers of the submodule `(TensorAlgebra.ι R).range`.  -/
TensorAlgebra.gradedAlgebra : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → GradedAlgebra fun x => (TensorAlgebra.ι R).range ^ x
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The universal property of the direct limit: maps from the components to another R-algebra
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit.
 -/
DirectLimit.NonUnitalAlgebra.lift : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      (G : ι → Type u_3) →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : CommSemiring R] →
                    [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] →
                      [inst_6 : (i : ι) → DistribMulAction R (G i)] →
                        [inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] →
                          [inst_8 : Nonempty ι] →
                            (P : Type u_7) →
                              [inst_9 : NonUnitalNonAssocSemiring P] →
                                [inst_10 : DistribMulAction R P] →
                                  (g : (i : ι) → G i →ₙₐ[R] P) →
                                    (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) →
                                      DirectLimit G f →ₙₐ[R] P
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.mulShift_one : ∀ {A : Type u_1} {G : Type u_2} [inst : Monoid G] (x : G → A), SymbolicDynamics.FullShift.mulShift 1 x = x
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- If a topological space `M` admits an atlas with locally path-connected charts,
then `M` itself is locally path-connected.  -/
ChartedSpace.locallyPathConnectedSpace : ∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M]
  [LocallyPathConnectedSpace H], LocallyPathConnectedSpace M
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.leftAdjointObjIsDefined_colimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor D C} {J : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  (R : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.HasColimit R]
  [CategoryTheory.Limits.HasColimitsOfShape J D],
  (∀ (j : J), F.leftAdjointObjIsDefined (R.obj j)) → F.leftAdjointObjIsDefined (CategoryTheory.Limits.colimit R)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.ext : ∀ {α : Type u} {x y : Std.PRange.UpwardEnumerable α},
  Std.PRange.succ? = Std.PRange.succ? → Std.PRange.succMany? = Std.PRange.succMany? → x = y
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Returns `.true` if `c` is satisfied by the current partial model,
`.undef` if `c` contains unassigned variables, and `.false` otherwise.
 -/
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.satisfied : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.GoalM Lean.LBool
-- Mathlib.Data.TwoPointing
TwoPointing.swap_fst : ∀ {α : Type u_1} (p : TwoPointing α), p.swap.toProd.1 = p.toProd.2
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atTop_leadingCoeff_div_of_degree_eq : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  P.degree = Q.degree →
    Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop
      (nhds (P.leadingCoeff / Q.leadingCoeff))
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite ISize
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_def : ∀ {α : Type u_1} (M : Matroid α), M.eRank = M.eRk M.E
-- Mathlib.Order.WithBot
Equiv.withTopCongr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β),
  e.withTopCongr = { toFun := WithTop.map ⇑e, invFun := WithTop.map ⇑e.symm, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftFZero.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Y Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y)
  (Q : CategoryTheory.ProjectiveResolution Z),
  CategoryTheory.ProjectiveResolution.liftFZero f P Q =
    CategoryTheory.Projective.factorThru (CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (Q.π.f 0)
-- Mathlib.Data.Fin.Basic
Fin.val_eq_val : ∀ {n : ℕ} (a b : Fin n), ↑a = ↑b ↔ a = b
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.id.toLax : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C), (CategoryTheory.Lax.StrongTrans.id F).toLax = CategoryTheory.Lax.LaxTrans.id F
-- Mathlib.Analysis.Calculus.Deriv.ZPow
deriv_zpow' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (m : ℤ), (deriv fun x => x ^ m) = fun x => ↑m * x ^ (m - 1)
-- Init.Data.Nat.Basic
Nat.le_add_right : ∀ (n k : ℕ), n ≤ n + k
-- Mathlib.Algebra.Free
Magma.AssocQuotient.hom_ext : ∀ {α : Type u} [inst : Mul α] {β : Type v} [inst_1 : Semigroup β] {f g : Magma.AssocQuotient α →ₙ* β},
  f.comp Magma.AssocQuotient.of = g.comp Magma.AssocQuotient.of → f = g
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.isClosedImmersion_iff_isAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.IsClosedImmersion f ↔
    AlgebraicGeometry.IsAffineHom f ∧
      ∀ (U : Y.Opens),
        AlgebraicGeometry.IsAffineOpen U →
          Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U))
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_finTwoArrow_vec : ∀ {α : Type u} {x : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (MeasureTheory.Measure.pi ![μ, ν]) (μ.prod ν)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMany!_eq_foldl_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β},
  ↑(t₁.insertMany! t₂) =
    Std.DTreeMap.Internal.Impl.foldl (fun acc k v => Std.DTreeMap.Internal.Impl.insert! k v acc) t₁ t₂
-- Mathlib.Topology.MetricSpace.HausdorffDimension
measure_zero_of_dimH_lt : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  {μ : MeasureTheory.Measure X} {d : NNReal},
  μ.AbsolutelyContinuous (MeasureTheory.Measure.hausdorffMeasure ↑d) → ∀ {s : Set X}, dimH s < ↑d → μ s = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.toSSetObjEquiv_naturality_apply : ∀ {X : TopCat} {n m : SimplexCategory} (f : n ⟶ m) (x : (TopCat.toSSet.obj X).obj (Opposite.op m))
  (z : ↑(stdSimplex ℝ (Fin (n.len + 1)))),
  ((X.toSSetObjEquiv (Opposite.op n)) ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map f.op)) x)) z =
    ((X.toSSetObjEquiv (Opposite.op m)) x) (stdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) z)
-- Mathlib.Topology.GDelta.Basic
/-- The empty set is nowhere dense.  -/
isNowhereDense_empty : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsNowhereDense ∅
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasHomology_of_hasKernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {Y Z : C}
  (g : Y ⟶ Z) (X : C) [CategoryTheory.Limits.HasKernel g],
  { X₁ := X, X₂ := Y, X₃ := Z, f := 0, g := g, zero := ⋯ }.HasHomology
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essSurj_of_comp_fully_faithful : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [(F.comp G).EssSurj] [G.Faithful] [G.Full],
  F.EssSurj
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Real.hasDerivAt_Gamma_nat : ∀ (n : ℕ), HasDerivAt Real.Gamma (↑n.factorial * (-Real.eulerMascheroniConstant + ↑(harmonic n))) (↑n + 1)
-- Mathlib.Order.WithBot
WithTop.untopD_eq_iff : ∀ {α : Type u_1} {d y : α} {x : WithTop α}, WithTop.untopD d x = y ↔ x = ↑y ∨ x = ⊤ ∧ y = d
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Entrypoint.mk.inj : ∀ {α : Type} {inst : DecidableEq α} {inst_1 : Hashable α} {aig : Std.Sat.AIG α} {ref : aig.Ref} {aig_1 : Std.Sat.AIG α}
  {ref_1 : aig_1.Ref}, { aig := aig, ref := ref } = { aig := aig_1, ref := ref_1 } → aig = aig_1 ∧ ref ≍ ref_1
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.exists_forall_apply_eq_pow : ∀ (k : Type u_1) [inst : Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (l : Type u_2) [inst_4 : Field l]
  [inst_5 : Algebra k l] [Finite l] (g : Gal(l/k)), ∃ i, ∀ (x : l), g x = x ^ Nat.card k ^ i
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.NormalizedMooreComplex.d_squared : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.NormalizedMooreComplex.objD X (n + 1))
      (AlgebraicTopology.NormalizedMooreComplex.objD X n) =
    0
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.ofNonUnitalRingHom_symm_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (hom : R →ₙ+* S) (inv : S →ₙ+* R) (hom_inv_id : inv.comp hom = NonUnitalRingHom.id R)
  (inv_hom_id : hom.comp inv = NonUnitalRingHom.id S) (a : S),
  (RingEquiv.ofNonUnitalRingHom hom inv hom_inv_id inv_hom_id).symm a = inv a
-- Mathlib.Algebra.Group.Defs
npowRec_succ : ∀ {M : Type u} [inst : One M] [inst_1 : Semigroup M] (n : ℕ),
  n ≠ 0 → ∀ (a : M), 1 * a = a → npowRec (n + 1) a = a * npowRec n a
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x')
  (y : ↑(Y.presheaf.stalk ((TopCat.Hom.hom f.base) x'))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
      ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) y) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x')) y)
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.mk.inj : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {inst : Semiring R} {inst_1 : AddCommMonoid E₁}
  {inst_2 : PartialOrder E₁} {inst_3 : AddCommMonoid E₂} {inst_4 : PartialOrder E₂} {inst_5 : Module R E₁}
  {inst_6 : Module R E₂} {toLinearMap : E₁ →ₗ[R] E₂} {monotone' : Monotone toLinearMap.toFun}
  {toLinearMap_1 : E₁ →ₗ[R] E₂} {monotone'_1 : Monotone toLinearMap_1.toFun},
  { toLinearMap := toLinearMap, monotone' := monotone' } = { toLinearMap := toLinearMap_1, monotone' := monotone'_1 } →
    toLinearMap = toLinearMap_1
-- Init.Data.Order.Ord
Std.LawfulEqCmp.toReflCmp : ∀ {α : Type u} {cmp : α → α → Ordering} [self : Std.LawfulEqCmp cmp], Std.ReflCmp cmp