mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.integralCLM_apply : ∀ (𝕜 : Type u_2) {D : Type u_4} {V : Type u_9} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace ℝ D] [inst_3 : NormedAddCommGroup V] [inst_4 : NormedSpace ℝ V] [inst_5 : NormedSpace 𝕜 V]
  [inst_6 : MeasurableSpace D] {μ : MeasureTheory.Measure D} [hμ : μ.HasTemperateGrowth] [inst_7 : BorelSpace D]
  [inst_8 : SecondCountableTopology D] (f : SchwartzMap D V), (SchwartzMap.integralCLM 𝕜 μ) f = ∫ (x : D), f x ∂μ
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.mk : (toBoolAlg : BoolAlg) → [isFintype : Fintype ↑toBoolAlg] → FinBoolAlg
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinalInterFilter_bot : ∀ {α : Type u} {c : Cardinal.{u}}, CardinalInterFilter ⊥ c
-- Mathlib.LinearAlgebra.Complex.Module
/-- The natural `LinearEquiv` from `ℂ` to `ℝ × ℝ`.  -/
Complex.equivRealProdLm : ℂ ≃ₗ[ℝ] ℝ × ℝ
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- A discriminator tree for the current module's declarations only.

Note: We use different discrimination trees for imported and current module
declarations since imported declarations are typically much more numerous but
not changed while the current module is edited.
 -/
Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef : Type → Type
-- Mathlib.Analysis.Convex.Segment
segment.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x y : E), segment 𝕜 x y = {z | ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a • x + b • y = z}
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.pred_le_iff : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α] [inst_1 : PredOrder α],
  Order.IsPredLimit b → (Order.pred a ≤ b ↔ a ≤ b)
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.left_eq_of_right_ne : ∀ {α : Type u_1} {β : Type u_2} {x y z w : α} {e : β} {G : Graph α β}, G.IsLink e x y → G.IsLink e z w → x ≠ z → x = w
-- Mathlib.Algebra.Order.Field.Basic
div_nonneg_of_nonpos : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a ≤ 0 → b ≤ 0 → 0 ≤ a / b
-- Lean.Language.Basic
Lean.Language.SnapshotBundle.mk.injEq : ∀ {α : Type} (old? : Option (Lean.Language.SyntaxGuarded (Lean.Language.SnapshotTask α))) (new : IO.Promise α)
  (old?_1 : Option (Lean.Language.SyntaxGuarded (Lean.Language.SnapshotTask α))) (new_1 : IO.Promise α),
  ({ old? := old?, new := new } = { old? := old?_1, new := new_1 }) = (old? = old?_1 ∧ new = new_1)
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.ha : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  (self : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f), t.app self.i = CategoryTheory.CategoryStruct.comp self.a f
-- Lean.Meta.Tactic.FunIndCollect
_private.Lean.Meta.Tactic.FunIndCollect.0.Lean.Meta.FunInd.collect.unsafe_impl_2 : Lean.Meta.FunIndInfo → Lean.MVarId → Lean.MetaM (Array Lean.Expr)
-- Mathlib.RingTheory.Valuation.LocalSubring
instIsIntegrallyClosedSubtypeMemSubring : ∀ {K : Type u_3} [inst : Field K] (V : ValuationSubring K), IsIntegrallyClosed ↥V.toSubring
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t ∈ ∂^k 𝒜` iff `t` is exactly `k` elements more than something in `𝒜`.  -/
Finset.mem_upShadow_iff_exists_mem_card_add : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} {k : ℕ},
  s ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ t.card + k = s.card
-- Mathlib.FieldTheory.AbelRuffini
gal_one_isSolvable : ∀ {F : Type u_1} [inst : Field F], Group.IsSolvable (Polynomial.Gal 1)
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.isBlock_iff_smul_eq_of_nonempty : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.div_zero : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I / 0 = 0
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.declName : Lean.Elab.Command.InductiveView → Lean.Name
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {M : CategoryTheory.Functor C MonCat}
  {x y : CategoryTheory.SubmonoidFunctor M}, x = y ↔ x.obj = y.obj
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Embedding.ofSurjective.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} (f f_1 : β → α) (e_f : f = f_1) (hf : Function.Surjective f),
  Function.Embedding.ofSurjective f hf = Function.Embedding.ofSurjective f_1 ⋯
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.dist_comm : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n), dist x y = dist y x
-- Init.Prelude
EStateM.instMonadExceptOfOfBacktrackable : {ε σ δ : Type u} → [EStateM.Backtrackable δ σ] → MonadExceptOf ε (EStateM ε σ)
-- Mathlib.Algebra.Order.SuccPred.TypeTags
Order.pred_ofMul : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : PredOrder X] (x : X),
  Order.pred (Additive.ofMul x) = Additive.ofMul (Order.pred x)
-- Mathlib.RingTheory.Binomial
Ring.multichoose_neg_of_lt : ∀ (n k : ℕ), n < k → Ring.multichoose (-↑n) k = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_inj : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] [Module.IsTorsionFree k V1] [IsCancelMulZero k] (c : P1) {r : k},
  r ≠ 0 → ∀ {p q : P1}, (AffineMap.homothety c r) p = (AffineMap.homothety c r) q ↔ p = q
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_self_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ y₁ : F}
  {h₁ : W.Nonsingular x₁ y₁},
  y₁ = W.negY x₁ y₁ → WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ = 0
-- Mathlib.Order.Interval.Multiset
/-- The multiset of elements `x` such that `a < x` and `x ≤ b`. Basically `Set.Ioc a b` as a
multiset.  -/
Multiset.Ioc : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → α → α → Multiset α
-- Init.Data.SInt.Bitwise
Int8.toBitVec_shiftLeft : ∀ (a b : Int8), (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 8
-- Mathlib.RingTheory.Extension.ExtendScalars
/-- Given an extension `P : Extension R S`, this is the linear equivalence between
the first homology of the naive cotangent complex of `S` over `P.Ring` and
the cotangent space of `P`.  -/
Algebra.Extension.h1CotangentEquivCotangent : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → Algebra.H1Cotangent P.Ring S ≃ₗ[S] P.Cotangent
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.inner_orthogonalProjectionOnto_eq_of_mem_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (u : ↥K) (v : E),
  inner 𝕜 u (K.orthogonalProjectionOnto v) = inner 𝕜 (↑u) v
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.fst_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.fst R M₁ M₂ ∘SL ContinuousLinearMap.inr R M₁ M₂ = 0
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_mono' : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal},
  (∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
    ∀ ⦃s₁ s₂ : Set α⦄, P s₁ → s₁ ⊆ s₂ → MeasureTheory.extend m s₁ ≤ MeasureTheory.extend m s₂
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f.op g.op)
      (CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op =
    (CategoryTheory.Limits.pullback.snd f g).op
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_right_le_size_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp], t₂.size ≤ (t₁ ∪ t₂).size
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.transvection_mem_commutator : ∀ {F : Type u_1} [inst : Field F] {a : F},
  a ≠ 0 →
    a ^ 2 ≠ 1 →
      ∀ {i j : Fin 2} (h : i ≠ j) (c : F),
        Matrix.SpecialLinearGroup.transvection h c ∈ commutator (Matrix.SpecialLinearGroup (Fin 2) F)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forall_mem_keysArray_iff_forall_mem_getKey : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {p : α → Prop}, (∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h)
-- Init.Coe
/-- Helper definition used by the elaborator. It is not meant to be used directly by users.

This is used for coercions between monads, in the case where we want to apply
a monad lift and a coercion on the result type at the same time.
 -/
Lean.Internal.liftCoeM : {m : Type u → Type v} →
  {n : Type u → Type w} → {α β : Type u} → [MonadLiftT m n] → [(a : α) → CoeT α a β] → [Monad n] → m α → n β
-- Mathlib.Tactic.CategoryTheory.Coherence.Basic
/-- The core function for `monoidal` and `bicategory` tactics.  -/
Mathlib.Tactic.BicategoryLike.main : (ρ : Type) →
  [Mathlib.Tactic.BicategoryLike.Context ρ] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
            [Mathlib.Tactic.BicategoryLike.MkMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
              [Mathlib.Tactic.BicategoryLike.MonadMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
                [Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
                  [Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality
                        (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
                    [Mathlib.Tactic.BicategoryLike.MkEqOfNaturality (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
                      Lean.Name → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.objEquiv_map_apply : ∀ {p q n m : ℕ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n }))
  (f : { len := m } ⟶ { len := n }) (i : Fin (m + 1)),
  (SSet.prodStdSimplex.objEquiv
        ((CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
                  (SSet.stdSimplex.obj { len := q })).map
              f.op))
          x))
      i =
    (SSet.prodStdSimplex.objEquiv x) ((SimplexCategory.Hom.toOrderHom f) i)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.measurable_density : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) {s : Set β}, MeasurableSet s → Measurable fun p => κ.density ν p.1 p.2 s
-- Init.System.IOError
IO.Error.mkTimeExpired : UInt32 → String → IO.Error
-- Mathlib.Topology.Closure
interior_iInter_of_finite : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort v} [Finite ι] (f : ι → Set X),
  interior (⋂ i, f i) = ⋂ i, interior (f i)
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Ordered.insertNew : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v : α} {path : RBTree.RBNode.Path α},
  RBTree.RBNode.Path.Ordered cmp path →
    RBTree.RBNode.Path.RootOrdered cmp path v → RBTree.RBNode.Ordered cmp (path.insertNew v)
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.exists₂_genWeightSpace_smul_add_eq_bot : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) [IsAddTorsionFree R] [IsDomain R] [Module.IsTorsionFree R M]
  [IsNoetherian R M],
  χ₁ ≠ 0 → ∃ p < 0, ∃ q > 0, LieModule.genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧ LieModule.genWeightSpace M (q • χ₁ + χ₂) = ⊥
-- Std.Sat.AIG.Basic
/-- Given a `cache`, valid with respect to some `decls`, we can extend the `decls` without
extending the cache and remain valid.
 -/
Std.Sat.AIG.Cache.WF.push_id : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)}
  {cache : Std.HashMap (Std.Sat.AIG.Decl α) ℕ} {decl : Std.Sat.AIG.Decl α},
  Std.Sat.AIG.Cache.WF decls cache → Std.Sat.AIG.Cache.WF (decls.push decl) cache
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k fallback : α}, (t.erase k).getKeyD k fallback = fallback
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_abs_right`. -/
Asymptotics.IsLittleO.abs_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
  f =o[l] u → f =o[l] fun x => |u x|
