mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat.injEq : ∀ (a b : Lean.Expr) (natStructId : ℕ) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) (a_1 b_1 : Lean.Expr)
  (natStructId_1 : ℕ) (lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat a b natStructId lhs rhs =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat a_1 b_1 natStructId_1 lhs_1 rhs_1) =
    (a = a_1 ∧ b = b_1 ∧ natStructId = natStructId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Lean.Parser.Types
Lean.Parser.ParserContextCore.mk : Lean.Parser.InputContext →
  Lean.Parser.ParserModuleContext →
    Lean.Parser.CacheableParserContext → Lean.Parser.TokenTable → Lean.Parser.ParserContextCore
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.mapCechNerve_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g)
  (n : SimplexCategoryᵒᵖ),
  (CategoryTheory.Arrow.mapCechNerve F).app n =
    CategoryTheory.Limits.WidePullback.lift
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom)
        (CategoryTheory.Arrow.Hom.right F))
      (fun i =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i)
          (CategoryTheory.Arrow.Hom.left F))
      ⋯
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The empty word `[]` only reduces to itself.  -/
FreeGroup.Red.nil_iff : ∀ {α : Type u} {L : List (α × Bool)}, FreeGroup.Red [] L ↔ L = []
-- Mathlib.Algebra.Module.SpanRank
/-- A submodule's `spanRank` is finite if and only if it is finitely generated.  -/
Submodule.spanRank_finite_iff_fg : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.spanRank < Cardinal.aleph0 ↔ p.FG
-- Init.Data.UInt.Basic
/-- The power operation, raising a 64-bit unsigned integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
UInt64.pow : UInt64 → ℕ → UInt64
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f f_1 : X ⟶ Z)
  (e_f : f = f_1) [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g g_1 : Y ⟶ Z) (e_g : g = g_1)
  (H :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g H =
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f_1 g_1 ⋯
-- Mathlib.Topology.UniformSpace.Basic
Uniform.continuousAt_iff'_left : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {b : β},
  ContinuousAt f b ↔ Filter.Tendsto (fun x => (f x, f b)) (nhds b) (uniformity α)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.snd_star : ∀ {R : Type u_1} {A : Type u_2} [inst : Star R] [inst_1 : Star A] (x : Unitization R A),
  (star x).toProd.2 = star x.toProd.2
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instMax : {E : Type u_3} → [inst : Group E] → Max (GroupSeminorm E)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_inter_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false →
        Std.DTreeMap.Internal.Impl.Const.getD (m₁.inter m₂ ⋯) k fallback = fallback
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
/-- The property of objects of `C` corresponding to `P : ObjectProperty Cᵒᵖ`.  -/
CategoryTheory.ObjectProperty.unop : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] → CategoryTheory.ObjectProperty Cᵒᵖ → CategoryTheory.ObjectProperty C
-- Mathlib.Data.FunLike.Group
FunLike.addCommGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : Neg F] [inst_5 : Sub F] [inst_6 : SMul ℤ F] [inst_7 : AddCommGroup β]
  [inst_8 : IsZeroApply F α β] [inst_9 : IsAddApply F α β] [inst_10 : IsNegApply F α β] [inst_11 : IsSubApply F α β]
  [inst_12 : IsSMulApply ℕ F α β] [inst_13 : IsSMulApply ℤ F α β],
  FunLike.addCommGroup = Function.Injective.addCommGroup (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Init.Data.Slice.Array.Basic
instSliceableArrayNatSubarray_3 : {α : Type u} → Std.Roc.Sliceable (Array α) ℕ (Subarray α)
-- Mathlib.Algebra.Group.Action.Defs
/-- **Alias** of `vadd_add_vadd_comm`. -/
vadd_add_vadd : ∀ {α : Type u_5} {β : Type u_6} [inst : Add α] [inst_1 : Add β] [inst_2 : VAdd α β] [VAddAssocClass α β β]
  [VAddAssocClass α α β] [VAddCommClass α β β] (a : α) (b : β) (c : α) (d : β), (a +ᵥ b) + (c +ᵥ d) = (a + c) +ᵥ b + d
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.iff_flat_and_formallyUnramified : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.Etale ↔ f.Flat ∧ f.FormallyUnramified ∧ f.FinitePresentation
-- Mathlib.Algebra.Order.IsBotOne
/-- Create an `OrderBot` instance, setting `0` as the bottom element.  -/
IsBotZeroClass.toOrderBot : (α : Type u_1) → [inst : LE α] → [inst_1 : Zero α] → [IsBotZeroClass α] → OrderBot α
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piLTLim_apply : ∀ {ι : Type u_6} [inst : LinearOrder ι] {X : ι → Type u_7} {i : ι} (hi : Order.IsSuccPrelimit i)
  (f : InverseSystem.piLT X i), (InverseSystem.piLTLim hi) f = ⟨fun j => InverseSystem.piLTProj ⋯ f, ⋯⟩
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_dvd' : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) {r : R},
  IsUnit r → p ∣ q → p.scaleRoots r ∣ q.scaleRoots r
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_left_H : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).left.H =
    X.E f₂₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯
