mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmooth_respectsIso : RingHom.RespectsIso @RingHom.IsStandardSmooth
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.instProductive : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] [Std.Iterators.Finite α m] [Std.Iterators.Productive α₂ m],
  Std.Iterators.Productive (Std.Iterators.Types.Flatten α α₂ β m) m
-- Mathlib.LinearAlgebra.Vandermonde
_private.Mathlib.LinearAlgebra.Vandermonde.0.Matrix.of_eval_descPochhammer_eq_mul_of_choose : ∀ {n : ℕ} (v : Fin n → ℕ),
  (Matrix.of fun i j => Polynomial.eval (↑(v i)) (descPochhammer ℤ ↑j)).det =
    ↑(∏ i, (↑i).factorial) * (Matrix.of fun i j => ↑((v i).choose ↑j)).det
-- Mathlib.ModelTheory.LanguageMap
/-- The language map adding constants.  -/
FirstOrder.Language.lhomWithConstants : (L : FirstOrder.Language) → (α : Type w') → L →ᴸ L.withConstants α
-- Lean.Meta.WrapInstance
Lean.Meta.backward.inferInstanceAs.wrap.data : Lean.Option Bool
-- Mathlib.Data.Nat.Totient
/-- Euler's totient function. This counts the number of naturals strictly less than `n` which are
coprime with `n`.  -/
Nat.totient : ℕ → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.Hom.inhabited : {J : Type w} → Inhabited (CategoryTheory.Limits.WidePushoutShape.Hom none none)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induce_top : ∀ {V : Type u_1} (s : Set V), SimpleGraph.induce s (SimpleGraph.completeGraph V) = SimpleGraph.completeGraph ↑s
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.comp_X_add_C : ∀ {R : Type u_1} [inst : CommSemiring R] {f : Polynomial R},
  f.Splits → ∀ (a : R), (f.comp (Polynomial.X + Polynomial.C a)).Splits
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mem_toSubfield : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (s : IntermediateField K L)
  (x : L), x ∈ s.toSubfield ↔ x ∈ s
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_apply_isPrimePow_not_prime : ∀ {n : ℕ}, IsPrimePow n → ¬Nat.Prime n → ArithmeticFunction.moebius n = 0
-- Mathlib.Order.RelSeries
/-- In ℕ, two entries in an `LTSeries` differ by at least the difference of their indices.
(Expressed in a way that avoids subtraction).
 -/
LTSeries.apply_add_index_le_apply_add_index_nat : ∀ (p : LTSeries ℕ) (i j : Fin (p.length + 1)), i ≤ j → p.toFun i + ↑j ≤ p.toFun j + ↑i
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.id : ∀ (α : Type u) [inst : Preorder α], LeftOrdContinuous id
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lcs_zero : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (N : LieSubmodule R L M),
  LieSubmodule.lcs 0 N = N
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_mem_smul_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset β} {a : α} {b : β},
  b ∈ s → a • b ∈ a • s
-- Init.Data.Float.Model.Float32
Float32.Model.instSub : Sub Float32.Model
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar_empty : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G), MeasureTheory.Measure.haar.chaar K₀ ⊥ = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {outWidth : ℕ} [inst_2 : SizeOf α]
  {w len : ℕ} (oldLayer : aig.RefVec (len * w)) (h : outWidth = (len + 1) / 2 * w) (hlen : 0 < len),
  sizeOf { w := w, len := len, oldLayer := oldLayer, h := h, hlen := hlen } =
    1 + sizeOf w + sizeOf len + sizeOf oldLayer + sizeOf h + sizeOf hlen
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The quotient by a discontinuous group action of a locally compact T₂ space is T₂.  -/
t2Space_of_properlyDiscontinuousSMul_of_t2Space : ∀ {Γ : Type u_4} [inst : Group Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : MulAction Γ T] [T2Space T]
  [LocallyCompactSpace T] [ContinuousConstSMul Γ T] [ProperlyDiscontinuousSMul Γ T],
  T2Space (Quotient (MulAction.orbitRel Γ T))
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.integrable_fourierPowSMulRight : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V}
  [SecondCountableTopology V] {n : ℕ},
  MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ →
    MeasureTheory.AEStronglyMeasurable f μ →
      MeasureTheory.Integrable (fun v => VectorFourier.fourierPowSMulRight L f v n) μ
