mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- **Alias** of `CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_lift`. -/
CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D}
  (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F) {c : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit (h.functor.obj c)) (s : CategoryTheory.Limits.Cone G),
  ((CategoryTheory.Limits.IsLimit.ofConeEquiv h) P).lift s =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (h.unitIso.hom.app s).hom
        (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom)
      (h.unitIso.inv.app c).hom
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.toUnconditionalSchauderBasis_coord : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (i : ι),
  b.toUnconditionalSchauderBasis.coord i = (innerSL 𝕜) (b i)
-- Mathlib.Data.Nat.Basic
/-- A subset of `ℕ` containing `k : ℕ` and closed under `Nat.succ` contains every `n ≥ k`.  -/
Nat.set_induction_bounded : ∀ {n k : ℕ} {S : Set ℕ}, k ∈ S → (∀ k ∈ S, k + 1 ∈ S) → k ≤ n → n ∈ S
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instDiv : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : DivisionRing R] → (v : Valuation R Γ₀) → Div (WithVal v)
-- Batteries.Control.AlternativeMonad
StateT.instAlternativeMonad : {σ : Type u_1} → (m : Type u_1 → Type u_2) → [AlternativeMonad m] → AlternativeMonad (StateT σ m)
-- Init.Data.List.Nat.InsertIdx
List.length_insertIdx : ∀ {α : Type u} {a : α} {i : ℕ} {as : List α},
  (as.insertIdx i a).length = if i ≤ as.length then as.length + 1 else as.length
-- Mathlib.Data.Finite.Defs
Set.infinite_or_finite : ∀ {α : Type u} (s : Set α), s.Infinite ∨ s.Finite
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An object `Y` is terminal iff for every `X` there is a unique morphism `X ⟶ Y`.  -/
CategoryTheory.Limits.isTerminalEquivUnique : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{1}) C) →
      (Y : C) →
        CategoryTheory.Limits.IsLimit
            { pt := Y,
              π := { app := fun X => id (CategoryTheory.Discrete.casesOn X fun as => ⋯.elim), naturality := ⋯ } } ≃
          ((X : C) → Unique (X ⟶ Y))
-- Init.Data.Vector.Lex
Vector.lt_irrefl : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2] (xs : Vector α n), ¬xs < xs
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_ofList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l → (Std.HashMap.ofList l).size = l.length
-- Init.Data.String.Slice
String.Slice.instOrd : Ord String.Slice
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_of_aestronglyMeasurable_trim : ∀ {β : Type u_2} [inst : TopologicalSpace β] {α : Type u_5} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) {f : α → β}, MeasureTheory.AEStronglyMeasurable f (μ.trim hm) → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.isCyclicallyReduced : ∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.IsReduced L → FreeAddGroup.IsCyclicallyReduced (FreeAddGroup.reduceCyclically L)
-- Mathlib.Order.Interval.Finset.Nat
Nat.range_succ_eq_Icc_zero : ∀ (n : ℕ), Finset.range (n + 1) = Finset.Icc 0 n
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.next.eq_1 : ∀ (x : String.Pos.Raw) (s : String) (b stopPos : String.Pos.Raw),
  { str := s, startPos := b, stopPos := stopPos }.next x =
    if x.offsetBy b = stopPos then x else { byteIdx := (String.Pos.Raw.next s (x.offsetBy b)).byteIdx - b.byteIdx }
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.notMem_neLocus : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → Zero (N a)] {f g : Π₀ (a : α), N a} {a : α}, a ∉ f.neLocus g ↔ f a = g a
-- Mathlib.Logic.Function.Basic
Function.surjective_eval : ∀ {α : Sort u} {β : α → Sort v} [h : ∀ (a : α), Nonempty (β a)] (a : α), Function.Surjective (Function.eval a)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.restrictScalarsEmbedding.eq_1 : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M],
  Submodule.restrictScalarsEmbedding S R M = { toFun := Submodule.restrictScalars S, inj' := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
CategoryTheory.MonoidalCategory.Limits.colimit.ι_desc_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {J : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F) (j : J) {Q : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.colimit.ι F j) Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.colimit.desc F c) Q) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (c.ι.app j) Q
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_countable : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] (f : α → ENNReal)
  {s : Set α}, s.Countable → ∫⁻ (a : α) in s, f a ∂μ = ∑' (a : ↑s), f ↑a * μ {↑a}