-- Lean.Compiler.LCNF.Basic
/-- A literal value.
 -/
Lean.Compiler.LCNF.LetValue.lit : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LitValue → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.tendsto_iterate_fixedPoint : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
  [inst_2 : CompleteSpace α] (x : α),
  Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds (ContractingWith.fixedPoint f hf))
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
Std.IterM.step_takeWhileWithPostcondition : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)},
  (Std.IterM.takeWhileWithPostcondition P it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← (P out).operation
        match __do_lift with
          | ⟨{ down := true }, h'⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.takeWhileWithPostcondition P it') out ⋯))
          | ⟨{ down := false }, h'⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.takeWhileWithPostcondition P it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Finset.finsuppAntidiagEquiv_symm_apply_apply : ∀ {ι : Type u_1} [inst : DecidableEq ι] {s : Finset ι} (n : ℕ) (f : Sym (↥s) n) (a : ↥s),
  ↑((s.finsuppAntidiagEquiv n).symm f) ↑a = Multiset.count a ↑f
-- Mathlib.LinearAlgebra.Determinant
/-- Conjugating a linear map by a linear equiv does not change its determinant.  -/
LinearMap.det_conj : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] {N : Type u_7}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] (f : M →ₗ[A] M) (e : M ≃ₗ[A] N),
  LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f
-- Std.Time.Date.ValidDate
_private.Std.Time.Date.ValidDate.0.Std.Time.Month.Ordinal.cumulativeDays.eq_1 : ∀ (leap : Bool) (month : Std.Time.Month.Ordinal),
  Std.Time.Month.Ordinal.cumulativeDays leap month =
    match Std.Time.Month.Ordinal.cumulativeSizes✝ with
    | ⟨months, p⟩ =>
      let index := (Std.Time.Internal.Bounded.LE.sub month 1).toFin Std.Time.Month.Ordinal.days._proof_1✝;
      have res := months[⋯.mp index];
      res + if leap = true ∧ ↑month > 2 then 1 else 0
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (obj : C → D) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y))
  (map_id :
    autoParam (∀ (X : C), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X))
      CategoryTheory.Functor.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
        map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (map g))
      CategoryTheory.Functor.map_comp._autoParam)
  (obj_1 : C → D) (map_1 : {X Y : C} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y))
  (map_id_1 :
    autoParam (∀ (X : C), map_1 (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj_1 X))
      CategoryTheory.Functor.map_id._autoParam)
  (map_comp_1 :
    autoParam
      (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
        map_1 (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map_1 f) (map_1 g))
      CategoryTheory.Functor.map_comp._autoParam),
  ({ obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
      { obj := obj_1, map := map_1, map_id := map_id_1, map_comp := map_comp_1 }) =
    (obj = obj_1 ∧ map ≍ map_1)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- A sequence of uniformly integrable functions which converges μ-a.e. converges in Lp.  -/
MeasureTheory.tendsto_Lp_finite_of_tendsto_ae_of_meas : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} [MeasureTheory.IsFiniteMeasure μ],
  1 ≤ p →
    p ≠ ⊤ →
      ∀ {f : ℕ → α → β} {g : α → β},
        (∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n)) →
          MeasureTheory.StronglyMeasurable g →
            MeasureTheory.MemLp g p μ →
              MeasureTheory.UnifIntegrable f p μ →
                (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
                  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.instComplSubtype : {R : Type u_1} → [inst : NonAssocRing R] → Compl { a // IsIdempotentElem a }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.mk.inj : ∀ {p : Int.Internal.Linear.Poly} {h : Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof} {p_1 : Int.Internal.Linear.Poly}
  {h_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof}, { p := p, h := h } = { p := p_1, h := h_1 } → p = p_1 ∧ h = h_1
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.widePullbackShapeEquiv_inverse_obj : ∀ {J : Type u_1} (a : CategoryTheory.WithTerminal (CategoryTheory.Discrete J)),
  CategoryTheory.WithTerminal.widePullbackShapeEquiv.inverse.obj a =
    CategoryTheory.WithTerminal.widePullbackShapeEquivObj✝.symm a
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedMessageDirection.default : Lean.JsonRpc.MessageDirection
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_half : ∀ {x : ℝ}, -Real.pi ≤ x → x ≤ Real.pi → Real.cos (x / 2) = √((1 + Real.cos x) / 2)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSpace.generateFrom_singleton_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α}, MeasurableSet s → MeasurableSpace.generateFrom {s} ≤ m
-- Mathlib.Algebra.Order.Group.PosPart
neg_le_negPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] (a : α), -a ≤ a⁻
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (X : CategoryTheory.CommMon (CategoryTheory.Functor C D)) (X_1 : C),
  (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso.hom.app X).hom.hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.X.obj X_1)
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.of_subsingleton : ∀ (R : Type u) (N : Type z) [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N] [Subsingleton N],
  Module.Free R N
