mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.hom_mk : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : CategoryTheory.CommaMorphism X.toComma Y.toComma)
  (hf : Q f.left) (hg : W f.right), { toCommaMorphism := f, prop_hom_left := hf, prop_hom_right := hg }.hom = f
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
SSet.coherentIso.invStructHom_invHomId : SSet.coherentIso.invStructHom.invHomId = SSet.coherentIso.invHomId
-- Mathlib.Data.List.DropRight
List.rtake_nil : ∀ {α : Type u_1} (n : ℕ), [].rtake n = []
-- Lean.Meta.Basic
Lean.Meta.AbstractMVarsResult.mk.sizeOf_spec : ∀ (paramNames : Array Lean.Name) (mvars : Array Lean.Expr) (expr : Lean.Expr),
  sizeOf { paramNames := paramNames, mvars := mvars, expr := expr } = 1 + sizeOf paramNames + sizeOf mvars + sizeOf expr
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.shift_comm : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.commShiftIso F₁ a).hom
      (CategoryTheory.Functor.whiskerRight τ (CategoryTheory.shiftFunctor D a)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).whiskerLeft τ)
      (CategoryTheory.Functor.commShiftIso F₂ a).hom
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.add : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f g : M → E'} {f' g' : TangentSpace I z →L[𝕜] E'} {s : Set M},
  HasMFDerivAt[s] f z f' → HasMFDerivAt[s] g z g' → HasMFDerivAt[s] (f + g) z (f' + g')
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureHelpContext : Lean.FromJson Lean.Lsp.SignatureHelpContext
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length_toList : ∀ {α : Type u} (s : Stream'.Seq α) (h : s.Terminates), (s.toList h).length = s.length h
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.prod_mono : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] {s₁ s₂ : Submonoid M}
  {t₁ t₂ : Submonoid N}, s₁ ≤ s₂ → t₁ ≤ t₂ → s₁.prod t₁ ≤ s₂.prod t₂
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.Hom.hom.eq_1 : ∀ {X Y : AddMonCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Mathlib.Analysis.InnerProductSpace.PiL2
Pi.orthonormalBasis_repr : ∀ {η : Type u_7} [inst : Fintype η] {ι : η → Type u_8} [inst_1 : (i : η) → Fintype (ι i)] {𝕜 : Type u_9}
  [inst_2 : RCLike 𝕜] {E : η → Type u_10} [inst_3 : (i : η) → NormedAddCommGroup (E i)]
  [inst_4 : (i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) (x : (i : η) → E i)
  (j : (i : η) × ι i), ((Pi.orthonormalBasis B).repr (WithLp.toLp 2 x)).ofLp j = ((B j.fst).repr (x j.fst)).ofLp j.snd
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.uncurry_apply : ∀ (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M]
  [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : IsScalarTower R A M] [inst_9 : AddCommMonoid N]
  [inst_10 : Module R N] [inst_11 : AddCommMonoid P] [inst_12 : Module R P] [inst_13 : Module A P]
  [inst_14 : IsScalarTower R A P] [inst_15 : Module B P] [inst_16 : IsScalarTower R B P] [inst_17 : SMulCommClass A B P]
  (f : M →ₗ[A] N →ₗ[R] P),
  (TensorProduct.AlgebraTensorModule.uncurry R A B M N P) f = TensorProduct.AlgebraTensorModule.lift f
-- Mathlib.RingTheory.LocalProperties.Semilocal
/-- A semilocal integral domain `A` is a PID if its localization at every maximal ideal is a PID.  -/
isPrincipalIdealRing_of_isPrincipalIdealRing_isLocalization_maximal : ∀ {R : Type u_1} [inst : CommRing R] [Finite (MaximalSpectrum R)] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2)
  [inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)]
  [inst_3 : (P : Ideal R) → [inst_3 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] [IsDomain R],
  (∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing (Rₚ P)) → IsPrincipalIdealRing R
-- Std.Time.Time.PlainTime
/-- Subtracts seconds from a `PlainTime`.
 -/
Std.Time.PlainTime.subSeconds : Std.Time.PlainTime → Std.Time.Second.Offset → Std.Time.PlainTime
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₄ = f.right.right
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.prevD_chainComplex : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) (j : ℕ),
  (prevD j) f = CategoryTheory.CategoryStruct.comp (f j (j + 1)) (Q.d (j + 1) j)
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_lt_toNNReal_iff' : ∀ {r p : ℝ}, r.toNNReal < p.toNNReal ↔ r < p ∧ 0 < p
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrRightEquiv_refl : ∀ {M : Type u_4} {N : Type u_8} [inst : AddZeroClass M] [inst_1 : AddMonoid N],
  (AddEquiv.refl N).addMonoidHomCongrRightEquiv = Equiv.refl (M →+ N)
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.mapFunctor_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) (a b : B) (f : a ⟶ b), (F.mapFunctor a b).obj f = F.map f
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are finite extensions of `F`,
such that rank of `A ⊔ B` is equal to the product of the rank of `A` and `B`,
then `A` and `B` are linearly disjoint.  -/
IntermediateField.LinearDisjoint.of_finrank_sup : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [FiniteDimensional F ↥A] [FiniteDimensional F ↥B],
  Module.finrank F ↥(A ⊔ B) = Module.finrank F ↥A * Module.finrank F ↥B → A.LinearDisjoint ↥B
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.memLp_top : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  {μ : MeasureTheory.Measure E} (f : ContDiffMapSupportedIn E F n K), MeasureTheory.MemLp ⇑f ⊤ μ
-- Mathlib.Order.BoundedOrder.Basic
IsBot.rec.eq_1 : ∀ {α : Type u} [inst : LE α] {motive : (x : α) → IsBot x → Sort u_1} (top : [inst_1 : OrderBot α] → motive ⊥ ⋯) (x : α)
  (hx : IsBot x), IsBot.rec top x hx = top
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendScalars.map'_id : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {M : ModuleCat R},
  ModuleCat.ExtendScalars.map' f (CategoryTheory.CategoryStruct.id M) =
    CategoryTheory.CategoryStruct.id (ModuleCat.ExtendScalars.obj' f M)
-- Mathlib.Analysis.Convex.KreinMilman
/-- **Krein-Milman theorem**: In an LCTVS, any compact convex set is the closure of the convex hull
of its extreme points.  -/
closure_convexHull_extremePoints : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [T2Space E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E},
  IsCompact s → Convex ℝ s → closure ((convexHull ℝ) (Set.extremePoints ℝ s)) = s
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add : ∀ {n a b c d : ℕ}, a ≡ b [MOD n] → c ≡ d [MOD n] → a + c ≡ b + d [MOD n]
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lsmul_apply : ∀ {R : Type u_2} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r : R)
  (m : M), ((LinearMap.lsmul R M) r) m = r • m
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
CategoryTheory.ObjectProperty.colimitsCardinalClosure_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (κ : Cardinal.{w})
  {Q : CategoryTheory.ObjectProperty C} [Q.IsClosedUnderIsomorphisms],
  (∀ (J : Type w) [inst_2 : CategoryTheory.SmallCategory J],
      HasCardinalLT (CategoryTheory.Arrow J) κ → Q.IsClosedUnderColimitsOfShape J) →
    P ≤ Q → P.colimitsCardinalClosure κ ≤ Q
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z : CategoryTheory.CommRingObjCat C} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Data.Matrix.Block
Matrix.toSquareBlock_def : ∀ {m : Type u_2} {α : Type u_12} {β : Type u_13} (M : Matrix m m α) (b : m → β) (k : β),
  M.toSquareBlock b k = Matrix.of fun i j => M ↑i ↑j
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.empty_sdiv : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] (t : Set β), ∅ /ₛ t = ∅
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_SpecMap : ∀ {n : Type u} {R S : CommRingCat} (φ : R ⟶ S),
  AlgebraicGeometry.AffineSpace.map n (AlgebraicGeometry.Spec.map φ) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.SpecIso n S).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))
        (AlgebraicGeometry.AffineSpace.SpecIso n R).inv)
