mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.val_inv_unit' : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α} (h : IsUnit a), ↑h.unit'⁻¹ = a⁻¹
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `contMDiffAt_localFrameCoeff`.

---

If `s` is `C^k` at `x`, so is its coefficient `b.localFrameCoeff e i` in the local frame
near `x` induced by `e` and `b`  -/
contMDiffAt_localFrame_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {k : WithTop ℕ∞}
  {x : M} [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  x ∈ e.baseSet →
    ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) x →
      ∀ (i : ι),
        ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) k
          ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) x
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.toAdd_unzero_eq_iff : ∀ {α : Type u_3} {a : WithZero (Multiplicative α)} (h : a ≠ 0) (b : α),
  Multiplicative.toAdd (WithZero.unzero h) = b ↔ a = ↑(Multiplicative.ofAdd b)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
/-- If the Lebesgue integral of a function is bounded by some constant on all sets with finite
measure in a sub-σ-algebra and the measure is σ-finite on that sub-σ-algebra, then the integral
over the whole space is bounded by that same constant.  -/
MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
  [MeasureTheory.SigmaFinite (μ.trim hm)] (C : ENNReal) {f : α → ENNReal},
  (∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) → ∫⁻ (x : α), f x ∂μ ≤ C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
EulerSine.integral_sin_mul_sin_mul_cos_pow_eq : ∀ {z : ℂ} {n : ℕ},
  2 ≤ n →
    z ≠ 0 →
      ∫ (x : ℝ) in 0..Real.pi / 2, Complex.sin (2 * z * ↑x) * ↑(Real.sin x) * ↑(Real.cos x) ^ (n - 1) =
        (↑n / (2 * z) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ n) -
          (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (n - 2)
-- Mathlib.CategoryTheory.Category.Bipointed
/-- Morphisms in `Bipointed`.  -/
Bipointed.Hom : Bipointed → Bipointed → Type u
-- Mathlib.Order.Filter.Defs
/-- The join of a filter of filters is defined by the relation `s ∈ join f ↔ {t | s ∈ t} ∈ f`.  -/
Filter.join : {α : Type u_1} → Filter (Filter α) → Filter α
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.instInhabitedMethod : Inhabited Aesop.ScriptGenerated.Method
-- Mathlib.Topology.Order
TopologicalSpace.gc_generateFrom : ∀ (α : Type u_1),
  GaloisConnection (fun t => OrderDual.toDual {s | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
/-- The SummationFilter on a locally finite order `G` corresponding to the symmetric
intervals `Ico (-N) N`·  -/
SummationFilter.symmetricIco : (G : Type u_1) → [Neg G] → [inst : Preorder G] → [LocallyFiniteOrder G] → SummationFilter G
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.e_assoc'_assoc : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (W X Y Z : C) {Z_1 : V} (h : (W ⟶[V] Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W X Z) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W Y Z) h)
-- Mathlib.Combinatorics.Hall.Finite
/-- First case of the inductive step: assuming that
`∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)`
and that the statement of **Hall's Marriage Theorem** is true for all
`ι'` of cardinality ≤ `n`, then it is true for `ι` of cardinality `n + 1`.
 -/
HallMarriageTheorem.hall_hard_inductive_step_A : ∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] {t : ι → Finset α} [inst_1 : Fintype ι] {n : ℕ},
  Fintype.card ι = n + 1 →
    (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) →
      (∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
          Fintype.card ι' ≤ n →
            (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x) →
        (∀ (s : Finset ι), s.Nonempty → s ≠ Finset.univ → s.card < (s.biUnion t).card) →
          ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
IsUnit.mem_nonZeroDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀}, IsUnit x → x ∈ nonZeroDivisors M₀
-- Mathlib.Logic.Relation
Equivalence.eqvGen_iff : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Equivalence r → (Relation.EqvGen r a b ↔ r a b)
-- Mathlib.LinearAlgebra.Ray
RayVector.ext : ∀ {R : Type u_1} {M : Type u_2} [inst : Zero M] {x y : RayVector R M},
  ↑((RayVector.equiv R M) x) = ↑((RayVector.equiv R M) y) → x = y
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
OpenPartialHomeomorph.contMDiffOn_extend : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {e : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I n M → ContMDiffOn I (modelWithCornersSelf 𝕜 E) n (↑(e.extend I)) e.source
-- Mathlib.Analysis.Calculus.MeanValue
/-- A function on `[a, b]` with the norm of the right derivative bounded by `C`
satisfies `‖f x - f a‖ ≤ C * (x - a)`.  -/
norm_image_sub_le_of_norm_deriv_right_le_segment : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} {C : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      (∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ C) → ∀ x ∈ Set.Icc a b, ‖f x - f a‖ ≤ C * (x - a)
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_ofNat_of_le : ∀ {v w : ℕ}, v ≤ w → ∀ (x : ℕ), BitVec.setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isRightKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F}
  (h : E.IsPointwiseRightKanExtension),
  (CategoryTheory.CostructuredArrow.left E).IsRightKanExtension (CategoryTheory.CostructuredArrow.hom E)
-- Mathlib.Order.CompleteLattice.Basic
IsGLB.iInf_eq : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {a : α}, IsGLB (Set.range f) a → ⨅ j, f j = a
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.mem_base_pretrivializationAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (self : VectorPrebundle R F E) (x : B), x ∈ (self.pretrivializationAt x).baseSet
-- Mathlib.Algebra.Order.Star.Basic
/-- A star projection `p` is less than or equal to a star projection `q` when `q * p = p`.  -/
IsStarProjection.le_of_mul_eq_right : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {p q : R},
  IsStarProjection p → IsStarProjection q → q * p = p → p ≤ q
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.HomologyData.map_iso : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.HomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.left.IsPreservedBy F]
  [inst_6 : h.right.IsPreservedBy F], (h.map F).iso = F.mapIso h.iso
-- Init.Data.BitVec.Lemmas
BitVec.replicate_succ : ∀ {w n : ℕ} {x : BitVec w}, BitVec.replicate (n + 1) x = BitVec.cast ⋯ (x ++ BitVec.replicate n x)
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.readNotificationAs : IO.FS.Stream → ℕ → String → (α : Type) → [Lean.FromJson α] → IO (Lean.JsonRpc.Notification α)
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_lcm_of_dvd_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ lcm c b
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.inv_mul_integral_comp_add_div : ∀ {a b : ℝ} {f : ℝ → ℝ} (c d : ℝ), c⁻¹ * ∫ (x : ℝ) in a..b, f (d + x / c) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.imageSieve_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {FA : A → A → Type u_1} {CA : A → Type w'} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C}
  (s : CategoryTheory.ToType (F.obj (Opposite.op U))),
  CategoryTheory.Presheaf.imageSieve f ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U))) s) = ⊤
