mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.forget.eq_1 : ∀ {W : Type v'} [inst : CategoryTheory.Category.{w', v'} W] [inst_1 : CategoryTheory.MonoidalCategory W] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory W C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory W D]
  (F : CategoryTheory.EnrichedFunctor W C D),
  F.forget =
    { obj := fun X => CategoryTheory.ForgetEnrichment.of W (F.obj (CategoryTheory.ForgetEnrichment.to W X)),
      map := fun {X Y} f =>
        CategoryTheory.ForgetEnrichment.homOf W
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homTo W f)
            (F.map (CategoryTheory.ForgetEnrichment.to W X) (CategoryTheory.ForgetEnrichment.to W Y))),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.integral_measureT : ∀ (f : ℝ → ℝ), ∫ (x : ℝ), f x ∂Polynomial.Chebyshev.measureT = ∫ (x : ℝ) in -1..1, f x * √(1 - x ^ 2)⁻¹
-- Lean.Meta.Match.CaseValues
Lean.Meta.instInhabitedCaseValuesSubgoal : Inhabited Lean.Meta.CaseValuesSubgoal
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.negPart_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Lattice Y] [inst_2 : AddCommGroup Y]
  (a : Function.locallyFinsuppWithin U Y) (x : X), a⁻ x = (a x)⁻
-- Mathlib.Data.Set.Prod
Set.fst_image_prod_subset : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), Prod.fst '' s ×ˢ t ⊆ s
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℂ_def : ∀ (s : ℂ), s.Gammaℂ = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.piecewise_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Preorder β] {s : Set α}
  {f₁ f₂ g₁ g₂ : MeasureTheory.SimpleFunc α β} {hs : MeasurableSet s},
  (∀ a ∈ s, f₁ a ≤ f₂ a) →
    (∀ a ∉ s, g₁ a ≤ g₂ a) →
      MeasureTheory.SimpleFunc.piecewise s hs f₁ g₁ ≤ MeasureTheory.SimpleFunc.piecewise s hs f₂ g₂
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.mem_normalizedFactors_iff : ∀ {R : Type u} [inst : Field R] {p q : Polynomial R} [inst_1 : DecidableEq R],
  q ≠ 0 → (p ∈ UniqueFactorizationMonoid.normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- A matrix representation of the quadratic form `Q : QuadraticForm R N` with respect to a
given basis. See also `QuadraticForm.toMatrix'` for the special case of `N = n → R` with
the standard basis.  -/
QuadraticForm.toMatrix : {R : Type u_3} →
  {N : Type u_5} →
    {n : Type w} →
      [Fintype n] →
        [DecidableEq n] →
          [inst : CommRing R] →
            [Invertible 2] →
              [inst_2 : AddCommGroup N] → [inst_3 : Module R N] → Module.Basis n R N → QuadraticForm R N → Matrix n n R
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (x y : M →₀ R),
  MonoidAlgebra.ofCoeff (x + y) = MonoidAlgebra.ofCoeff x + MonoidAlgebra.ofCoeff y
-- Mathlib.Topology.Algebra.UniformMulAction
uniformContinuous_mul_right' : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R),
  UniformContinuous fun b => b * a
-- Mathlib.Data.Set.Countable
Set.Countable.image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} {s : Set α} {t : Set β},
  s.Countable → t.Countable → ∀ (f : α → β → γ), (Set.image2 f s t).Countable
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.forceRegularApp : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context → Bool
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.revlexWF.match_1.eq_4 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (pw₁ : Lean.Grind.CommRing.Power)
  (m₁ : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power) (m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m))
  (h_3 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit)
  (h_4 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (match Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => h_2 p m
    | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => h_3 p m
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_4 pw₁ m₁ pw₂ m₂) =
    h_4 pw₁ m₁ pw₂ m₂
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.add_f_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D) (i : ι), (f + g).f i = f.f i + g.f i
-- Mathlib.CategoryTheory.Sites.LocallyInjective
/-- If `F : Cᵒᵖ ⥤ D` is a presheaf with values in a concrete category, if `x` and `y` are
elements in `F.obj X`, this is the sieve of `X.unop` consisting of morphisms `f`
such that `F.map f.op x = F.map f.op y`.  -/
CategoryTheory.Presheaf.equalizerSieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {FD : D → D → Type u_1} →
          {CD : D → Type w} →
            [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
              [inst_3 : CategoryTheory.ConcreteCategory D FD] →
                {F : CategoryTheory.Functor Cᵒᵖ D} →
                  {X : Cᵒᵖ} →
                    CategoryTheory.ToType (F.obj X) →
                      CategoryTheory.ToType (F.obj X) → CategoryTheory.Sieve (Opposite.unop X)
-- Mathlib.Order.LatticeIntervals
Set.Ioc.semilatticeSup : {α : Type u_1} → [inst : SemilatticeSup α] → {a b : α} → SemilatticeSup ↑(Set.Ioc a b)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_mul_left_left : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime (x + y * z) y
-- Mathlib.Analysis.Convex.Quasiconvex
Antitone.quasiconvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Antitone f → QuasiconvexOn 𝕜 Set.univ f
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- Constructor for sections of a presheaf of modules.  -/
PresheafOfModules.sectionsMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M : PresheafOfModules R} →
        (s : (X : Cᵒᵖ) → ↑(M.obj X)) →
          (∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), (CategoryTheory.ConcreteCategory.hom (M.map f)) (s X) = s Y) → M.sections