-- Lean.Widget.InteractiveGoal
/-- The ids for each variable. Should have the same length as `names`.  -/
Lean.Widget.InteractiveHypothesisBundle.fvarIds : Lean.Widget.InteractiveHypothesisBundle → Array Lean.FVarId
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.normalize_testAgainstNN : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω)
  [inst_1 : TopologicalSpace Ω],
  μ ≠ 0 →
    ∀ (f : BoundedContinuousFunction Ω NNReal),
      μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.isBasis_restrict_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I X Y : Set α}, M.IsBasis I X → X ⊆ Y → (M.restrict Y).IsBasis I X
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.setLIntegral_condLExp_trim : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] (X : Ω → ENNReal) {s : Set Ω},
  MeasurableSet s → ∫⁻ (ω : Ω) in s, P⁻[X | mΩ] ω ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
-- Mathlib.Algebra.Category.BoolRing
instBooleanAlgebraCarrierToBddLatToBddDistLat : {X : BoolAlg} → BooleanAlgebra ↑X.toBddDistLat.toBddLat.toLat
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Fundamental theorem of calculus-2**, on semi-infinite intervals `(a, +∞)`.
When a function has a limit at infinity `m`, and its derivative is integrable, then the
integral of the derivative on `(a, +∞)` is `m - f a`. Version assuming differentiability
on `(a, +∞)` and continuity at `a⁺`.