-- Mathlib.Order.Interval.Finset.Defs
/-- `x ∈ finsetIio a ↔ x < a`  -/
LocallyFiniteOrderBot.finset_mem_Iio : ∀ {α : Type u_1} {inst : Preorder α} [self : LocallyFiniteOrderBot α] (a x : α),
  x ∈ LocallyFiniteOrderBot.finsetIio a ↔ x < a
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `Dense.sdiff_singleton`.

---

Removing a non-isolated point from a dense set, one still obtains a dense set.  -/
Dense.diff_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X},
  Dense s → ∀ (x : X) [(nhdsWithin x {x}ᶜ).NeBot], Dense (s \ {x})
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObj.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {R : C} →
          [toRingObj : CategoryTheory.RingObj R] →
            [toIsCommMonObj : CategoryTheory.IsCommMonObj R] → CategoryTheory.CommRingObj R
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase_dup.sizeOf_spec : ∀ (c : Lean.Meta.Grind.AC.EqCnstr), sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.erase_dup c) = 1 + sizeOf c
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.digitsAux0.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Data.NNReal.Defs
NNReal.mk_one : NNReal.mk 1 ⋯ = 1
-- Lean.SubExpr
Lean.SubExpr.Pos.pushLetValue : Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Init.Data.Int.DivMod.Bootstrap
Int.add_mul_emod_self_right : ∀ (a b c : ℤ), (a + b * c) % c = a % c
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `final_comp` below.  -/
CategoryTheory.Functor.final_equivalence_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.IsEquivalence] [G.Final], (F.comp G).Final
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presieve.le_of_factorsThru_sieve : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} (S : CategoryTheory.Presieve X)
  (T : CategoryTheory.Sieve X), S.FactorsThru T.arrows → S ≤ T.arrows
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsUniversalColimit.whiskerEquivalence : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {K : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} K] (e : J ≌ K) {F : CategoryTheory.Functor K C}
  {c : CategoryTheory.Limits.Cocone F},
  CategoryTheory.IsUniversalColimit c →
    CategoryTheory.IsUniversalColimit (CategoryTheory.Limits.Cocone.whisker e.functor c)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- Fréchet derivative of the two-variable Jacobi theta function.  -/
