mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  (S T : J.Cover X), (∀ ⦃Y : C⦄ (f : Y ⟶ X), (↑S).arrows f ↔ (↑T).arrows f) → S = T
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.continuous_const_rpow : ∀ {a : ℝ}, a ≠ 0 → Continuous fun x => a ^ x
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.utf8DecodeChar?_eq_assemble₂ : ∀ {b : ByteArray} (hb : 2 ≤ b.size),
  ByteArray.utf8DecodeChar?.parseFirstByte b[0] = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
    b.utf8DecodeChar? 0 = ByteArray.utf8DecodeChar?.assemble₂ b[0] b[1]
-- Mathlib.Analysis.InnerProductSpace.MulOpposite
Module.Basis.mulOpposite_is_orthonormal_iff : ∀ {𝕜 : Type u_1} {H : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  {ι : Type u_3} (b : Module.Basis ι 𝕜 H), Orthonormal 𝕜 ⇑b.mulOpposite ↔ Orthonormal 𝕜 ⇑b
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_take_mul_prod_drop : ∀ {M : Type u_4} [inst : Monoid M] (L : List M) (i : ℕ), (List.take i L).prod * (List.drop i L).prod = L.prod
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.ext : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.IrreducibleCloseds α}, ↑s = ↑t → s = t
-- Batteries.Tactic.NoMatch
/-- The syntax `intro.` is deprecated in favor of `nofun`.
 -/
Batteries.Tactic.introDot : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.det_surjective : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Nonempty n],
  Function.Surjective ⇑Matrix.GeneralLinearGroup.det
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_erase!_eq_of_not_compare_minKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ¬compare k t.minKey! = Ordering.eq → (Std.DTreeMap.Internal.Impl.erase! k t).minKey! = t.minKey!
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsSeparator.isDetector : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Balanced C] {G : C},
  CategoryTheory.IsSeparator G → CategoryTheory.IsDetector G
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddCommGrpCat.FilteredColimits.G.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommGrpCat),
  AddCommGrpCat.FilteredColimits.G F =
    AddGrpCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))
-- Mathlib.Data.List.Shortlex
/-- If two lists `s` and `t` have the same length, `s` is smaller than `t` under the shortlex order
over a relation `r` exactly when `s` is smaller than `t` under the lexicographic order over `r`.  -/
List.shortlex_iff_lex : ∀ {α : Type u_1} {r : α → α → Prop} {s t : List α}, s.length = t.length → (List.Shortlex r s t ↔ List.Lex r s t)
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.mk.injEq : ∀ (ref : Lean.Syntax) (terminationBy?? : Option Lean.Syntax) (terminationBy? : Option Lean.Elab.TerminationBy)
  (partialFixpoint? : Option Lean.Elab.PartialFixpoint) (decreasingBy? : Option Lean.Elab.DecreasingBy)
  (extraParams : ℕ) (ref_1 : Lean.Syntax) (terminationBy??_1 : Option Lean.Syntax)
  (terminationBy?_1 : Option Lean.Elab.TerminationBy) (partialFixpoint?_1 : Option Lean.Elab.PartialFixpoint)
  (decreasingBy?_1 : Option Lean.Elab.DecreasingBy) (extraParams_1 : ℕ),
  ({ ref := ref, terminationBy?? := terminationBy??, terminationBy? := terminationBy?,
        partialFixpoint? := partialFixpoint?, decreasingBy? := decreasingBy?, extraParams := extraParams } =
      { ref := ref_1, terminationBy?? := terminationBy??_1, terminationBy? := terminationBy?_1,
        partialFixpoint? := partialFixpoint?_1, decreasingBy? := decreasingBy?_1, extraParams := extraParams_1 }) =
    (ref = ref_1 ∧
      terminationBy?? = terminationBy??_1 ∧
        terminationBy? = terminationBy?_1 ∧
          partialFixpoint? = partialFixpoint?_1 ∧ decreasingBy? = decreasingBy?_1 ∧ extraParams = extraParams_1)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Given three points on a circle, the center of that circle may be expressed explicitly as a
