mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitor_naturality : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) {Y : C}
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X X' : CategoryTheory.GradedObject J D) (φ : X ⟶ X')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
      (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom φ
-- Init.Core
/-- Implementation detail.  -/
Thunk.fnImpl : {α : Type u_1} → Thunk α → Unit → α
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The `i`th arrow of `F : ComposableArrows C n`.  -/
CategoryTheory.ComposableArrows.arrow : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      CategoryTheory.ComposableArrows C n →
        (i : ℕ) → autoParam (i < n) CategoryTheory.ComposableArrows.arrow._auto_1 → CategoryTheory.ComposableArrows C 1
-- Mathlib.Order.Nucleus
Nucleus.instBoundedOrder : {X : Type u_1} → [inst : SemilatticeInf X] → [OrderTop X] → BoundedOrder (Nucleus X)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.lowerSemicontinuous_add : LowerSemicontinuous fun p => p.1 + p.2
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsMulRightInvariant.map_mul_right_eq_self : ∀ {G : Type u_1} {inst : MeasurableSpace G} {inst_1 : Mul G} {μ : MeasureTheory.Measure G}
  [self : μ.IsMulRightInvariant] (g : G), MeasureTheory.Measure.map (fun x => x * g) μ = μ
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.map_comp_ιMulti : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  (exteriorPower.map n f).compAlternatingMap (exteriorPower.ιMulti R n) = (exteriorPower.ιMulti R n).compLinearMap f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, a ∈ t.insert k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Batteries.Data.List.Basic
List.replaceF.eq_1 : ∀ {α : Type u_1} (f : α → Option α), List.replaceF f [] = []
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_eq : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → MeasureTheory.ae (μ.restrict s) = MeasureTheory.ae μ ⊓ Filter.principal s
-- Mathlib.Data.Multiset.Sym
Multiset.monotone_sym2 : ∀ {α : Type u_1}, Monotone Multiset.sym2
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.forInStep_eq_foldlM.match_1.eq_1 : ∀ {δ : Type u_1} (motive : ForInStep δ → Sort u_2) (d : δ) (h_1 : (d : δ) → motive (ForInStep.yield d))
  (h_2 : (d : δ) → motive (ForInStep.done d)),
  (match ForInStep.yield d with
    | ForInStep.yield d => h_1 d
    | ForInStep.done d => h_2 d) =
    h_1 d
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isPreconnected_nonempty_subsets : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, IsPreconnected s → IsPreconnected {K | (↑K).Nonempty ∧ ↑K ⊆ s}
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.inv_pos : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 < p⁻¹
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Extract an isomorphism
`L.pointwiseRightKanExtension F ⋙ G ≅ L.pointwiseRightKanExtension (F ⋙ G)` when `G` preserves
right Kan extensions.  -/
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  (F : CategoryTheory.Functor A B) →
                    (L : CategoryTheory.Functor A C) →
                      [inst_4 : G.PreservesPointwiseRightKanExtension F L] →
                        [inst_5 : L.HasPointwiseRightKanExtension F] →
                          (L.pointwiseRightKanExtension F).comp G ≅ L.pointwiseRightKanExtension (F.comp G)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
intervalIntegral.integrable_comp_mul_deriv_iff_of_deriv_nonpos : ∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), f' x ≤ 0) →
        (IntervalIntegrable (fun x => (g ∘ f) x * f' x) MeasureTheory.volume a b ↔
          IntervalIntegrable g MeasureTheory.volume (f a) (f b))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.induce_self_verts : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G'.induce G'.verts = G'
-- Mathlib.Logic.Embedding.Basic
subtypeOrLeftEmbedding_apply : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] (x : { x // p x ∨ q x }),
  (subtypeOrLeftEmbedding p q) x = if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- The `(m * n)`-th Chebyshev `T` polynomial is the composition of the `m`-th and `n`-th.  -/
Polynomial.Chebyshev.T_mul : ∀ (R : Type u_1) [inst : CommRing R] (m n : ℤ),
  Polynomial.Chebyshev.T R (m * n) = (Polynomial.Chebyshev.T R m).comp (Polynomial.Chebyshev.T R n)
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Wrapper around `Expr.int?` that also allows `Nat.cast`.  -/
Lean.Elab.Tactic.Omega.intCast? : Lean.Expr → Option ℤ
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSMul : {β : Type u_2} → {α : Type u_1} → [SMul β α] → SMul β αᵒᵈ
-- Mathlib.Topology.Compactness.Compact
/-- The complement to a compact set belongs to a filter `f` if each `x ∈ s` has a neighborhood `t`
within `s` such that `tᶜ` belongs to `f`.  -/
IsCompact.compl_mem_sets_of_nhdsWithin : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ {f : Filter X}, (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, tᶜ ∈ f) → sᶜ ∈ f
-- Mathlib.Algebra.Group.Commute.Hom
Commute.of_map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {x y : M} [inst_2 : FunLike F M N]
  [MulHomClass F M N] {f : F}, Function.Injective ⇑f → Commute (f x) (f y) → Commute x y
-- Mathlib.Algebra.Algebra.Operations
Submodule.comap_unop_pow : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
  (n : ℕ),
  Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) (M ^ n) =
    Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) M ^ n
