mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.IsFiltered.isSifted : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFiltered C], CategoryTheory.IsSifted C
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TacticMVarKind.fieldAutoParam.sizeOf_spec : ∀ (fieldName structName : Lean.Name),
  sizeOf (Lean.Elab.Term.TacticMVarKind.fieldAutoParam fieldName structName) = 1 + sizeOf fieldName + sizeOf structName
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.h_mem_cartanSubalgebra' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι] (i : ↥b.support)
  (hi : RootPairing.GeckConstruction.h i ∈ RootPairing.GeckConstruction.lieAlgebra b),
  ⟨RootPairing.GeckConstruction.h i, hi⟩ ∈ RootPairing.GeckConstruction.cartanSubalgebra' b
-- Lean.Parser.Term.Doc
/-- Adds a recommended spelling to the environment.  -/
Lean.Parser.Term.Doc.addRecommendedSpelling : Lean.Environment → Lean.Parser.Term.Doc.RecommendedSpelling → Array Lean.Name → Lean.Environment
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mkAux.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ d₀_1 : X₁ ⟶ X₀) (e_d₀ : d₀ = d₀_1) (d₁ d₁_1 : X₂ ⟶ X₁) (e_d₁ : d₁ = d₁_1)
  (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ succ_1 :
    (S : CategoryTheory.ShortComplex V) →
      (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0),
  succ = succ_1 →
    ∀ (a a_1 : ℕ),
      a = a_1 → ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ a = ChainComplex.mkAux X₀ X₁ X₂ d₀_1 d₁_1 ⋯ succ_1 a_1
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_roo_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  (Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi
-- Mathlib.Analysis.Complex.Basic
Complex.conjCAE_toLinearMap : Complex.conjCAE.toLinearMap = Complex.conjAe.toLinearMap
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_rev_Iio : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.rev (Finset.Iio i) = Finset.Ioi i.rev
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositions_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u} W f ↔
    ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f
-- Mathlib.Order.Disjoint
symm_codisjoint : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α], Std.Symm Codisjoint
-- Aesop.BuiltinRules.Split
Aesop.BuiltinRules.splitTarget : Aesop.RuleTac
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The universal property of the exterior power.  -/
exteriorPower.presentation.isPresentationCore : (R : Type u) →
  [inst : CommRing R] →
    (n : ℕ) →
      (M : Type u_1) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            (exteriorPower.presentation.relationsSolutionEquiv.symm (exteriorPower.ιMulti R n)).IsPresentationCore
