mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Limits.Preserves
CategoryTheory.MonoidalCategory.Limits.preservesCoLimit_curriedTensor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {J : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J] (F : CategoryTheory.Functor J C)
  [h : ∀ (c : C), CategoryTheory.Limits.PreservesColimit F (CategoryTheory.MonoidalCategory.tensorRight c)],
  CategoryTheory.Limits.PreservesColimit F (CategoryTheory.MonoidalCategory.curriedTensor C)
-- Mathlib.Order.Lex
Lex.exists : ∀ {α : Type u_1} {p : Lex α → Prop}, (∃ a, p a) ↔ ∃ a, p (toLex a)
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.lt_iff_exists_lt : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α], Order.IsPredLimit b → (b < a ↔ ∃ c, b < c ∧ c < a)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.ker_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] {f g : CategoryTheory.Arrow C} (u : f ⟶ g),
  (CategoryTheory.Limits.ker C).map u =
    CategoryTheory.Limits.kernel.lift g.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f.hom) (CategoryTheory.Arrow.Hom.left u)) ⋯
-- Mathlib.Tactic.Determinant.Bird.Cert
Mathlib.Tactic.Determinant.CertCache.mk : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα) →
        Std.HashMap (ℕ × ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα) →
          Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα) → Mathlib.Tactic.Determinant.CertCache rα
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.one_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R] (n : ℤ), 1 ^ n = 1
-- Init.Control.Lawful.Basic
LawfulMonad.toLawfulApplicative : ∀ {m : Type u → Type v} {inst : Monad m} [self : LawfulMonad m], LawfulApplicative m
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommSemigroup α],
  Lex.instAddCommSemigroup = { toAddSemigroup := Lex.instAddSemigroup, add_comm := ⋯ }
-- Mathlib.Algebra.Algebra.Prod
/-- Second projection as `AlgHom`.  -/
AlgHom.snd : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → A × B →ₐ[R] B
-- Mathlib.Data.Seq.Computation
Computation.BisimO.eq_2 : ∀ {α : Type u} (R : Computation α → Computation α → Prop) (s s' : Computation α),
  Computation.BisimO R (Sum.inr s) (Sum.inr s') = R s s'
-- Mathlib.Data.Num.Lemmas
PosNum.cmp_eq : ∀ (m n : PosNum), m.cmp n = Ordering.eq ↔ m = n
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonPlainGoal.toJson : Lean.Lsp.PlainGoal → Lean.Json
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.hasLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}
  [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, max u₁ v₁} (CategoryTheory.Over X)],
  CategoryTheory.Limits.HasLimitsOfSize.{w, w', max u₁ v₁, max u₁ v₁} (CategoryTheory.Subobject X)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_hom_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).counitIso.hom.app X_1).snd.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.snd.obj X_2)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.exists_ofOrder_eq_natCard : ∀ {α : Type u_1} [inst : Group α] [h : IsCyclic α], ∃ g, orderOf g = Nat.card α
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.of.eq_1 : ∀ (k : Type u_1) (G : Type u_2) [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k],
  SkewMonoidAlgebra.of k G = { toFun := fun a => SkewMonoidAlgebra.single a 1, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- The Lie bracket of two vector fields in a manifold, within a set.  -/
VectorField.mlieBracketWithin : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      ((x : M) → TangentSpace I x) → ((x : M) → TangentSpace I x) → Set M → (x₀ : M) → TangentSpace I x₀
-- Mathlib.Data.Multiset.Count
Multiset.coe_count : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), Multiset.count a ↑l = List.count a l
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.val_addUnitsLift_symm_apply_apply : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousAdd M] (f : AddUnits C(X, M)) (x : X), ↑((ContinuousMap.addUnitsLift.symm f) x) = ↑f x
-- Lean.PrettyPrinter.Formatter
/-- Resets the state associated with the lead word,
inhibiting any automatic whitespace insertion between tokens.
 -/