-- Mathlib.Algebra.Group.Center
Set.mem_addCentralizer : ∀ {M : Type u_1} {S : Set M} [inst : Add M] {c : M}, c ∈ S.addCentralizer ↔ ∀ m ∈ S, m + c = c + m
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.map_add_right : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] [inst_13 : AddCommMonoid Q]
  [inst_14 : Module R Q] (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q),
  TensorProduct.AlgebraTensorModule.map f (g₁ + g₂) =
    TensorProduct.AlgebraTensorModule.map f g₁ + TensorProduct.AlgebraTensorModule.map f g₂
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_self_pow : ∀ {p k : ℕ}, Nat.Prime p → p ^ k / p ^ (p ^ k).factorization p = 1
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.Hom.mk.injEq : ∀ {M N : SemiNormedGrp₁} (hom' : NormedAddGroupHom M.carrier N.carrier) (normNoninc : hom'.NormNoninc)
  (hom'_1 : NormedAddGroupHom M.carrier N.carrier) (normNoninc_1 : hom'_1.NormNoninc),
  ({ hom' := hom', normNoninc := normNoninc } = { hom' := hom'_1, normNoninc := normNoninc_1 }) = (hom' = hom'_1)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.match_1.eq_5 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match ByteArray.utf8DecodeChar?.FirstByte.threeMore with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 ()
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 ()
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 ()
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 ()
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 ()) =
    h_5 ()
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_tilted_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (fun x => Real.exp (f x)) ν →
      MeasureTheory.llr μ (ν.tilted f) =ᵐ[μ] fun x =>
        -f x + Real.log (∫ (z : α), Real.exp (f z) ∂ν) + MeasureTheory.llr μ ν x
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- The first morphism of triangles given by an octahedron.  -/
CategoryTheory.Triangulated.Octahedron.triangleMorphism₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                        {v₁₂ : X₂ ⟶ Z₁₂} →
                          {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                            {h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles} →
                              {v₂₃ : X₃ ⟶ Z₂₃} →
                                {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                  {h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                    {v₁₃ : X₃ ⟶ Z₁₃} →
                                      {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                        {h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                          CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃ →
                                            (CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ⟶
                                              CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.le_multiplicity_of_le_emultiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α},
  FiniteMultiplicity a b → ∀ {n : ℕ}, ↑n ≤ emultiplicity a b → n ≤ multiplicity a b
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the
value.  -/
Summable : {α : Type u_1} →
  {β : Type u_2} →
    [AddCommMonoid α] →
      [TopologicalSpace α] → (β → α) → optParam (SummationFilter β) (SummationFilter.unconditional β) → Prop
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.symm_trans : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ f₂ : C(X, Y)}
  (F : f₀.Homotopy f₁) (G : f₁.Homotopy f₂), (F.trans G).symm = G.symm.trans F.symm
-- Lean.Util.SCC
Lean.SCC.Data.mk : Option ℕ → Option ℕ → Bool → Lean.SCC.Data
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- Curried `C^n` functions are `C^n` in the first coordinate.  -/
ContMDiffWithinAt.curry_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {y : M'} {s : Set (M × M')},
  ContMDiffWithinAt (I.prod I') J n (Function.uncurry f) s (x, y) →
    ContMDiffWithinAt I J n (fun x => f x y) {x | (x, y) ∈ s} x
-- Init.Data.Int.Order
Int.sign_nonpos_iff : ∀ {x : ℤ}, x.sign ≤ 0 ↔ x ≤ 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
cot_series_rep' : ∀ {x : ℂ},
  x ∈ Complex.integerComplement →
    ↑Real.pi * (↑Real.pi * x).cot - 1 / x = ∑' (n : ℕ), (1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1)))
-- Init.Data.List.ToArray
List.idxOf?_toArray : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l : List α), l.toArray.idxOf? a = List.idxOf? a l
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
ContDiffOn.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : ℕ∞},
  ContDiffOn ℝ (↑n) f s → ContDiffOn ℝ (↑n) (fun x => Real.arctan (f x)) s
-- Std.Http.Data.URI.Basic
Std.Http.URI.Port.value.inj : ∀ {port port_1 : UInt16}, Std.Http.URI.Port.value port = Std.Http.URI.Port.value port_1 → port = port_1
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
IsStrongFEPair.hg₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → P.g₀ = 0
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.neg_mem_range_root_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {x : M},
  -x ∈ Set.range ⇑P.root ↔ x ∈ Set.range ⇑P.root
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.ProjectivePresentation.epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (self : CategoryTheory.ProjectivePresentation X),
  CategoryTheory.Epi self.f
-- Mathlib.Tactic.NormNum.Result
/-- A "raw rat cast" is an expression of the form:

* `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
* `(Int.rawCast (Int.negOfNat lit) : α)` where `lit` is a nonzero raw natural number literal
* `(NNRat.rawCast n d : α)` where `n` is a raw nat literal, `d` is a raw nat literal, and `d` is not
  `1` or `0`.
* `(Rat.rawCast (Int.negOfNat n) d : α)` where `n` is a raw nat literal,
  `d` is a raw nat literal, `n` is not `0`, and `d` is not `1` or `0`.

This representation is used by tactics like `ring` to decrease the number of typeclass arguments
required in each use of a number literal at type `α`.
 -/
Rat.rawCast : {α : Type u} → [DivisionRing α] → ℤ → ℕ → α
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.ne_bot_iff_exists_adj : ∀ {V : Type u} {G : SimpleGraph V}, G ≠ ⊥ ↔ ∃ a b, G.Adj a b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, (Std.DTreeMap.Internal.Impl.alter! k f t).get? k = f (t.get? k)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.natCast_lt_epsilon : ∀ (n : ℕ) (o : Ordinal.{u_1}), ↑n < o.epsilon
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.coe_inf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (S T : NonUnitalStarSubalgebra R A), ↑(S ⊓ T) = ↑S ∩ ↑T
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE : ∀ (p : ℤ), (ComplexShape.embeddingUpIntGE p).IsRelIff
-- Init.Data.List.Control
/-- Applies a monadic function that returns an `Option` to each element of a list, collecting the
non-`none` values.

`O(|l|)`.

Example:
```lean example
#eval [1, 2, 5, 2, 7, 7].filterMapM fun x => do
  IO.println s!"Examining {x}"
  if x > 2 then return some (2 * x)
  else return none
```
```output
Examining 1
Examining 2
Examining 5
Examining 2
Examining 7
Examining 7
```
```output
[10, 14, 14]
```
 -/
List.filterMapM : {m : Type u → Type v} → [Monad m] → {α : Type w} → {β : Type u} → (α → m (Option β)) → List α → m (List β)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The limit of `F` represents the functor taking `W` to
the set of cones on `F` with cone point `W`.  -/
CategoryTheory.Limits.IsLimit.natIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit t →
              ((CategoryTheory.yoneda.obj t.pt).comp CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cones)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry?.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1 with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2 =>
      h_3 size k v l size_2 k_2 v_2 l_1 r h r_2) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limitEquivSections_symm_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasLimit F] (x : ↑F.sections) (j : J),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j))
      ((CategoryTheory.Limits.Types.limitEquivSections F).symm x) =
    ↑x j
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.coe_negOrderIso_apply : ∀ {G : Type u_2} [inst : AddGroup G] (a : AddSubmonoid G), ↑(AddSubmonoid.negOrderIso a) = -↑a
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_fst_prod : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, f' =O[l] fun x => (f' x, g' x)
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.cancel_factors_eq_div : ∀ {α : Type u_1} [inst : Field α] {n e e' : α}, n * e = e' → n ≠ 0 → e = e' / n
-- Mathlib.RingTheory.DedekindDomain.Different
/-- Under the AKLB setting, `Iᵛ := traceDual A K (I : Submodule B L)` is the
`Submodule B L` such that `x ∈ Iᵛ ↔ ∀ y ∈ I, Tr(x, y) ∈ A`  -/
Submodule.traceDual : (A : Type u_1) →
  (K : Type u_2) →
    {L : Type u} →
      {B : Type u_3} →
        [inst : CommRing A] →
          [inst_1 : Field K] →
            [inst_2 : CommRing B] →
              [inst_3 : Field L] →
                [inst_4 : Algebra A K] →
                  [inst_5 : Algebra B L] →
                    [inst_6 : Algebra A B] →
                      [inst_7 : Algebra K L] →
                        [inst_8 : Algebra A L] →
                          [IsScalarTower A K L] → [IsScalarTower A B L] → Submodule B L → Submodule B L
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (w : ℕ) (input : aig.RefVec w)
  (newWidth curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s =
    if hcurr1 : curr < newWidth then
      if hcurr2 : curr < w then
        have s := s.push (input.get curr hcurr2);
        Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth (curr + 1) ⋯ s
      else
        have zeroRef := aig.mkConstCached false;
        have s := s.push zeroRef;
        Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth (curr + 1) ⋯ s
    else
      have hcurr := ⋯;
      { aig := aig, vec := hcurr ▸ s }
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_sdiff_self : ∀ {α : Type u_1} (t s s' : Set α), t.ite s s' \ t = s' \ t
-- Mathlib.Tactic.CrossRefAttribute
/-- `#stacks_tags` retrieves all declarations that have the `stacks` attribute.

For each found declaration, it prints a line
```
'declaration_name' corresponds to tag 'declaration_tag'.
```
The variant `#stacks_tags!` also adds the theorem statement (for theorems)
or declaration type (for definitions, structures, instances, etc.) after each summary line.
 -/
Mathlib.CrossRef.stacksTags : Lean.ParserDescr
-- Lean.Util.MonadCache
Lean.MonadCacheT : {ω : Type} → (α : Type) → Type → (m : Type → Type) → [STWorld ω m] → [BEq α] → [Hashable α] → Type → Type