-- Mathlib.Order.SupIndep
iSupIndep_map_orderIso_iff : ∀ {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β)
  {a : ι → α}, iSupIndep (⇑f ∘ a) ↔ iSupIndep a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.instInfSet.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α],
  WithBot.instInfSet =
    {
      sInf := fun S =>
        if ⊥ ∈ S then ⊥ else if BddBelow ((fun a => ↑a) ⁻¹' S) then ↑(sInf ((fun a => ↑a) ⁻¹' S)) else ⊥ }
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
alternatingGroup.subgroup_eq_top_of_isPreprimitive : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  4 < Nat.card α →
    ∀ (G : Subgroup ↥(alternatingGroup α)) [hG' : MulAction.IsPreprimitive (↥G) α] {s : Set α},
      MulAction.stabilizer (↥(alternatingGroup α)) s ≤ G → G = ⊤
-- Lean.Parser.Basic
Lean.Parser.sepBy1Fn : Bool → Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.foldlM_eq_foldlM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} {a : Type u_1} {f : a → α → β → m a}
  {init : a} [inst : Monad m] [LawfulMonad m] {t : RBTree.RBMap α β cmp},
  RBTree.RBMap.foldlM f init t = List.foldlM (fun r p => f r p.1 p.2) init t.toList
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- If `R` is a Noetherian ring and `M` is a finite `R`-module, then the natural map
given by `AdicCompletion.ofTensorProduct` is an isomorphism.  -/
AdicCompletion.ofTensorProduct_bijective_of_finite_of_isNoetherian : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsNoetherianRing R] [Module.Finite R M], Function.Bijective ⇑(AdicCompletion.ofTensorProduct I M)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.exists_mem_notMem : ∀ {α : Type u_1} {n : ℕ}, 1 ≤ n → ↑n < ENat.card α → ∀ {a b : α}, a ≠ b → ∃ s, a ∈ s ∧ b ∉ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The Weierstrass curve base changed to an algebra `A` over `R`.  -/
WeierstrassCurve.baseChange : {R : Type u} →
  [inst : CommRing R] → WeierstrassCurve R → (A : Type v) → [inst_1 : CommRing A] → [Algebra R A] → WeierstrassCurve A
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` has normal form on `U`, then `f` equals `toMeromorphicNFOn f U`.
 -/
toMeromorphicNFOn_eq_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, toMeromorphicNFOn f U = f ↔ MeromorphicNFOn f U
-- Mathlib.Order.Filter.IsBounded
Filter.isBounded_le_of_top : ∀ {α : Type u_1} [inst : LE α] [OrderTop α] {f : Filter α}, Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f
-- Mathlib.Analysis.Analytic.CPolynomial
HasFiniteFPowerSeriesOnBall.neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f pf x n r → HasFiniteFPowerSeriesOnBall (-f) (-pf) x n r
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.norm_le_half_period : ∀ (p : ℝ) {x : AddCircle p}, p ≠ 0 → ‖x‖ ≤ |p| / 2
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.op_map_comp_obj : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑Z)ᵒᵖ),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).op.obj U =
    (TopologicalSpace.Opens.map f).op.obj ((TopologicalSpace.Opens.map g).op.obj U)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.domDomRestrictₗ.eq_1 : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [inst_5 : DecidablePred P],
  f.domDomRestrictₗ P = { toFun := fun z => f.domDomRestrict P z, map_update_add' := ⋯, map_update_smul' := ⋯ }
-- Mathlib.Topology.Category.Profinite.Extend
/-- A functor `StructuredArrow S toProfinite ⥤ FintypeCat` whose limit in `Profinite` is isomorphic
to `S`.
 -/
Profinite.fintypeDiagram' : (S : Profinite) → CategoryTheory.Functor (CategoryTheory.StructuredArrow S FintypeCat.toProfinite) FintypeCat
-- Mathlib.GroupTheory.CoprodI
/-- The free product of free groups is itself a free group.  -/
Monoid.CoprodI.instIsFreeGroup : ∀ {ι : Type u_4} (G : ι → Type u_5) [inst : (i : ι) → Group (G i)] [∀ (i : ι), IsFreeGroup (G i)],
  IsFreeGroup (Monoid.CoprodI G)
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ico_disjoint_Ico_same : ∀ {α : Type v} [inst : Preorder α] {a b c : α}, Disjoint (Set.Ico a b) (Set.Ico b c)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.isIdempotentElem_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], IsIdempotentElem K.starProjection
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.mk_surjective : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V), Function.Surjective ⇑(Representation.Coinvariants.mk ρ)
-- Init.Data.List.MapIdx
List.mapFinIdx.go.eq_def : ∀ {α : Type u_1} {β : Type u_2} (as : List α) (f : (i : ℕ) → α → i < as.length → β) (bs : List α) (acc : Array β)
  (a : bs.length + acc.size = as.length),
  List.mapFinIdx.go as f bs acc a =
    match bs, acc, a with
    | [], acc, h => acc.toList
    | a :: as_1, acc, h => List.mapFinIdx.go as f as_1 (acc.push (f acc.size a ⋯)) ⋯
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.sectionsMap_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M N P : PresheafOfModules R} (f : M ⟶ N) (g : N ⟶ P) (s : M.sections),
  PresheafOfModules.sectionsMap (CategoryTheory.CategoryStruct.comp f g) s =
    PresheafOfModules.sectionsMap g (PresheafOfModules.sectionsMap f s)
-- Mathlib.Topology.Bases
MapClusterPt.exists_seq_tendsto : ∀ {α : Type u} [t : TopologicalSpace α] [FirstCountableTopology α] {ι : Type u_1} {f : Filter ι}
  [f.IsCountablyGenerated] {x : α} {u : ι → α},
  MapClusterPt x f u → ∃ ψ, Filter.Tendsto (u ∘ ψ) Filter.atTop (nhds x) ∧ Filter.Tendsto ψ Filter.atTop f
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCommMonoidOfMulOpposite : {M : Type u_1} → [CommMonoid Mᵐᵒᵖ] → CommMonoid Mᵈᵐᵃ
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul self.X) self.actLeft =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X self.X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.actLeft)
        self.actLeft)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- The Radon-Nikodym derivative of a sigma-finite measure `μ` with respect to another
measure `ν` is `ν`-almost everywhere finite.  -/
MeasureTheory.Measure.rnDeriv_lt_top : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ⊤
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The canonical projection into the colimit, as a quotient type.  -/
AddMonCat.FilteredColimits.M.mk : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) → (j : J) × ↑(F.obj j) → AddMonCat.FilteredColimits.M F
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.leftRel_r_eq_leftCosetEquivalence : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), ⇑(QuotientGroup.leftRel s) = LeftCosetEquivalence ↑s
-- Init.Data.Array.Basic
PSigma.mk.congr_simp : ∀ {α : Sort u} {β : α → Sort v} (fst : α) (snd snd_1 : β fst), snd = snd_1 → ⟨fst, snd⟩ = ⟨fst, snd_1⟩
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyoneda_map_app : ∀ {X Y : CommMonCatᵒᵖ} (f : X ⟶ Y) (N : CommMonCat),
  (CommMonCat.coyoneda.map f).app N = CommMonCat.ofHom (CommMonCat.Hom.hom f.unop).compHom'
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The underlying element of the completion `(v.valuation K).Completion`.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      {K : Type u_2} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              {v : IsDedekindDomain.HeightOneSpectrum R} →
                IsDedekindDomain.HeightOneSpectrum.adicCompletion K v →
                  (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion
-- Init.Data.SInt.Lemmas
Int64.toInt_mod : ∀ (a b : Int64), (a % b).toInt = a.toInt.tmod b.toInt
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (δ : CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPre F)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁ δ).app X₁).app X₂).app X₃ =
    (δ.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).app X₃
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
MeasureTheory.Measure.condKernel_def : ∀ {α : Type u_5} {Ω : Type u_6} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (ρ : MeasureTheory.Measure (α × Ω)) [inst_2 : MeasureTheory.IsFiniteMeasure ρ],
  ρ.condKernel = (ProbabilityTheory.Kernel.const Unit ρ).condKernelUnitBorel.comap (fun a => ((), a)) ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.add_iInter_subset : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Add α] (s : Set α) (t : ι → Set α), s + ⋂ i, t i ⊆ ⋂ i, s + t i
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Div β]
  [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (f i / f j) (f k / f l) κ μ
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.disjoint_ker_of_nondegenerate_restrict : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} {W : Submodule R M},
  (B.domRestrict₁₂ W W).Nondegenerate → Disjoint W B.ker
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.Ordered.erase : ∀ {α : Type u_1} {cmp : α → α → Ordering} {path : RBTree.RBNode.Path α} {t : RBTree.RBNode α},
  RBTree.RBNode.Path.Ordered cmp path →
    RBTree.RBNode.Ordered cmp t →
      RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp path) t → RBTree.RBNode.Ordered cmp (path.erase t)
-- Lean.Linter.Init
Lean.Linter.isLinterEnabledByOptions : Lean.Name → Lean.Linter.LinterOptions → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.lift_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g) CategoryTheory.Limits.biprod.snd = g
-- Init.Data.AC
Lean.Data.AC.instInhabitedExpr : Inhabited Lean.Data.AC.Expr
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Extract the isomorphism between
`colim (uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G))` and
`(G.obj (colim K₁)).obj (colim K₂)` from a `PreservesLimit₂` instance, provided the relevant
limits exist.  -/
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    (K₁ : CategoryTheory.Functor J₁ C₁) →
                      (K₂ : CategoryTheory.Functor J₂ C₂) →
                        (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                          [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] →
                            [inst_6 : CategoryTheory.Limits.HasLimit K₁] →
                              [inst_7 : CategoryTheory.Limits.HasLimit K₂] →
                                CategoryTheory.Limits.limit
                                    (CategoryTheory.Functor.uncurry.obj
                                      ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) ≅
                                  (G.obj (CategoryTheory.Limits.limit K₁)).obj (CategoryTheory.Limits.limit K₂)
-- Mathlib.Order.Interval.Set.Disjoint
/-- If two half-open intervals are disjoint and the endpoint of one lies in the other,
then it must be equal to the endpoint of the other.  -/
Set.eq_of_Ico_disjoint : ∀ {α : Type v} [inst : LinearOrder α] {x₁ x₂ y₁ y₂ : α},
  Disjoint (Set.Ico x₁ x₂) (Set.Ico y₁ y₂) → x₁ < x₂ → x₂ ∈ Set.Ico y₁ y₂ → y₁ = x₂
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_mono : ∀ {G : Type u_1} [inst : AddGroup G] (n : ℕ), Monotone fun S => S.lowerCentralSeries n
-- Mathlib.MeasureTheory.Integral.Prod
/-- The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of)
the symmetric version of Fubini's theorem is measurable.  -/
MeasureTheory.StronglyMeasurable.integral_prod_left' : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [MeasureTheory.SFinite μ]
  ⦃f : α × β → E⦄, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun y => ∫ (x : α), f (x, y) ∂μ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPushoutsAgainst.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.MorphismProperty C},
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), P' f → P.HasPushoutsAlong f) → P.HasPushoutsAgainst P'
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.rooIterator.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound upperBound : α),
  Std.DTreeMap.Internal.rooIterator t lowerBound upperBound =
    {
      internalState :=
        { iter := Std.DTreeMap.Internal.Zipper.prependMapGT t lowerBound Std.DTreeMap.Internal.Zipper.done,
          upper := upperBound } }
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_nonempty : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E),
  (B.polar s).Nonempty
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.eq_1 : ∀ (motive : FirstOrder.Field.FieldAxiom → Sort u_1) (h_1 : Unit → motive FirstOrder.Field.FieldAxiom.addAssoc)
  (h_2 : Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd)
  (h_3 : Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel)
  (h_4 : Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) (h_5 : Unit → motive FirstOrder.Field.FieldAxiom.mulComm)
  (h_6 : Unit → motive FirstOrder.Field.FieldAxiom.oneMul) (h_7 : Unit → motive FirstOrder.Field.FieldAxiom.existsInv)
  (h_8 : Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib)
  (h_9 : Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE),
  (match FirstOrder.Field.FieldAxiom.addAssoc with
    | FirstOrder.Field.FieldAxiom.addAssoc => h_1 ()
    | FirstOrder.Field.FieldAxiom.zeroAdd => h_2 ()
    | FirstOrder.Field.FieldAxiom.negAddCancel => h_3 ()
    | FirstOrder.Field.FieldAxiom.mulAssoc => h_4 ()
    | FirstOrder.Field.FieldAxiom.mulComm => h_5 ()
    | FirstOrder.Field.FieldAxiom.oneMul => h_6 ()
    | FirstOrder.Field.FieldAxiom.existsInv => h_7 ()
    | FirstOrder.Field.FieldAxiom.leftDistrib => h_8 ()
    | FirstOrder.Field.FieldAxiom.existsPairNE => h_9 ()) =
    h_1 ()
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.skeleton_le_skeletonOfMono : ∀ {X Y : SSet} (i : X ⟶ Y) (n : ℕ), Y.skeleton n ≤ (SSet.skeletonOfMono i) n
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_subset_smul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (I : Submodule R A) (N : Submodule R M), ↑I • ↑N ⊆ ↑(I • N)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_finCongr_Ioc : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.map (finCongr h).toEmbedding (Finset.Ioc i j) = Finset.Ioc (Fin.cast h i) (Fin.cast h j)
-- Lean.Meta.Hint
Lean.Meta.Hint.Suggestion.toTryThisSuggestion : Lean.Meta.Hint.Suggestion → Lean.Meta.Tactic.TryThis.Suggestion
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Lean.Expr
/-- Return `true` iff `a` and `b` are equal.
Binder names and annotations are taken into account.
 -/
Lean.Expr.equal : Lean.Expr → Lean.Expr → Bool
-- Mathlib.Analysis.Analytic.Constructions
alternatingGeometricSeries.eq_1 : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A],
  alternatingGeometricSeries 𝕜 A = FormalMultilinearSeries.ofScalars A fun n => (-1) ^ n
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_smul : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {S : Type u_3} [inst_1 : SMulZeroClass S k] (a : S)
  (b : SkewMonoidAlgebra k G), (a • b).coeff = a • b.coeff
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The map from `kernel f` into the source of `f`.  -/
CategoryTheory.Limits.kernel.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (f : X ⟶ Y) → [inst_2 : CategoryTheory.Limits.HasKernel f] → CategoryTheory.Limits.kernel f ⟶ X
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.isometryEquivMap.coe_apply : ∀ {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁'] [inst_2 : NormedSpace 𝕜 V₁'] [inst_3 : MetricSpace P₁']
  [inst_4 : NormedAddTorsor V₁' P₁'] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (φ : P₁' →ᵃⁱ[𝕜] P₂) (E : AffineSubspace 𝕜 P₁')
  [inst_9 : Nonempty ↥E] (g : ↥E), ↑((AffineSubspace.isometryEquivMap φ E) g) = φ ↑g
-- Lean.DocString.Types
Lean.Doc.instBEqDescItem.beq : {α : Type u_1} → {β : Type u_2} → [BEq α] → [BEq β] → Lean.Doc.DescItem α β → Lean.Doc.DescItem α β → Bool