multiple (by half the inverse of the tangent of the angle at one of those points) of a `π / 2`
rotation of the vector between the other two points, plus the midpoint of those points.  -/
EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  p₁ ∈ s →
    p₂ ∈ s →
      p₃ ∈ s →
        p₁ ≠ p₂ →
          p₁ ≠ p₃ →
            p₂ ≠ p₃ →
              ((EuclideanGeometry.oangle p₁ p₂ p₃).tan⁻¹ / 2) •
                    (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (p₃ -ᵥ p₁) +ᵥ
                  midpoint ℝ p₁ p₃ =
                s.center
-- Mathlib.Data.List.AList
AList.keys_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} (s : AList β),
  (AList.insert a b s).keys = a :: s.keys.erase a
-- Mathlib.Algebra.Lie.Matrix
lieEquivMatrix'_symm_apply : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (A : Matrix n n R),
  lieEquivMatrix'.symm A = Matrix.toLin' A
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.divRight.eq_1 : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul Gᵐᵒᵖ G] (c : G),
  IsometryEquiv.divRight c = { toEquiv := Equiv.divRight c, isometry_toFun := ⋯ }
-- Mathlib.Algebra.Group.Equiv.Defs
AddHom.toAddEquiv.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (g : N →ₙ+ M)
  (h₁ : g.comp f = AddHom.id M) (h₂ : f.comp g = AddHom.id N),
  f.toAddEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.rel_of_isEqv : ∀ {α : Type u_1} {r : α → α → Bool} {xs ys : Array α},
  xs.isEqv ys r = true → ∃ (h : xs.size = ys.size), ∀ (i : ℕ) (h' : i < xs.size), r xs[i] ys[i] = true
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instOrderBot : {V : Type u} → {G : SimpleGraph V} → OrderBot G.Finsubgraph
-- Lean.MetavarContext
Lean.MetavarContext.levelMVarToParam : Lean.MetavarContext →
  (Lean.Name → Bool) →
    (Lean.LMVarId → Bool) → Lean.Expr → optParam Lean.Name `u → optParam ℕ 1 → Lean.MetavarContext.UnivMVarParamResult
-- Mathlib.Algebra.Category.MonCat.Limits
/-- We show that the forgetful functor `CommMonCat ⥤ MonCat` creates limits.

All we need to do is notice that the limit point has a `CommMonoid` instance available,
and then reuse the existing limit.  -/
CommMonCat.forget₂CreatesLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommMonCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] →
        CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommMonCat MonCat)
-- Mathlib.Util.CountHeartbeats
/-- Guard the minimal number of heartbeats used in the enclosed command.

This is most useful in the context of debugging and minimizing an example of a slow declaration.
By guarding the number of heartbeats used in the slow declaration,
an error message will be generated if a minimization step makes the slow behaviour go away.

The default number of minimal heartbeats is the value of `maxHeartbeats` (typically 200000).
Alternatively, you can specify a number of heartbeats to guard against,
using the syntax `guard_min_heartbeats n in cmd`.

The optional `approximately` keyword rounds down the heartbeats to the nearest thousand.
This helps make the tests more stable to small changes in heartbeats.
To use this functionality, use `guard_min_heartbeats approximately (n)? in cmd`.
 -/
Mathlib.CountHeartbeats.commandGuard_min_heartbeatsApproximately_In__ : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.X_mul_monomial : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R),
  Polynomial.X * (Polynomial.monomial n) r = (Polynomial.monomial (n + 1)) r
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
SemimoduleCat.MonoidalCategory.braiding_hom_apply : ∀ {R : Type u} [inst : CommSemiring R] {M N : SemimoduleCat R} (m : ↑M) (n : ↑N),
  (CategoryTheory.ConcreteCategory.hom (β_ M N).hom) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.UseImplicitLambdaResult.no.sizeOf_spec : sizeOf Lean.Elab.Term.UseImplicitLambdaResult.no = 1
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualRestrict_leftInverse : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (W : Subspace K V),
  Function.LeftInverse ⇑(Submodule.dualRestrict W) ⇑W.dualLift
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst : ∀ (X Y : Type u),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).inv
      CategoryTheory.Limits.prod.fst =
    TypeCat.ofHom Prod.fst
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasDerivAtFilter.add` -/
HasDerivAtFilter.fun_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → HasDerivAtFilter g g' L → HasDerivAtFilter (fun i => f i + g i) (f' + g') L
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_inverse : ∀ {C : Type (u₁ + 1)} [inst : CategoryTheory.LargeCategory C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C],
  (CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts C).inverse = CategoryTheory.Mat_.embedding C
-- Mathlib.Data.Set.Insert
Set.range_ite_const : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} [inst : DecidablePred p] {x y : β},
  (∃ a, p a) → (∃ a, ¬p a) → (Set.range fun a => if p a then x else y) = {x, y}
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The functor `uliftFunctor : AddCommGrpCat.{u} ⥤ AddCommGrpCat.{max u v}` preserves colimits
of arbitrary size.
 -/