-- Lean.Data.AssocList
/-- List-like type to avoid extra level of indirection  -/
Lean.AssocList : Type u → Type v → Type (max u v)
-- Init.Data.Range.Polymorphic.UInt
UInt64.instLeast? : Std.PRange.Least? UInt64
-- Lean.Elab.Quotation
/-- an "alternative" of patterns plus right-hand side  -/
Lean.Elab.Term.Quotation.Alt : Type
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.submartingale_of_setIntegral_le_succ : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → ℝ},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ) →
        MeasureTheory.Submartingale f 𝒢 μ
-- Mathlib.Order.Category.BddDistLat
BddDistLat.dualEquiv_functor : BddDistLat.dualEquiv.functor = BddDistLat.dual
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.BallPackage.instInhabited : (α : Type u_1) → Inhabited (Besicovitch.BallPackage α α)
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq'.induct_unfolding : ∀ (motive : Lean.Grind.AC.Expr → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Prop),
  (∀ (s : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var),
      motive (Lean.Grind.AC.Expr.var x) s (Lean.Grind.AC.Seq.cons x s)) →
    (∀ (s : Lean.Grind.AC.Seq) (a b : Lean.Grind.AC.Expr),
        motive b s (b.toSeq' s) →
          motive a (b.toSeq' s) (a.toSeq' (b.toSeq' s)) → motive (a.op b) s (a.toSeq' (b.toSeq' s))) →
      ∀ (e : Lean.Grind.AC.Expr) (s : Lean.Grind.AC.Seq), motive e s (e.toSeq' s)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitMonoid : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) → [CategoryTheory.IsFiltered J] → Monoid (MonCat.FilteredColimits.M F)
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionsResult : Type
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.exists_forall_norm_le : ∀ {R : Type u_2} [inst : NormedRing R] [IsAbsoluteValue norm] [ProperSpace R] (p : Polynomial R),
  ∃ x, ∀ (y : R), ‖Polynomial.eval x p‖ ≤ ‖Polynomial.eval y p‖
-- Mathlib.Analysis.Complex.Circle
Circle.coe_div : ∀ (z w : Circle), ↑(z / w) = ↑z / ↑w
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.precomp_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  {J' : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} J'] (G : CategoryTheory.Functor J' J) (x : J')
  (a : F.obj (G.obj x)), (c.precomp G).ι x a = c.ι (G.obj x) a
-- Mathlib.LinearAlgebra.BilinearMap
IsBilinearMap.add_right : ∀ {R : Type u_1} [inst : CommSemiring R] {E : Type u_2} [inst_1 : AddCommMonoid E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommMonoid F] [inst_4 : Module R F] {G : Type u_4} [inst_5 : AddCommMonoid G] [inst_6 : Module R G]
  {f : E → F → G}, IsBilinearMap R f → ∀ (x : E) (y₁ y₂ : F), f x (y₁ + y₂) = f x y₁ + f x y₂
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_toLp : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
  (f : (i : ι) → β i), ‖WithLp.toLp ⊤ f‖ = ‖f‖
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeEmpty.match_1.splitter : (motive : Fin 0 → Sort u_1) → (x : Fin 0) → motive x
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.decidableMemZPowers.eq_1 : ∀ {G : Type u_1} [inst : Group G] {a : G},
  Subgroup.decidableMemZPowers = Classical.decPred fun x => x ∈ Subgroup.zpowers a
-- Mathlib.Algebra.Category.Grp.AB
CategoryTheory.Limits.productIsProduct'.eq_1 : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }],
  CategoryTheory.Limits.productIsProduct' X =
    { lift := fun s => CategoryTheory.Limits.Pi.lift fun j => s.π.app { as := j }, fac := ⋯, uniq := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- The type (I) simplex reconstructed from a type (II) simplex.  -/
SSet.prodStdSimplex.pairingCore.IsType₂.simplex : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} →
      {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} →
        SSet.prodStdSimplex.pairingCore.IsType₂ x →
          {d : ℕ} →
            x.dim = d →
              (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := m + 1 })
                    (SSet.stdSimplex.obj { len := n })).obj
                (Opposite.op { len := d + 1 })
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.map_injective_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f), Function.Injective (TopologicalSpace.Compacts.map f hf) ↔ Function.Injective f
-- Mathlib.Topology.EMetricSpace.Defs
edist_triangle_right : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y z : α), edist x y ≤ edist x z + edist y z
-- Lean.Server.Requests
Lean.Server.RequestM.runInIO : {α : Type} → Lean.Server.RequestM α → Lean.Server.RequestContext → IO α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHint.toJson : Lean.Lsp.InlayHint → Lean.Json
-- Mathlib.GroupTheory.Perm.Fin
Fin.coe_cycleRange_of_le : ∀ {n : ℕ} {i j : Fin n}, i ≤ j → ↑(j.cycleRange i) = if i = j then 0 else ↑i + 1
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.rpow_eq_nhds_of_neg : ∀ {p : ℝ × ℝ},
  p.1 < 0 → (fun x => x.1 ^ x.2) =ᶠ[nhds p] fun x => Real.exp (Real.log x.1 * x.2) * Real.cos (x.2 * Real.pi)
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.ofEq_rfl : ∀ {R : Type u_1} {M₁ : Type u_3} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M₁] [inst_4 : Module R N] {Q : QuadraticMap R M₁ N},
  QuadraticMap.Isometry.ofEq ⋯ = QuadraticMap.Isometry.id Q
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.mapObj_ext : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p] {A : C} {j : J} (f g : X.mapObj p j ⟶ A),
  (∀ (i : I) (hij : p i = j),
      CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) f =
        CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) g) →
    f = g