Lean.PrettyPrinter.Formatter.resetLeadWord : Lean.PrettyPrinter.FormatterM Unit
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_iff_forall_mul_nonpos`. -/
AntivaryOn.sub_mul_sub_nonpos : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α}
  {s : Set ι}, AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.pi_target : ∀ {ι : Type u_5} {αi : ι → Type u_6} {βi : ι → Type u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)),
  (PartialEquiv.pi ei).target = Set.univ.pi fun i => (ei i).target
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- The reduction formula for the integral of `sin x ^ n` for any natural `n ≥ 2`.  -/
integral_sin_pow : ∀ {a b : ℝ} (n : ℕ),
  ∫ (x : ℝ) in a..b, Real.sin x ^ (n + 2) =
    (Real.sin a ^ (n + 1) * Real.cos a - Real.sin b ^ (n + 1) * Real.cos b) / (↑n + 2) +
      (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, Real.sin x ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ0_j : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Fact (IsUnit 3)], (WeierstrassCurve.ofJ0 R).j = 0
-- Mathlib.Analysis.SumIntegralComparisons
AntitoneOn.integral_le_sum_Ico : ∀ {a b : ℕ} {f : ℝ → ℝ}, a ≤ b → AntitoneOn f (Set.Icc ↑a ↑b) → ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ x ∈ Finset.Ico a b, f ↑x
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.isOrderedCancelAddMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α],
  IsOrderedCancelAddMonoid { x // 0 ≤ x }
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.mulI_symplComp : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] {S : ClosedSubmodule ℝ H},
  S.symplComp.mulI = S.mulI.symplComp
-- Mathlib.Order.WellFoundedSet
Set.IsWF.min_le : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty), a ∈ s → hs.min hn ≤ a
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
fderiv_exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → fderiv ℝ (fun x => Real.exp (f x)) x = Real.exp (f x) • fderiv ℝ f x
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.is_quotient_mk : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M} (m : M),
  Quotient.mk'' m = LieSubmodule.Quotient.mk m
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `le_neg_add_iff_add_le`. -/
add_le_of_le_neg_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, b ≤ -a + c → a + b ≤ c
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.lift_mk : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {M : Type u_3}
  [inst_3 : Monoid M] {f : GL n R →* M} (hf : f.comp (Matrix.GeneralLinearGroup.scalar n) = 1) (g : GL n R),
  (Matrix.ProjGenLinGroup.lift f hf) (Matrix.ProjGenLinGroup.mk g) = f g
-- Mathlib.Topology.Connected.LocallyConnected
locallyConnectedSpace_iff_connected_basis : ∀ {α : Type u} [inst : TopologicalSpace α],
  LocallyConnectedSpace α ↔ ∀ (x : α), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsPreconnected s) id
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_val_image_eq_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  (s : Set ↥p), Submodule.span R (Subtype.val '' s) = p ↔ Submodule.span R s = ⊤
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.abs_apply : ∀ {S : Type u_6} [inst : Ring S] [inst_1 : LinearOrder S] [inst_2 : IsStrictOrderedRing S] (a : S),
  AbsoluteValue.abs a = |a|
-- Mathlib.Data.Nat.Choose.Multinomial
/-- The **multinomial theorem**.  -/
Finset.sum_pow_eq_sum_piAntidiag_of_commute : ∀ {α : Type u_1} {R : Type u_2} [inst : DecidableEq α] [inst_1 : Semiring R] (s : Finset α) (f : α → R)
  (hc : (↑s).Pairwise (Function.onFun Commute f)) (n : ℕ),
  (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(Nat.multinomial s k) * s.noncommProd (fun i => f i ^ k i) ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- A helper structure in order to construct a pairing for a subcomplex of a
simplicial set `X`. The main difference with `Pairing` is that we provide
an index type `ι` and a function `dim : ι → ℕ` which allow to
parametrize type (I) simplices as `simplex s : X _⦋dim s + 1⦌` for `s : ι`,
and type (II) simplices as a face of `simplex s` in `X _⦋dim s⦌`.  -/
SSet.Subcomplex.PairingCore : {X : SSet} → X.Subcomplex → Type (max u (v + 1))
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_le : ∀ {α : Type u} [inst : Semiring α] {s : Set α} {I : Ideal α}, Ideal.span s ≤ I ↔ s ⊆ ↑I
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- The right adjoint of `Cocone.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)`.

Auxiliary definition for `functorialityAdjunction`.
 -/
CategoryTheory.Adjunction.functorialityRightAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  (K : CategoryTheory.Functor J C) →
                    CategoryTheory.Functor (CategoryTheory.Limits.Cocone (K.comp F)) (CategoryTheory.Limits.Cocone K)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.RespectsIso.diagonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {P : CategoryTheory.MorphismProperty C} [P.RespectsIso], P.diagonal.RespectsIso
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R]
  (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)),
  ↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x)) =
    (NumberField.HeightOneSpectrum.adicAbv K v) ((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)) x)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_inj : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S T : Subsemiring R}, S.op = T.op ↔ S = T
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableWithinAt_fun_neg_iff : ∀ {𝕜 : 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}
  {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 (fun y => -f y) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprPath : Repr Std.Http.URI.Path
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.congr.eq_1 : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [inst_2 : (i : ι) → CommRing (G' i)]
  {f' : (i j : ι) → i ≤ j → G' i →+* G' j} (e : (i : ι) → G i ≃+* G' i)
  (he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)),
  Ring.DirectLimit.congr e he =
    RingEquiv.ofRingHom (Ring.DirectLimit.map (fun x => ↑(e x)) he) (Ring.DirectLimit.map (fun i => ↑(e i).symm) ⋯) ⋯ ⋯
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_dvd_norm_of_mem : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  {I : Ideal S} {x : S}, x ∈ I → ↑(Ideal.absNorm I) ∣ (Algebra.norm ℤ) x
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.Γ_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
  (X : ChainComplex C ℕ) (Δ : SimplexCategoryᵒᵖ),
  (CategoryTheory.Idempotents.DoldKan.Γ.obj X).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ X Δ
-- Mathlib.Data.Set.Insert
Set.disjoint_singleton_left : ∀ {α : Type u_1} {s : Set α} {a : α}, Disjoint {a} s ↔ a ∉ s
-- Mathlib.Topology.Order.LiminfLimsup
/-- If a function has a limit, then its limsup coincides with its limit.  -/
Filter.Tendsto.limsup_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {f : Filter β} {u : β → α} {a : α} [f.NeBot], Filter.Tendsto u f (nhds a) → Filter.limsup u f = a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.toList_inj : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp]
  {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp},
  Std.ExtDTreeMap.Const.toList t₁ = Std.ExtDTreeMap.Const.toList t₂ ↔ t₁ = t₂
-- Init.Data.List.Lemmas
List.any_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {p : β → Bool}, (List.map f l).any p = l.any (p ∘ f)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone is a colimit cocone if and only if the corresponding bicone is a colimit
cocone.  -/
CategoryTheory.Limits.BinaryBicone.toBiconeIsColimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.BinaryBicone X Y) →
          CategoryTheory.Limits.IsColimit b.toBicone.toCocone ≃ CategoryTheory.Limits.IsColimit b.toCocone
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
/-- **Alias** of `BinaryTree.treesOfNumNodesEq`.  -/
Tree.treesOfNumNodesEq : ℕ → Finset (Tree Unit)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.Coindep.exists_isBase_subset_compl : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Coindep X → ∃ B, M.IsBase B ∧ B ⊆ M.E \ X
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zmodEquivZPowers.eq_1 : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k),
  h.zmodEquivZPowers =
    AddEquiv.ofBijective
      (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i => Additive.ofMul ⟨(fun x => ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
      ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
/-- If `C, D` has all limits of shape `J`, and `G` preserves them, then `preservesLimitsIso` is
functorial w.r.t. `F`.  -/
CategoryTheory.preservesLimitNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            [inst_2 : CategoryTheory.Category.{w', w} J] →
              [CategoryTheory.Limits.PreservesLimitsOfShape J G] →
                [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D] →
                  [inst_5 : CategoryTheory.Limits.HasLimitsOfShape J C] →
                    CategoryTheory.Limits.lim.comp G ≅
                      ((CategoryTheory.Functor.whiskeringRight J C D).obj G).comp CategoryTheory.Limits.lim
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂Measurable_mk_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : BorelSpace β] [inst_7 : MeasurableSpace γ]
  [inst_8 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_9 : BorelSpace γ]
  [inst_10 : SecondCountableTopologyEither β γ] [inst_11 : MeasurableSpace δ]
  [inst_12 : TopologicalSpace.PseudoMetrizableSpace δ] [inst_13 : OpensMeasurableSpace δ]
  [inst_14 : SecondCountableTopology δ] (g : β → γ → δ) (hg : Measurable (Function.uncurry g)) (f₁ : α → β) (f₂ : α → γ)
  (hf₁ : MeasureTheory.AEStronglyMeasurable f₁ μ) (hf₂ : MeasureTheory.AEStronglyMeasurable f₂ μ),
  MeasureTheory.AEEqFun.comp₂Measurable g hg (MeasureTheory.AEEqFun.mk f₁ hf₁) (MeasureTheory.AEEqFun.mk f₂ hf₂) =
    MeasureTheory.AEEqFun.mk (fun a => g (f₁ a) (f₂ a)) ⋯
-- Aesop.Tree.ExtractScript
Aesop.MVarClusterRef.extractScriptCore : Aesop.MVarClusterRef → Aesop.ExtractScriptM Unit
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Auxiliary definition for `OneHypercoverDenseData.essSurj.presheafObjObjIso`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        (G₀ : CategoryTheory.Sheaf J₀ A) →
                          (X₀ : C₀) →
                            (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf data G₀).obj
                                (Opposite.op (F.obj X₀)) ⟶
                              G₀.obj.obj (Opposite.op X₀)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- On an open set, `f : ℂ → E` is analytic iff it is differentiable  -/
Complex.analyticOnNhd_iff_differentiableOn : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ},
  IsOpen s → (AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.exists_congr : ∀ {σs : List (Type u)} {α : Sort u_1} {Φ Ψ : α → Std.Do.SPred σs}, (∀ (a : α), Φ a ⊣⊢ₛ Ψ a) → (∃ a, Φ a) ⊣⊢ₛ ∃ a, Ψ a
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.forget₂_TopCat_obj : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {X : TopModuleCat R},
  ↑((CategoryTheory.forget₂ (TopModuleCat R) TopCat).obj X) = ↑X.toModuleCat
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.subtype_apply : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] {S' : A} (x : ↥S'),
  (MulMemClass.subtype S') x = ↑x
-- Mathlib.Util.Superscript
/-- Applies the alignment mapping to a `Substring`.  -/
_private.Mathlib.Util.Superscript.0.Mathlib.Tactic.Superscript.scriptFnNoAntiquot.alignSubstr : Lean.Parser.ParserContext → Array (String.Pos.Raw × String.Pos.Raw) → Substring.Raw → Substring.Raw
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Ordinal.cof_ord_cof`. -/
Ordinal.cof_cof : ∀ (o : Ordinal.{u_1}), o.cof.ord.cof = o.cof
-- Init.Data.String.Defs
String.Pos.Raw.isValidForSlice_rawEndPos : ∀ {s : String.Slice}, String.Pos.Raw.IsValidForSlice s s.rawEndPos
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balLeft.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (b : RBTree.RBNode α) →
          (z : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c))
  (h_3 : (r : RBTree.RBNode α) → motive r),
  (match RBTree.RBNode.node RBTree.RBColor.black a y b with
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_1 a y b
    | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c => h_2 a y b z c
    | r => h_3 r) =
    h_1 a y b