AddCommGrpCat.instPreservesColimitsOfSizeUliftFunctor : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} AddCommGrpCat.uliftFunctor
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insert.go.match_1.congr_eq_1 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.lt),
  x = Ordering.eq →
    (match x with
      | Ordering.eq => h_1 ()
      | Ordering.gt => h_2 ()
      | Ordering.lt => h_3 ()) ≍
      h_1 ()
-- Init.Data.Nat.Basic
Nat.le_pred_iff_lt : ∀ {n : ℕ} {m : ℕ}, 0 < m → (n ≤ m.pred ↔ n < m)
-- Mathlib.Algebra.Group.Units.Equiv
AddUnits.addRight.eq_1 : ∀ {M : Type u_3} [inst : AddMonoid M] (u : AddUnits M),
  u.addRight = { toFun := fun x => x + ↑u, invFun := fun x => x + ↑(-u), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Group.Ideal
/-- A (left) additive semigroup ideal in an additive semigroup `M` is a set `s` such
that `a + b ∈ s` whenever `b ∈ s`.  -/
AddSemigroupIdeal : (M : Type u_1) → [Add M] → Type u_1
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousNeg.mk : ∀ {G : Type u} [inst : TopologicalSpace G] [inst_1 : Neg G], (Continuous fun a => -a) → ContinuousNeg G
-- Mathlib.Order.Interval.Finset.Basic
Finset.mem_uIcc_of_le : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, a ≤ x → x ≤ b → x ∈ Finset.uIcc a b
-- Mathlib.Analysis.Convex.StrictConvexSpace
abs_lt_norm_sub_of_not_sameRay : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
  ¬SameRay ℝ x y → |‖x‖ - ‖y‖| < ‖x - y‖
-- Mathlib.Order.Concept
Concept.isExtent_iff_exists_concept : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α}, Order.IsExtent r s ↔ ∃ c, c.extent = s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_le_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k km : α} (hc : k ∈ t), t.minKey?.get ⋯ = km → (compare km k).isLE = true
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- Smooth morphisms are locally of finite presentation.  -/
AlgebraicGeometry.instLocallyOfFinitePresentationOfSmooth : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [hf : AlgebraicGeometry.Smooth f],
  AlgebraicGeometry.LocallyOfFinitePresentation f