jacobiTheta₂_fderiv : ℂ → ℂ → ℂ × ℂ →L[ℂ] ℂ
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- Populate a `context` object for evaluating `e`.  -/
Mathlib.Tactic.Bicategory.mkContext? : Lean.Expr → Lean.MetaM (Option Mathlib.Tactic.Bicategory.Context)
-- Std.Data.HashMap.Lemmas
Std.HashMap.equiv_iff_keys_unit_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ ↔ m₁.keys.Perm m₂.keys
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.coe_ringHom : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        {I : Ideal A} →
          {J : Ideal B} → (hI : DividedPowers I) → (hJ : DividedPowers J) → CoeOut (hI.DPMorphism hJ) (A →+* B)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.below : {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → a.Trimmed → Prop} →
  {basis : Tactic.ComputeAsymptotics.Basis} →
    {a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis} → a.Trimmed → Prop
-- Mathlib.AlgebraicGeometry.Morphisms.Descent
/-- If `P` is local at the source, every quasi-compact scheme is dominated by an
affine scheme via `p : Y ⟶ X` such that `p` satisfies `P`.
 -/
AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isZariskiLocalAtSource : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (X : AlgebraicGeometry.Scheme) [CompactSpace ↥X]
  [AlgebraicGeometry.IsZariskiLocalAtSource P] [P.ContainsIdentities],
  ∃ Y p, AlgebraicGeometry.Surjective p ∧ P p ∧ AlgebraicGeometry.IsAffine Y
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  [addMon : CategoryTheory.AddMonObj X] (X_1 : C) (addMon_1 : CategoryTheory.AddMonObj X_1),
  ({ X := X, addMon := addMon } = { X := X_1, addMon := addMon_1 }) = (X = X_1 ∧ addMon ≍ addMon_1)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        (toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f) →
                          ((j : J) →
                              ¬IsMax j →
                                HomotopicalAlgebra.AttachCells (basicCell j)
                                  (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯))) →
                            HomotopicalAlgebra.RelativeCellComplex basicCell f
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.len_eq_of_isIso : ∀ {x y : SimplexCategory} (f : x ⟶ y) [CategoryTheory.IsIso f], x.len = y.len
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instRespectsIsoFullSubcategoryWeakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {P : CategoryTheory.ObjectProperty C} [(HomotopicalAlgebra.weakEquivalences C).RespectsIso],
  (HomotopicalAlgebra.weakEquivalences P.FullSubcategory).RespectsIso
-- Mathlib.SetTheory.Ordinal.Basic
/-- The ordinal corresponding to a cardinal `c` is the least ordinal whose cardinal is `c`.  -/
Cardinal.ord : Cardinal.{u} → Ordinal.{u}
-- Mathlib.Algebra.Group.Finsupp
Finsupp.uniqueAddEquiv_symm_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (i : ι) [inst_1 : Subsingleton ι] (b : M),
  (Finsupp.uniqueAddEquiv i).symm b = fun₀ | i => b
-- Init.Data.String.Pattern.Basic
/-- Checks whether the slice ends with the pattern. If it does, the slice is returned with the
  suffix removed; otherwise the result is `none`.
   -/
