mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.ZMod.Aut
/-- The automorphism group of `ZMod n` is isomorphic to the group of units of `ZMod n`.  -/
ZMod.AddAutEquivUnits : (n : ℕ) → AddAut (ZMod n) ≃+ Additive (ZMod n)ˣ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.fst_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C),
  (CategoryTheory.SemiCartesianMonoidalCategory.fst M N).hom = CategoryTheory.SemiCartesianMonoidalCategory.fst M.X N.X
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
/-- The pullback of an ideal sheaf.  -/
AlgebraicGeometry.Scheme.IdealSheafData.comap : {X Y : AlgebraicGeometry.Scheme} → Y.IdealSheafData → (X ⟶ Y) → X.IdealSheafData
-- Mathlib.Data.Fin.VecNotation
/-- `vecCons h t` prepends an entry `h` to a vector `t`.

The inverse functions are `vecHead` and `vecTail`.
The notation `![a, b, ...]` expands to `vecCons a (vecCons b ...)`.
 -/
Matrix.vecCons : {α : Type u} → {n : ℕ} → α → (Fin n → α) → Fin n.succ → α
-- Lean.Compiler.LCNF.Types
/-- The boxed version of types.
 -/
Lean.Compiler.LCNF.ImpureType.Lean.Expr.boxed : Lean.Expr → Lean.Expr
-- Mathlib.Analysis.Convex.Strict
StrictConvex.add_smul_mem : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x y : E} [AddRightStrictMono 𝕜],
  StrictConvex 𝕜 s → x ∈ s → x + y ∈ s → y ≠ 0 → ∀ {t : 𝕜}, 0 < t → t < 1 → x + t • y ∈ interior s
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
MvQPF.Comp.instMvFunctor : {n m : ℕ} →
  {F : TypeVec.{u} n → Type u_1} →
    {G : Fin2 n → TypeVec.{u} m → Type u} →
      [MvFunctor F] → [(i : Fin2 n) → MvFunctor (G i)] → MvFunctor (MvQPF.Comp F G)
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of an integrable function is smaller than its mean.  -/
MeasureTheory.exists_le_average : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  μ ≠ 0 → MeasureTheory.Integrable f μ → ∃ x, f x ≤ ⨍ (a : α), f a ∂μ
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'_toMatrix' : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (f : (n → R) →ₗ[R] m → R), Matrix.toLin' (LinearMap.toMatrix' f) = f
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.subOneIntegralPowerBasis.eq_1 : ∀ {n : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : NeZero n] [inst_2 : CharZero K]
  [inst_3 : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n),
  hζ.subOneIntegralPowerBasis = PowerBasis.ofAdjoinEqTop' ⋯ ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_unitOfList_le : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.ExtTreeMap.unitOfList l cmp).size ≤ l.length
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.sup_adj : ∀ {V : Type u} (x y : SimpleGraph V) (v w : V), (x ⊔ y).Adj v w ↔ x.Adj v w ∨ y.Adj v w
-- Mathlib.Algebra.CharP.Defs
expChar_ne_zero : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [hR : ExpChar R p], p ≠ 0
-- Batteries.Tactic.Trans
/-- `trans` applies to a goal whose target has the form `t ~ u` where `~` is a transitive relation,
that is, a relation which has a transitivity lemma tagged with the attribute [trans].

* `trans s` replaces the goal with the two subgoals `t ~ s` and `s ~ u`.
* If `s` is omitted, then a metavariable is used instead.

Additionally, `trans` also applies to a goal whose target has the form `t → u`,
in which case it replaces the goal with `t → s` and `s → u`.
 -/
Batteries.Tactic.tacticTrans___ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
/-- Auxiliary theorem used to prove `toBaseChange_reverse` without needing induction.  -/
CliffordAlgebra.toBaseChange_comp_reverseOp : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V),
  (AlgHom.op (CliffordAlgebra.toBaseChange A Q)).comp CliffordAlgebra.reverseOp =
    (↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
      ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) CliffordAlgebra.reverseOp).comp
        (CliffordAlgebra.toBaseChange A Q))