-- Mathlib.Data.PNat.Notation
/-- The underlying natural number  -/
PNat.val : ℕ+ → ℕ
-- Mathlib.CategoryTheory.Iso
CategoryTheory.isIso_of_comp_hom_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (g : Y ⟶ X) [CategoryTheory.IsIso g] {f : X ⟶ Y},
  CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X → CategoryTheory.IsIso f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).min ⋯ = t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)))
      CategoryTheory.Oplax.LaxTrans.Modification.naturality._autoParam)
  (app_1 : (a : B) → η.app a ⟶ θ.app a)
  (naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b)))
      CategoryTheory.Oplax.LaxTrans.Modification.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool}
  {k fallback : α}, (Std.HashSet.filter f m).getD k fallback = (Option.filter f (m.get? k)).getD fallback
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.adj_penultimate : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, ¬p.Nil → G.Adj p.penultimate w
-- Std.Data.Iterators.Producers.Repeat
Std.Iterators.Types.RepeatIterator.mk : {α : Type u} → {f : α → α} → α → Std.Iterators.Types.RepeatIterator α f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} (hom : M.X ⟶ N.X) [isAddMonHom_hom : CategoryTheory.IsAddMonHom hom]
  (hom_1 : M.X ⟶ N.X) (isAddMonHom_hom_1 : CategoryTheory.IsAddMonHom hom_1),
  ({ hom := hom, isAddMonHom_hom := isAddMonHom_hom } = { hom := hom_1, isAddMonHom_hom := isAddMonHom_hom_1 }) =
    (hom = hom_1)
-- Mathlib.Tactic.Explode.Datatypes
/-- The row number, starting from `0`. This is set by `Entries.add`.  -/
Mathlib.Explode.Entry.line : Mathlib.Explode.Entry → Option ℕ
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.dvd_of_mem_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a p : Associates α},
  p ∈ a.factors → p ∣ a
-- Mathlib.Geometry.Manifold.SmoothEmbedding
Manifold.isSmoothEmbedding_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : NormedAddCommGroup E₃] [inst_4 : NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8}
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] (I : ModelWithCorners 𝕜 E₁ H)
  (J : ModelWithCorners 𝕜 E₃ G) {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N),
  Manifold.IsSmoothEmbedding I J n f ↔ Manifold.IsImmersion I J n f ∧ Topology.IsEmbedding f
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_toIcoMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a₁ a₂ b : α), toIocMod hp a₁ (toIcoMod hp a₂ b) = toIocMod hp a₁ b
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.instGeometricallyConnectedFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyConnected g],
  AlgebraicGeometry.GeometricallyConnected (CategoryTheory.Limits.pullback.fst f g)
-- Lean.Syntax
Lean.Syntax.TopDown.mk.sizeOf_spec : ∀ (firstChoiceOnly : Bool) (stx : Lean.Syntax),
  sizeOf { firstChoiceOnly := firstChoiceOnly, stx := stx } = 1 + sizeOf firstChoiceOnly + sizeOf stx
-- Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
HomotopicalAlgebra.FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.FibrantObject.localizerMorphism C).arrow.HasRightResolutions
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (j : Fin (n + 1)),
  CategoryTheory.CategoryStruct.comp (self.h j.succ) (Y.δ j.castSucc.succ) =
    CategoryTheory.CategoryStruct.comp (self.h j.castSucc) (Y.δ j.castSucc.succ)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Nat.iterate.match_1.splitter : {α : Sort u_2} →
  (motive : ℕ → α → Sort u_1) →
    (x : ℕ) → (x_1 : α) → ((a : α) → motive 0 a) → ((k : ℕ) → (a : α) → motive k.succ a) → motive x x_1