-- Std.Time.Date.Unit.Day
Std.Time.Day.instOfNatOffset : {n : ℕ} → OfNat Std.Time.Day.Offset n
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearCnstr? : Lean.Expr → Lean.Meta.Simp.Arith.Nat.ToLinear.M (Option Lean.Meta.Simp.Arith.Nat.LinearCnstr)
-- Lean.Meta.Tactic.Grind.Extension
/-- It stores universe parameter names for universe polymorphic proofs.
Recall that it is non-empty only when we elaborate an expression provided by the user.
When `proof` is just a constant, we can use the universe parameter names stored in the declaration.
 -/
Lean.Meta.Grind.EMatchTheorem.levelParams : Lean.Meta.Grind.EMatchTheorem → Array Lean.Name
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.toListRev_dropWhile_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.dropWhile P it).toListRev = (List.dropWhile P it.toList).reverse
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.bitwise.eq_def : ∀ (f : Bool → Bool → Bool) (n m : ℕ),
  Nat.bitwise f n m =
    if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        have r := Nat.bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.associator_def : ∀ (R : Type u) [inst : CommRing R] (X Y Z : CoalgCat R),
  CategoryTheory.MonoidalCategoryStruct.associator X Y Z =
    (Coalgebra.TensorProduct.assoc R R ↑X.toModuleCat ↑Y.toModuleCat ↑Z.toModuleCat).toCoalgIso
