mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.SetBernoulli
/-- The product of bernoulli distributions with parameter `p` on the set `u : Set V` is the measure
on `Set V` such that each element of `u` is taken with probability `p`, and the elements outside of
`u` are never taken.  -/
ProbabilityTheory.«termSetBer(_,_)» : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_eq_norm_mul_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), RCLike.re (inner 𝕜 x x) = ‖x‖ * ‖x‖
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.equivToOverUnit_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.equivToOverUnit C).inverse = CategoryTheory.toOverUnit C
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.self_iff_nonZeroDivisors_eq_isUnit : ∀ {R : Type u_1} [inst : CommRing R], IsFractionRing R R ↔ nonZeroDivisors R = IsUnit.submonoid R
-- Mathlib.Order.Hom.BoundedLattice
/-- Reinterpret a finitary supremum homomorphism as a finitary infimum homomorphism between the dual
lattices.  -/
SupBotHom.dual : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] → [inst_1 : Bot α] → [inst_2 : Max β] → [inst_3 : Bot β] → SupBotHom α β ≃ InfTopHom αᵒᵈ βᵒᵈ
-- Lean.Elab.Term.TermElabM
/-- Node kind for the `Lean.Elab.Term.elabToSyntax` functionality.
It is an implementation detail of `Lean.Elab.Term.elabToSyntax`.
 -/
Lean.Parser.Term.elabToSyntax : Lean.Parser.Parser
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is analytic on a neighborhood of a set `s`, then it has a Taylor series given
by the sequence of its derivatives. Note that, if the function were just analytic on `s`, then
one would have to use instead the sequence of derivatives inside the set, as in
`AnalyticOn.hasFTaylorSeriesUpToOn`.  -/
AnalyticOnNhd.hasFTaylorSeriesUpToOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} [CompleteSpace F] (n : WithTop ℕ∞), AnalyticOnNhd 𝕜 f s → HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 f) s
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.comap_map_eq_self_of_injective : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (s : Subring R), Subring.comap f (Subring.map f s) = s
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonDidOpenTextDocumentParams : Lean.FromJson Lean.Lsp.DidOpenTextDocumentParams
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, panicking if no such key exists.
 -/
