mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.ContMDiffCovariantDerivative.contMDiff : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {E : Type u_2} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {H : Type u_3} {inst_3 : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  {inst_4 : TopologicalSpace M} {inst_5 : ChartedSpace H M} {F : Type u_5} {inst_6 : NormedAddCommGroup F}
  {inst_7 : NormedSpace 𝕜 F} {V : M → Type u_6} {inst_8 : TopologicalSpace (Bundle.TotalSpace F V)}
  {inst_9 : (x : M) → AddCommGroup (V x)} {inst_10 : (x : M) → Module 𝕜 (V x)}
  {inst_11 : (x : M) → TopologicalSpace (V x)} {inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)}
  {inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)} {inst_14 : FiberBundle F V} {inst_15 : IsManifold I 1 M}
  {inst_16 : VectorBundle 𝕜 F V} {cov : CovariantDerivative I F V} {k : WithTop ℕ∞}
  [self : cov.ContMDiffCovariantDerivative k], ContMDiffCovariantDerivativeOn F k (↑cov) Set.univ
-- Mathlib.Order.Category.FinPartOrd
/-- Constructs an isomorphism of finite partial orders from an order isomorphism between them.  -/
FinPartOrd.Iso.mk : {α β : FinPartOrd} → ↑α.toPartOrd ≃o ↑β.toPartOrd → (α ≅ β)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- Note this is more general than `IsSelfAdjoint.conjugate` as `B` can be rectangular.  -/
Matrix.isHermitian_mul_mul_conjTranspose : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  {A : Matrix m m α} (B : Matrix n m α), A.IsHermitian → (B * A * B.conjTranspose).IsHermitian
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqLambdaTheoremType : BEq Mathlib.Meta.FunProp.LambdaTheoremType
-- Mathlib.Data.List.Sigma
List.perm_dlookup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) {l₁ l₂ : List (Sigma β)},
  l₁.NodupKeys → l₁.Perm l₂ → List.dlookup a l₁ = List.dlookup a l₂
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- The canonical isomorphism from the opposite of the product to the coproduct in the opposite
category.
 -/
CategoryTheory.Limits.opProductIsoCoproduct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Type u_1} →
      (Z : α → C) → [inst_1 : CategoryTheory.Limits.HasProduct Z] → Opposite.op (∏ᶜ Z) ≅ ∐ fun x => Opposite.op (Z x)
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.Hom.rel_comp_apply₂ : ∀ {X Y Z : CategoryTheory.RelCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) (z : Z),
  (x, z) ∈ (CategoryTheory.CategoryStruct.comp f g).rel ↔ ∃ y, (x, y) ∈ f.rel ∧ (y, z) ∈ g.rel
-- Mathlib.Topology.ContinuousMap.Defs
/-- The function `X → Y`  -/
ContinuousMap.toFun : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → X → Y
-- Mathlib.Analysis.Normed.Module.Ball.Action
isScalarTower_closedBall_closedBall_ball : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [inst_5 : NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E],
  IsScalarTower ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.Sign.zero : Tactic.ComputeAsymptotics.UnitMonomial.Sign
-- Mathlib.Algebra.Lie.Solvable
_private.Mathlib.Algebra.Lie.Solvable.0.LieIdeal.coe_derivedSeries_eq_int_aux : ∀ (R₁ : Type u_1) (R₂ : Type u_2) (L : Type u_3) [inst : CommRing R₁] [inst_1 : CommRing R₂] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R₁ L] [inst_4 : LieAlgebra R₂ L] (k : ℕ),
  (∀ (x : L), x ∈ LieAlgebra.derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ LieAlgebra.derivedSeriesOfIdeal R₂ L k ⊤) →
    have I := LieAlgebra.derivedSeriesOfIdeal R₂ L k ⊤;
    have S := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x};
    ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)