-- Mathlib.Algebra.Order.IsBotOne
zero_le : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Zero α] [IsBotZeroClass α] {a : α}, 0 ≤ a
-- Mathlib.Order.Antisymmetrization
AntisymmRel.le : ∀ {α : Type u_1} {a b : α} [inst : LE α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → a ≤ b
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.dist_sq_eq_iff_mem_orthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2 ↔ q ∈ s.orthRadius p
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_C : ∀ {R : Type u_1} [inst : Semiring R] (r c : R), (Polynomial.C c).scaleRoots r = Polynomial.C c
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
/-- [Kerodon Tag 01BB](https://kerodon.net/tag/01BB) -/
SSet.quasicategory_iff_of_isTerminal : ∀ {X Y : SSet} (p : X ⟶ Y) (hY : CategoryTheory.Limits.IsTerminal Y), X.Quasicategory ↔ SSet.InnerFibration p
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.dual_map : ∀ {X Y : FinBoolAlg} (f : X ⟶ Y),
  FinBoolAlg.dual.map f =
    CategoryTheory.InducedCategory.homMk (BoolAlg.ofHom (BoundedLatticeHom.dual (BoolAlg.Hom.hom f.hom)))
-- Init.Data.Nat.Lemmas
Nat.min_assoc : ∀ (a b c : ℕ), min (min a b) c = min a (min b c)
-- Mathlib.Algebra.Algebra.StrictPositivity
IsStrictlyPositive.conjugate_of_isUnit_of_isSelfAdjoint : ∀ {A : Type u_1} [inst : Semiring A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A] (a b : A),
  IsUnit b →
    autoParam (IsSelfAdjoint b) IsStrictlyPositive.conjugate_of_isUnit_of_isSelfAdjoint._auto_1 →
      autoParam (IsStrictlyPositive a) IsStrictlyPositive.conjugate_of_isUnit_of_isSelfAdjoint._auto_3 →
        IsStrictlyPositive (b * a * b)
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.any : ∀ {l m r : List Char} (f : Char → Bool) {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → Substring.Raw.Legacy.any s f = m.any f
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.rename_homogeneousComponent : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {τ : Type u_5} {φ : σ → τ} (n : ℕ) (p : MvPolynomial σ R),
  (MvPolynomial.rename φ) ((MvPolynomial.homogeneousComponent n) p) =
    (MvPolynomial.homogeneousComponent n) ((MvPolynomial.rename φ) p)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mkActionCore.go : Array (Lean.Meta.Grind.SolverExtension Lean.Meta.Grind.SolverExtensionState) →
  ℕ → Lean.Meta.Grind.Action → Lean.Meta.Grind.Action
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial.eq_1 : ∀ (n : ℕ), n.descFactorial 0 = 1
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ v₁_1 : Module.Basis n R M₁),
  v₁ = v₁_1 → ∀ (v₂ v₂_1 : Module.Basis m R M₂), v₂ = v₂_1 → Matrix.toLin v₁ v₂ = Matrix.toLin v₁_1 v₂_1
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.mk.injEq : ∀ {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] (obj : V → W)
  (map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)) (obj_1 : V → W) (map_1 : {X Y : V} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y)),
  ({ obj := obj, map := map } = { obj := obj_1, map := map_1 }) = (obj = obj_1 ∧ map ≍ map_1)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.shutdown : ℕ → Lean.Lsp.Ipc.IpcM Unit
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.mem_prev : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsTruncLE]
  {i' : ι'} {j : ι}, c'.Rel i' (e.f j) → ∃ i, e.f i = i'
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.totallyBounded_iSup : ∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} [Finite ι] {f : ι → Filter α},
  (⨆ i, f i).TotallyBounded ↔ ∀ (i : ι), (f i).TotallyBounded