Std.TreeMap.Raw.getKeyGE! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap.Raw α β cmp → α → α
-- Mathlib.Data.Finset.NAry
/-- If each partial application of `f` is injective, and images of `s` under those partial
applications are disjoint (but not necessarily distinct!), then the size of `t` divides the size of
`Finset.image₂ f s t`.  -/
Finset.card_dvd_card_image₂_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  (∀ a ∈ s, Function.Injective (f a)) →
    ((fun a => Finset.image (f a) t) '' ↑s).PairwiseDisjoint id → t.card ∣ (Finset.image₂ f s t).card
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.setLIntegral_rnDeriv_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (s : Set α),
  ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ μ s
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.instLocalization : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FormallyUnramified R S] (M : Submonoid S), Algebra.FormallyUnramified R (Localization M)
-- Init.Core
/-- `HEq.ndrec` specialized to homogeneous heterogeneous equality  -/
HEq.homo_ndrec : {α : Sort u2} → {a : α} → {motive : α → Sort u1} → motive a → {b : α} → a ≍ b → motive b
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- the second "projection" from the (pre)path object  -/
HomotopicalAlgebra.PrepathObject.p₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {A : C} → (self : HomotopicalAlgebra.PrepathObject A) → self.P ⟶ A
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.«term_▷_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Order.Monotone
csInf_mem_closure : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, s.Nonempty → BddBelow s → sInf s ∈ closure s
-- Plausible.Testable
/-- If `q → p`, then `¬ p → ¬ q` which means that testing `p` can allow us
to find counter-examples to `q`.  -/
Plausible.TestResult.imp : {p q : Prop} → (q → p) → Plausible.TestResult p → optParam (Unit ⊕' (p → q)) (PSum.inl ()) → Plausible.TestResult q
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalSeminormedCommRing : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalSeminormedCommRing β] → NonUnitalSeminormedCommRing (ZeroAtInftyContinuousMap α β)
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.lhss : Lean.Meta.Match.MkMatcherInput → List Lean.Meta.Match.AltLHS
-- Init.Data.ToString.Basic
instToStringRaw : ToString Substring.Raw
-- Mathlib.Algebra.BigOperators.Associated
Prime.exists_mem_multiset_map_dvd : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] {p : M₀},
  Prime p → ∀ {s : Multiset ι} {f : ι → M₀}, p ∣ (Multiset.map f s).prod → ∃ a ∈ s, p ∣ f a
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
summable_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [IsEmpty β], Summable f L
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_σ_succ_assoc : ∀ {n : ℕ} {i : Fin (n + 1)} {Z : SimplexCategoryGenRel} (h : SimplexCategoryGenRel.mk n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.succ)
      (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ i) h) =
    h
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ}
  [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) [inst_3 : L.IsLeftKanExtension α]
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) (E : ℰ),
  CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv L α P E =
    (CategoryTheory.Limits.IsColimit.homEquiv
          (CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).trans
      (CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A P E)
-- Mathlib.Analysis.RCLike.Basic
LinearIsometryEquiv.symm_units_smul : ∀ {𝕜 : Type u_3} {W : Type u_5} {G : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : NormedSpace 𝕜 W] [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (e : G ≃ₗᵢ[𝕜] W)
  (α : ↥(unitary 𝕜)), (α • e).symm = α⁻¹ • e.symm
-- Init.Data.Option.Lemmas
Option.instAssociativeOr : ∀ {α : Type u_1}, Std.Associative Option.or
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.replicate.congr_simp : ∀ {w w' : ℕ} (n n_1 : ℕ) (e_n : n = n_1) (expr expr_1 : Std.Tactic.BVDecide.BVExpr w),
  expr = expr_1 →
    ∀ (h : w' = w * n),
      Std.Tactic.BVDecide.BVExpr.replicate n expr h = Std.Tactic.BVDecide.BVExpr.replicate n_1 expr_1 ⋯
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mem_mk : ∀ {R : Type u} [inst : NonAssocSemiring R] {toSubmonoid : Submonoid R}
  (add_mem : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier)
  (zero_mem : 0 ∈ toSubmonoid.carrier) {x : R},
  x ∈ { toSubmonoid := toSubmonoid, add_mem' := add_mem, zero_mem' := zero_mem } ↔ x ∈ toSubmonoid
-- Mathlib.Algebra.Order.ToIntervalMod
_private.Mathlib.Algebra.Order.ToIntervalMod.0.toIxxMod_cyclic_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {x₁ x₂ x₃ : α}, toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ → toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
-- Lean.Meta.Tactic.Cleanup
_private.Lean.Meta.Tactic.Cleanup.0.Lean.Meta.cleanupCore.addUsedFVar : Lean.FVarId → StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_le_of_mem_cycleFactorsFinset : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f g : Equiv.Perm α},
  f ∈ g.cycleFactorsFinset → f.cycleType ≤ g.cycleType
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `getStained stx` expects `stx` to be an argument of a node of `SyntaxNodeKind`
`Lean.Parser.Tactic.location`.
Typically, we apply `getStained` to the output of `getLocs`.

See `getStained!` for a similar function.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.getStained : Lean.Syntax → (optParam (Lean.Syntax → Bool) fun x => false) → Std.HashSet Mathlib.Linter.Flexible.Stained✝
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.State.delimitsLocal : {σ : Type} → Lean.ScopedEnvExtension.State σ → Bool
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getEntryGT? k = Std.DTreeMap.Internal.Impl.getEntryGT?.go k none
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The range of an `AddMonoidHom` is an `AddSubmonoid`.  -/
AddMonoidHom.mrange : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {F : Type u_4} → [inst_2 : FunLike F M N] → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid N
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.codRestrict : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} {f : α → β},
  Measurable f → ∀ (h : ∀ (y : α), f y ∈ s), Measurable (Set.codRestrict f s h)
-- Mathlib.Logic.Equiv.Defs
/-- Conjugate a map `f : α → α` by an equivalence `α ≃ β`.  -/
Equiv.conj : {α : Sort u} → {β : Sort v} → α ≃ β → (α → α) ≃ (β → β)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
/-- `WithCStarModule.equiv` as a linear equivalence.  -/
WithCStarModule.linearEquiv : (R : Type u_1) →
  (A : Type u_3) →
    (E : Type u_4) →
      [inst : Semiring R] → [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → WithCStarModule A E ≃ₗ[R] E
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableOn_prod_module_iff : ∀ {𝕜 : 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_17} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_18} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂] {s : Set M}
  (f : M → F₁ × F₂), MDiff[s] f ↔ MDiff[s] (Prod.fst ∘ f) ∧ MDiff[s] (Prod.snd ∘ f)
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.instIsPushout : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (R' : Type u_4)
  (S' : Type u_5) [inst_3 : CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S]
  [inst_6 : Algebra S S'] [IsFractionRing S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R S S']
  [inst_10 : CommRing R'] [inst_11 : Algebra R R'] [IsFractionRing R R'] [inst_13 : Algebra R' S']
  [inst_14 : IsScalarTower R R' S'], Algebra.IsPushout R R' S S'
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instDivInvMonoid : {α : Type u_1} → [DivInvMonoid α] → DivInvMonoid (WithZero α)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- the second map `R → L`  -/
CategoryTheory.Limits.MulticospanShape.snd : (self : CategoryTheory.Limits.MulticospanShape) → self.R → self.L
-- Mathlib.GroupTheory.Sylow
Sylow.coe_comapOfInjective : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (P : Sylow p G) {K : Type u_2} [inst_1 : Group K] (ϕ : K →* G)
  (hϕ : Function.Injective ⇑ϕ) (h : ↑P ≤ ϕ.range), ↑(P.comapOfInjective ϕ hϕ h) = Subgroup.comap ϕ ↑P
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Flipping the sign of `coef` flips the sign of `toFun`. The theorem is stated in this form,
because it allows one to rewrite the `t.toFun basis` expression. It is used below in cases where we
want to reduce the case of `t.coef < 0` to `t.coef > 0`.  -/
Tactic.ComputeAsymptotics.Monomial.neg_toFun : ∀ {t : Tactic.ComputeAsymptotics.Monomial} {basis : Tactic.ComputeAsymptotics.Basis}, t.toFun basis = -t.neg.toFun basis
-- Init.Data.Float.Float
/-- Divides 64-bit floating-point numbers according to IEEE 754. Typically used via the `/` operator.

In Lean, division by zero typically yields zero. For `Float`, it instead yields either `Inf`,
`-Inf`, or `NaN`.

This function has a logical model in terms of `Float.Model`. It is compiled to the C division operator.
 -/
Float.div : Float → Float → Float
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.TaggedState : Type
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `c` is a limit cone for a functor `F : C ⥤ H` and `α : L ⋙ F' ⟶ F` is the counit of any
right Kan extension `F' : D ⥤ H` of `F` along `L : C ⥤ D`, then `coneOfIsRightKanExtension α c` is
a limit cone, too.  -/
CategoryTheory.Functor.isLimitConeOfIsRightKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : L.comp F' ⟶ F) →
                    [inst_3 : F'.IsRightKanExtension α] →
                      {c : CategoryTheory.Limits.Cone F} →
                        CategoryTheory.Limits.IsLimit c →
                          CategoryTheory.Limits.IsLimit (F'.coneOfIsRightKanExtension α c)
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.karoubiUniversal₁_inverse : ∀ (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],
  (CategoryTheory.Idempotents.karoubiUniversal₁ C D).inverse =
    (CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C)
          (CategoryTheory.Idempotents.Karoubi D)).obj
      (CategoryTheory.Idempotents.toKaroubi C)
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.SpecialLinearGroup.instTopologicalSpace : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommRing R] → [TopologicalSpace R] → TopologicalSpace (Matrix.SpecialLinearGroup n R)
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- The underlying isomorphism of a partial isomorphism.  -/
AlgebraicGeometry.Scheme.PartialIso.iso : {X Y : AlgebraicGeometry.Scheme} → (self : X.PartialIso Y) → ↑self.source ≅ ↑self.target
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyι_inv_hom_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i] {Z : C} (h_1 : K.opcycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.isoHomologyι i j hj h).inv
      (CategoryTheory.CategoryStruct.comp (K.homologyι i) h_1) =
    h_1
-- Mathlib.Algebra.Homology.Localization
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app : ∀ {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] (F : CategoryTheory.Functor C D) {ι : Type u_3} {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.CategoryWithHomology C] [inst_5 : CategoryTheory.CategoryWithHomology D]
  [inst_6 : (HomologicalComplex.quasiIso D c).HasLocalization] [inst_7 : F.Additive] [inst_8 : F.PreservesHomology]
  [inst_9 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_10 : c.QFactorsThroughHomotopy C]
  [inst_11 : c.QFactorsThroughHomotopy D]
  [inst_12 : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)]
  (K : HomologicalComplex C c),
  (F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient C c).obj K) =
    CategoryTheory.CategoryStruct.comp
      ((F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K))
      (CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K)
        (CategoryTheory.CategoryStruct.comp
          ((HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K))
          (HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K))))