-- Init.Data.SInt.Lemmas
Int8.toBitVec_one : Int8.toBitVec 1 = 1#8
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  [inst_1 : Inhabited (β a)] {v : β k}, (m.insert k v).get! a = if h : (k == a) = true then cast ⋯ v else m.get! a
-- Mathlib.Data.DFinsupp.Module
DFinsupp.filter_smul : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : (i : ι) → SMulZeroClass γ (β i)]
  (p : ι → Prop) [inst_2 : DecidablePred p] (r : γ) (f : Π₀ (i : ι), β i),
  DFinsupp.filter p (r • f) = r • DFinsupp.filter p f
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.mul_left : ∀ {α : Type u_1} [inst : Monoid α] {a b c : α}, FiniteMultiplicity a (b * c) → FiniteMultiplicity a b
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- If `C` is a `V`-enriched ordinary category, and `C` has suitable limits,
then `J ⥤ C` is also a `J ⥤ V`-enriched ordinary category.  -/
CategoryTheory.Enriched.FunctorCategory.functorEnrichedCategory : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u₂) →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          (J : Type u₃) →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                [∀ (F₁ F₂ : CategoryTheory.Functor J C),
                      CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] →
                  CategoryTheory.EnrichedCategory (CategoryTheory.Functor J V) (CategoryTheory.Functor J C)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_cosh_ofReal_re : ∀ (x : ℝ), ↑(Complex.cosh ↑x).re = Complex.cosh ↑x
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.derivSeries_eq_zero : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}, p (n + 1) = 0 → p.derivSeries n = 0
-- Init.Data.List.Nat.Basic
List.dropLast.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : List α) (h_1 : Unit → motive []) (h_2 : (head : α) → motive [head])
  (h_3 : (a : α) → (as : List α) → motive (a :: as)),
  x = [] →
    (match x with
      | [] => h_1 ()
      | [head] => h_2 head
      | a :: as => h_3 a as) ≍
      h_1 ()
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.continuous : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} (F : f₀.HomotopyWith f₁ P), Continuous ⇑F
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeConnected.zero : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsEdgeConnected 0
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
/-- Sorts assignment first by expression generation and then `Expr.lt`  -/
_private.Lean.Meta.Tactic.Grind.Arith.ModelUtil.0.Lean.Meta.Grind.Arith.sortModel : Lean.Meta.Grind.Goal → Array (Lean.Expr × ℚ) → Array (Lean.Expr × ℚ)
-- Mathlib.CategoryTheory.Category.Basic
/-- Notation for whiskering an equation by a morphism (on the right).
If `f g : X ⟶ Y` and `w : f = g` and `h : Y ⟶ Z`, then `w =≫ h : f ≫ h = g ≫ h`.
 -/
CategoryTheory.«term_=≫_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.eta_q_eq_pow : ∀ (n : ℕ) (z : ℂ), ModularForm.eta_q n z = Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ (n + 1)
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_prod_val : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Encodable β] (n : ℕ),
  Encodable.decode n =
    (Encodable.decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (Encodable.decode (Nat.unpair n).2)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
/-- If a closed set has a thickening with finite measure, then the measure of its
`r`-thickenings converge to its measure as `r > 0` tends to `0`.  -/
tendsto_measure_thickening_of_isClosed : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  (∃ R > 0, μ (Metric.thickening R s) ≠ ⊤) →
    IsClosed s → Filter.Tendsto (fun r => μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (μ s))
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.listProd : ∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
  {ι : Type u_16} {L : List ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'},
  (∀ i ∈ L, f i =Θ[l] g i) →
    (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =Θ[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
-- Mathlib.SetTheory.Cardinal.CountableCover
/-- If a set `t` is eventually covered by a countable family of sets, all with cardinality at
most `a`, then the cardinality of `t` is also bounded by `a`.  -/
Cardinal.mk_subtype_le_of_countable_eventually_mem : ∀ {α : Type u} {ι : Type v} {a : Cardinal.{u}} [Countable ι] {f : ι → Set α} {l : Filter ι} [l.NeBot] {t : Set α},
  (∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) ≤ a) → Cardinal.mk ↑t ≤ a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, m.isEmpty = true → m.getKeyD a fallback = fallback
-- Lean.Elab.InfoTree.Types
Lean.Elab.CustomInfo.mk : Lean.Syntax → Dynamic → Lean.Elab.CustomInfo
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.comp_assoc : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] [inst_3 : AddCommMonoid B] [inst_4 : Module R B]
  [inst_5 : AddCommMonoid C] [inst_6 : Module R C] [inst_7 : AddCommMonoid D] [inst_8 : Module R D]
  [inst_9 : CoalgebraStruct R A] [inst_10 : CoalgebraStruct R B] [inst_11 : CoalgebraStruct R C]
  [inst_12 : CoalgebraStruct R D] (φ₁ : C →ₗc[R] D) (φ₂ : B →ₗc[R] C) (φ₃ : A →ₗc[R] B),
  (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
-- Mathlib.Topology.Order.OrderClosed
continuousWithinAt_Icc_iff_Ici : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α]
  [inst_3 : TopologicalSpace β] {a b : α} {f : α → β},
  b < a → (ContinuousWithinAt f (Set.Icc b a) b ↔ ContinuousWithinAt f (Set.Ici b) b)
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_1.eq_4 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match true, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_4 ()
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.inter_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ m₃ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₂.Equiv m₃ → (m₁ ∩ m₂).Equiv (m₁ ∩ m₃)
-- Init.GrindInstances.ToInt
Lean.Grind.instAddUInt32UintOfNatNat : Lean.Grind.ToInt.Add UInt32 (Lean.Grind.IntInterval.uint 32)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.vcomp_naturality_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G)
  (θ : CategoryTheory.Oplax.StrongTrans G H) {a b : B} (f : a ⟶ b),
  ((η.vcomp θ).naturality f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).inv)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (θ.app b)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).inv (θ.app b))
            (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (θ.app b)).hom)))
