mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.comp_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.LeftHomologyData}
  {h₂ : S₂.LeftHomologyData} {h₃ : S₃.LeftHomologyData} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
  (ψ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₂ h₃),
  (ψ.comp ψ').φH = CategoryTheory.CategoryStruct.comp ψ.φH ψ'.φH
-- Mathlib.Data.Fin.Embedding
Fin.natAdd_castLEEmb.eq_1 : ∀ {n m : ℕ} (hmn : n ≤ m), Fin.natAdd_castLEEmb hmn = (Fin.addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding
-- Lean.Meta.Tactic.Cases
Lean.Meta.ByCasesSubgoal.mvarId : Lean.Meta.ByCasesSubgoal → Lean.MVarId
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.cons_vecMul_cons : ∀ {α : Type u} {n : ℕ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] (x : α) (v : Fin n → α) (w : o' → α)
  (B : Fin n → o' → α),
  Matrix.vecMul (Matrix.vecCons x v) (Matrix.of (Matrix.vecCons w B)) = x • w + Matrix.vecMul v (Matrix.of B)
-- Plausible.Gen
/-- Given a list of example generators, choose one to create an example.  -/
Plausible.Gen.oneOf : {α : Type u} → (xs : Array (Plausible.Gen α)) → autoParam (0 < xs.size) Plausible.Gen.oneOf._auto_1 → Plausible.Gen α
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
/-- The continuous functional calculus of a Hermitian matrix as a triple product using the
spectral theorem. Note that this actually operates on bare functions since every function is
continuous on the spectrum of a matrix, since the spectrum is finite. This is shown to be equal to
the generic continuous functional calculus API in `Matrix.IsHermitian.cfc_eq`. In general, users
should prefer the generic API, especially because it will make rewriting easier.  -/
Matrix.IsHermitian.cfc : {n : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] → [Fintype n] → [DecidableEq n] → {A : Matrix n n 𝕜} → A.IsHermitian → (ℝ → ℝ) → Matrix n n 𝕜
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.GeometricallyIntegral.geometrically_isIntegral : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.GeometricallyIntegral f],
  AlgebraicGeometry.geometrically AlgebraicGeometry.IsIntegral f
-- Mathlib.Data.Finset.Disjoint
Finset.disjUnion_inj_right : ∀ {α : Type u_2} {s t₁ t₂ : Finset α} (h₁ : Disjoint s t₁) (h₂ : Disjoint s t₂),
  s.disjUnion t₁ h₁ = s.disjUnion t₂ h₂ ↔ t₁ = t₂
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyRel.trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {f₀ f₁ f₂ : X ⟶ Y} [HomotopicalAlgebra.IsCofibrant X],
  HomotopicalAlgebra.LeftHomotopyRel f₀ f₁ →
    HomotopicalAlgebra.LeftHomotopyRel f₁ f₂ → HomotopicalAlgebra.LeftHomotopyRel f₀ f₂
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.mk : {P : Type u_2} → [inst : MetricSpace P] → P → ℝ → EuclideanGeometry.Sphere P
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_add_sphere_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), {x} + Metric.sphere 0 δ = Metric.sphere x δ
-- Mathlib.Data.Nat.Digits.Defs
Nat.toDigitsCore_lens_eq_aux : ∀ (b f n : ℕ) (l1 l2 : List Char),
  l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The naturality condition.  -/
CategoryTheory.Oplax.LaxTrans.Modification.naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Oplax.LaxTrans.Modification η θ)
  {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (F.map f) (θ.app b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f))
      (CategoryTheory.CategoryStruct.comp (θ.naturality f) h) =
    CategoryTheory.CategoryStruct.comp (η.naturality f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b)) h)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.const.match_1.eq_2 : ∀ (motive : Tactic.ComputeAsymptotics.Basis → Sort u_1) (basis_hd : ℝ → ℝ) (basis_tl : List (ℝ → ℝ))
  (h_1 : Unit → motive []) (h_2 : (basis_hd : ℝ → ℝ) → (basis_tl : List (ℝ → ℝ)) → motive (basis_hd :: basis_tl)),
  (match basis_hd :: basis_tl with
    | [] => h_1 ()
    | basis_hd :: basis_tl => h_2 basis_hd basis_tl) =
    h_2 basis_hd basis_tl