-- Mathlib.Algebra.Lie.TensorProduct
TensorProduct.LieModule.toLinearMap_map : ∀ {R : Type u} [inst : CommRing R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃}
  [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N]
  [inst_9 : LieRingModule L N] [inst_10 : LieModule R L N] [inst_11 : AddCommGroup P] [inst_12 : Module R P]
  [inst_13 : LieRingModule L P] [inst_14 : LieModule R L P] [inst_15 : AddCommGroup Q] [inst_16 : Module R Q]
  [inst_17 : LieRingModule L Q] [inst_18 : LieModule R L Q] (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q),
  ↑(TensorProduct.LieModule.map f g) = TensorProduct.map ↑f ↑g
-- Mathlib.Analysis.InnerProductSpace.OfNorm
_private.Mathlib.Analysis.InnerProductSpace.OfNorm.0.inner_.eq_1 : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (x y : E),
  inner_✝ 𝕜 x y =
    4⁻¹ *
      ((algebraMap ℝ 𝕜) ‖x + y‖ * (algebraMap ℝ 𝕜) ‖x + y‖ - (algebraMap ℝ 𝕜) ‖x - y‖ * (algebraMap ℝ 𝕜) ‖x - y‖ +
          RCLike.I * (algebraMap ℝ 𝕜) ‖RCLike.I • x + y‖ * (algebraMap ℝ 𝕜) ‖RCLike.I • x + y‖ -
        RCLike.I * (algebraMap ℝ 𝕜) ‖RCLike.I • x - y‖ * (algebraMap ℝ 𝕜) ‖RCLike.I • x - y‖)