-- Lean.Elab.MutualInductive
/-- We don't assign the metavariable in the resulting universe right away in `inferResultingUniverse`.
The issue is that there may be level metavariables in the assignment that will eventually become
parameters, and we want to be sure we assign once we can normalize the level being assigned.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ResultingUniverseResult : Type
-- Init.Data.Char.Lemmas
Char.toNat_mk : ∀ {val : UInt32} {h : val.isValidChar}, { val := val, valid := h }.toNat = val.toNat
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (cmp ((t.insertIfNew k v).minKey ⋯) k).isLE = true
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} (a b : ℕ),
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.partialTraj κ a b)
-- Init.Internal.Order.Basic
Lean.Order.is_sup_unique : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] {c : α → Prop} {s₁ s₂ : α},
  Lean.Order.is_sup c s₁ → Lean.Order.is_sup c s₂ → s₁ = s₂
-- Init.SizeOf
/-- Every type `α` has a default `SizeOf` instance that just returns `0`
for every element of `α`.
 -/
default.sizeOf : (α : Sort u) → α → ℕ
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.eq_comp_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : Y ⟶ X) [inst_1 : CategoryTheory.IsIso α]
  {f : Z ⟶ X} {g : Z ⟶ Y},
  g = CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) ↔ CategoryTheory.CategoryStruct.comp g α = f
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.request.inj : ∀ {id : Lean.JsonRpc.RequestID} {method : String} {params? : Option Lean.Json.Structured}
  {id_1 : Lean.JsonRpc.RequestID} {method_1 : String} {params?_1 : Option Lean.Json.Structured},
  Lean.JsonRpc.Message.request id method params? = Lean.JsonRpc.Message.request id_1 method_1 params?_1 →
    id = id_1 ∧ method = method_1 ∧ params? = params?_1
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.id_tfst : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t] {α β : Type u} (x : t α β),
  Bitraversable.tfst pure x = pure x
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_diagonal : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : Preorder α] [inst_1 : Zero R] [inst_2 : DecidableEq m]
  (d : m → R), (Matrix.diagonal d).BlockTriangular b
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_obj_left : ∀ {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) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).inverse.obj X).left = X.left
-- Init.Data.Range.Polymorphic.Fin
Fin.instLeast?OfNeZeroNat : {n : ℕ} → [NeZero n] → Std.PRange.Least? (Fin n)
-- Lean.DocString.Parser
/-- How many underscores introduced the current level of emphasis? `none` means no emphasis here.
 -/
Lean.Doc.Parser.InlineCtxt.emphDepth : Lean.Doc.Parser.InlineCtxt → Option ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The initial vertex of a 2-simplex in a 2-truncated simplicial set.  -/
SSet.Truncated.ev0₂ : {V : SSet.Truncated 2} →
  V.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 }) → SSet.OneTruncation₂ V
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.instMonoHomologyMapIntι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n₁ : ℤ),
  CategoryTheory.Mono
    (HomologicalComplex.homologyMap (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι✝ f n₁) n₁)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Report places where `omega` can be replaced by `lia`.  -/
omegaToLia : Mathlib.TacticAnalysis.Config
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is strictly between the other two, the angle at the first point
is zero.  -/
Sbtw.angle₂₁₃_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₂ p₁ p₃ = 0
-- Std.Time.DateTime.Timestamp
Std.Time.instLTTimestamp : LT Std.Time.Timestamp
-- Mathlib.Tactic.Widget.StringDiagram
/-- The vertical position of the node in the string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.AtomNode.vPos : Mathlib.Tactic.Widget.StringDiagram.AtomNode → ℕ
-- Mathlib.Algebra.Star.Unitary
Unitary.star_mem : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R → star U ∈ unitary R
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_base_coe : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥↑((TopologicalSpace.Opens.map f.base).obj U)),
  ↑((f ∣_ U) x) = f ↑x
