mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Limits
/-- A version with more restrictive universes. See `IsAffineOpen.iSup_of_disjoint`.  -/
_private.Mathlib.AlgebraicGeometry.Limits.0.AlgebraicGeometry.IsAffineOpen.iSup_of_disjoint_aux : ∀ {ι : Type u} {X : AlgebraicGeometry.Scheme} [Finite ι] {U : ι → X.Opens},
  (∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)) →
    Pairwise (Function.onFun Disjoint U) → AlgebraicGeometry.IsAffineOpen (iSup U)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.writeRequest : {α : Type u_1} → [Lean.ToJson α] → Lean.JsonRpc.Request α → Lean.Lsp.Ipc.IpcM Unit
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- If `s` is a splitting of a simplicial object `X` in a preadditive category,
`s.nondegComplex` is a chain complex which is given in degree `n` by
the nondegenerate `n`-simplices of `X`. This chain complex should be thought
as the normalized chain complex of `X` because of the isomorphism
`toKaroubiNondegComplexIsoN₁`.  -/
CategoryTheory.SimplicialObject.Splitting.nondegComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} → X.Splitting → [inst_1 : CategoryTheory.Preadditive C] → ChainComplex C ℕ
-- Mathlib.Algebra.Lie.TransferInstance
/-- An equivalence `e : L' ≃ L` gives a Lie algebra equivalence `L' ≃ₗ⁅R⁆ L` where the algebraic
structures on `L'` are obtained by transporting the structures on `L` back along `e`.  -/
Equiv.lieEquiv : (R : Type u_1) →
  {L' : Type u_2} →
    {L : Type u_3} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (e : L' ≃ L) → L' ≃ₗ⁅R⁆ L
-- Lean.Expr
Lean.Expr.forallInfo : (a : Lean.Expr) → a.isForall = true → Lean.BinderInfo
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.instOrderTopology : OrderTopology Ordinal.{u}
-- Init.Prelude
Add.mk : {α : Type u} → (α → α → α) → Add α
-- Lean.Elab.Term.TermElabM
/-- Elaborate `x` with `stx` on the macro stack and produce macro expansion info  -/
Lean.Elab.Term.withMacroExpansion : {n : Type → Type u_1} →
  {α : Type} → [Monad n] → [MonadControlT Lean.Elab.TermElabM n] → Lean.Syntax → Lean.Syntax → n α → n α
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extendedHom_eq_zero_iff : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K},
  (FractionalIdeal.extendedHom L B) I = 0 ↔ I = 0
-- Mathlib.AlgebraicTopology.Quasicategory.Basic
SSet.quasicategory_of_hasLiftingProperty : ∀ (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X),
  (∀ {n : ℕ} {i : Fin (n + 1)},
      0 < i → i < Fin.last n → CategoryTheory.HasLiftingProperty (SSet.horn n i).ι (t.from S)) →
    S.Quasicategory
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.lineCount_eq : ∀ {P : Type u_1} (L : Type u_2) [inst : Membership P L] [inst_1 : Configuration.ProjectivePlane P L] [Finite P]
  [Finite L] (p : P), Configuration.lineCount L p = Configuration.ProjectivePlane.order P L + 1
-- Mathlib.Order.Hom.Lattice
/-- `id` as an `InfHom`.  -/
InfHom.id : (α : Type u_2) → [inst : Min α] → InfHom α α
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.stieltjesFunctionRightLim.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {E : Type u_2}
  [inst_3 : NormedAddCommGroup E] [inst_4 : CompleteSpace E] {f f_1 : α → E} (e_f : f = f_1)
  (hf : BoundedVariationOn f Set.univ) (x₀ x₀_1 : α),
  x₀ = x₀_1 → hf.stieltjesFunctionRightLim x₀ = ⋯.stieltjesFunctionRightLim x₀_1
-- Mathlib.Algebra.Free
FreeMagma.traverse_pure' : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β), traverse F ∘ pure = fun x => pure <$> F x
-- Mathlib.Logic.Equiv.PartialEquiv
/-- **Alias** of the forward direction of `PartialEquiv.IsImage.iff_preimage_eq`. -/
PartialEquiv.IsImage.preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.IsImage s t → e.source ∩ ↑e ⁻¹' t = e.source ∩ s
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.limitPresheafOfModules_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [inst_2 :
    ∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections]
  (X : Cᵒᵖ),
  (PresheafOfModules.limitPresheafOfModules F).obj X =
    CategoryTheory.Limits.limit (F.comp (PresheafOfModules.evaluation R X))
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C)
  {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso X t).hom.right = ⋯.isoPullback.inv
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
the common arrows will agree with those of the original path `f`. In particular,
an arrow `i` with `i + 1 < j` can be identified with the same arrow in `f`.  -/
SSet.Truncated.StrictSegal.spine_δ_arrow_lt : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n) (f : X.Path (m + 1)) {i : Fin m}
  {j : Fin (m + 2)},
  i.succ.castSucc < j →
    (X.spine m ⋯
            ((CategoryTheory.ConcreteCategory.hom
                (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op))
              (sx.spineToSimplex (m + 1) ⋯ f))).arrow
        i =
      f.arrow i.castSucc
