mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
AlternatingMap.measure.congr_simp : ∀ {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] [inst_2 : MeasurableSpace G]
  [inst_3 : BorelSpace G] [inst_4 : FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)]
  (ω ω_1 : G [⋀^Fin n]→ₗ[ℝ] ℝ), ω = ω_1 → ω.measure = ω_1.measure
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams)
  (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (context? : Option Lean.Lsp.SignatureHelpContext),
  sizeOf
      { toTextDocumentPositionParams := toTextDocumentPositionParams,
        toWorkDoneProgressParams := toWorkDoneProgressParams, context? := context? } =
    1 + sizeOf toTextDocumentPositionParams + sizeOf toWorkDoneProgressParams + sizeOf context?
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- The proposition that two elements of a bilinear form space are orthogonal. For orthogonality
of an indexed set of elements, use `BilinForm.iIsOrtho`.  -/
LinearMap.BilinForm.IsOrtho : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → M → M → Prop
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.isAffineOpen_opensRange : ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Scheme.Hom.opensRange f)
-- Mathlib.CategoryTheory.Monad.Basic
/-- The identity comonad.  -/
CategoryTheory.Comonad.id : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Comonad C
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.inclusion.toFun_eq_coe : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : MulAction M α] (s : SubMulAction M α),
  s.inclusion.toFun = Subtype.val
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.ByteSlice.foldrM.loop.eq_def : ∀ {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : UInt8 → β → m β) (as : ByteSlice) (i : ℕ) (acc : β),
  ByteSlice.foldrM.loop✝ f as i acc =
    if h : i < as.size then do
      let newAcc ← f as[as.size - 1 - i] acc
      ByteSlice.foldrM.loop✝ f as (i + 1) newAcc
    else pure acc
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.leftInvSeq_reverse : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.leftInvSeq ω.reverse = (cs.rightInvSeq ω).reverse
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.instPosMulReflectLEIdeal : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A], PosMulReflectLE (Ideal A)
-- Mathlib.GroupTheory.Congruence.BigOperators
Con.coe_finsetProd : ∀ {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] (c : Con M) (s : Finset ι) (f : ι → M),
  ↑(s.prod f) = ∏ i ∈ s, ↑(f i)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_sum : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_9} (s : Finset ι) (B : ι → LinearMap.BilinMap R M N),
  (∑ i ∈ s, B i).toQuadraticMap = ∑ i ∈ s, (B i).toQuadraticMap
-- Init.Data.BitVec.Lemmas
BitVec.abs.eq_1 : ∀ {n : ℕ} (x : BitVec n), x.abs = if x.msb = true then x.neg else x
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.coe_linearEquiv : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : Semiring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  ⇑(WithLp.linearEquiv p K V) = WithLp.ofLp
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_ofSnowflaking_eq_preimage : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (s : Set (Metric.Snowflaking X α hα₀ hα₁)),
  ⇑Metric.Snowflaking.ofSnowflaking '' s = ⇑Metric.Snowflaking.toSnowflaking ⁻¹' s
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.subset_space : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E}, s ∈ K.faces → ↑s ⊆ K.space
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.intMinSealed : (n : ℕ) → BitVec n
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_finset_singleton : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : DecidableEq α] (b : α),
  AddAction.stabilizer G {b} = AddAction.stabilizer G b
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.map_sConvexComb : ∀ {R : Type u_1} {I : Type u_6} {J : Type u_7} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] (s : Convexity.StdSimplex R (Convexity.StdSimplex R I)) (f : I → J),
  Convexity.StdSimplex.map f (Convexity.sConvexComb s) =
    Convexity.sConvexComb (Convexity.StdSimplex.map (Convexity.StdSimplex.map f) s)
-- Mathlib.Order.Hom.BoundedLattice
/-- The function preserves the bottom element. The preferred spelling is `map_bot`.  -/
SupBotHom.map_bot' : ∀ {α : Type u_6} {β : Type u_7} [inst : Max α] [inst_1 : Max β] [inst_2 : Bot α] [inst_3 : Bot β]
  (self : SupBotHom α β), self.toFun ⊥ = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S}
  (self : h.LiftStruct g₁ g₂ b), CategoryTheory.CategoryStruct.comp self.f h.p₂ = g₂