-- Init.Prelude
/-- Converts a natural number to a 16-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than `2^16`.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.ofNatLT : (n : ℕ) → n < UInt16.size → UInt16
-- Mathlib.Algebra.Group.Basic
zpow_comm : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (m n : ℤ), (a ^ m) ^ n = (a ^ n) ^ m
-- Lean.Meta.Tactic.Simp.Main
/-- Applies the result `r` for `type` (which is inhabited by `val`). Returns `none` if the goal was closed. Returns `some (val', type')`
otherwise, where `val' : type'` and `type'` is the simplified `type`.

This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context.  -/
Lean.Meta.applySimpResult : Lean.MVarId →
  Lean.Expr → Lean.Expr → Lean.Meta.Simp.Result → optParam Bool true → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCancelCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCancelCommMonoid α],
  Lex.instAddCancelCommMonoid = { toAddCommMonoid := Lex.instAddCommMonoid, toIsLeftCancelAdd := ⋯ }
-- Mathlib.Condensed.Discrete.LocallyConstant
LightCondSet.LocallyConstant.instFullLightCondensedTypeDiscrete : (LightCondensed.discrete (Type u)).Full
-- Std.Net.Addr
/-- Build the IPv4 address `a.b.c.d`.
 -/
Std.Net.IPv4Addr.ofParts : UInt8 → UInt8 → UInt8 → UInt8 → Std.Net.IPv4Addr
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opFunctor_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y)
  (n : SimplexCategoryᵒᵖ),
  (SimplicialObject.opFunctor.map f).app n =
    CategoryTheory.CategoryStruct.comp SimplicialObject.opObjIso.hom
      (CategoryTheory.CategoryStruct.comp (f.app n) SimplicialObject.opObjIso.inv)
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.mk.inj : ∀ {definition? : Option Lean.Lsp.RefInfo.Location} {usages : Array Lean.Lsp.RefInfo.Location}
  {definition?_1 : Option Lean.Lsp.RefInfo.Location} {usages_1 : Array Lean.Lsp.RefInfo.Location},
  { definition? := definition?, usages := usages } = { definition? := definition?_1, usages := usages_1 } →
    definition? = definition?_1 ∧ usages = usages_1
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.linearIndependent_rows_of_isUnit : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} [inst_1 : Fintype m] {A : Matrix m m R} [inst_2 : DecidableEq m],
  IsUnit A → LinearIndependent R A.row
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_toBasis_repr : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E),
  b.toBasis.equivFun = b.repr.toLinearEquiv ≪≫ₗ WithLp.linearEquiv 2 𝕜 (ι → 𝕜)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instNSMul : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : AddMonoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffAdd I' n G] → SMul ℕ (ContMDiffMap I I' N G n)