-- Mathlib.Order.Filter.Pointwise
Filter.neg.instNeBot : ∀ {α : Type u_2} [inst : Neg α] {f : Filter α} [f.NeBot], (-f).NeBot
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- If `𝒰` is a directed open cover of `X`, to glue morphisms `{gᵢ : 𝒰ᵢ ⟶ Y}` over `S` it suffices
to check compatibility with the transition maps.  -/
AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected : {S : AlgebraicGeometry.Scheme} →
  {X : CategoryTheory.Over S} →
    (𝒰 : X.left.OpenCover) →
      [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] →
        [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
          {Y : CategoryTheory.Over S} →
            (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) →
              (∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i) →
                (∀ (i : 𝒰.I₀),
                    CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom) →
                  (X ⟶ Y)
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- `MonoidAlgebra.mapDomain` as a linear map.  -/
MonoidAlgebra.mapDomainLinearMap : (R : Type u_1) →
  (S : Type u_2) →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] → [inst_2 : Module R S] → (M → N) → MonoidAlgebra S M →ₗ[R] MonoidAlgebra S N
-- Init.System.ST
/-- An auxiliary class used to infer the “state” of `EST` and `ST` monads.
 -/
STWorld : outParam Type → (Type → Type) → Type
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_count : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (f : α → ENNReal),
  ∫⁻ (a : α), f a ∂MeasureTheory.Measure.count = ∑' (a : α), f a
-- Mathlib.Data.Set.Semiring
SetSemiring.up_le_up : ∀ {α : Type u_1} {s t : Set α}, Set.up s ≤ Set.up t ↔ s ⊆ t
-- Mathlib.RingTheory.Ideal.GoingUp
/-- This technical lemma asserts the existence of a polynomial `p` in an ideal `P ⊂ R[x]`
that is non-zero in the quotient `R / (P ∩ R) [x]`.  The assumptions are equivalent to
`P ≠ 0` and `P ∩ R = (0)`.
 -/
Ideal.exists_nonzero_mem_of_ne_bot : ∀ {R : Type u_1} [inst : CommRing R] {P : Ideal (Polynomial R)},
  P ≠ ⊥ →
    (∀ (x : R), Polynomial.C x ∈ P → x = 0) →
      ∃ p ∈ P, Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) p ≠ 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x) (x : Lean.Grind.CommRing.Var),
  a = Lean.Grind.CommRing.Expr.var x →
    (match a with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | x => h_3 x) ≍
      h_2 x
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.natDegree_basisDivisor_of_ne : ∀ {F : Type u_1} [inst : Field F] {x y : F}, x ≠ y → (Lagrange.basisDivisor x y).natDegree = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'] {Z_1 : C} (h : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f g) g') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (CategoryTheory.CategoryStruct.comp g' g))
      h
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.Const.getThenInsertIfNew? : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → β → Option β × Std.DTreeMap.Raw α (fun x => β) cmp
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.maxDegree_mono : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableRel H.Adj] (f : G.Copy H), G.maxDegree ≤ H.maxDegree
-- Mathlib.Data.Set.Subsingleton
Set.strictAntiOn_singleton : ∀ {α : Type u} {β : Type v} {a : α} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β), StrictAntiOn f {a}
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_lt_add : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {x y : R} {g : Γ₀}, g < v x → g < v y → g < v (x + y)
-- Lean.Parser.Command
Lean.Parser.Command.importPath.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Nat.Choose.Multinomial
Finsupp.multinomial_eq : ∀ {α : Type u_1} (f : α →₀ ℕ), f.multinomial = Nat.multinomial f.support ⇑f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instSymmetricCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.SymmetricCategory C] → CategoryTheory.SymmetricCategory (CategoryTheory.Mon C)
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.DTreeMap.Raw.Const.entryAtIdx! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap.Raw α (fun x => β) cmp → ℕ → α × β
-- Mathlib.Algebra.Lie.Basic
/-- A morphism of Lie algebras (denoted as `L₁ →ₗ⁅R⁆ L₂`)
is a linear map respecting the bracket operations.  -/
LieHom : (R : Type u_1) →
  (L : Type u_2) →
    (L' : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] → [LieAlgebra R L] → [inst_3 : LieRing L'] → [LieAlgebra R L'] → Type (max u_2 u_3)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).maxKey? = some k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.ofRowLens.congr_simp : ∀ (w w_1 : List ℕ) (e_w : w = w_1) (hw : w.SortedGE), YoungDiagram.ofRowLens w hw = YoungDiagram.ofRowLens w_1 ⋯
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If `b` is a binary bicone such that `b.inr` is a kernel of `b.fst`, then `b` is a bilimit
bicone.  -/
CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.IsLimit b.fstKernelFork → b.IsBilimit
-- Mathlib.RingTheory.Derivation.Basic
Derivation.linearEquiv_coe_comp : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  {N : Type u_5} [inst_6 : AddCommMonoid N] [inst_7 : Module A N] [inst_8 : Module R N] [inst_9 : IsScalarTower R A M]
  [inst_10 : IsScalarTower R A N] (e : M ≃ₗ[A] N), ⇑(e.compDer D) = ⇑(↑R ↑e ∘ₗ ↑D)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} (self : L.Hom L'), CategoryTheory.CategoryStruct.comp (Φ.functor.map self.f) L'.w = L.w
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).obj Y).hom = (Y.right.hom, Y.hom)
-- Mathlib.Topology.Order
/-- **Alias** of the forward direction of `TopologicalSpace.nontrivial_iff_exists_not_inseparable`. -/
NontrivialTopology.exists_not_inseparable : ∀ {α : Type u} {t : TopologicalSpace α}, NontrivialTopology α → ∃ x y, ¬Inseparable x y
-- Mathlib.RingTheory.FilteredAlgebra.Basic
/-- For a family of subsets `σ` of semiring `R`, an increasing series `F` in `σ` is
a ring filtration if `IsFiltration F F_lt` and the pointwise multiplication of `F i` and `F j`
is in `F (i + j)`.  -/
IsRingFiltration : {ι : Type u_1} →
  {R : Type u_2} →
    {σ : Type u_3} →
      [AddMonoid ι] → [PartialOrder ι] → [Preorder σ] → [Semiring R] → [SetLike σ R] → (ι → σ) → outParam (ι → σ) → Prop