-- Mathlib.RingTheory.Finiteness.Defs
AddMonoid.FG.to_moduleFinite_nat : ∀ {M : Type u_6} [inst : AddCommMonoid M] [AddMonoid.FG M], Module.Finite ℕ M
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.cons : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {r : R}
  {rs : List R},
  IsSMulRegular M r → RingTheory.Sequence.IsRegular (QuotSMulTop r M) rs → RingTheory.Sequence.IsRegular M (r :: rs)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.sin_arg : ∀ (x : ℂ), Real.sin x.arg = x.im / ‖x‖
-- Mathlib.Data.List.TFAE
List.TFAE.eq_1 : ∀ (l : List Prop), l.TFAE = ∀ x ∈ l, ∀ y ∈ l, x ↔ y
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : Semiring M] (f g : AddMonoidAlgebra M ι),
  (f + g).toDirectSum = f.toDirectSum + g.toDirectSum
-- Mathlib.Data.Finsupp.Basic
Finsupp.mk_mem_graph : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) {a : α}, a ∈ f.support → (a, f a) ∈ f.graph
-- Mathlib.Data.Set.Card
Set.union_ne_univ_of_ncard_add_ncard_lt : ∀ {α : Type u_1} {s t : Set α}, s.ncard + t.ncard < Nat.card α → s ∪ t ≠ Set.univ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `H⁰(G, A)` is isomorphic
to the kernel of `ρ(g) - Id(A)`.  -/
Rep.FiniteCyclicGroup.groupCohomologyIso₀ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      (A : Rep.{u, u, u} k G) →
        (g : G) →
          (∀ (x : G), x ∈ Subgroup.zpowers g) →
            (groupCohomology A 0 ≅
              ModuleCat.of k ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker)
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.renameFunAuxImage : ∀ {σ : Type u_1} {τ : Type u_2} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : DecidableEq σ]
  [inst_2 : DecidableEq τ] (x : τ →₀ ℕ),
  Finset.image
      (fun x =>
        match x with
        | (fst, b) => (b.1 + b.2, b))
      ⋯.toFinset =
    ⋯.toFinset
-- Mathlib.Algebra.Order.Group.Defs
LinearOrderedAddCommGroup.to_noMaxOrder : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α], NoMaxOrder α
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.mem_chartAt_source_of_eq_one : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s) {i : ι}
  {x : M}, ↑(fs.toFun i) x = 1 → x ∈ (chartAt H (fs.c i)).source
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instCompleteLattice.eq_1 : ∀ (M : Type u_1) [inst : AddZeroClass M],
  SaturatedAddSubmonoid.instCompleteLattice M =
    { toPartialOrder := inferInstance, sup := SemilatticeSup.sup, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯,
      inf := Lattice.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯,
      toSupSet := (AddSubmonoid.giSaturation M).liftCompleteLattice.toSupSet, isLUB_sSup := ⋯,
      toInfSet := inferInstance.toInfSet, isGLB_sInf := ⋯, toTop := inferInstance, le_top := ⋯,
      toOrderBot := (AddSubmonoid.giSaturation M).liftCompleteLattice.toOrderBot }
-- Mathlib.Algebra.Group.Int.TypeTags
Int.toAdd_zpow : ∀ (a : Multiplicative ℤ) (b : ℤ), Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
-- Mathlib.ModelTheory.Definability
/-- The set where two definable functions agree is definable.  -/
Set.DefinableFun.ofPred_eq : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {A : Set M} {f g : (α → M) → M},
  Set.DefinableFun L A f → Set.DefinableFun L A g → A.Definable L {v | f v = g v}
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.isInducing_inducingFn : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F], Topology.IsInducing ⇑(ContinuousLinearMapWOT.inducingFn σ E F)
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instRightCancelSemigroup : {α : Type u_1} → [LeftCancelSemigroup α] → RightCancelSemigroup αᵐᵒᵖ
-- Mathlib.CategoryTheory.Monoidal.Functor.Types
CategoryTheory.ε_def : ∀ (F : Type u_1 → Type u_2) [inst : Applicative F] [inst_1 : LawfulApplicative F],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.ofTypeFunctor F) = TypeCat.ofHom fun x => pure PUnit.unit
-- Init.Control.Lawful.Basic
/-- Lawful monads are those that satisfy a certain behavioral specification. While all instances of
`Monad` should satisfy these laws, not all implementations are required to prove this.

`LawfulMonad.mk'` is an alternative constructor that contains useful defaults for many fields.
 -/