-- Init.Control.ExceptCps
ExceptCpsT.runK_bind_lift : ∀ {m : Type u_1 → Type u_2} {α ε β : Type u_1} {s : ε} {a : Type u_1} {ok : β → m a} {error : ε → m a} [inst : Monad m]
  (x : m α) (f : α → ExceptCpsT ε m β),
  (ExceptCpsT.lift x >>= f).runK s ok error = do
    let a_1 ← x
    (f a_1).runK s ok error
-- Aesop.Rule
Aesop.UnfoldRule.mk : Lean.Name → Option Lean.Name → Aesop.UnfoldRule
-- Std.Time.Date.Unit.Year
Std.Time.Year.instOfNatOffset : {n : ℕ} → OfNat Std.Time.Year.Offset n
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_rec' : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → ℕ} {g : α → β}
  {h : α → ℕ × β → β},
  Primrec f → Primrec g → Primrec₂ h → Primrec fun a => Nat.rec (g a) (fun n IH => h a (n, IH)) (f a)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.nhdsUniv : ∀ (a : ℝ), intervalIntegral.FTCFilter a (nhdsWithin a Set.univ) (nhds a)
-- Mathlib.Data.Complex.Basic
/-- The product of a set on the real axis and a set on the imaginary axis of the complex plane,
denoted by `s ×ℂ t`.  -/
Complex.«term_×ℂ_» : Lean.TrailingParserDescr
-- Lean.Meta.InferType
/-- Given `n` and a non-dependent function type `α₁ → α₂ → ... → αₙ → Sort u`, returns the
types `α₁, α₂, ..., αₙ`. Throws an error if there are not at least `n` argument types or if a
later argument type depends on a prior one (i.e., it's a dependent function type).

This can be used to infer the expected type of the alternatives when constructing a `MatcherApp`.
 -/
Lean.Meta.arrowDomainsN : ℕ → Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The right adjoint of an oplax monoidal functor is lax monoidal.  -/
CategoryTheory.Adjunction.rightAdjointLaxMonoidal : {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] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} → (F ⊣ G) → [F.OplaxMonoidal] → G.LaxMonoidal
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator_ne_zero : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete], ↑(Valuation.IsRankOneDiscrete.generator v) ≠ 0
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.RightFraction₂.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W x)] {X' : C} (s : X' ⟶ X) (hs : W s)
  (f f' : X' ⟶ Y),
  sizeOf { X' := X', s := s, hs := hs, f := f, f' := f' } = 1 + sizeOf X' + sizeOf s + sizeOf hs + sizeOf f + sizeOf f'
-- Init.Data.Array.Find
Array.find?_filterMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} {p : β → Bool},
  Array.find? p (Array.filterMap f xs) = (Array.find? (fun a => Option.any p (f a)) xs).bind f
-- Init.Data.SInt.Lemmas
Int32.toInt_le : ∀ (x : Int32), x.toInt ≤ Int32.maxValue.toInt
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_hom_app : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : B'),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso hF).hom.app X =
    CategoryTheory.CategoryStruct.comp (hF.inv.app (eA.inverse.obj (e'.inverse.obj X)))
      (CategoryTheory.CategoryStruct.comp (e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj X)))
        (e'.counitIso.hom.app X))
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_congr : ∀ {o₁ o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}) (ho : o₁ = o₂),
  o₁.blsub f = o₂.blsub fun a h => f a ⋯
-- Mathlib.FieldTheory.Relrank
IntermediateField.inf_relfinrank_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E),
  (A ⊓ B).relfinrank B = A.relfinrank B
-- Mathlib.Topology.Separation.Regular
Topology.IsInducing.regularSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [RegularSpace X] [inst_2 : TopologicalSpace Y] {f : Y → X},
  Topology.IsInducing f → RegularSpace Y
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_zero_eq_const : SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
    SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3 =
  SimplexCategory.Truncated.Hom.tr ({ len := 0 }.const { len := 0 + 1 } 1)
    SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.map_add_right_Ico : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  [ExistsAddOfLE α] [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Finset.map (addRightEmbedding c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.SpecMap_preimage_basicOpen : ∀ {R S : CommRingCat} (f : R ⟶ S) (r : ↑R),
  (TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map f).base).obj (PrimeSpectrum.basicOpen r) =
    PrimeSpectrum.basicOpen ((CategoryTheory.ConcreteCategory.hom f) r)
-- Mathlib.CategoryTheory.Subfunctor.OfSection
CategoryTheory.Subfunctor.ofSection_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ}
  (x : F.obj X) (G : CategoryTheory.Subfunctor F), CategoryTheory.Subfunctor.ofSection x ≤ G ↔ x ∈ G.obj X
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.cast : Lean.Name → Lean.Name → Lean.Name → Lean.Name → Lean.Name → Mathlib.Tactic.UnfoldBoundary.UnfoldEntry
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.powerBasis_basis : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), h.powerBasis.basis = h.basis
-- Mathlib.RingTheory.Multiplicity
emultiplicity_le_emultiplicity_of_dvd_right : ∀ {α : Type u_1} [inst : Monoid α] {a b c : α}, b ∣ c → emultiplicity a b ≤ emultiplicity a c
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k a : α} {fallback v : β},
  Std.DHashMap.Const.getD (m.insertIfNew k v) a fallback =
    if (k == a) = true ∧ k ∉ m then v else Std.DHashMap.Const.getD m a fallback
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.instGroupSubtypeMatrixSumMemSubmonoidSymplecticGroup : {l : Type u_1} →
  {R : Type u_2} →
    [inst : DecidableEq l] → [inst_1 : Fintype l] → [inst_2 : CommRing R] → Group ↥(Matrix.symplecticGroup l R)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.aux_summable_add : ∀ {k : ℕ}, 1 ≤ k → ∀ (x : ℂ), Summable fun n => (x + (↑n + 1)) ^ (-1 - ↑k)