-- Init.Data.Order.Classes
Std.IsPreorder.le_trans : ∀ {α : Type u} {inst : LE α} [self : Std.IsPreorder α] (a b c : α), a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- If the norm of every monic linear polynomial over `ℂ`, evaluated at some `x : F`,
is bounded below by `M`, then the norm of the value at `x - algebraMap ℂ F c` of a monic polynomial
of degree `n` is bounded below by `M ^ n`. This follows by induction from the fact that
every monic polynomial over `ℂ` factors as a product of monic linear polynomials.  -/
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.Complex.le_aeval_of_isMonicOfDegree : ∀ {F : Type u_1} [inst : NormedRing F] [NormOneClass F] [NormMulClass F] [inst_3 : NormedAlgebra ℂ F] (x : F) {M : ℝ},
  0 ≤ M →
    (∀ (z' : ℂ), M ≤ ‖x - (algebraMap ℂ F) z'‖) →
      ∀ {p : Polynomial ℂ} {n : ℕ},
        p.IsMonicOfDegree n → ∀ (c : ℂ), M ^ n ≤ ‖(Polynomial.aeval (x - (algebraMap ℂ F) c)) p‖
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.iSup_skeleton : ∀ (X : SSet), ⨆ n, X.skeleton n = ⊤
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {fallback : γ},
  (Std.TreeMap.map f t).getD k fallback = (Option.map (f k) t[k]?).getD fallback
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.augment_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C)
  (f : X₀ ⟶ X.obj { len := 0 })
  (w :
    ∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
      CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)),
  (X.augment X₀ f w).left = X₀
-- Lean.Elab.Tactic.Simp
/-- User options. Registering a global option `tactic.simp.user.myOption` enables the tactic
configurations `(user.myOption := ...)` and `+user.myOption`.  -/
Lean.Meta.DSimp.ConfigWithOptions.userConfig : Lean.Meta.DSimp.ConfigWithOptions → Lean.Options
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.CommandCodeActions.mk.injEq : ∀ (onAnyCmd : Array Lean.CodeAction.CommandCodeAction) (onCmd : Lean.NameMap (Array Lean.CodeAction.CommandCodeAction))
  (onAnyCmd_1 : Array Lean.CodeAction.CommandCodeAction)
  (onCmd_1 : Lean.NameMap (Array Lean.CodeAction.CommandCodeAction)),
  ({ onAnyCmd := onAnyCmd, onCmd := onCmd } = { onAnyCmd := onAnyCmd_1, onCmd := onCmd_1 }) =
    (onAnyCmd = onAnyCmd_1 ∧ onCmd = onCmd_1)
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.add.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m, Int.ofNat n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_1 m n
-- Init.Data.Vector.Basic
/-- Pad a vector on the right with a given element.

Note that we immediately simplify this to an `++` operation,
and do not provide separate verification theorems.
 -/
Vector.rightpad : {α : Type u_1} → {m : ℕ} → (n : ℕ) → α → Vector α m → Vector α (max n m)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (F : CategoryTheory.Functor C D) →
                    (G : CategoryTheory.Functor D E) → [F.LaxMonoidal] → [G.LaxMonoidal] → (F.comp G).LaxMonoidal
-- Std.Time.Format
/-- Parses a `String` in the rfc850 format and returns a `DateTime`.
 -/
Std.Time.DateTime.fromRFC850String : String → Except String Std.Time.DateTime
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_add_self : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], μ.rnDeriv (ν + μ) =ᵐ[μ] fun x => (ν.rnDeriv μ x + 1)⁻¹
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The map sending a function `f : α →ᵤ[𝔖] β` to the family of restrictions of `f` to each `s ∈ 𝔖`
(each coordinate equipped with its respective uniform structure `s →ᵤ β`) induces the uniformity on
`α →ᵤ[𝔖] β`.  -/
UniformOnFun.isUniformInducing_pi_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)},
  IsUniformInducing fun f s => UniformFun.ofFun ((↑s).domRestrict ((UniformOnFun.toFun 𝔖) f))
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_3 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) (id : ℕ)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_3 id c rupHints
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  (M : Matrix m n α) (v : n → α) (i : m), M.mulVec v i = M.row i ⬝ᵥ v
-- Mathlib.Data.ENNReal.Real
/-- Extension for the `positivity` tactic: `ENNReal.ofReal`.  -/
Mathlib.Meta.Positivity.evalENNRealOfReal : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Complex.hasStrictDerivAt_cpow_const : ∀ {x c : ℂ}, x ∈ Complex.slitPlane → HasStrictDerivAt (fun z => z ^ c) (c * x ^ (c - 1)) x
-- Mathlib.Topology.ContinuousMap.Basic
/-- The obvious triangle induced by `IsQuotientMap.lift` commutes:
```
     g
  X --→ Z
  |   ↗
f |  / hf.lift g h
  v /
  Y
```
 -/