Note that such a function always has a limit at infinity,
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi`.  -/
MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto : ∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} {m : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E],
  ContinuousWithinAt f (Set.Ici a) a →
    (∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x) →
      MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume →
        Filter.Tendsto f Filter.atTop (nhds m) → ∫ (x : ℝ) in Set.Ioi a, f' x = m - f a
-- Mathlib.Tactic.ITauto
/-- A reified inductive proof type for intuitionistic propositional logic.  -/
Mathlib.Tactic.ITauto.Proof : Type
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_one : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] [inst_1 : One G] [NormOneClass G], ‖1‖₊ = 1
-- Mathlib.Algebra.Category.MonCat.Basic
MulEquiv.toCommMonCatIso_hom : ∀ {X Y : Type u} [inst : CommMonoid X] [inst_1 : CommMonoid Y] (e : X ≃* Y),
  e.toCommMonCatIso.hom = CommMonCat.ofHom e.toMonoidHom
-- Mathlib.Analysis.Normed.Field.ProperSpace
/-- A weakly locally compact normed field is proper.
This is a specialization of `ProperSpace.of_locallyCompactSpace`
which holds for `NormedSpace`s but requires more imports.  -/
ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] [WeaklyLocallyCompactSpace 𝕜], ProperSpace 𝕜
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.tmulEquivDep_apply : ∀ {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (N : ι ⊕ ι₂ → Type u_12)
  [inst_1 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)] [inst_2 : (i : ι ⊕ ι₂) → Module R (N i)] (a : (i₁ : ι) → N (Sum.inl i₁))
  (b : (i₂ : ι₂) → N (Sum.inr i₂)),
  (PiTensorProduct.tmulEquivDep R N)
      (((PiTensorProduct.tprod R) fun i₁ => a i₁) ⊗ₜ[R] (PiTensorProduct.tprod R) fun i₂ => b i₂) =
    ⨂ₜ[R] (i : ι ⊕ ι₂), Sum.rec a b i
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.isAdjointPair_equiv' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {n : Type u_5} [inst_1 : Fintype n] (J A A' : Matrix n n R₂)
  [inst_2 : DecidableEq n] (P : Matrix n n R₂),
  IsUnit P →
    ((P.transpose * J * P).IsAdjointPair (P.transpose * J * P) A A' ↔ J.IsAdjointPair J (P * A * P⁻¹) (P * A' * P⁻¹))
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.unsortedEigenvectorBasis.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n),
  LinearMap.IsSymmetric.unsortedEigenvectorBasis✝ hT hn = DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- The topology on an `R`-module `M` associated to an ideal `M`. Submodules $I^n M$,
written `I^n • ⊤` form a basis of neighborhoods of zero.  -/
Ideal.adicModuleTopology : {R : Type u_1} →
  [inst : CommRing R] → Ideal R → (M : Type u_2) → [inst_1 : AddCommGroup M] → [Module R M] → TopologicalSpace M
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.rank.eq_2 : ∀ {α : Type u_1} (a : α) (c s : Batteries.BinomialHeap.Imp.HeapNode α),
  (Batteries.BinomialHeap.Imp.HeapNode.node a c s).rank = s.rank + 1
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.isGalois : ∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension S K L], IsGalois K L
-- Lean.Meta.Tactic.Contradiction
Lean.Meta.ElimEmptyInductive.instMonadBacktrackSavedStateM : Lean.MonadBacktrack Lean.Meta.SavedState Lean.Meta.ElimEmptyInductive.M
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_toAddSubmonoid : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M),
  (Submodule.map f p).toAddSubmonoid = AddSubmonoid.map (↑f) p.toAddSubmonoid
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instIsScalarTowerCircle : IsScalarTower Circle Circle Complex.UnitClosedDisc
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.le_tprod : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} [L.NeBot] [L.LeAtTop],
  Multipliable f L → ∀ (i : ι), (∀ (j : ι), j ≠ i → 1 ≤ f j) → f i ≤ ∏'[L] (i : ι), f i
-- Mathlib.Data.List.ModifyLast
List.modifyLast.go.eq_3 : ∀ {α : Type u_1} (f : α → α) (a : Array α) (x_2 : α) (xs : List α),
  (xs = [] → False) → List.modifyLast.go f (x_2 :: xs) a = List.modifyLast.go f xs (a.push x_2)
-- Mathlib.Tactic.NormNum.IsSquare
Mathlib.Meta.NormNum.isSquare_nat_of_isNat : ∀ (a n : ℕ), Mathlib.Meta.NormNum.IsNat a n → ∀ (m : ℕ), m * m = n → IsSquare a
-- Init.Data.Vector.Lex
Vector.map_le : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} [inst : LT α] [inst_1 : LT β] [Std.Asymm fun x1 x2 => x1 < x2]
  [Std.Trichotomous fun x1 x2 => x1 < x2] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {xs ys : Vector α n} {f : α → β}, (∀ (x y : α), x < y → f x < f y) → xs ≤ ys → Vector.map f xs ≤ Vector.map f ys
-- Lean.Elab.App
/-- Elaborate the given argument with the given expected type.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabElim.elabArg : Lean.Elab.Term.Arg → Lean.Expr → Lean.Elab.Term.ElabElim.M Lean.Expr
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atBot_mono : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {l : Filter α} {f g : α → β},
  (∀ (n : α), g n ≤ f n) → Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l Filter.atBot
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.coeffs_toPresentation_subset_coeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ), P.coeffs ⊆ P.coeffs
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_sq : ∀ (x : NNReal), NNReal.sqrt (x ^ 2) = x
-- Mathlib.Order.Booleanisation
Booleanisation.instDistribLattice : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → DistribLattice (Booleanisation α)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.A.eq_1 : ∀ {𝕜 : 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)
  (L : E →L[𝕜] F) (r ε : ℝ),
  FDerivMeasurableAux.A f L r ε =
    {x | ∃ r' ∈ Set.Ioc (r / 2) r, ∀ y ∈ Metric.ball x r', ∀ z ∈ Metric.ball x r', ‖f z - f y - L (z - y)‖ < ε * r}
-- Init.Data.SInt.Lemmas
Int16.ofNat_le_iff_le : ∀ {a b : ℕ}, a < 2 ^ 15 → b < 2 ^ 15 → (Int16.ofNat a ≤ Int16.ofNat b ↔ a ≤ b)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.snd_comp_inr : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂],
  ContinuousLinearMap.snd R M₁ M₂ ∘SL ContinuousLinearMap.inr R M₁ M₂ = ContinuousLinearMap.id R M₂
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`.  -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              CategoryTheory.Functor (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))
                (CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
-- Mathlib.Order.BoundedOrder.Basic
/-- `⊥` is the least element  -/
OrderBot.bot_le : ∀ {α : Type u} {inst : LE α} [self : OrderBot α] (a : α), ⊥ ≤ a
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Lattice.BicartSq.le₂₄ : ∀ {T : Type u} {x₁ x₂ x₃ x₄ : T} [inst : Lattice T], Lattice.BicartSq x₁ x₂ x₃ x₄ → x₂ ≤ x₄
-- Mathlib.Data.List.Basic
List.length_eq_three : ∀ {α : Type u} {l : List α}, l.length = 3 ↔ ∃ a b c, l = [a, b, c]
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.formatTactic : Lean.Syntax → Lean.CoreM Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom
      (CategoryTheory.Limits.pullback.fst i₁ i₂) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
        (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.comp_fst_add_comp_snd : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁] [inst_9 : AddCommMonoid M₂]
  [inst_10 : Module R M₂] (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M),
  f₁ ∘SL ContinuousLinearMap.fst R M₁ M₂ + f₂ ∘SL ContinuousLinearMap.snd R M₁ M₂ = f₁.coprod f₂
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_2}
  [inst_1 : Preorder J] [inst_2 : OrderBot J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c),
  (∀ (j : J), W (F.map (CategoryTheory.homOfLE ⋯))) → W.colimitsOfShape J (c.ι.app ⊥)
-- Mathlib.Data.Multiset.Bind
Multiset.coe_join : ∀ {α : Type u_1} (L : List (List α)), (↑(List.map Multiset.ofList L)).join = ↑L.flatten
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_biUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J), (π.biUnion πi).iUnion = ⋃ J ∈ π, (πi J).iUnion
-- Lean.Meta.Instances
Lean.Meta.defaultInstanceExtension : Lean.SimplePersistentEnvExtension Lean.Meta.DefaultInstanceEntry Lean.Meta.DefaultInstances
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.aux : Turing.PartrecToTM2.K'
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The evaluation map is continuous, as a joint function of `u` and `x`.  -/
BoundedContinuousFunction.instContinuousEval : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β],
  ContinuousEval (BoundedContinuousFunction α β) α β