-- Mathlib.Algebra.GroupWithZero.Hom
/-- `MonoidWithZeroHom` down-cast to a `ZeroHom`, forgetting the monoidal property.  -/
MonoidWithZeroHom.coeToZeroHom : {α : Type u_2} →
  {β : Type u_3} → [inst : MulZeroOneClass α] → [inst_1 : MulZeroOneClass β] → Coe (α →*₀ β) (ZeroHom α β)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Given a finite family of `ModelWithCorners` `I i` on `(E i, H i)`, we define the model with
corners `pi I` on `(Π i, E i, ModelPi H)`. See note [Manifold type tags] for explanation about
`ModelPi H`.  -/
ModelWithCorners.pi : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {ι : Type v} →
      [inst_1 : Fintype ι] →
        {E : ι → Type w} →
          [inst_2 : (i : ι) → NormedAddCommGroup (E i)] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] →
              {H : ι → Type u'} →
                [inst_4 : (i : ι) → TopologicalSpace (H i)] →
                  ((i : ι) → ModelWithCorners 𝕜 (E i) (H i)) → ModelWithCorners 𝕜 ((i : ι) → E i) (ModelPi H)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- A particular case of Sard's Theorem. If `f` is a `C¹` smooth map from a real vector space to a
real vector space `F` of strictly larger dimension, then the complement of the range of `f` is dense
in `F`.  -/
ContDiff.dense_compl_range_of_finrank_lt_finrank : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F},
  ContDiff ℝ 1 f → Module.finrank ℝ E < Module.finrank ℝ F → Dense (Set.range f)ᶜ
-- Init.Data.SInt.Bitwise
Int32.toUInt32_or : ∀ (a b : Int32), (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (w : ℕ) (input input_1 : aig.RefVec w),
  input = input_1 →
    ∀ (newWidth curr : ℕ) (hcurr : curr ≤ newWidth) (s s_1 : aig.RefVec curr),
      s = s_1 →
        Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s =
          Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input_1 newWidth curr hcurr s_1
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.embeddingUpNat_f : ∀ (n : ℕ), ComplexShape.embeddingUpNat.f n = ↑n
-- Mathlib.Tactic.Simps.Basic
/-- Make `Simp.Context` giving data instead of Syntax. Doesn't support arguments.
Intended to be very similar to `Lean.Elab.Tactic.mkSimpContext`
Todo: support arguments.  -/
Lean.Meta.mkSimpContext : optParam Lean.Meta.Simp.Config { } →
  optParam Bool false →
    optParam Lean.Elab.Tactic.SimpKind Lean.Elab.Tactic.SimpKind.simp →
      optParam Lean.Elab.Tactic.Simp.DischargeWrapper Lean.Elab.Tactic.Simp.DischargeWrapper.default →
        optParam Bool false → Lean.MetaM Lean.Meta.Simp.Context
-- Lean.Elab.Tactic.Grind.Main
/-- Position for the `only` child syntax in the `grind` tactic.  -/
Lean.Elab.Tactic.grindOnlyPos : ℕ
-- Lean.Elab.DeclModifiers
/-- Given a declaration identifier (e.g., `ident (".{" ident,+ "}")?`) that may contain explicit universe parameters
- Ensure the new universe parameters do not shadow universe parameters declared using `universe` command.
- Create the fully qualified named for the declaration using the current namespace, and given `modifiers`
- Create a short version for recursively referring to the declaration. Recall that the `protected` modifier affects the generation of the short name.

The result also contains the universe parameters provided using `universe` command, and the `.{...}` notation.

This commands also stores the doc string stored in `modifiers`.
 -/
Lean.Elab.expandDeclId : Lean.Name → List Lean.Name → Lean.Syntax → Lean.Elab.Modifiers → Lean.Elab.TermElabM Lean.Elab.ExpandDeclIdResult
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.tensor_right : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y] →
          CategoryTheory.MonoidalCoherence X (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Coyoneda.fullyFaithful_preimage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ}
  (f : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y),
  CategoryTheory.Coyoneda.fullyFaithful.preimage f =
    Quiver.Hom.op
      ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.unop X)))
        (CategoryTheory.CategoryStruct.id (Opposite.unop X)))