-- Mathlib.Data.Multiset.Pi
Multiset.pi_zero : ∀ {α : Type u_1} [inst : DecidableEq α] {β : α → Type u_2} (t : (a : α) → Multiset (β a)),
  Multiset.pi 0 t = {Multiset.Pi.empty β}
-- Mathlib.RingTheory.Derivation.Basic
Derivation.leibniz_pow : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  (a : A) (n : ℕ), D (a ^ n) = n • a ^ (n - 1) • D a
-- Mathlib.Topology.Homotopy.Contractible
/-- A map is nullhomotopic if it is homotopic to a constant map.  -/
ContinuousMap.Nullhomotopic : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → Prop
-- Lean.Meta.Tactic.Grind.Main
/-- A helper combinator for executing a `grind`-based terminal tactic.
Given an input goal `mvarId`, it cleans up local hypotheses corresponding to internal details,
creates an auxiliary meta-variable `mvarId'`, and executes `k mvarId'`.
`withNewMCtxDepth` is used to prevent metavariables from being accidentally assigned by
`grind`'s `isDefEq` calls. After `grind` finishes, delayed metavariable assignments are
resolved, and the resulting proof is assigned to the original goal.

See issue #11806 and issue #12242 for motivating examples.
 -/
Lean.Meta.Grind.withProtectedMCtx : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadControlT Lean.MetaM m] →
        [MonadLiftT Lean.MetaM m] →
          [MonadExcept Lean.Exception m] →
            [Lean.MonadRuntimeException m] → Lean.Grind.Config → Lean.MVarId → (Lean.MVarId → m α) → m α
-- Init.Data.Vector.Zip
Vector.map_prod_left_eq_zip : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β},
  Vector.map (fun x => (x, f x)) xs = xs.zip (Vector.map f xs)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- **Alias** of the forward direction of `SpectrumRestricts.mul_comm_iff`. -/
SpectrumRestricts.mul_comm : ∀ {R : Type u_6} {S : Type u_7} {A : Type u_8} [inst : Semifield R] [inst_1 : Field S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a b : A} {f : S → R},
  SpectrumRestricts (a * b) f → SpectrumRestricts (b * a) f