LawfulMonad : (m : Type u → Type v) → [Monad m] → Prop
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.prob_add_prob_compl : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasurableSet s → μ s + μ sᶜ = 1
-- Mathlib.Data.Fintype.Order
Set.Finite.exists_ge : ∀ {α : Type u_2} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {s : Set α}, s.Finite → ∃ M, ∀ i ∈ s, M ≤ i
-- Lean.Elab.Tactic.Grind.Main
_private.Lean.Elab.Tactic.Grind.Main.0.Lean.Elab.Tactic.elabGrindPattern.go : Option (Lean.TSyntax `ident) →
  Lean.TSyntax `ident →
    Lean.Syntax.TSepArray `term "," →
      Option (Lean.TSyntax `Lean.Parser.Command.grindPatternCnstrs) →
        Lean.AttributeKind → Lean.Elab.Command.CommandElabM Unit
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.TreeMap.Raw.maxEntryD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α × β → α × β
-- Mathlib.Data.Set.Sups
Set.sups_eq_self : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α}, s ⊻ s = s ↔ SupClosed s
-- Mathlib.RingTheory.Polynomial.Quotient
/-- For a commutative ring $R$, evaluating a polynomial at an element $y \in R$ induces an
isomorphism of $R$-algebras $R[X] / \langle x, X - y \rangle \cong R / \langle x \rangle$.  -/
Polynomial.quotientSpanCXSubCAlgEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    (x y : R) → (Polynomial R ⧸ Ideal.span {Polynomial.C x, Polynomial.X - Polynomial.C y}) ≃ₐ[R] R ⧸ Ideal.span {x}
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.Computability.TuringMachine.Tape
/-- The quotient map turning a `List` into a `ListBlank`.  -/
Turing.ListBlank.mk : {Γ : Type u_1} → [inst : Inhabited Γ] → List Γ → Turing.ListBlank Γ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → (Std.DTreeMap.Raw.Const.unitOfList l cmp).size = l.length
-- Mathlib.Algebra.Ring.Divisibility.Basic
dvd_iff_dvd_of_dvd_sub : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b - c → (a ∣ b ↔ a ∣ c)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.mem_toSet_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  (f : CategoryTheory.Arrow C), f ∈ P.toSet ↔ P f.hom
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_zero : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M], ⇑0 = 1
-- Mathlib.RingTheory.Congruence.Basic
/-- The algebra morphism from `R` to the quotient by a ring congruence.  -/
RingCon.mkₐ : (α : Type u_1) →
  {R : Type u_3} →
    [inst : CommSemiring α] → [inst_1 : Semiring R] → [inst_2 : Algebra α R] → (c : RingCon R) → R →ₐ[α] c.Quotient
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} {B : Type w} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  [inst_7 : SizeOf R] [inst_8 : SizeOf A] [inst_9 : SizeOf B] (toCoalgEquiv : A ≃ₗc[R] B)
  (map_mul' : ∀ (x y : A), toCoalgEquiv.toFun (x * y) = toCoalgEquiv.toFun x * toCoalgEquiv.toFun y),
  sizeOf { toCoalgEquiv := toCoalgEquiv, map_mul' := map_mul' } = 1 + sizeOf toCoalgEquiv
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} {x : α}
  {y : β}, ContinuousWithinAt f s x → ContinuousWithinAt g t y → ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_induction_nonempty : ∀ {M : Type u_3} [inst : CommMonoid M] {s : Multiset M} (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a * b)) → s ≠ ∅ → (∀ a ∈ s, p a) → p s.prod
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- **Riesz's theorem**: a T2 topological vector space over a complete non-trivial normed field
which admits a totally bounded neighborhood of `0` is finite-dimensional.  -/
FiniteDimensional.of_totallyBounded_nhds_zero : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {Eᵤ : Type u_6} [inst_2 : AddCommGroup Eᵤ]
  [inst_3 : Module 𝕜 Eᵤ] [inst_4 : UniformSpace Eᵤ] [T2Space Eᵤ] [IsUniformAddGroup Eᵤ] [ContinuousSMul 𝕜 Eᵤ]
  {U : Set Eᵤ}, U ∈ nhds 0 → TotallyBounded U → FiniteDimensional 𝕜 Eᵤ