-- Mathlib.Order.PartialSups
Pi.partialSups_apply : ∀ {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] {τ : Type u_4} {π : τ → Type u_5}
  [inst_2 : (t : τ) → SemilatticeSup (π t)] (f : ι → (t : τ) → π t) (i : ι) (t : τ),
  (partialSups f) i t = (partialSups fun x => f x t) i
-- Mathlib.Logic.Equiv.Defs
Equiv.nontrivial : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Nontrivial β], Nontrivial α
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
/-- `circleMap` is injective on `Ico a b` if the distance between `a` and `b` is at most `2π`.  -/
injOn_circleMap_of_abs_sub_le' : ∀ {a b R : ℝ} {c : ℂ}, R ≠ 0 → b - a ≤ 2 * Real.pi → Set.InjOn (circleMap c R) (Set.Ico a b)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.not_continuousAt_deriv_qaryEntropy_one : ∀ {q : ℕ}, ¬ContinuousAt (deriv (Real.qaryEntropy q)) 1
-- Mathlib.Data.FinEnum.Option
/-- A recursor principle for finite-and-enumerable types, analogous to `Nat.rec`.
It effectively says that every `FinEnum` is either `Empty` or `Option α`, up to an `Equiv` mediated
by `Fin`s of equal cardinality.
In contrast to the `Fintype` case, data can be transported along such an `Equiv`.
Also, since order matters, the choice of element that gets replaced by `Option.none` has
to be provided for every step.

Since every `FinEnum` instance implies a `Fintype` instance and `Prop` is squashed already,
`Fintype.induction_empty_option` can be used if a `Prop` needs to be constructed.
Cf. `Data.Fintype.Option`
 -/
FinEnum.recEmptyOption : {P : Type u → Sort v} →
  ((n : ℕ) → Fin (n + 1)) →
    ({α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → FinEnum.card β = FinEnum.card α → P α → P β) →
      P PEmpty.{u + 1} → ({α : Type u} → FinEnum α → P α → P (Option α)) → (α : Type u) → [FinEnum α] → P α
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_eq_none : ∀ {n : ℕ} {i j : Fin (n + 1)}, (finSuccEquiv' i) j = none ↔ i = j
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roo.toArray_iter_eq_toArray : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roo α}, r.iter.toArray = r.toArray