-- Lean.Elab.InfoTree.Main
Lean.Elab.ContextInfo.runMetaM : {α : Type} → Lean.Elab.ContextInfo → Lean.LocalContext → Lean.MetaM α → IO α
-- Mathlib.Algebra.GCDMonoid.Finset
/-- The gcd of a finset of integers is nonnegative.  -/
Finset.Int.finsetGcd_nonneg : ∀ {ι : Type u_1} {s : Finset ι} {f : ι → ℤ}, 0 ≤ s.gcd f
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.quotEquivOfEqBot_apply_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  (hp : p = ⊥) (x : M), (p.quotEquivOfEqBot hp) (Submodule.Quotient.mk x) = x
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mrange_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mrange (MonoidHom.snd M N) = ⊤
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.eq_iff_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) {x y : M}, f x = f y ↔ g x = g y
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertMany_list_singleton : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] {k : α}
  {v : β k}, ↑(m.insertMany [⟨k, v⟩]) = m.insert k v
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.isBase_of_spanning : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis I X → M.Spanning X → M.IsBase I
-- Init.Data.Float.Model.Float
/-- Converts a `USize` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofUSize : USize → Float.Model
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.AC.DiseqCnstr → Sort u} {motive_2 : Lean.Meta.Grind.AC.DiseqCnstrProof → Sort u}
  (t : Lean.Meta.Grind.AC.DiseqCnstr) (F_1 : (t : Lean.Meta.Grind.AC.DiseqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.AC.DiseqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Meta.Grind.AC.DiseqCnstr.brecOn.go t F_1 F_2).2
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.curryAddEquiv_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (m : M)
  (n : N) (r : R),
  MonoidAlgebra.curryAddEquiv (MonoidAlgebra.single (m, n) r) = MonoidAlgebra.single m (MonoidAlgebra.single n r)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.sup_adj : ∀ {V : Type u} {G : SimpleGraph V} {G₁ G₂ : G.Subgraph} {a b : V}, (G₁ ⊔ G₂).Adj a b ↔ G₁.Adj a b ∨ G₂.Adj a b
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
/-- If `X` is a limit indexed by `J` of objects satisfying a property `P`, then
any object that is isomorphic to `X` also is.  -/
CategoryTheory.ObjectProperty.LimitOfShape.ofIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} → P.LimitOfShape J X → {Y : C} → (X ≅ Y) → P.LimitOfShape J Y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryGED_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : α × β}, t₁.Equiv t₂ → t₁.getEntryGED k fallback = t₂.getEntryGED k fallback
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor `Comma L₁ R ⥤ Comma L₃ R` induced by the composition of two natural transformations
`l : L₁ ⟶ L₂` and `l' : L₂ ⟶ L₃` is naturally isomorphic to the composition of the two functors
induced by these natural transformations.  -/
CategoryTheory.Comma.mapLeftComp : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (R : CategoryTheory.Functor B T) →
              {L₁ L₂ L₃ : CategoryTheory.Functor A T} →
                (l : L₁ ⟶ L₂) →
                  (l' : L₂ ⟶ L₃) →
                    CategoryTheory.Comma.mapLeft R (CategoryTheory.CategoryStruct.comp l l') ≅
                      (CategoryTheory.Comma.mapLeft R l').comp (CategoryTheory.Comma.mapLeft R l)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Pulling back along a composition is naturally isomorphic to
the composition of the pullbacks.  -/
CategoryTheory.GrothendieckTopology.pullbackComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) → J.pullback (CategoryTheory.CategoryStruct.comp f g) ≅ (J.pullback g).comp (J.pullback f)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Rel.trans : ∀ {α : Type u_1} (r : α → α → Prop) [IsTrans α r] {s t u : Multiset α},
  Multiset.Rel r s t → Multiset.Rel r t u → Multiset.Rel r s u
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_sdiff_Ioi_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Ici a \ Set.Ioi a = {a}
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} →
          (n : ℕ) → aig.RefVec w → aig.RefVec n → ℕ → Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.eq_of_forall_apply_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ ν : MeasureTheory.FiniteMeasure Ω),
  (∀ (s : Set Ω), MeasurableSet s → μ s = ν s) → μ = ν