-- Mathlib.Data.PFunctor.Multivariate.W
/-- A path from the root of a tree to one of its node  -/
MvPFunctor.WPath : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → P.last.W → Fin2 n → Type u
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
/-- Pull an opposite additive subsemigroup back to a subsemigroup
along `AddOpposite.op`  -/
AddSubsemigroup.unop : {M : Type u_2} → [inst : Add M] → AddSubsemigroup Mᵃᵒᵖ → AddSubsemigroup M
-- Mathlib.Algebra.Homology.BifunctorHomotopy
HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} (f₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂}
  {f₂ f₂' : K₂ ⟶ L₂} (h₂ : Homotopy f₂ f₂') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (i₁ : I₁) (i₂ i₂' : I₂) (j j' : J) (h : c₁.π c₂ c (i₁, i₂') = j),
  c₂.prev i₂' = i₂ →
    ∀ {Z : D} (h_1 : (L₁.mapBifunctor L₂ F c).X j' ⟶ Z),
      CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h)
          (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMapHomotopy.hom₂ f₁ h₂ F c j j') h_1) =
        CategoryTheory.CategoryStruct.comp
          (c₁.ε₂ c₂ c (i₁, i₂) •
            CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂'))
              (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (h₂.hom i₂' i₂))
                (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j')))
          h_1
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.pi : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup F]
  [inst_2 : TopologicalSpace F] [inst_3 : Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8}
  [inst_4 : (i : ι) → AddCommGroup (E i)] [inst_5 : (i : ι) → Module 𝕜 (E i)]
  [inst_6 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {f : (i : ι) → α → E i},
  (∀ (i : ι), f i =o[𝕜; l] g) → (fun x i => f i x) =o[𝕜; l] g
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Intersection of two `1`-hypercovers.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.inter : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {S : C} →
        [CategoryTheory.Limits.HasPullbacks C] →
          (E : J.OneHypercover S) →
            (F : J.OneHypercover S) →
              [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] →
                [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
                      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
                        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] →
                  J.OneHypercover S
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_op : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx (Lean.Grind.AC.Seq.cons x s) =
    ctx.op (Lean.Grind.AC.Var.denote ctx x) (Lean.Grind.AC.Seq.denote ctx s)
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.NotPowerCertificate.mk.sizeOf_spec : ∀ {m n : Q(ℕ)} (k : Q(ℕ)) (pf_left : Q(«$k» ^ «$n» < «$m»)) (pf_right : Q(«$m» < («$k» + 1) ^ «$n»)),
  sizeOf { k := k, pf_left := pf_left, pf_right := pf_right } = 1 + sizeOf k + sizeOf pf_left + sizeOf pf_right
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits of shape `Jᵒᵖ`, then `F : C ⥤ D` preserves colimits
of shape `J`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F.op], CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.support_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (p : PMF α), (PMF.map f p).support = f '' p.support
-- Mathlib.Algebra.Category.Ring.Epi
RingHom.surjective_of_epi_of_finite : ∀ {R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.Epi f],
  (CommRingCat.Hom.hom f).Finite → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.checkInstances : Lean.Option Bool
-- Mathlib.ModelTheory.Order
/-- The language homomorphism sending the unique symbol `≤` of `Language.order` to `≤` in an ordered
language.  -/
FirstOrder.Language.orderLHom : (L : FirstOrder.Language) → [L.IsOrdered] → FirstOrder.Language.order →ᴸ L
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (p : Z ⟶ X) (g : Z ⟶ Y),
  CategoryTheory.CategoryStruct.comp (G.map p) f = G.map g →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F f) (F.obj.map p.op) =
      F.obj.map g.op
-- Init.Data.Vector.Basic
_private.Init.Data.Vector.Basic.0.Vector.flatMapM.go : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {n : ℕ} →
      {β : Type u_1} →
        {k : ℕ} →
          [Monad m] → Vector α n → (α → m (Vector β k)) → (i : ℕ) → i ≤ n → Vector β (i * k) → m (Vector β (n * k))
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.continuousAt_fderiv : ∀ {𝕜 : 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} {x : E}
  {n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → n ≠ 0 → ContinuousAt (fderiv 𝕜 f) x
-- Init.Data.Fin.OverflowAware
Fin.addNat?_eq_some : ∀ {n m : ℕ} {i : Fin n} (h : ↑i + m < n), i.addNat? m = some ⟨↑i + m, h⟩
-- Init.Prelude
/-- Alias for `Or.inr`.  -/
Or.intro_right : ∀ {b : Prop} (a : Prop), b → a ∨ b
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatTrans_id : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W],
  RF.rightDerivedNatTrans RF α α W (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id RF
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_div_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E), Metric.ball x δ / {y} = Metric.ball (x / y) δ
-- Lean.Data.NameTrie
Lean.NamePart.lt : Lean.NamePart → Lean.NamePart → Bool
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.GrothendieckTopology.instIsStableUnderBaseChangeToPrecoverage : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] (J : CategoryTheory.GrothendieckTopology C),
  J.toPrecoverage.IsStableUnderBaseChange