mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.oreDiv_add_oreDiv : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] {r r' : X} {s s' : ↥S},
  r /ₒ s + r' /ₒ s' =
    (OreLocalization.oreDenom (↑s) s' • r + OreLocalization.oreNum (↑s) s' • r') /ₒ
      (OreLocalization.oreDenom (↑s) s' * s)
-- Lean.Elab.InfoTree.Types
Lean.Elab.MacroExpansionInfo.mk.sizeOf_spec : ∀ (lctx : Lean.LocalContext) (stx output : Lean.Syntax),
  sizeOf { lctx := lctx, stx := stx, output := output } = 1 + sizeOf lctx + sizeOf stx + sizeOf output
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.LocallyQuasiFinite.quasiFinite_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.LocallyQuasiFinite f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).QuasiFinite
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.RwKind.valid.injEq : ∀ (motiveTypeCorrect : Bool) (occ : Option ℕ) (motiveTypeCorrect_1 : Bool) (occ_1 : Option ℕ),
  (Mathlib.Tactic.ClickSuggestions.RwKind.valid motiveTypeCorrect occ =
      Mathlib.Tactic.ClickSuggestions.RwKind.valid motiveTypeCorrect_1 occ_1) =
    (motiveTypeCorrect = motiveTypeCorrect_1 ∧ occ = occ_1)
-- Mathlib.Data.ENat.Basic
RingHom.ENatMap_apply : ∀ {S : Type u_2} [inst : CommSemiring S] [inst_1 : PartialOrder S] [inst_2 : CanonicallyOrderedAdd S]
  [inst_3 : DecidableEq S] [inst_4 : Nontrivial S] (f : ℕ →+* S) (hf : Function.Injective ⇑f),
  ⇑(f.ENatMap hf) = (↑(f.toMonoidWithZeroHom.ENatMap hf)).toFun
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- *Weak approximation for infinite places*
The number field `K` is dense when embedded diagonally in the product
`(v : InfinitePlace K) → WithAbs v.1`, in which `WithAbs v.1` represents `K` equipped with the
topology coming from the infinite place `v`.
 -/
NumberField.InfinitePlace.denseRange_algebraMap_pi : ∀ (K : Type u_1) [inst : Field K] [NumberField K],
  DenseRange ⇑(algebraMap K ((v : NumberField.InfinitePlace K) → WithAbs ↑v))
-- Mathlib.Order.WithBot
WithBot.map_bot : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), WithBot.map f ⊥ = ⊥
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ [Algebra.IsAlgebraic F L], Module.rank ↥A ↥(IntermediateField.extendScalars ⋯) = Module.rank F L
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_iInf : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_3} [Finite ι] {f : ι → Subgroup G},
  (∀ (i : ι), (f i).FiniteIndex) → (⨅ i, f i).FiniteIndex
-- Mathlib.CategoryTheory.Yoneda
/-- The identity functor on `Type v` is corepresented by `PUnit`.  -/
CategoryTheory.Functor.CorepresentableBy.id : (CategoryTheory.Functor.id (Type v)).CorepresentableBy PUnit.{v + 1}
-- Init.Data.List.Basic
List.append.eq_def : ∀ {α : Type u_1} (x x_1 : List α),
  x.append x_1 =
    match x, x_1 with
    | [], bs => bs
    | a :: as, bs => a :: as.append bs
-- Mathlib.Analysis.Complex.JensenFormula
/-- If  `g : ℂ → ℂ` is analytic without zero on the closed ball with center `c` and radius `R`, then the
circle average `circleAverage (log ‖g ·‖) c R` equals `log ‖g c‖`.
 -/