-- Mathlib.CategoryTheory.Products.Bifunctor
CategoryTheory.Bifunctor.diagonal : ∀ {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) E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g))
      (F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y'))) =
    F.map (CategoryTheory.Prod.mkHom f g)
-- Init.Data.ByteArray.Basic
/-- A monadic left fold on `ByteArray` that iterates over an array from low to high indices,
computing a running value.

Each element of the array is combined with the value from the prior elements using a monadic
function `f`. The initial value `init` is the starting value before any elements have
been processed.
 -/
ByteArray.foldlM : {β : Type v} →
  {m : Type v → Type w} → [Monad m] → (β → UInt8 → m β) → β → (as : ByteArray) → optParam ℕ 0 → optParam ℕ as.size → m β
-- Init.Data.Int.Basic
Int.instLTInt : LT ℤ
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.forIn_filterMapWithPostcondition.match_1.eq_1 : ∀ {β₂ : Type u_1} (motive : Option β₂ → Sort u_2) (c : β₂) (h_1 : (c : β₂) → motive (some c))
  (h_2 : Unit → motive none),
  (match some c with
    | some c => h_1 c
    | none => h_2 ()) =
    h_1 c
-- Mathlib.Topology.Bases
TopologicalSpace.isOpen_biUnion_countable : ∀ {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {ι : Type u_1} (I : Set ι) (s : ι → Set α),
  (∀ i ∈ I, IsOpen (s i)) → ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.denoteExpr : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.GoalM Lean.Expr