-- Mathlib.Order.Comparable
antisymmRel_compl_apply : ∀ {α : Type u_1} {a b : α} (r : α → α → Prop), AntisymmRel rᶜ a b ↔ IncompRel r a b
-- Mathlib.Algebra.GroupWithZero.Action.Units
SemiconjBy.smul_left_iff₀ : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α} [inst_2 : Mul β]
  [SMulCommClass α β β] [IsScalarTower α β β] {x y z : β}, a ≠ 0 → (SemiconjBy (a • x) y z ↔ SemiconjBy x y z)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.nonsingularPointEquiv_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} (h : W'.Nonsingular x y),
  W'.nonsingularPointEquiv (WeierstrassCurve.Affine.Point.some x y h) = some ⟨(x, y), h⟩
-- Mathlib.Analysis.Convex.Basic
Convex.mem_smul_of_zero_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {x : E}, 0 ∈ s → x ∈ s → ∀ {t : 𝕜}, 1 ≤ t → x ∈ t • s
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rcc_eq_zero : ∀ {m n i : ℕ}, n + 1 ≤ i + m → (m...=n).toList[i]! = 0
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.structureMap_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} {x : (i : ι) → ↑(A i)} (i : ι),
  (RestrictedProduct.structureMap R A 𝓕 x) i = ↑(x i)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The additive closure of a non-unital subsemigroup is a non-unital subsemiring.  -/
Subsemigroup.nonUnitalSubsemiringClosure : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → Subsemigroup R → NonUnitalSubsemiring R
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.rnDeriv_tilted_left_self : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.SigmaFinite μ],
  AEMeasurable f μ →
    (μ.tilted f).rnDeriv μ =ᵐ[μ] fun x => ENNReal.ofReal (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ)
-- Init.System.IO
/-- Add or remove environment variables for the child process.

The child process inherits the parent's environment, as modified by `env`. Keys in the array are
the names of environment variables. A `none`, causes the entry to be removed from the environment,
and `some` sets the variable to the new value, adding it if necessary. Variables are processed from left to right.
 -/
IO.Process.SpawnArgs.env : IO.Process.SpawnArgs → Array (String × Option String)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.trans_assoc : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {V₄ : Type u_7} {P : Type u_10} {P₂ : Type u_11}
  {P₃ : Type u_12} {P₄ : Type u_13} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P]
  [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂] [inst_7 : PseudoMetricSpace P₂]
  [inst_8 : NormedAddTorsor V₂ P₂] [inst_9 : SeminormedAddCommGroup V₃] [inst_10 : NormedSpace 𝕜 V₃]
  [inst_11 : PseudoMetricSpace P₃] [inst_12 : NormedAddTorsor V₃ P₃] [inst_13 : SeminormedAddCommGroup V₄]
  [inst_14 : NormedSpace 𝕜 V₄] [inst_15 : PseudoMetricSpace P₄] [inst_16 : NormedAddTorsor V₄ P₄] (ePP₂ : P ≃ᵃⁱ[𝕜] P₂)
  (eP₂G : P₂ ≃ᵃⁱ[𝕜] P₃) (eGG' : P₃ ≃ᵃⁱ[𝕜] P₄), ePP₂.trans (eP₂G.trans eGG') = (ePP₂.trans eP₂G).trans eGG'
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.mulEquivCongrRight_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsMonHom e.hom] (X : C)
  (a : ↑((CategoryTheory.yonedaMon.obj { X := M, mon := inst_2 }).obj (Opposite.op X))),
  (CategoryTheory.Hom.mulEquivCongrRight e X) a =
    (MonCat.Hom.hom (MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom e.hom X))) a
-- Mathlib.Logic.Embedding.Basic
subtypeOrLeftEmbedding_apply_left : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] (x : { x // p x ∨ q x }) (hx : p ↑x),
  (subtypeOrLeftEmbedding p q) x = Sum.inl ⟨↑x, hx⟩
-- Mathlib.Order.LatticeIntervals
/-- `Icc a b` has a top element whenever `a ≤ b`.  -/
Set.Icc.instOrderTopElemOfFactLe : {α : Type u_1} → {a b : α} → [inst : Preorder α] → [Fact (a ≤ b)] → OrderTop ↑(Set.Icc a b)
-- Init.Core
/-- An alternative induction or recursion operator for defining binary operations on quotients that can
be used when the target type is a subsingleton.

In these cases, the proof that the function respects the quotient's equivalence relation is trivial,
so any function can be lifted.
 -/
Quotient.recOnSubsingleton₂ : {α : Sort uA} →
  {β : Sort uB} →
    {s₁ : Setoid α} →
      {s₂ : Setoid β} →
        {motive : Quotient s₁ → Quotient s₂ → Sort uC} →
          [s : ∀ (a : α) (b : β), Subsingleton (motive ⟦a⟧ ⟦b⟧)] →
            (q₁ : Quotient s₁) → (q₂ : Quotient s₂) → ((a : α) → (b : β) → motive ⟦a⟧ ⟦b⟧) → motive q₁ q₂