-- Mathlib.Algebra.AddConstMap.Basic
/-- Auxiliary lemmas for the "monotonicity on a fundamental interval implies monotonicity" lemmas.
We formulate it for any relation so that the proof works both for `Monotone` and `StrictMono`.  -/
AddConstMapClass.rel_map_of_Icc : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
  [inst_2 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [inst_5 : AddGroup H] [AddConstMapClass F G H a b]
  {f : F} {R : H → H → Prop} [IsTrans H R] [hR : CovariantClass H H (fun x y => y + x) R],
  0 < a →
    ∀ {l : G},
      (∀ x ∈ Set.Icc l (l + a), ∀ y ∈ Set.Icc l (l + a), x < y → R (f x) (f y)) →
        Relator.LiftFun (fun x1 x2 => x1 < x2) R ⇑f ⇑f
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_cons_cons_cons_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {n : ℕ} (a b : K) (x : Fin n → K),
  Height.logHeight (Matrix.vecCons a (Matrix.vecCons b (Matrix.vecCons 0 x))) =
    Height.logHeight (Matrix.vecCons a (Matrix.vecCons b x))
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_comp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ L₃ : CategoryTheory.Functor C D} {R₁ R₂ R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (adj₃ : L₃ ⊣ R₃) (α : L₂ ⟶ L₁) (β : L₃ ⟶ L₂),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
      ((CategoryTheory.conjugateEquiv adj₂ adj₃) β) =
    (CategoryTheory.conjugateEquiv adj₁ adj₃) (CategoryTheory.CategoryStruct.comp β α)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- See `MulAction.isBlock_subgroup` for a version that works for the left action of a group on
itself.  -/
MulAction.isBlock_subgroup' : ∀ {G : Type u_1} [inst : Group G] {S : Type u_3} {H : Type u_4} [inst_1 : Group H] [inst_2 : SetLike S H]
  [SubgroupClass S H] {s : S} [inst_4 : MulAction G H] [IsScalarTower G Hᵐᵒᵖ H], MulAction.IsBlock G ↑s
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- A null homotopic map `K.cylinder ⟶ K.cylinder` which identifies to
`π K ≫ ι₀ K - 𝟙 _`, see `nullHomotopicMap_eq`.  -/
HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] → K.cylinder ⟶ K.cylinder
-- Mathlib.FieldTheory.Laurent
RatFunc.laurent_C : ∀ {R : Type u} [inst : CommRing R] (r : R) [inst_1 : IsDomain R] (x : R),
  (RatFunc.laurent r) (RatFunc.C x) = RatFunc.C x