-- Batteries.Lean.Meta.Basic
/-- Obtain all unassigned metavariables from the given `MetavarContext`. If
`includeDelayed` is `true`, delayed-assigned metavariables are considered
unassigned.
 -/
Lean.MetavarContext.unassignedExprMVars : Lean.MetavarContext → optParam Bool false → Array Lean.MVarId
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.Λ'.Supports.match_1.eq_4 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K')
  (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.clear p k q with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k s q => h_2 k s q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret k => h_8 k) =
    h_4 p k q
-- Mathlib.RingTheory.Valuation.Basic
Valuation.mk.inj : ∀ {R : Type u_3} {Γ₀ : Type u_4} {inst : LinearOrderedCommMonoidWithZero Γ₀} {inst_1 : Ring R}
  {toMonoidWithZeroHom : R →*₀ Γ₀}
  {map_add_le_max' :
    ∀ (x y : R),
      (↑toMonoidWithZeroHom).toFun (x + y) ≤ max ((↑toMonoidWithZeroHom).toFun x) ((↑toMonoidWithZeroHom).toFun y)}
  {toMonoidWithZeroHom_1 : R →*₀ Γ₀}
  {map_add_le_max'_1 :
    ∀ (x y : R),
      (↑toMonoidWithZeroHom_1).toFun (x + y) ≤
        max ((↑toMonoidWithZeroHom_1).toFun x) ((↑toMonoidWithZeroHom_1).toFun y)},
  { toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' } =
      { toMonoidWithZeroHom := toMonoidWithZeroHom_1, map_add_le_max' := map_add_le_max'_1 } →
    toMonoidWithZeroHom = toMonoidWithZeroHom_1
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.lift.congr_simp : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] (φ φ_1 : G →* M)
  (e_φ : φ = φ_1) (HN : N ≤ φ.ker), QuotientGroup.lift N φ HN = QuotientGroup.lift N φ_1 ⋯
-- Mathlib.Order.CountableSupClosed
countableInfClosure_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (s : Set α) (t : Set β),
  countableInfClosure (s ×ˢ t) = countableInfClosure s ×ˢ countableInfClosure t
-- Mathlib.Data.Finset.Powerset
/-- For predicate `p` decidable on ssubsets, it is decidable whether `p` holds for every ssubset.  -/
Finset.decidableForallOfDecidableSSubsets : {α : Type u_1} →
  [DecidableEq α] →
    {s : Finset α} →
      {p : (t : Finset α) → t ⊂ s → Prop} →
        [(t : Finset α) → (h : t ⊂ s) → Decidable (p t h)] → Decidable (∀ (t : Finset α) (h : t ⊂ s), p t h)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.eq_ratNorm : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ_[p]), ‖q‖ = ↑q.ratNorm
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.comp_mul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M),
  CategoryTheory.CategoryStruct.comp f (g₁ * g₂) =
    CategoryTheory.CategoryStruct.comp f g₁ * CategoryTheory.CategoryStruct.comp f g₂
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranCounit_app_app_ranAdjunction_unit_app_app : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (G : CategoryTheory.Functor D H) (X : C),
  CategoryTheory.CategoryStruct.comp (((L.ranAdjunction H).unit.app G).app (L.obj X))
      ((L.ranCounit.app (L.comp G)).app X) =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Functor D H)).obj G).obj (L.obj X))