-- Mathlib.Data.Fin.Tuple.Take
Fin.castLE.eq_1 : ∀ {n m : ℕ} (h : n ≤ m) (i : Fin n), Fin.castLE h i = ⟨↑i, ⋯⟩
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.edist_eq' : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (self : α →ᵈ β),
  ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (self.toFun x) (self.toFun y) = ↑r * edist x y
-- Mathlib.Algebra.Module.Presentation.Tautological
/-- The type which parametrizes the tautological relations in an `A`-module `M`.  -/
Module.Presentation.tautological.R : Type u → Type v → Type (max u v)
-- Mathlib.Order.Closure
LowerAdjoint.instInhabitedId : {α : Type u_1} → [inst : Preorder α] → Inhabited (LowerAdjoint id)
-- Mathlib.Data.NNReal.Basic
NNReal.toReal_le : ∀ (a b : NNReal), a ≤ b ↔ ↑a ≤ ↑b
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_3, u_2} D} {inst_2 : CategoryTheory.Category.{v_5, u_3} H}
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (W : CategoryTheory.MorphismProperty C) {inst_3 : L.IsLocalization W}
  [self : RF.IsRightDerivedFunctor α W], RF.IsLeftKanExtension α
-- Init.Data.BitVec.Lemmas
/-- A bitvector interpreted as a natural number is strictly smaller than `2 ^ i` if and only if
all bits at position `i` or higher are false.  -/
BitVec.toNat_lt_iff_getLsbD_eq_false : ∀ {w : ℕ} {x : BitVec w}, ∀ i < w, x.toNat < 2 ^ i ↔ ∀ (k : ℕ), x.getLsbD (i + k) = false
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.le_comap_ker : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] (g : G),
  Representation.Coinvariants.ker (MonoidHom.comp ρ S.subtype) ≤
    Submodule.comap (ρ g) (Representation.Coinvariants.ker (MonoidHom.comp ρ S.subtype))
-- Init.Data.List.Lemmas
List.getElem_concat_length : ∀ {α : Type u_1} {l : List α} {a : α} {i : ℕ}, i = l.length → ∀ (w : i < (l ++ [a]).length), (l ++ [a])[i] = a
-- Mathlib.RingTheory.Regular.Category
ModuleCat.smulShortComplex_X₂_carrier : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) (r : R), ↑(M.smulShortComplex r).X₂ = ↑M
-- Init.Data.Hashable
instHashableFin : {n : ℕ} → Hashable (Fin n)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKey_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {he : Std.ExtDTreeMap.Const.modify t k f ≠ ∅},
  (Std.ExtDTreeMap.Const.modify t k f).maxKey he = if cmp (t.maxKey ⋯) k = Ordering.eq then k else t.maxKey ⋯
-- Mathlib.Algebra.Group.WithOne.Basic
MulEquiv.withOneCongr_refl : ∀ {α : Type u} [inst : Mul α], (MulEquiv.refl α).withOneCongr = MulEquiv.refl (WithOne α)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.one_smul' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : ArithmeticFunction M), 1 • b = b
-- Init.Data.UInt.Bitwise
UInt32.ofFin_rev : ∀ (a : Fin UInt32.size), UInt32.ofFin a.rev = ~~~UInt32.ofFin a
-- Init.Data.Option.Lemmas
Option.getD_eq_iff : ∀ {α : Type u_1} {o : Option α} {a b : α}, o.getD a = b ↔ o = some b ∨ o = none ∧ a = b
-- Init.Data.Array.Lemmas
Array.mem_of_getElem? : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α}, xs[i]? = some a → a ∈ xs
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.specialUnitaryGroup.coe_star : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A : ↥(Matrix.specialUnitaryGroup n α)), ↑(star A) = star ↑A
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.isAlgebraic_adjoin_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  {s : Set S}, (Algebra.adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x