-- Mathlib.Data.EReal.Basic
EReal.coe_eq_zero : ∀ {x : ℝ}, ↑x = 0 ↔ x = 0
-- Lean.Parser.Term
Lean.Parser.Term.matchAlts.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Aesop.Forward.State
Aesop.instBEqRawHyp.beq : Aesop.RawHyp → Aesop.RawHyp → Bool
-- Init.Grind.AC
Lean.Grind.AC.Seq.insert.induct_unfolding : ∀ (x : Lean.Grind.AC.Var) (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Prop),
  (∀ (x_1 : Lean.Grind.AC.Var),
      Nat.blt x x_1 = true →
        motive (Lean.Grind.AC.Seq.var x_1) (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.var x_1))) →
    (∀ (x_1 : Lean.Grind.AC.Var),
        ¬Nat.blt x x_1 = true →
          motive (Lean.Grind.AC.Seq.var x_1) (Lean.Grind.AC.Seq.cons x_1 (Lean.Grind.AC.Seq.var x))) →
      (∀ (x_1 : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
          Nat.blt x x_1 = true →
            motive (Lean.Grind.AC.Seq.cons x_1 s) (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.cons x_1 s))) →
        (∀ (x_1 : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
            ¬Nat.blt x x_1 = true →
              motive s (Lean.Grind.AC.Seq.insert x s) →
                motive (Lean.Grind.AC.Seq.cons x_1 s) (Lean.Grind.AC.Seq.cons x_1 (Lean.Grind.AC.Seq.insert x s))) →
          ∀ (s : Lean.Grind.AC.Seq), motive s (Lean.Grind.AC.Seq.insert x s)
-- Aesop.Forward.PremiseIndex
Aesop.instOrdPremiseIndex : Ord Aesop.PremiseIndex
-- Lean.Meta.Closure
Lean.Meta.Closure.ClosureM : Type → Type
-- Mathlib.Algebra.Order.SuccPred
Order.le_sub_one_iff_of_not_isMin : ∀ {α : Type u_1} {x y : α} [inst : Preorder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α],
  ¬IsMin y → (x ≤ y - 1 ↔ x < y)
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.smallPretopology.congr_simp : ∀ (P P_1 : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (e_P : P = P_1)
  (Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [inst_1 : P.IsMultiplicative] [inst_2 : P.RespectsIso]
  [inst_3 : Q.IsStableUnderComposition] [inst_4 : Q.IsStableUnderBaseChange] [inst_5 : Q.HasOfPostcompProperty Q],
  AlgebraicGeometry.Scheme.smallPretopology P Q = AlgebraicGeometry.Scheme.smallPretopology P_1 Q
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instSndPullbackConeOfLeft : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion
    (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeft f g).snd
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.vadd : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s : Set α} {a : α},
  IsUpperSet s → IsUpperSet (a +ᵥ s)
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.integrable : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [inst_3 : LE E],
  MeasureTheory.Supermartingale f ℱ μ → ∀ (i : ι), MeasureTheory.Integrable (f i) μ
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal.eq_6 : ∀ (f g : Turing.ToPartrec.Code),
  Turing.ToPartrec.stepNormal (f.case g) = fun k v =>
    Nat.rec (Turing.ToPartrec.stepNormal f k v.tail) (fun y x => Turing.ToPartrec.stepNormal g k (y :: v.tail)) v.headI
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.next_ofSliceFrom : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : String.Slice.Pos.ofSliceFrom p ≠ s.endPos},
  (String.Slice.Pos.ofSliceFrom p).next h = String.Slice.Pos.ofSliceFrom (p.next ⋯)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.μNatIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C × C),
  (CategoryTheory.Functor.Monoidal.μNatIso F).hom.app X = CategoryTheory.Functor.LaxMonoidal.μ F X.1 X.2
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The center of isomorphic (not necessarily unital or associative) semirings are isomorphic.  -/
NonUnitalSubsemiring.centerCongr : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        R ≃+* S → ↥(NonUnitalSubsemiring.center R) ≃+* ↥(NonUnitalSubsemiring.center S)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Measurable.congr_ae : ∀ {α : Type u_5} {β : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [_hμ : μ.IsComplete] {f g : α → β}, Measurable f → f =ᵐ[μ] g → Measurable g
-- Mathlib.Topology.Instances.CantorSet
preCantorSet.eq_def : ∀ (x : ℕ),
  preCantorSet x =
    match x with
    | 0 => Set.Icc 0 1
    | n.succ => (fun x => x / 3) '' preCantorSet n ∪ (fun x => (2 + x) / 3) '' preCantorSet n
-- Mathlib.Topology.Compactness.CompactSystem
IsCompactSystem.of_IsEmpty : ∀ {α : Type u_1} [IsEmpty α] (S : Set (Set α)), IsCompactSystem S
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.instIsStrictOrderedModuleRat : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  IsStrictOrderedModule ℚ (DivisibleHull M)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationRestrict : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {s : Set X} [MeasureTheory.IsFiniteMeasure μ.variation],
  MeasureTheory.IsFiniteMeasure (μ.restrict s).variation
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_ne_zero_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, MeasureTheory.Measure.count s ≠ 0 ↔ s.Nonempty
-- Init.Data.String.Lemmas.FindPos
String.posGE_toSlice : ∀ {s : String} {p : String.Pos.Raw} (h : p ≤ s.toSlice.rawEndPos), s.toSlice.posGE p h = (s.posGE p h).toSlice
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.SubmersivePresentation.isStandardSmooth : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] [Finite ι] (P : Algebra.SubmersivePresentation R S ι σ), Algebra.IsStandardSmooth R S
-- Mathlib.Topology.AlexandrovDiscrete
gc_nhdsKer_interior : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α], GaloisConnection nhdsKer interior
-- Lean.Declaration
Lean.RecursorVal.mk.inj : ∀ {toConstantVal : Lean.ConstantVal} {all : List Lean.Name} {numParams numIndices numMotives numMinors : ℕ}
  {rules : List Lean.RecursorRule} {k isUnsafe : Bool} {toConstantVal_1 : Lean.ConstantVal} {all_1 : List Lean.Name}
  {numParams_1 numIndices_1 numMotives_1 numMinors_1 : ℕ} {rules_1 : List Lean.RecursorRule} {k_1 isUnsafe_1 : Bool},
  { toConstantVal := toConstantVal, all := all, numParams := numParams, numIndices := numIndices,
        numMotives := numMotives, numMinors := numMinors, rules := rules, k := k, isUnsafe := isUnsafe } =
      { toConstantVal := toConstantVal_1, all := all_1, numParams := numParams_1, numIndices := numIndices_1,
        numMotives := numMotives_1, numMinors := numMinors_1, rules := rules_1, k := k_1, isUnsafe := isUnsafe_1 } →
    toConstantVal = toConstantVal_1 ∧
      all = all_1 ∧
        numParams = numParams_1 ∧
          numIndices = numIndices_1 ∧
            numMotives = numMotives_1 ∧ numMinors = numMinors_1 ∧ rules = rules_1 ∧ k = k_1 ∧ isUnsafe = isUnsafe_1