-- Mathlib.Data.Stream.Init
Stream'.head_even : ∀ {α : Type u} (s : Stream' α), s.even.head = s.head
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_of_mul_apply_aux : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddMonoid ι] [inst_5 : SetLike.GradedMonoid A] {i : ι}
  (r : ↥(A i)) (r' : DirectSum ι fun i => ↥(A i)) {j n : ι},
  (∀ (x : ι), i + x = n ↔ x = j) → ↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = ↑r * ↑(r' j)
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of `f₁ + f₂` is larger than or equal to the minimum of the divisors of `f₁` and `f₂`,
respectively.
 -/
MeromorphicOn.min_divisor_le_divisor_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {z : 𝕜} {U : Set 𝕜},
  MeromorphicOn f₁ U →
    MeromorphicOn f₂ U →
      z ∈ U →
        meromorphicOrderAt (f₁ + f₂) z ≠ ⊤ →
          min ((MeromorphicOn.divisor f₁ U) z) ((MeromorphicOn.divisor f₂ U) z) ≤ (MeromorphicOn.divisor (f₁ + f₂) U) z
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.eval_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (F : CategoryTheory.Functor C A)
  {X Y : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Y),
  ((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F).map f =
    CategoryTheory.Limits.Sigma.desc fun i =>
      CategoryTheory.CategoryStruct.comp (F.map (f.φ i)) (CategoryTheory.Limits.Sigma.ι (F.obj ∘ Y.obj) (f.f i))
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_pow : ∀ (a : ENNReal) (n : ℕ), (a ^ n).toNNReal = a.toNNReal ^ n
-- Lean.Elab.InfoTree.Types
/-- Info for an error name provided as an identifier to one of the named-error macros (`throwNamedError`
or similar).

Note that this is *not* added for `Name` terms passed to the underlying functions (e.g.,
`Lean.throwNamedError`), though these functions generally should not be invoked directly anyway.
 -/
Lean.Elab.ErrorNameInfo : Type
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.smul_measure : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {R : Type u_5} [inst_1 : SMul R ENNReal] [inst_2 : IsScalarTower R ENNReal ENNReal],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : R), MeasureTheory.AEStronglyMeasurable f (c • μ)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.smul_def : ∀ {R : Type u} [inst : NonAssocRing R] {α : Type u_1} [inst_1 : SMul R α] {S : Subring R} (g : ↥S) (m : α),
  g • m = ↑g • m
-- Mathlib.Algebra.Group.Defs
/-- Any `AddCommMagma G` that
satisfies `IsRightCancelAdd G` also satisfies `IsLeftCancelAdd G`.  -/
AddCommMagma.IsRightCancelAdd.toIsLeftCancelAdd : ∀ (G : Type u) [inst : AddCommMagma G] [IsRightCancelAdd G], IsLeftCancelAdd G
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- Order of vanishing function for elements of a ring.
 -/
Ring.ord : (R : Type u_1) → [Ring R] → R → ℕ∞
-- Mathlib.Order.LatticeIntervals
Set.Iic.instLatticeElem : {α : Type u_1} → {a : α} → [inst : Lattice α] → Lattice ↑(Set.Iic a)
-- Init.Prelude
Nat.zero_le : ∀ (n : ℕ), 0 ≤ n
-- Mathlib.Data.Matrix.Basic
Equiv.mapMatrix_refl : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11}, (Equiv.refl α).mapMatrix = Equiv.refl (Matrix m n α)
-- Mathlib.Analysis.Normed.Group.Basic
enorm_one' : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedMonoid E], ‖1‖ₑ = 0
-- Init.Data.List.Control
List.foldrM_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {b : β},
  List.foldrM f b [] = pure b
-- Mathlib.Data.UInt
UInt32.instCommMonoid : CommMonoid UInt32
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A union indexed by a finite set is totally bounded
if and only if each set of the family is totally bounded.  -/
totallyBounded_biUnion : ∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Type u_1} {I : Set ι},
  I.Finite → ∀ {s : ι → Set α}, TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
-- Mathlib.LinearAlgebra.Pi
Fin.consLinearEquiv_symm_apply : ∀ (R : Type u) {n : ℕ} (M : Fin n.succ → Type u_1) [inst : Semiring R] [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)]
  [inst_2 : (i : Fin n.succ) → Module R (M i)] (a : (i : Fin (n + 1)) → M i),
  (Fin.consLinearEquiv R M).symm a = (Fin.consEquiv M).invFun a
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldRedeclInfo.stx : Lean.Elab.FieldRedeclInfo → Lean.Syntax
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_vert_isIso_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} [CategoryTheory.Epi g] [CategoryTheory.IsIso inl],
  CategoryTheory.CommSq f g inl inr → CategoryTheory.IsPushout f g inl inr