-- Std.Data.TreeSet.Raw.Basic
/-- Computes the union of the given tree sets. If both maps contain elements that are equal according
to the comparison function, the element contained in the second argument will appear in the result.

This function always merges the smaller set into the larger set.
 -/
Std.TreeSet.Raw.union : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_homOfLE_assoc : ∀ (X : AlgebraicGeometry.Scheme) {U V W : X.Opens} (e₁ : U ≤ V) (e₂ : V ≤ W) {Z : AlgebraicGeometry.Scheme}
  (h : ↑W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.homOfLE e₁) (CategoryTheory.CategoryStruct.comp (X.homOfLE e₂) h) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) h
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α}, k ∈ Std.ExtHashMap.filter f m → k ∈ m
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- By `infer_instance` for `Algebra.QuasiFiniteAt R p`.  -/
Algebra.WeaklyQuasiFiniteAt.finite_residueField : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [inst_3 : q.IsPrime] [inst_4 : p.IsPrime] [inst_5 : q.LiesOver p] [Algebra.WeaklyQuasiFiniteAt R q]
  [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q], Module.Finite p.ResidueField q.ResidueField
-- Batteries.Data.List.Lemmas
List.mem_insertP : ∀ {α : Type u_1} (p : α → Bool) (a : α) (l : List α), a ∈ List.insertP p a l
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_inclusion : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S T : L.Substructure M} (h : S ≤ T),
  ⇑(FirstOrder.Language.Substructure.inclusion h) = Set.inclusion h
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceRErase.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (hrb_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced) (size : ℕ)
  (k_1 : α) (v_1 : β k_1)
  (hrb_4 :
    (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
        Std.DTreeMap.Internal.Impl.leaf).Balanced)
  (hlr_3 :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
      (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
          Std.DTreeMap.Internal.Impl.leaf).size
      Std.DTreeMap.Internal.Impl.leaf.size),
  Std.DTreeMap.Internal.Impl.balanceRErase k v Std.DTreeMap.Internal.Impl.leaf
      (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
      hrb_2 hrb_4 hlr_3 =
    Std.DTreeMap.Internal.Impl.inner 2 k v Std.DTreeMap.Internal.Impl.leaf
      (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mk.inj : ∀ {A : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} A} {B : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {T : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} T}
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} {toComma : CategoryTheory.Comma L R}
  {prop : P toComma.hom} {toComma_1 : CategoryTheory.Comma L R} {prop_1 : P toComma_1.hom},
  { toComma := toComma, prop := prop } = { toComma := toComma_1, prop := prop_1 } → toComma = toComma_1
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_cancel' : ∀ {a b : ℤ}, a ∣ b → a * b.fdiv a = b
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_mul_C' : ∀ {R : Type u} {S : Type v} {a : R} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
  Commute (f a) x → Polynomial.eval₂ f x (p * Polynomial.C a) = Polynomial.eval₂ f x p * f a
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instLEOrdinal : LE Std.Time.Week.OfYear.Ordinal
-- Mathlib.Data.Nat.Log
Nat.clog_anti_left : ∀ {b c n : ℕ}, 1 < c → c ≤ b → Nat.clog b n ≤ Nat.clog c n
-- Mathlib.Geometry.Euclidean.Projection
/-- The `orthogonalProjection` lies in the orthogonal subspace.  -/
EuclideanGeometry.orthogonalProjection_mem_orthogonal : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  ↑((EuclideanGeometry.orthogonalProjection s) p) ∈ AffineSubspace.mk' p s.directionᗮ
-- Mathlib.Topology.Homotopy.Lifting
/-- The monodromy action of the fundamental group at `x` on the fiber over `x`.  -/
IsCoveringMap.monodromyPerm : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} → IsCoveringMap p → (x : X) → FundamentalGroup X x →* Equiv.Perm ↑(p ⁻¹' {x})
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.add_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive] {u v : CategoryTheory.Comma L R}
  (α β : u ⟶ v), (α + β).right = α.right + β.right
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u} →
    {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u} →
      {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u} →
        {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u} →
          {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u} →
            {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} →
              (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) →
                ((t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t) →
                  ((t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t) →
                    ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t) →
                      ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t) →
                        ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t) →
                          ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t) →
                            ((t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t) →
                              motive_6 t ×' t.below