Topology.IsQuotientMap.lift_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : C(X, Y)} (hf : Topology.IsQuotientMap ⇑f) (g : C(X, Z))
  (h : Function.FactorsThrough ⇑g ⇑f), (hf.lift g h).comp f = g
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.nonMemberSubfamily.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)), Finset.nonMemberSubfamily a 𝒜 = {s ∈ 𝒜 | a ∉ s}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.forM_eq_forM_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α × β → m PUnit.{w + 1}},
  forM t f = forM t.toList f
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.mul : ∀ {M : Type u_4} [inst : Mul M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {s t : Set M} {a b c d : M},
  JoinedIn s a b → JoinedIn t c d → JoinedIn (s * t) (a * c) (b * d)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.opcyclesMap_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.opcyclesMap (-φ) = -CategoryTheory.ShortComplex.opcyclesMap φ
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Reinterpret a `ContinuousAddMonoidHom` as an `AddMonoidHom`.  -/
ContinuousAddMonoidHom.toAddMonoidHom : {A : Type u_7} →
  {B : Type u_8} →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → (A →ₜ+ B) → A →+ B
-- Mathlib.Algebra.Order.Group.Indicator
Set.mabs_mulIndicator_symmDiff : ∀ {α : Type u_2} {M : Type u_3} [inst : CommGroup M] [inst_1 : Lattice M] (s t : Set α) (f : α → M) (x : α),
  |(symmDiff s t).mulIndicator f x|ₘ = |s.mulIndicator f x / t.mulIndicator f x|ₘ
-- Mathlib.Algebra.Homology.LocalCohomology
/-- Local cohomology agrees on ideals with the same radical.  -/
localCohomology.isoOfSameRadical : {R : Type u} →
  [inst : CommRing R] →
    {J K : Ideal R} → [IsNoetherian R R] → J.radical = K.radical → (i : ℕ) → localCohomology J i ≅ localCohomology K i
-- Mathlib.Data.Matrix.Basic
Matrix.diagLinearMap_apply : ∀ (n : Type u_3) (R : Type u_7) (α : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid α] [inst_2 : Module R α]
  (a : Matrix n n α) (a_1 : n), (Matrix.diagLinearMap n R α) a a_1 = (↑(Matrix.diagAddMonoidHom n α)).toFun a a_1
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.below.symm : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {motive : (a a_1 : M) → ConGen.Rel r a a_1 → Prop} {x y : M}
  (a : ConGen.Rel r x y), ConGen.Rel.below a → motive x y a → ConGen.Rel.below ⋯
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_div_two_pow : ∀ {a b n : ℕ}, (a ||| b) / 2 ^ n = a / 2 ^ n ||| b / 2 ^ n
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisRight_symm_apply : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq κ]
  (𝒞 : Module.Basis κ R N) (b : κ →₀ M),
  (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm b = b.sum fun i m => m ⊗ₜ[R] 𝒞 i
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.bminor.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) {p : ℕ} (i j : Fin n) (α : Fin p → Fin n),
  BirdDet.bminor✝ A i j α = (A.submatrix (Fin.cons i α) (Fin.cons j α)).det
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Paste two pushout squares "horizontally" to obtain another pushout square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
|            |            |
v₁₁          v₁₂          v₁₃
↓            ↓            ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
```
 -/
CategoryTheory.IsPushout.paste_horiz : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
  CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ →
    CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂ →
      CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
        (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂)
-- Mathlib.Data.PFun
PFun.core_restrict : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), (↑f).core s = f ⁻¹' s
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂_run'_eq_mergeSort : ∀ {α : Type u_1} {l' : List α} {le : α → α → Bool} {n : ℕ} (l : { l // l.length = n }),
  l' = (↑l).reverse → List.MergeSort.Internal.mergeSortTR₂.run'✝ le l = l'.mergeSort le
-- Mathlib.Order.ModularLattice
instIsModularLatticeOrderDual : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α], IsModularLattice αᵒᵈ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_map : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [LawfulBEq α] [inst_3 : Inhabited γ] {f : α → β → γ} {k : α},
  m.WF →
    Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.map f m) k = (Option.map (f k) (Std.DHashMap.Raw.Const.get? m k)).get!
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Weekday.Ordinal n
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The ring map from `A⁰_ f` to the global sections of the structure sheaf of the projective spectrum
of `A` restricted to the basic open set `D(f)`.

Mathematically, the map is the same as `awayToSection`.
 -/
AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                CommRingCat.of (HomogeneousLocalization.Away 𝒜 f) ⟶
                  AlgebraicGeometry.LocallyRingedSpace.Γ.obj
                    (Opposite.op ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯))
-- Lean.CompactedRegion
/-- Saves arbitrary data to a compacted region on disk.

The `α` type parameter is erased at the runtime/extern boundary: the compactor walks the live
object graph rooted at `data` regardless of its Lean type. `α` is purely a hint for the caller to
align save and load sites. Mismatched types between save and load yield undefined behavior on use.

`key` is hashed to derive a deterministic mmap base address; for module saves, pass the module
`Name`. `depRegions` are loaded compacted regions (typically from imports) whose objects should
not be re-serialized. `prev`, when present, likewise allows for reuse of objects from prior saves
in the same session.

If `allowClosures` is `true`, closures in the compacted data are tolerated and the file is written
in the extended `v3` olean format (which may become the default in the future). This is an
EXPERIMENTAL option. The saving and loading process must be using identical executables, including
dependent libraries. When `false`, encountering a closure is an error and the file is written in the
old `v2` format.

Returns a `Compactor` that may be passed as `prev` to subsequent saves. Unsafe because the
returned `Compactor` carries thread-safety and `depRegions` lifetime contracts the type system
cannot enforce; see `Compactor`.
 -/
Lean.CompactedRegion.save : {α : Type} →
  System.FilePath →
    Lean.Name → α → Array Lean.CompactedRegion → Option Lean.Compactor → optParam Bool false → IO Lean.Compactor
-- Mathlib.Algebra.Module.Basic
Set.smul_indicator_one_apply : ∀ {α : Type u_1} {R : Type u_2} [inst : MulZeroOneClass R] (s : Set α) (r : R) (a : α),
  r • s.indicator 1 a = s.indicator (fun x => r) a
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.forIn_filterMap : ∀ {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : Std.Internal.Do.Assertion Pred]
  [inst_4 : Std.Internal.Do.Assertion EPred] [inst_5 : Std.Internal.Do.WPMonad n Pred EPred] [inst_6 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [inst_8 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_10 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] {it : Std.IterM m β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)}
  {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc =>
        match f out with
        | some c => g c acc
        | none => pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.IterM.filterMap f it) init g ⦃ Q; eQ ⦄
-- Mathlib.Computability.RecursiveIn
Nat.Primrec.recursiveIn : ∀ {O : Set (ℕ →. ℕ)} {f : ℕ → ℕ}, Nat.Primrec f → Nat.RecursiveIn O fun n => ↑(some (f n))
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.tendsto_nhds_iff_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α] {β : Type u_3} {f : β → α}
  {l : Filter β} {x : α}, Filter.Tendsto f l (nhds x) ↔ ∀ y < x, ∀ᶠ (z : β) in l, y < f z
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl).destruct = some (exp, coef, tl)
-- Lean.Parser.Basic
/-- The `colGe` parser requires that the next token starts from at least the column of the saved
position (see `withPosition`), but allows it to be more indented.
This can be used for whitespace sensitive syntax to ensure that a block does not go outside a
certain indentation scope. For example it is used in the lean grammar for `else if`, to ensure
that the `else` is not less indented than the `if` it matches with.

This parser has arity 0 - it does not capture anything.  -/
Lean.Parser.checkColGe : optParam String "checkColGe" → Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_eq_top_of_span_eq_top : ∀ (R : Type u_1) {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [IsScalarTower R S M] (s : Set M),
  Submodule.span R s = ⊤ → Submodule.span S s = ⊤
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieRing.assoc_symm : ∀ {L : Type u_2} [inst : RightPreLieRing L] (x y z : L), associator x y z = associator x z y
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `upperSemiContinuous_inv_iff`. -/
LowerSemicontinuous.inv : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} [inst_1 : PartialOrder β] [inst_2 : CommGroup β]
  [IsOrderedMonoid β], LowerSemicontinuous f → UpperSemicontinuous f⁻¹
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommSemiring.toQFn? : Lean.Meta.Sym.Arith.CommSemiring → Option Lean.Expr
-- Mathlib.Control.ULiftable
Except.instULiftable : {ε : Type u₀} → ULiftable (Except ε) (Except ε)
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.mk.inj : ∀ {α : Type u_8} {β : Type u_9} {inst : SupSet α} {inst_1 : SupSet β} {toFun : α → β}
  {map_sSup' : ∀ (s : Set α), toFun (sSup s) = sSup (toFun '' s)} {toFun_1 : α → β}
  {map_sSup'_1 : ∀ (s : Set α), toFun_1 (sSup s) = sSup (toFun_1 '' s)},
  { toFun := toFun, map_sSup' := map_sSup' } = { toFun := toFun_1, map_sSup' := map_sSup'_1 } → toFun = toFun_1