-- Std.Data.TreeSet.Basic
/-- Transforms a list into a tree set.  -/
Std.TreeSet.ofList : {α : Type u} → List α → (cmp : autoParam (α → α → Ordering) Std.TreeSet.ofList._auto_1) → Std.TreeSet α cmp
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp.congr_simp : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantTo i₀) [inst_2 : CategoryTheory.IsCofiltered J] (j : J), h.coneπApp j = h.coneπApp j
-- Mathlib.Algebra.Group.Shrink
equivShrink_symm_neg : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Neg α] (x : Shrink.{v, u_2} α),
  (equivShrink α).symm (-x) = -(equivShrink α).symm x
-- Mathlib.Algebra.GCDMonoid.FinsetLemmas
Finset.lcm_dvd_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Finset ι)
  (f : ι → α), s.lcm f ∣ s.prod f
-- Mathlib.Order.Basic
Prop.instCompl : Compl Prop
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_imp : ∀ {σs : List (Type u)} {φ₁ φ₂ : Prop}, (⌜φ₁⌝ → ⌜φ₂⌝) ⊣⊢ₛ ⌜φ₁ → φ₂⌝
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_eq_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Set α} (hf : (s ∩ Function.support f).Finite),
  ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ hf.toFinset, f i
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.coe_toEquiv : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), ⇑h.toEquiv = ⇑h
-- Lean.Setup
Lean.instToJsonPlugin.toJson : Lean.Plugin → Lean.Json
-- Mathlib.Control.Monad.Cont
ContT.run_withContT : ∀ {r : Type u} {m : Type u → Type v} {α β : Type w} (f : (β → m r) → α → m r) (x : ContT r m α),
  (ContT.withContT f x).run = x.run ∘ f
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.universally_isOpenMap : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.UniversallyOpen f],
  (AlgebraicGeometry.topologically @IsOpenMap).universally f
-- Mathlib.Topology.Category.Stonean.Basic
/-- Every Stonean space is projective in `Stonean`.  -/
Stonean.instProjective : ∀ (X : Stonean), CategoryTheory.Projective X
-- Init.Omega.LinearCombo
/-- Implementation of addition on `LinearCombo`.  -/
Lean.Omega.LinearCombo.add : Lean.Omega.LinearCombo → Lean.Omega.LinearCombo → Lean.Omega.LinearCombo
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoid.End.zero_apply : ∀ {M : Type uM} [inst : AddCommMonoid M] (m : M), 0 m = 0
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- If the integrals of `char` with respect to two finite measures `P` and `P'` coincide, then
`P = P'`.  -/
MeasureTheory.ext_of_integral_char_eq : ∀ {W : Type u_1} [inst : AddCommGroup W] [inst_1 : Module ℝ W] [inst_2 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {V : Type u_2} [inst_3 : AddCommGroup V] [inst_4 : Module ℝ V] [inst_5 : PseudoEMetricSpace V]
  [inst_6 : MeasurableSpace V] [BorelSpace V] [CompleteSpace V] [SecondCountableTopology V] {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ}
  (he : Continuous ⇑e),
  e ≠ 1 →
    (∀ (v : V), v ≠ 0 → L v ≠ 0) →
      ∀ (hL : Continuous fun p => (L p.1) p.2) {P P' : MeasureTheory.Measure V} [MeasureTheory.IsFiniteMeasure P]
        [MeasureTheory.IsFiniteMeasure P'],
        (∀ (w : W),
            ∫ (v : V), (BoundedContinuousFunction.char he hL w) v ∂P =
              ∫ (v : V), (BoundedContinuousFunction.char he hL w) v ∂P') →
          P = P'