AnalyticOnNhd.circleAverage_log_norm_of_ne_zero : ∀ {R : ℝ} {c : ℂ} {g : ℂ → ℂ},
  AnalyticOnNhd ℂ g (Metric.closedBall c |R|) →
    (∀ u ∈ Metric.closedBall c |R|, g u ≠ 0) → Real.circleAverage (fun x => Real.log ‖g x‖) c R = Real.log ‖g c‖
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- Simplices of the standard simplex identify to morphisms in `SimplexCategory`.  -/
SSet.stdSimplex.objEquiv : {n : SimplexCategory} → {m : SimplexCategoryᵒᵖ} → (SSet.stdSimplex.obj n).obj m ≃ (Opposite.unop m ⟶ n)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 → W.negMap ⟦P⟧ = ⟦![P 0 / P 2 ^ 2, W.toAffine.negY (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3), 1]⟧
-- Lean.Elab.Quotation
/-- match step based on kind and, optionally, arity of discriminant
If `arity` is given, that number of new discriminants is introduced. `covered` patterns should then introduce the
same number of new patterns.
We actually check the arity at run time only in the case of `null` nodes since it should otherwise by implied by
the node kind.
without arity: `($x:k)
with arity: any quotation without an antiquotation head pattern  -/
Lean.Elab.Term.Quotation.HeadCheck.shape : List Lean.SyntaxNodeKind → Option ℕ → Lean.Elab.Term.Quotation.HeadCheck
-- Batteries.Data.List.Basic
/-- Tail-recursive helper function for `scanlM` and `scanrM`  -/
List.scanAuxM : {m : Type u_1 → Type u_2} → {β : Type u_1} → {α : Type u_3} → [Monad m] → (β → α → m β) → β → List α → m (List β)
-- Init.Data.Nat.Lemmas
Nat.mul_eq_left : ∀ {a b : ℕ}, a ≠ 0 → (a * b = a ↔ b = 1)
-- Mathlib.Order.UpperLower.Closure
/-- `upperClosure` forms a reversed Galois insertion with the coercion from upper sets to sets.  -/
giUpperClosureCoe : {α : Type u_1} →
  [inst : Preorder α] → GaloisInsertion (⇑OrderDual.toDual ∘ upperClosure) (SetLike.coe ∘ ⇑OrderDual.ofDual)
-- Mathlib.Algebra.Order.AddTorsor
instCovariantClassHSMulLeOfIsOrderedSMul : ∀ {G : Type u_1} {P : Type u_2} [inst : LE G] [inst_1 : LE P] [inst_2 : SMul G P] [IsOrderedSMul G P],
  CovariantClass G P (fun x1 x2 => x1 • x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has countable coproducts is said to have countable `AB4Star` provided that
countable products are exact.
 -/
CategoryTheory.CountableAB4Star : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasCountableProducts C] → Prop
-- Mathlib.Tactic.NormNum.GCD
/-- Evaluates the `Int.lcm` function.  -/
Mathlib.Meta.NormNum.evalIntLCM : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.add_comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b : X ⟶ Y), a + b = b + a
-- Mathlib.Order.CompleteLattice.Basic
sSup_le_sSup_of_subset_insert_bot : ∀ {α : Type u_1} [inst : CompleteLattice α] {s t : Set α}, s ⊆ insert ⊥ t → sSup s ≤ sSup t
-- Std.Time.Date.PlainDate
/-- The day component of the date. It is represented as an `Ordinal` type from `Day`.  -/
Std.Time.PlainDate.day : Std.Time.PlainDate → Std.Time.Day.Ordinal
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Equivalence.isLeftAdjoint_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.inverse.IsLeftAdjoint
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux2 : ∀ {H : Type u_1} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H']
  [inst_2 : TopologicalSpace M'] [inst_3 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ (g : H → M') {x : H} {s : Set H},
      f ∈ StructureGroupoid.maximalAtlas M' G' →
        g x ∈ f.source → ContinuousWithinAt g s x → (P (↑(chartAt H' (g x)) ∘ g) s x ↔ P (↑f ∘ g) s x)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The preimage of a set `s` under a linear map `f` with nonzero determinant has measure
equal to `μ s` times the absolute value of the inverse of the determinant of `f`.  -/
MeasureTheory.Measure.addHaar_preimage_linearMap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E →ₗ[ℝ] E},
  LinearMap.det f ≠ 0 → ∀ (s : Set E), μ (⇑f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s
-- Std.Http.Data.URI.Basic
Std.Http.instToStringURI : ToString Std.Http.URI
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context.mk.sizeOf_spec : ∀ (toIntId : ℕ), sizeOf { toIntId := toIntId } = 1 + sizeOf toIntId
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.instNormalizationMonoid : {R : Type u} → [inst : CommRing R] → [NoZeroDivisors R] → [NormalizationMonoid R] → NormalizationMonoid (Polynomial R)
-- Mathlib.Algebra.Group.Defs
CommGroup.toCancelCommMonoid.eq_1 : ∀ {G : Type u_1} [inst : CommGroup G],
  CommGroup.toCancelCommMonoid = { toMonoid := inst.toMonoid, mul_comm := ⋯, toIsLeftCancelMul := ⋯ }
-- Batteries.Recycling.RBTree.Lemmas
/-- The list of elements to the left of the hole.
(This function is intended for specification purposes only.)  -/
RBTree.RBNode.Path.listL : {α : Type u_1} → RBTree.RBNode.Path α → List α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_inj_of_lt_of_lt_pi_div_two : ∀ {x y : ℝ},
  -(Real.pi / 2) < x → x < Real.pi / 2 → -(Real.pi / 2) < y → y < Real.pi / 2 → Real.tan x = Real.tan y → x = y
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The Hecke coset module with coefficients in `Z`: the finitely-supported `Z`-linear
combinations of double cosets `H₁\Δ/H₂`. For `H₁ = H₂` this is the underlying module of the
Hecke ring `𝕋 Δ H Z` (see `HeckeRing`). The coefficients `Z` need only carry a `Zero` for the
type to make sense; algebraic structure is added by the instances below at the weakest level each
requires.  -/
HeckeCosetModule : {G : Type u_1} →
  [inst : Group G] → Submonoid G → Subgroup G → Subgroup G → (Z : Type u_2) → [Zero Z] → Type (max u_2 u_1)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.aut_one : ∀ {S : Type u_1} {R : Type u_2} [inst : Mul R] [inst_1 : Add R] [inst_2 : Star R] [inst_3 : SMul S R],
  1 = StarAlgEquiv.refl S R
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.powers_toFun : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R) (n : ℕ),
  (HahnSeries.SummableFamily.powers x) n = (if 0 < x.orderTop then x else 0) ^ n
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_performRupCheck_insertRup : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ),
      ((f.insertRupUnits c.negate).1.performRupCheck rupHints).2.2.1 = true →
        Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f (f.insert c)
-- Mathlib.Topology.UniformSpace.HeineCantor
/-- A continuous family of functions `α → β → γ` tends uniformly to its value at `x`
if `α` is weakly locally compact and `β` is compact.  -/
Continuous.tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [WeaklyLocallyCompactSpace α] [CompactSpace β] [inst_4 : UniformSpace γ] (f : α → β → γ),
  Continuous ↿f → ∀ (x : α), TendstoUniformly f (f x) (nhds x)
-- Lean.Meta.Tactic.Grind.AC.Util
_private.Lean.Meta.Tactic.Grind.AC.Util.0.Lean.Meta.Grind.AC.getOpId?.go : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.CategoryTheory.Comma.Final
/-- Let `A` and `B` be filtered categories, `R : B ⥤ T` be final and `L : A ⥤ T`. Then, the
comma category `Comma L R` is filtered.  -/
CategoryTheory.Comma.isFiltered_of_final : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsFiltered A] [CategoryTheory.IsFiltered B] [R.Final],
  CategoryTheory.IsFiltered (CategoryTheory.Comma L R)
-- Mathlib.Algebra.Notation.Prod
Prod.snd_inv : ∀ {G : Type u_8} {H : Type u_9} [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.2 = p.2⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.map_comp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasEnd F'] (f : F ⟶ F')
  {F'' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_4 : CategoryTheory.Limits.HasEnd F'']
  (g : F' ⟶ F''),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.map f) (CategoryTheory.Limits.end_.map g) =
    CategoryTheory.Limits.end_.map (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.wideCospan_obj : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C)
  (arrows : (j : J) → objs j ⟶ B) (j : CategoryTheory.Limits.WidePullbackShape J),
  (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows).obj j = Option.casesOn j B objs
-- Mathlib.CategoryTheory.Limits.FintypeCat
equivEquivIso.eq_1 : ∀ {X Y : Type u}, equivEquivIso = equivIsoIso.toEquiv
-- Mathlib.Algebra.Group.Equiv.Defs
EmbeddingLike.map_ne_one_iff : ∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M}, f x ≠ 1 ↔ x ≠ 1
-- Mathlib.Order.SymmDiff
inf_symmDiff_distrib_left : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α), a ⊓ symmDiff b c = symmDiff (a ⊓ b) (a ⊓ c)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_norm : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.core_cert lhs rhs p = true →
    Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs →
      Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.Logic.Equiv.Defs
Equiv.forall_congr : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β),
  (∀ (a : α), p a ↔ q (e a)) → ((∀ (a : α), p a) ↔ ∀ (b : β), q b)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Indep.contract_isBase_iff : ∀ {α : Type u_1} {M : Matroid α} {I B : Set α}, M.Indep I → ((M.contract I).IsBase B ↔ M.IsBase (B ∪ I) ∧ Disjoint B I)
-- Mathlib.RingTheory.Bialgebra.Quotient
Bialgebra.Quotient.mkBialgHom_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Bialgebra R A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] [inst_4 : (Submodule.restrictScalars R I).IsCoideal] (a : A),
  (Bialgebra.Quotient.mkBialgHom I) a = (Ideal.Quotient.mk I) a
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A functor `WithInitial C ⥤ D` can be seen as an element of the comma category
`Comma (const C) (𝟭 (C ⥤ D))`.  -/
CategoryTheory.WithInitial.mkCommaObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor (CategoryTheory.WithInitial C) D →
          CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D))
-- Mathlib.Order.CompleteLatticeIntervals
Set.Iic.coe_biInf : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLattice α] {a : α} (f : ι → ↑(Set.Iic a)) (p : ι → Prop),
  ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.continuousOn_evenKernel : ∀ (a : UnitAddCircle), ContinuousOn (HurwitzZeta.evenKernel a) (Set.Ioi 0)
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.lift.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePair R) (x x_1 : S) (e_x : x = x_1) (h : P.HasMap x), P.lift x h = P.lift x_1 ⋯
-- Mathlib.Algebra.Homology.Bifunctor
/-- The second differential on a summand of `mapBifunctor K₁ K₂ F c`  -/
HomologicalComplex.mapBifunctor.d₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [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] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            (K₁ : HomologicalComplex C₁ c₁) →
                              (K₂ : HomologicalComplex C₂ c₂) →
                                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  [inst_6 : F.PreservesZeroMorphisms] →
                                    [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      (c : ComplexShape J) →
                                        [inst_8 : TotalComplexShape c₁ c₂ c] →
                                          [inst_9 : K₁.HasMapBifunctor K₂ F c] →
                                            [inst_10 : DecidableEq J] →
                                              (i₁ : I₁) →
                                                (i₂ : I₂) →
                                                  (j : J) →
                                                    (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X j
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart.instSigmaFinite : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ],
  MeasureTheory.SigmaFinite (μ.singularPart ν)
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- (Implementation). Use `openCoverOfBase` instead.  -/
AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' : {X Y Z : AlgebraicGeometry.Scheme} →
  Z.OpenCover → (f : X ⟶ Z) → (g : Y ⟶ Z) → (CategoryTheory.Limits.pullback f g).OpenCover
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.smul_mem' : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (self : ConvexCone R M) ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ self.carrier → c • x ∈ self.carrier
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.map_coe : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous f → ∀ (a : α), UniformSpace.Completion.map f ↑a = ↑(f a)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv_apply : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M']
  [inst_5 : Module R M'] [inst_6 : TopologicalSpace M'] [inst_7 : AddCommMonoid N] [inst_8 : Module R N]
  [inst_9 : TopologicalSpace N] (e : M ≃L[R] M'),
  ⇑e.continuousAlternatingMapCongrLeftEquiv = fun f => f.compContinuousLinearMap ↑e.symm
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertOffsetZ : Std.Time.OffsetZ → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Order.Interval.Finset.Nat
Finset.range_add_eq_union : ∀ (a b : ℕ), Finset.range (a + b) = Finset.range a ∪ Finset.map (addLeftEmbedding a) (Finset.range b)
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.Entrypoint.relabelNat' : {α : Type} →
  [inst : DecidableEq α] → [inst_1 : Hashable α] → Std.Sat.AIG.Entrypoint α → Std.Sat.AIG.Entrypoint ℕ × Std.HashMap α ℕ
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.continuousOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {c : NNReal}, ApproximatesLinearOn f f' s c → ContinuousOn f s
-- Mathlib.Geometry.Euclidean.Volume.Measure
instIsAddRightInvariantEuclideanHausdorffMeasureOfIsIsometricVAddAddOpposite : ∀ {X : Type u_1} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] [inst_3 : AddGroup X]
  [IsIsometricVAdd Xᵃᵒᵖ X] (d : ℕ), (MeasureTheory.Measure.euclideanHausdorffMeasure d).IsAddRightInvariant
-- Init.Data.String.Bootstrap
String.Pos.Raw.Internal.sub : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, panicking if no such key exists.
 -/
Std.ExtTreeMap.getKeyGE! : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeMap α β cmp → α → α
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mem_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (x : G), x ∈ K.toAddSubmonoid ↔ x ∈ K
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesCokernel.π_iso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] {Z : D}
  (h : CategoryTheory.Limits.cokernel (G.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.π f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G f).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (G.map f)) h
-- Init.Grind.Attr
/-- Like `@[lia]`, but also prints the pattern(s) selected by `lia` as info messages.  -/
Lean.Parser.Attr.lia? : Lean.ParserDescr
-- Mathlib.Order.Fin.Basic
Fin.strictMono_castSucc : ∀ {n : ℕ}, StrictMono Fin.castSucc
-- Lean.Elab.Tactic.Config
/-- Elaborates a tactic configuration.  -/
Lean.Elab.Tactic.elabConfig : Bool → Lean.Name → Array Lean.Elab.Tactic.ConfigItemView → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.Normed.Lp.PiLp
_private.Mathlib.Analysis.Normed.Lp.PiLp.0.PiLp.edist_apply_le_edist_aux : ∀ {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [Fact (1 ≤ p)] [inst : (i : ι) → PseudoEMetricSpace (β i)]
  [inst_1 : Fintype ι] (x y : PiLp p β) (i : ι), edist (x.ofLp i) (y.ofLp i) ≤ edist x y
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tsum_setProd_singleton_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Set β)
  (c : γ) (f : β × γ → α), ∑' (x : ↑(s ×ˢ {c})), f ↑x = ∑' (b : ↑s), f (↑b, c)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.instIsStrictlyGEMidHAddIntOfNat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)],
  (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.mid✝ f n₀).IsStrictlyGE (n₀ + 1)