-- Mathlib.Algebra.Field.Defs
/-- A `DivisionSemiring` is a `Semiring` with multiplicative inverses for nonzero elements.

An instance of `DivisionSemiring K` includes maps `nnratCast : ℚ≥0 → K` and `nnqsmul : ℚ≥0 → K → K`.
Those two fields are needed to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance since we
need to control the specific definitions for some special cases of `K` (in particular `K = ℚ≥0`
itself). See also note [forgetful inheritance].

If the division semiring has positive characteristic `p`, our division by zero convention forces
`nnratCast (1 / p) = 1 / 0 = 0`.  -/
DivisionSemiring : Type u_2 → Type u_2
-- Init.Grind.AC
Lean.Grind.AC.superpose_head_idempotent_cert : Lean.Grind.AC.Var → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Geometry.Convex.Hull
Convexity.IsAffineMap.image_convexHull : ∀ {R : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  {f : X → Y},
  Convexity.IsAffineMap R f → ∀ (s : Set X), f '' (Convexity.convexHull R) s = (Convexity.convexHull R) (f '' s)
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂},
  autoParam Φ.HasRightResolutions
      CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.hasRightResolutions._autoParam →
    CategoryTheory.TwoSquare.GuitartExact
        (CategoryTheory.CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom →
      Φ.IsRightDerivabilityStructure
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff.eq_1 : ∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  (f : AddCircle T → E) (n : ℤ), fourierCoeff f n = ∫ (t : AddCircle T), (fourier (-n)) t • f t ∂AddCircle.haarAddCircle
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.IsQuotient.norm_lift : ∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  {f : NormedAddGroupHom M N}, f.IsQuotient → ∀ {ε : ℝ}, 0 < ε → ∀ (n : N), ∃ m, f m = n ∧ ‖m‖ < ‖n‖ + ε
-- Init.Data.AC
Lean.Data.AC.ContextInformation : Sort u → Sort (max 1 u)
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_mul_trunc : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (f g : PowerSeries R),
  (PowerSeries.trunc n) (f * ↑((PowerSeries.trunc n) g)) = (PowerSeries.trunc n) (f * g)
-- Mathlib.RingTheory.FiniteType
AlgHom.FiniteType.id : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  (AlgHom.id R A).FiniteType
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extInv_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt)
  (w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j)
      CategoryTheory.Limits.Cone.extInv._auto_1),
  (CategoryTheory.Limits.Cone.extInv φ w).inv.hom = φ.inv
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Reinterpret an additive homomorphism as a `ℤ`-linear map.  -/
AddMonoidHom.toIntLinearMap : {M : Type u_8} → {M₂ : Type u_10} → [inst : AddCommGroup M] → [inst_1 : AddCommGroup M₂] → (M →+ M₂) → M →ₗ[ℤ] M₂
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.Finset.Sups
Finset.sdiff_mem_diffs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α} {a b : α},
  a ∈ s → b ∈ t → a \ b ∈ s.diffs t