String.Slice.Pattern.BackwardPattern.skipSuffixOfNonempty? : {ρ : Type} →
  (pat : ρ) → [self : String.Slice.Pattern.BackwardPattern pat] → (s : String.Slice) → s.isEmpty = false → Option s.Pos
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.star_apply : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) {u v : U} (e : u ⟶ v),
  φ.star u (Quiver.Star.mk e) = Quiver.Star.mk (φ.map e)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientInfToPiQuotient_mk : ∀ {R : Type u} [inst : Ring R] {ι : Type u_1} (I : ι → Ideal R) [inst_1 : ∀ (i : ι), (I i).IsTwoSided] (x : R),
  (Ideal.quotientInfToPiQuotient I) ((Ideal.Quotient.mk (⨅ i, I i)) x) = fun i => (Ideal.Quotient.mk (I i)) x
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.instEquivLike : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → EquivLike (α ≃ᵐ β) α β
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_ne_top : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a b : WithTop α}, a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤
-- Mathlib.Algebra.Module.PID
Submodule.liftQSpanSingleton.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {R₂ : Type u_3}
  {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂} (x : M)
  (f f_1 : M →ₛₗ[τ₁₂] M₂) (e_f : f = f_1) (h : f x = 0),
  Submodule.liftQSpanSingleton x f h = Submodule.liftQSpanSingleton x f_1 ⋯
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.Path.mk.congr_simp : ∀ {X : TopCat} {x y : ↑X} (hom hom_1 : TopCat.I ⟶ X) (e_hom : hom = hom_1)
  (hom₀ : (CategoryTheory.ConcreteCategory.hom hom) 0 = x) (hom₁ : (CategoryTheory.ConcreteCategory.hom hom) 1 = y),
  { hom := hom, hom₀ := hom₀, hom₁ := hom₁ } = { hom := hom_1, hom₀ := ⋯, hom₁ := ⋯ }
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsPosSemidef.mk : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I₁ : R →+* R}
  [inst_3 : LE R] {B : M →ₛₗ[I₁] M →ₗ[R] R}, B.IsSymm → B.IsNonneg → B.IsPosSemidef
-- Mathlib.Algebra.Homology.Homotopy
/-- A constructor for a `Homotopy e 0`, for `e` a chain map between `ℕ`-indexed chain complexes,
working by induction.

You need to provide the components of the homotopy in degrees 0 and 1,
show that these satisfy the homotopy condition,
and then give a construction of each component,
and the fact that it satisfies the homotopy condition,
using as an inductive hypothesis the data and homotopy condition for the previous two components.
 -/
Homotopy.mkInductive : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {P Q : ChainComplex V ℕ} →
        (e : P ⟶ Q) →
          (zero : P.X 0 ⟶ Q.X 1) →
            e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0) →
              (one : P.X 1 ⟶ Q.X 2) →
                e.f 1 =
                    CategoryTheory.CategoryStruct.comp (P.d 1 0) zero +
                      CategoryTheory.CategoryStruct.comp one (Q.d 2 1) →
                  ((n : ℕ) →
                      (p :
                          (f : P.X n ⟶ Q.X (n + 1)) ×'
                            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                              e.f (n + 1) =
                                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
                        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
                          e.f (n + 2) =
                            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
                              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) →
                    Homotopy e 0
-- Mathlib.Algebra.Module.Submodule.Map
/-- For any `R` submodules `p` and `q`, `p ⊓ q` as a submodule of `q`.  -/
Submodule.submoduleOf : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → (q : Submodule R M) → Submodule R ↥q
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonWorkspaceEditClientCapabilities : Lean.ToJson Lean.Lsp.WorkspaceEditClientCapabilities
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.cg_def : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M], FirstOrder.Language.Structure.CG L M ↔ ⊤.CG
-- Mathlib.Algebra.Group.Prod
Prod.instAddCommSemigroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommSemigroup G] [inst_1 : AddCommSemigroup H],
  Prod.instAddCommSemigroup = { toAddSemigroup := Prod.instAddSemigroup, add_comm := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Function.Injective.hasSum_map_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {L : SummationFilter γ} {g : γ → β} (hg : Function.Injective g),
  HasSum f a (L.map { toFun := g, inj' := hg }) ↔ HasSum (f ∘ g) a L
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, k ∈ Std.TreeMap.Raw.ofList l cmp ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_sub_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a - x) ⁻¹' Set.Iic b = Set.Ici (a - b)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.continuousWithinAt_insert : ∀ {𝕜 : 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} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → ContinuousWithinAt f (insert x s) x
-- Init.Data.Sum.Basic
/-- Transforms a sum according to functions on each type.

This function maps `α ⊕ β` to `α' ⊕ β'`, sending `α` to `α'` and `β` to `β'`.
 -/
Sum.map : {α : Type u_1} → {α' : Type u_2} → {β : Type u_3} → {β' : Type u_4} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'