-- Mathlib.Algebra.Lie.Abelian
LieAlgebra.abelian_of_le_center : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  ∀ I ≤ LieAlgebra.center R L, IsLieAbelian ↥I
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mono_homMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A.left ⟶ B.left)
  (w : CategoryTheory.CategoryStruct.comp (S.map f) B.hom = A.hom) [h : CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.CostructuredArrow.homMk f w)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.latticeBasis.eq_1 : ∀ (L : PeriodPair),
  L.latticeBasis = (Module.Basis.span ⋯).map (LinearEquiv.ofEq (Submodule.span ℤ (Set.range ![L.ω₁, L.ω₂])) L.lattice ⋯)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.nonempty_attachCells_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} (g : (a : α) → A a ⟶ B a)
  {X₁ X₂ : C} (f : X₁ ⟶ X₂),
  Nonempty (HomotopicalAlgebra.AttachCells g f) ↔
    (CategoryTheory.MorphismProperty.coproducts.{w, v, u} (CategoryTheory.MorphismProperty.ofHoms g)).pushouts f
-- Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
/-- The type of homotopies between morphisms `X ⟶ Y` of simplicial sets.
The data consists of a morphism `h : X ⊗ Δ[1] ⟶ Y` which induces
both `f` and `g`, see the lemmas `SSet.Homotopy.h₀` and `SSet.Homotopy.h₁`.  -/
SSet.Homotopy : {X Y : SSet} → (X ⟶ Y) → (X ⟶ Y) → Type u
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.range_prodMap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {G' : Type u_7} {N' : Type u_8} [inst_2 : Group G']
  [inst_3 : Group N'] (f : G →* N) (g : G' →* N'), (f.prodMap g).range = f.range.prod g.range
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Ioo_bot : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Ioo ⊥ ↑a = Set.Iio a
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C},
  autoParam
      (∀ (J : Type w) [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
        W.IsStableUnderTransfiniteCompositionOfShape J)
      CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.isStableUnderTransfiniteCompositionOfShape._autoParam →
    W.IsStableUnderTransfiniteComposition
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAtFilter_sub_const_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}
  {f' : E →L[𝕜] F} {L : Filter (E × E)} (c : F), HasFDerivAtFilter (fun x => f x - c) f' L ↔ HasFDerivAtFilter f f' L
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α]
  [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ {f : α → E} {t : Set α},
      MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (hxx' : x = x'),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)
      (X.presheaf.stalkSpecializes ⋯) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x')
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRoc : {α : Type u_1} → [DecidableEq α] → DecidableEq (Std.Roc α)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The domain of the local trivialisation (i.e., a subset of the bundle `Z`'s base):
outside of it, the pretrivialisation returns a junk value  -/
Bundle.Trivialization.baseSet : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : TopologicalSpace Z] → {proj : Z → B} → Bundle.Trivialization F proj → Set B
-- Mathlib.Analysis.Convex.Intrinsic
Convex.intrinsicClosure : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : AddCommGroup V]
  [inst_3 : Module 𝕜 V] [inst_4 : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousConstSMul 𝕜 V] {s : Set V},
  Convex 𝕜 s → Convex 𝕜 (intrinsicClosure 𝕜 s)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_nsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - ↑m
-- Init.Data.Array.MinMax
Array.foldl_max : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] [Std.Associative max] {xs : Array α} {a : α},
  Array.foldl max a xs = a ⊔ xs.max?.getD a
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.iInf : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrderBot ι]
  [inst_1 : TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι]
  {κ : Type u_4} [Countable κ] {f : MeasureTheory.Filtration ι m} {τ : κ → Ω → WithTop ι} [f.IsRightContinuous],
  (∀ (n : κ), MeasureTheory.IsStoppingTime f (τ n)) → MeasureTheory.IsStoppingTime f fun ω => ⨅ n, τ n ω
-- Mathlib.Geometry.Manifold.Notation
/-- If the type of `e` is a non-dependent function between spaces `src` and `tgt`, try to find a
model with corners on both `src` and `tgt`. If successful, return both models.

We pass `e` instead of just its type for better diagnostics.