-- Mathlib.Data.Finset.Insert
Finset.cons_nonempty : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s), (Finset.cons a s h).Nonempty
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a - b‖ ≤ ‖a‖ + ‖b‖
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_erase_univ : ∀ {ι : Type u_1} {π : ι → Sort u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] (i : ι) (f g : (i : ι) → π i),
  (Finset.univ.erase i).piecewise f g = Function.update f i (g i)
-- Mathlib.Analysis.Analytic.Order
/-- A version of **Taylor's theorem** for analytic functions in one variable, with the error
term of the form `z ^ n` times a function analytic at 0.

(See `AnalyticAt.exists_eventuallyEq_sum_add_pow_mul` for a version asserting equality on a
neighbourhood of `0` rather than globally.)  -/
AnalyticAt.exists_eq_sum_add_pow_mul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {f : 𝕜 → E},
  AnalyticAt 𝕜 f 0 →
    ∀ (n : ℕ),
      ∃ F,
        AnalyticAt 𝕜 F 0 ∧
          ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
-- Mathlib.RingTheory.Localization.Finiteness
Submodule.of_localizationSpan : ∀ {R : Type u} [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  (s : Set R), Ideal.span s = ⊤ → (∀ (g : ↑s), (Submodule.localized (Submonoid.powers ↑g) N).FG) → N.FG
-- Mathlib.Order.Fin.Basic
Fin.natAdd_inj : ∀ {n : ℕ} (m : ℕ) {i j : Fin n}, Fin.natAdd m i = Fin.natAdd m j ↔ i = j
-- Mathlib.Algebra.BigOperators.Finsupp.Fin
Finsupp.sum_cons : ∀ {M : Type u_1} [inst : AddCommMonoid M] (n : ℕ) (σ : Fin n →₀ M) (i : M),
  ((Finsupp.cons i σ).sum fun x e => e) = i + σ.sum fun x e => e
-- Mathlib.Topology.Defs.Basic
/-- A topology on `X`.  -/
TopologicalSpace : Type u → Type u
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Expect.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_sum_compl : ∀ {α : Type u_1} (s : Set α), Cardinal.mk ↑s + Cardinal.mk ↑sᶜ = Cardinal.mk α
-- Mathlib.RingTheory.MvPolynomial.Basic
/-- The monomials form a basis on `MvPolynomial σ R`.  -/
MvPolynomial.basisMonomials : (σ : Type u) → (R : Type v) → [inst : CommSemiring R] → Module.Basis (σ →₀ ℕ) R (MvPolynomial σ R)
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousAt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α},
  UpperSemicontinuousAt f x ↔ ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhds x, f x' < y