-- Mathlib.ModelTheory.Order
FirstOrder.Language.denselyOrderedSentence.eq_1 : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered],
  L.denselyOrderedSentence =
    ((((FirstOrder.Language.var ∘ Sum.inr) 0).lt ((FirstOrder.Language.var ∘ Sum.inr) 1)).imp
          (((FirstOrder.Language.var ∘ Sum.inr) 0).lt ((FirstOrder.Language.var ∘ Sum.inr) 2) ⊓
              ((FirstOrder.Language.var ∘ Sum.inr) 2).lt ((FirstOrder.Language.var ∘ Sum.inr) 1)).ex).all.all
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the pure predicate `p` returns `true` for
all elements emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of `it` are
examined in order of iteration.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toListRev` always terminates after finitely many steps.
 -/
Std.IterM.all : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → (β → Bool) → Std.IterM m β → m (ULift.{w, 0} Bool)
-- Lean.Setup
Lean.ModuleArtifacts.oleanParts : Lean.ModuleArtifacts → Array System.FilePath
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A convenient way to show that a binary fan is a limit.  -/
CategoryTheory.Limits.BinaryFan.IsLimit.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (s : CategoryTheory.Limits.BinaryFan X Y) →
        (lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)) →
          (∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.fst = f) →
            (∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.snd = g) →
              (∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt),
                  CategoryTheory.CategoryStruct.comp m s.fst = f →
                    CategoryTheory.CategoryStruct.comp m s.snd = g → m = lift f g) →
                CategoryTheory.Limits.IsLimit s
-- Std.Data.TreeSet.Slice
Std.TreeSet.instSliceableRioSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.instSliceableRioSlice._auto_1) →
    Std.Rio.Sliceable (Std.TreeSet α cmp) α (Std.DTreeMap.Internal.Unit.RioSlice α)
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting'_nth_eq : ∀ (n : ℕ), (Nat.nth Nat.Prime n).primeCounting' = n
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertListIfNewUnit_le : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α},
  (Std.Internal.List.insertListIfNewUnit l toInsert).length ≤ l.length + toInsert.length
-- Std.Http.Protocol.H1
/-- Builds the externally exposed `PulledChunk` value from parsed body bytes.

When body consumption is currently internal-only (e.g. request body being
drained after a response was already sent), returns `none`.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.mkPulledChunk? : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir →
    Bool →
      Bool →
        Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue) →
          ByteSlice → Option Std.Http.Protocol.H1.PulledChunk
-- Mathlib.Data.Set.Subset
Set.preimage_val_iInter : ∀ {ι : Sort u_1} {α : Type u_2} {A : Set α} {s : ι → Set α}, Subtype.val ⁻¹' ⋂ i, s i = ⋂ i, Subtype.val ⁻¹' s i
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given `x y : R` and localizations `S`, `P` away from `x` and `y * x`
respectively, the homomorphism induced from `S` to `P`.  -/
IsLocalization.Away.awayToAwayLeft : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] →
              (x : R) →
                [IsLocalization.Away x S] → (y : R) → [inst_5 : Algebra R P] → [IsLocalization.Away (y * x) P] → S →+* P
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso'_hom_naturality : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (S₁.map F).HasHomology] [inst_8 : (S₂.map F).HasHomology]
  [inst_9 : F.PreservesRightHomologyOf S₁] [inst_10 : F.PreservesRightHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
      (S₂.mapHomologyIso' F).hom =
    CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).hom (F.map (CategoryTheory.ShortComplex.homologyMap φ))
-- Plausible.Shrinkable
Plausible.ULift.shrinkable : {α : Type u_1} → [Plausible.Shrinkable α] → Plausible.Shrinkable (ULift.{u_2, u_1} α)
-- Lean.Parser.Basic
Lean.Parser.charLitFnAux : String.Pos.Raw → Lean.Parser.ParserFn
-- Mathlib.Order.Completion
DedekindCut.principal_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {c : DedekindCut α}, DedekindCut.principal a ≤ c ↔ a ∈ c.left
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinitaryCardAugment_indep : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug :
    ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).Indep =
    Indep
-- Init.Data.SInt.Lemmas
ISize.toBitVec_one : ISize.toBitVec 1 = 1#System.Platform.numBits
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p n : ℤ}
  (α : CochainComplex.HomComplex.Cocycle ((CochainComplex.singleFunctor C p).obj X) K n) (q : ℤ) (h : p + n = q)
  (q' : ℤ) (hq' : q + 1 = q'),
  ∃ f,
    ∃ (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0),
      CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf = α
-- Aesop.Stats.Basic
Aesop.ForwardClusterStateStats.instantiationStats : Aesop.ForwardClusterStateStats → Array Aesop.ForwardInstantiationStats
-- Init.System.Platform
System.Platform.le_numBits : 32 ≤ System.Platform.numBits
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} {l : List α},
  m.WF → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) m l)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.comp_tendsto : ∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  {l' : Filter ι'} {φ : ι → Set α},
  MeasureTheory.AECover μ l φ → ∀ {u : ι' → ι}, Filter.Tendsto u l' l → MeasureTheory.AECover μ l' (φ ∘ u)