If `es` is `some`, we verify that `src` and the type of `es` are definitionally equal.  -/
Manifold.Elab.findModels : Lean.Expr → Option Lean.Expr → Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_inv : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.normSq z⁻¹ = (RCLike.normSq z)⁻¹
-- Mathlib.RingTheory.Ideal.Operations
IsCoprime.add_eq : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J → I + J = 1
-- Mathlib.RingTheory.HahnSeries.Basic
/-- The orderTop of a Hahn series `x` is a minimal element of `WithTop Γ` where `x` has a nonzero
coefficient if `x ≠ 0`, and is `⊤` when `x = 0`.  -/
HahnSeries.orderTop : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → HahnSeries Γ R → WithTop Γ
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Unfold the definition of `id`.
This exists to streamline the proofs of `MonoidalClosed.id_comp` and `MonoidalClosed.comp_id`  -/
CategoryTheory.MonoidalClosed.id_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x : C)
  [inst_2 : CategoryTheory.Closed x],
  CategoryTheory.MonoidalClosed.id x =
    CategoryTheory.MonoidalClosed.curry (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).hom
-- Init.Data.Int.Order
Int.add_nonneg_iff_neg_le' : ∀ {a b : ℤ}, 0 ≤ a + b ↔ -a ≤ b
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.comm' : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c}
  (self : A.Hom B) (i j : ι),
  c.Rel i j →
    CategoryTheory.CategoryStruct.comp (self.f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (self.f j)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_rankFinite : ∀ {α : Type u_1} {E I : Set α}, I.Finite → (Matroid.uniqueBaseOn I E).RankFinite
-- Mathlib.Tactic.Ring.RingNF
/-- Evaluates an expression `e` into a normalized representation as a polynomial.

This is a variant of `Mathlib.Tactic.Ring.eval`, the main driver of the `ring` tactic.
It differs in
* operating on `Expr` (input) and `Simp.Result` (output), rather than typed `Qq` versions of these;
* throwing an error if the expression `e` is an atom for the `ring` tactic.
 -/
Mathlib.Tactic.RingNF.evalExpr : Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result
-- Init.Data.List.SplitOn.Lemmas
List.splitOnPPrepend_nil_right : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, List.splitOnPPrepend p xs [] = List.splitOnP p xs
-- Mathlib.Topology.Order.Basic
/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`,
provided `a` is neither a bottom element nor a top element.  -/
mem_nhds_iff_exists_Ioo_subset' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  (∃ l, l < a) → (∃ u, a < u) → (s ∈ nhds a ↔ ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s)
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.noetherianSpace_of_isAffineOpen : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  AlgebraicGeometry.IsAffineOpen U →
    ∀ [IsNoetherianRing ↑(X.presheaf.obj (Opposite.op U))], TopologicalSpace.NoetherianSpace ↥↑U
-- Mathlib.Topology.Baire.Lemmas
/-- An open subset of a Baire space is Baire.  -/
IsOpen.baireSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {s : Set X}, IsOpen s → BaireSpace ↑s
-- Mathlib.Tactic.IntervalCases
/-- A strictly less-than lower bound `n ≱ e` or upper bound `e ≱ n`. (`interval_cases` uses
less-equal exclusively, so less-than bounds are actually written as not-less-equal
with flipped arguments.)  -/
Mathlib.Tactic.IntervalCases.Bound.lt : ℤ → Mathlib.Tactic.IntervalCases.Bound
-- Init.Data.List.MinMax
List.min?_mem : ∀ {α : Type u_1} {a : α} [inst : Min α] [Std.MinEqOr α] {xs : List α}, xs.min? = some a → a ∈ xs
-- Init.Data.List.TakeDrop
List.take.eq_1 : ∀ {α : Type u} (x : List α), List.take 0 x = []
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR.go.eq_2 : ∀ {α : Type u_1} (a : α) (a_1 : ℕ) (a_2 : Array α), (a_1 = 0 → False) → List.insertIdxTR.go✝ a a_1 [] a_2 = a_2.toList
-- Mathlib.Topology.Metrizable.Urysohn
/-- For a regular topological space with second countable topology,
there exists an inducing map to `l^∞ = ℕ →ᵇ ℝ`.  -/
TopologicalSpace.exists_isInducing_l_infty : ∀ (X : Type u_1) [inst : TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X], ∃ f, Topology.IsInducing f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul f)
        CategoryTheory.MonObj.mul) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) f)
          CategoryTheory.MonObj.mul))
      CategoryTheory.MonObj.mul
-- Mathlib.Topology.Algebra.Ring.Basic
DiscreteTopology.topologicalSemiring : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocSemiring R] [DiscreteTopology R],
  IsTopologicalSemiring R
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_ground_eq : ∀ {α : Type u_1} {M : Matroid α} {R : Set α}, (M.restrict R).E = R
-- Init.Data.Random
StdGen.mk.sizeOf_spec : ∀ (s1 s2 : ℕ), sizeOf { s1 := s1, s2 := s2 } = 1 + sizeOf s1 + sizeOf s2
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.neg : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f : α → β} {a : α}, IsLocalMax f a → IsLocalMin (fun x => -f x) a
-- Aesop.Search.SearchM
Aesop.NormSimpContext.simprocs : Aesop.NormSimpContext → Lean.Meta.Simp.SimprocsArray
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientEquivProdOfLE.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t),
  AddSubgroup.quotientEquivProdOfLE h_le = AddSubgroup.quotientEquivProdOfLE' h_le Quotient.out ⋯
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
SimpleGraph.chromaticNumber_cycleGraph_of_even : ∀ (n : ℕ), 2 ≤ n → Even n → (SimpleGraph.cycleGraph n).chromaticNumber = 2
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_eq_get_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : a ∈ m}, m[a] = m[a]?.get ⋯
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzOnWith.of_le_add : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {f : α → ℝ},
  (∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y) → LipschitzOnWith 1 f s
-- Mathlib.Order.Bounds.Basic
isGLB_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsGLB (Set.Ici a) a
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
Filter.EventuallyEq.lineDifferentiableWithinAt_iff_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₀ f₁ : E → F}
  {s : Set E} {x v : E},
  f₀ =ᶠ[nhdsWithin x s] f₁ → x ∈ s → (LineDifferentiableWithinAt 𝕜 f₀ s x v ↔ LineDifferentiableWithinAt 𝕜 f₁ s x v)
-- Mathlib.LinearAlgebra.Orientation
/-- Fix a positive orientation.  -/
Module.Oriented.positiveOrientation : {R : Type u_1} →
  {inst : CommSemiring R} →
    {inst_1 : PartialOrder R} →
      {inst_2 : IsStrictOrderedRing R} →
        {M : Type u_2} →
          {inst_3 : AddCommMonoid M} →
            {inst_4 : Module R M} → {ι : Type u_4} → [self : Module.Oriented R M ι] → Orientation R M ι
-- Mathlib.Analysis.Convex.Jensen
/-- Convex **Jensen's inequality**, `Finset.centerMass` version.  -/
ConvexOn.map_centerMass_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  ConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, p i ∈ s) → f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.strictMonoOn_edgeSet : ∀ {V : Type u_1} {G : SimpleGraph V},
  StrictMonoOn SimpleGraph.Subgraph.edgeSet (Set.ofPred SimpleGraph.Subgraph.IsMatching)
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.lan_flat_of_flat : ∀ {C D : Type u₁} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D] (E : Type u₂)
  [inst_2 : CategoryTheory.Category.{u₁, u₂} E] {FE : E → E → Type u_1} {CE : E → Type u₁}
  [inst_3 : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [inst_4 : CategoryTheory.ConcreteCategory E FE]
  [CategoryTheory.Limits.HasLimits E] [inst_6 : CategoryTheory.Limits.HasColimits E]
  [CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget E)]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget E)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] (F : CategoryTheory.Functor C D)
  [CategoryTheory.RepresentablyFlat F], CategoryTheory.RepresentablyFlat F.op.lan
-- Mathlib.Data.Rel.Cover
SetRel.IsCover.eq_1 : ∀ {X : Type u_1} (U : SetRel X X) (s N : Set X), U.IsCover s N = ∀ ⦃x : X⦄, x ∈ s → ∃ y ∈ N, (x, y) ∈ U
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_eq_ofIntTruncate : ∀ {x : ℤ} {h₁ : Int32.minValue.toInt ≤ x} {h₂ : x ≤ Int32.maxValue.toInt}, Int32.ofIntLE x h₁ h₂ = Int32.ofIntClamp x
-- Mathlib.Data.Set.Semiring
SetSemiring.up_down : ∀ {α : Type u_1} (s : SetSemiring α), Set.up (SetSemiring.down s) = s
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxiHasSize.eq_1 : Int16.instRxiHasSize = { size := fun lo => (2 ^ 15 - lo.toInt).toNat }
-- Init.Data.List.Basic
/-- Combines two lists into a list of pairs in which the first and second components are the
corresponding elements of each list. The resulting list is the length of the shorter of the input
lists.

`O(min |xs| |ys|)`.

Examples:
* `["Mon", "Tue", "Wed"].zip [1, 2, 3] = [("Mon", 1), ("Tue", 2), ("Wed", 3)]`
* `["Mon", "Tue", "Wed"].zip [1, 2] = [("Mon", 1), ("Tue", 2)]`
* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`
 -/
List.zip : {α : Type u} → {β : Type v} → List α → List β → List (α × β)
-- Lean.Meta.Tactic.Grind.CasesMatch
/-- Returns `true` if `e` is of the form `∀ ..., _ = _ ... -> False`.
The lhs of each equation must not have loose bound variables.
Recall that the `lhs` should correspond to variables in a given alternative.
For example, the given match-condition
```
∀ (head : Nat) (tail : List Nat), a = 1 → as = head :: tail → False
```
is generated for the second alternative at
```
def f : List Nat → List Nat → Nat
  | _, 1 :: _ :: _ => ...
  | _, a :: as => ...
  | _, _  => ...
```
That is, `a` must be different from `1`, or `as` must not be of the form `_ :: _`. That is,
they must not be a match for the first alternative.
**Note**: We were *not* previously checking whether the `lhs` did not have loose bound variables.
This missing check caused a panic at `tryToProveFalse` function at `MatchCond.lean` because
it assumes the `lhs` does not have loose bound variables.
**Note**: This function is an approximation. It may return `true` for terms that do not
correspond to match-conditions.
 -/
Lean.Meta.Grind.isMatchCondCandidate : Lean.Expr → Bool
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
StrongDual.extendRCLikeL_apply : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (fr : StrongDual ℝ F), StrongDual.extendRCLikeL fr = fr.extendRCLike
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodUnique_apply : ∀ (R : Type u_8) (M : Type u_9) (N : Type u_10) [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace N] [inst_4 : AddCommMonoid N] [inst_5 : Unique N]
  [inst_6 : Module R M] [inst_7 : Module R N] (x : M × N), (ContinuousLinearEquiv.prodUnique R M N) x = x.1
-- Mathlib.Data.Setoid.Partition
Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty : ∀ {α : Type u_2} {s : Set (Set α)}, s.PairwiseDisjoint id → (∀ (a : α), ∃ x ∈ s, a ∈ x) → ∅ ∉ s → Setoid.IsPartition s
-- Lean.Meta.Tactic.Grind.Attr
/-- Auxiliary function for registering `grind`, `grind!`, `grind?`, and `grind!?` attributes.
`grind!` is like `grind` but selects minimal indexable subterms.
The `grind?` and `grind!?` are aliases for `grind` and `grind!` which displays patterns using `logInfo`.
It is just a convenience for users.
 -/
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.mkGrindAttr : Lean.Name → Bool → Bool → Lean.Meta.Grind.Extension → autoParam Lean.Name Lean.Meta.Grind.mkGrindAttr._auto_1✝ → IO Unit
-- Mathlib.Algebra.Divisibility.Basic
/-- **Alias** of `dvd_mul_of_dvd_left`. -/
Dvd.dvd.mul_right : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ b * c
-- Lean.DocString.Extension
Lean.instInhabitedVersoModuleDocs.default : Lean.VersoModuleDocs