-- Mathlib.Order.Atoms
Set.Iio_eq_singleton_bot_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Set.Iio a = {⊥} ↔ IsAtom a
-- Mathlib.Algebra.Tropical.Basic
Tropical.tropEquiv_coe_fn : ∀ {R : Type u}, ⇑Tropical.tropEquiv = Tropical.trop
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_erase_eq_of_not_compare_eq_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, ¬cmp k (t.max ⋯) = Ordering.eq → (t.erase k).max he = t.max ⋯
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.WF.mk : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.inner.WF → t.WF
-- Std.Time.Date.Unit.Weekday
/-- Converts a `Ordinal` representing a day index into a corresponding `Weekday`. This function is useful
for mapping numerical representations to days of the week.
 -/
Std.Time.Weekday.ofOrdinal : Std.Time.Weekday.Ordinal → Std.Time.Weekday
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The inclusion functor `BifibrantObject.HoCat C ⥤ FibrantObject.HoCat C`.  -/
HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject.HoCat C) (HomotopicalAlgebra.FibrantObject.HoCat C)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- If `M` is a faithfully flat module, then for all linear maps `f`, the map `id ⊗ f = 0`, if and only
if `f = 0`.  -/
Module.FaithfullyFlat.zero_iff_lTensor_zero : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [h : Module.FaithfullyFlat R M] {N : Type u_1} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type u_2}
  [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'), f = 0 ↔ LinearMap.lTensor M f = 0
-- Mathlib.Data.Nat.ModEq
Nat.ext_div_modEq_iff : ∀ (n a b : ℕ), a = b ↔ a / n = b / n ∧ a ≡ b [MOD n]
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Groupoid C} {x y : CategoryTheory.Subgroupoid C}, x = y ↔ x.arrows = y.arrows
-- Lean.Server.InfoUtils
_private.Lean.Server.InfoUtils.0.Lean.Elab.InfoTree.goalsAt?.hasNestedTactic : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw → Lean.Elab.InfoTree → Bool
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.testBit.match_1.eq_2 : ∀ (motive : ℤ → ℕ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) n)
  (h_2 : (m n : ℕ) → motive (Int.negSucc m) n),
  (match Int.negSucc m, n with
    | Int.ofNat m, n => h_1 m n
    | Int.negSucc m, n => h_2 m n) =
    h_2 m n
-- Mathlib.Data.Finset.NoncommProd
MonoidHom.pi_ext : ∀ {ι : Type u_2} {γ : Type u_5} [inst : Monoid γ] {M : ι → Type u_6} [inst_1 : (i : ι) → Monoid (M i)] [Finite ι]
  [inst_3 : DecidableEq ι] {f g : ((i : ι) → M i) →* γ},
  (∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)) → f = g
-- Mathlib.Data.ENNReal.Operations
/-- See `ENNReal.eq_sub_of_add_eq'` for a version assuming that `b = a + c` itself is finite rather
than `c`.  -/
ENNReal.eq_sub_of_add_eq : ∀ {a b c : ENNReal}, c ≠ ⊤ → a + c = b → a = b - c
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- If `C` has all colimits of diagrams `parallelFamily f`, then it has all wide coequalizers  -/
CategoryTheory.Limits.hasWideCoequalizers_of_hasColimit_parallelFamily : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)},
      CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelFamily f)],
  CategoryTheory.Limits.HasWideCoequalizers C