mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.whiskerLeft_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) {N₁ N₂ : Bimod Y Z} (f : N₁ ⟶ N₂),
  (M.whiskerLeft f).hom =
    CategoryTheory.Limits.colimMap
      (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.actRight N₁.X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X Y.X N₁.X).hom
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X N₁.actLeft))
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.actRight N₂.X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X Y.X N₂.X).hom
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X N₂.actLeft))
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X Y.X)
          f.hom)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X f.hom) ⋯ ⋯)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- **Alias** of `Algebra.TensorProduct.commRight_symm_tmul`. -/
Algebra.TensorProduct.Algebra.TensorProduct.commRight_symm_tmul : ∀ (R : Type uR) {S : Type uS} {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (s : S) (a : A),
  (Algebra.TensorProduct.commRight R S A).symm (a ⊗ₜ[R] s) = s ⊗ₜ[R] a
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instHasZeroMorphisms.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrp.instHasZeroMorphisms =
    { zero := CategoryTheory.AddGrp.instZeroHom, comp_zero := ⋯, zero_comp := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.dite_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (P : Prop) [inst : Decidable P] (A : P → Matrix m n α)
  (B : ¬P → Matrix m n α) (i : m) (j : n), dite P A B i j = if x : P then A x i j else B x i j
-- Mathlib.Data.Set.Operations
/-- `f '' s` denotes the image of `s : Set α` under the function `f : α → β`.  -/
Set.term_''_ : Lean.TrailingParserDescr
-- Init.Data.String.Basic
ByteArray.utf8Decode?.go.match_1.congr_eq_2 : ∀ (motive : Option Char → Sort u_1) (x : Option Char) (h_1 : x = none → motive none)
  (h_2 : (c : Char) → x = some c → motive (some c)) (c : Char) (heq_1 : x = some c),
  (match h : x with
    | none => h_1 h
    | some c => h_2 c h) ≍
    h_2 c heq_1
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.det.eq_1 : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R],
  Matrix.GeneralLinearGroup.det =
    { toFun := fun A => { val := (↑A).det, inv := (↑A⁻¹).det, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯,
      map_mul' := ⋯ }
-- Std.Http.Data.Status
/-- 201 Created
 -/
Std.Http.Status.created : Std.Http.Status
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.reflection_map : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {V₂ : Type u_4} {P₂ : Type u_5} [inst_3 : NormedAddCommGroup V₂]
  [inst_4 : InnerProductSpace 𝕜 V₂] [inst_5 : MetricSpace P] [inst_6 : NormedAddTorsor V P] [inst_7 : MetricSpace P₂]
  [inst_8 : NormedAddTorsor V₂ P₂] (s : AffineSubspace 𝕜 P) [inst_9 : Nonempty ↥s]
  [inst_10 : s.direction.HasOrthogonalProjection] (f : P →ᵃⁱ[𝕜] P₂)
  [inst_11 : (AffineSubspace.map f.toAffineMap s).direction.HasOrthogonalProjection] (p : P),
  (EuclideanGeometry.reflection (AffineSubspace.map f.toAffineMap s)) (f p) = f ((EuclideanGeometry.reflection s) p)
-- Lean.Parser.Command
/-- `unlock_limits` disables all built-in resource limit options (currently `maxRecDepth`,
`maxHeartbeats`, and `synthInstance.maxHeartbeats`) in the current scope by setting them to 0.
 -/
Lean.Parser.Command.unlock_limits : Lean.Parser.Parser
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.continuous_cosh : Continuous Real.cosh
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Pair.mk.congr_simp : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι}
  (toPair toPair_1 : Monoid.CoprodI.Word.Pair G i) (e_toPair : toPair = toPair_1)
  (normalized : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ toPair.tail.toList → g ∈ d.set i_1),
  { toPair := toPair, normalized := normalized } = { toPair := toPair_1, normalized := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.instHashablePoly_lean.hash : Int.Internal.Linear.Poly → UInt64
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {f : α → Bool} {k : α}, (Std.ExtTreeSet.filter f t).get! k = (Option.filter f (t.get? k)).get!
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map_bot : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), WithOne.map f 1 = 1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.curriedTensor_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X).obj Y = CategoryTheory.MonoidalCategoryStruct.tensorObj X Y
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.LiesOver.mk_embedding_comp : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [w.LiesOver v],
  NumberField.InfinitePlace.mk (w.embedding.comp (algebraMap K L)) = v
-- Lean.Elab.Tactic.ElabTerm
_private.Lean.Elab.Tactic.ElabTerm.0.Lean.Elab.Tactic.runTermElab.go : {α : Type} → Lean.Elab.TermElabM α → Bool → Lean.Elab.TermElabM α
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Debug `grind` by identifying places where it does not yet supersede `ring`.  -/
linter.tacticAnalysis.regressions.ringToGrind : Lean.Option Bool
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.instAddMonoidPoint : {R : Type u_1} → [inst : CommRing R] → {σ : Type u_3} → (F : FormalGroup R) → AddMonoid (F.Point σ)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_def : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A)
  (p : Polynomial R), (Polynomial.aeval x) p = Polynomial.eval₂ (algebraMap R A) x p
-- Mathlib.Algebra.Group.Shrink
Shrink.instMul : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Mul α] → Mul (Shrink.{v, u_2} α)
-- Mathlib.Data.List.Map2
List.zipRight_cons_cons : ∀ {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β),
  (a :: as).zipRight (b :: bs) = (some a, b) :: as.zipRight bs
-- Init.Data.Rat.Lemmas
Rat.neg_le_iff : ∀ {a b : ℚ}, -a ≤ b ↔ -b ≤ a
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.pow_eq_one_iff_dvd : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → ∀ (l : ℕ), ζ ^ l = 1 ↔ k ∣ l
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.inaccessible.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Meta.Match.Pattern.inaccessible e) = 1 + sizeOf e
-- Mathlib.Data.Finsupp.Defs
Finsupp.mem_support_onFinset : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Finset α} {f : α → M} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) {a : α},
  a ∈ (Finsupp.onFinset s f hf).support ↔ f a ≠ 0
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.toNNReal_prod : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → ENNReal), (∏ i ∈ s, f i).toNNReal = ∏ i ∈ s, (f i).toNNReal
-- Init.Data.Nat.Gcd
Nat.gcd_eq_right : ∀ {m n : ℕ}, n ∣ m → m.gcd n = n
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α),
  ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).unitIso.hom.app P).f.f n = P.p.f n
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.builder_nameUnfold : Lean.ParserDescr
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.prod_surjective : ∀ {α : Type u} [inst : Group α], Function.Surjective ⇑FreeGroup.prod
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_one_iff : ∀ {V : Type u} {G : SimpleGraph V}, G.Colorable 1 ↔ G = ⊥
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.zsmul_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : AddGroup γ] [inst_4 : IsTopologicalAddGroup γ] (f : C(β, γ)) (z : ℤ)
  (g : C(α, β)), (z • f).comp g = z • f.comp g
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.sum_pow_add_indicator_eq_zero : ∀ {p : ℕ} (l : ℕ) [inst : Fact (Nat.Prime p)], (∑ v ∈ Finset.Ico 1 p, ↑v ^ l + if p - 1 ∣ l then 1 else 0) = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The image under a `MonoidHom` of the `Submonoid` generated by a set equals the `Submonoid`
generated by the image of the set.  -/
MonoidHom.map_mclosure : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) (s : Set M), Submonoid.map f (Submonoid.closure s) = Submonoid.closure (⇑f '' s)
-- Std.Http.Data.Chunk
Std.Http.Chunk.instHashableExtensionName : Hashable Std.Http.Chunk.ExtensionName
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.ofNonUnitalRingHom_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (hom : R →ₙ+* S) (inv : S →ₙ+* R) (hom_inv_id : inv.comp hom = NonUnitalRingHom.id R)
  (inv_hom_id : hom.comp inv = NonUnitalRingHom.id S) (a : R),
  (RingEquiv.ofNonUnitalRingHom hom inv hom_inv_id inv_hom_id) a = hom a
-- Init.Data.Nat.Lemmas
Nat.succ_ne_succ : ∀ {m n : ℕ}, m.succ ≠ n.succ ↔ m ≠ n
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- The underlying `Matroid`  -/
Matroid.Matroidᵣ.toMatroid : {α : Type u_2} → Matroid.Matroidᵣ α → Matroid α
-- Mathlib.Order.WithBot
WithBot.map₂.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3}, WithBot.map₂ = Option.map₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_union_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {fallback : β},
  Std.DTreeMap.Internal.Impl.contains k m₁ = false →
    Std.DTreeMap.Internal.Impl.Const.getD (m₁.union m₂ ⋯ ⋯) k fallback =
      Std.DTreeMap.Internal.Impl.Const.getD m₂ k fallback
-- Mathlib.Data.Complex.Basic
Complex.conj_inv : ∀ (x : ℂ), (starRingEnd ℂ) x⁻¹ = ((starRingEnd ℂ) x)⁻¹
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.associated_of_ordFrac_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (x y : K),
  (Ring.ordFrac R) x = (Ring.ordFrac R) y → ∃ u, u • x = y
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimit.ι_desc_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (H : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimit H]
  (c : CategoryTheory.Limits.Cocone H) (j : J) (k : K) {Z : C} (h : c.pt.obj k ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι H j).app k)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.desc H c).app k) h) =
    CategoryTheory.CategoryStruct.comp ((c.ι.app j).app k) h
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.continuous_circleTransform : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ},
  0 < R →
    ∀ {f : ℂ → E} {z w : ℂ},
      ContinuousOn f (Metric.sphere z R) → w ∈ Metric.ball z R → Continuous (Complex.circleTransform R z w f)
-- Mathlib.Data.Nat.Cast.Order.Ring
Nat.abs_cast : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : Lattice R] [IsOrderedRing R] (n : ℕ), |↑n| = ↑n
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_natCast : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (n : ℕ), ⇑↑n = n • ⇑(CentroidHom.id α)
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Multiplication by a nonzero element is right cancellative.  -/
IsRightCancelMulZero.mul_right_cancel_of_ne_zero : ∀ {M₀ : Type u} {inst : Mul M₀} {inst_1 : Zero M₀} [self : IsRightCancelMulZero M₀] {a : M₀}, a ≠ 0 → IsRightRegular a
-- Lean.Meta.Match.Match
Lean.Meta.Match.backward.match.rowMajor : Lean.Option Bool
-- Init.Data.List.Lemmas
List.decide_mem_cons : ∀ {α : Type u_1} {a y : α} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List α},
  decide (y ∈ a :: l) = (y == a || decide (y ∈ l))
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
_private.Mathlib.Topology.ContinuousMap.ZeroAtInfty.0.ZeroAtInftyContinuousMap.«term_→co_» : Lean.TrailingParserDescr
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_subset_Ioo_union_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a c ⊆ Set.Ioo a b ∪ Set.Icc b c
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- The module filter basis associated to a ring filter basis and a compatible submodule basis.
This allows to build a topological module structure compatible with the given module structure
and the topology associated to the given ring filter basis.  -/
RingFilterBasis.moduleFilterBasis : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [Nonempty ι] →
              (BR : RingFilterBasis R) → {B : ι → Submodule R M} → BR.SubmodulesBasis B → ModuleFilterBasis R M
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.naturality_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.δ f.f₃.τ₁ = CategoryTheory.CategoryStruct.comp f.f₀.τ₃ S₂.δ
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftId.eq_1 : ∀ {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] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T),
  CategoryTheory.Comma.mapLeftId L R =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Comma.isoMk
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapLeft R (CategoryTheory.CategoryStruct.id L)).obj X).left)
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapLeft R (CategoryTheory.CategoryStruct.id L)).obj X).right)
          ⋯)
      ⋯
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {K₁ K₁' : HomologicalComplex C₁ c₁} (f : K₁ ⟶ K₁')
  (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ : I₂),
  ((((F.mapBifunctorHomologicalComplex c₁ c₂).map f).app K₂).f i₁).f i₂ = (F.map (f.f i₁)).app (K₂.X i₂)
-- Lean.Expr
Lean.instBEqBinderInfo.beq : Lean.BinderInfo → Lean.BinderInfo → Bool
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorCounitIso : ∀ {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] (E : C ≌ D) (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : E.functor.CommShift A]
  [inst_6 : E.inverse.CommShift A] [E.CommShift A], CategoryTheory.NatTrans.CommShift E.counitIso.hom A
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.comp_injective : ∀ {R : Type v} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type w}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B) [Algebra.FormallyUnramified R A],
  I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.foldrM_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} {δ : Type w}
  {m : Type w → Type w'} [Std.TransOrd α] [inst : Monad m] [LawfulMonad m],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {f : (a : α) → β a → δ → m δ} {init : δ},
          Std.DTreeMap.Internal.Impl.foldrM f init t₁ = Std.DTreeMap.Internal.Impl.foldrM f init t₂
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.limitπAddMonoidHom.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] (j : J),
  AddMonCat.limitπAddMonoidHom F j =
    {
      toFun :=
        ⇑(CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).π.app j)),
      map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_eq_none_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.minKey? = none ↔ t.isEmpty = true)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.CotangentSpace.exact : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  Function.Exact ⇑(LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
    ⇑(Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- Let `M` be a `C^1` manifold with model `I` on `(E, H)`.
Then `tangentBundleCore I M` is the vector bundle core for the tangent bundle over `M`.
It is indexed by the atlas of `M`, with fiber `E` and its change of coordinates from the chart `i`
to the chart `j` at point `x : M` is the derivative of the composite
```
  I.symm   i.symm    j     I
E -----> H -----> M --> H --> E
```
within the set `range I ⊆ E` at `I (i x) : E`.  -/
tangentBundleCore : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (M : Type u_6) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → [IsManifold I 1 M] → VectorBundleCore 𝕜 M E ↑(atlas H M)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.finIdxOf?.eq_1 : ∀ {α : Type u} [inst : BEq α] (xs : Array α) (v : α), xs.finIdxOf? v = xs.idxOfAux v 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Finset.prod_preimage' : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [inst : CommMonoid β] (f : ι → κ)
  [inst_1 : DecidablePred fun x => x ∈ Set.range f] (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β),
  ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s with x ∈ Set.range f, g x
-- Init.Data.Int.DivMod.Lemmas
Int.emod_sub_emod : ∀ (m n k : ℤ), (m % n - k) % n = (m - k) % n
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.instCoeFunForallTypeVecType : {n : ℕ} → CoeFun (MvPFunctor.{u} n) fun x => TypeVec.{u} n → Type u
-- Init.Data.Array.Lemmas
Array.replace_singleton : ∀ {α : Type u_1} [inst : BEq α] {a b c : α}, #[a].replace b c = #[if (a == b) = true then c else a]
-- Mathlib.Analysis.Calculus.Taylor
taylorWithinEval_succ : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ x : ℝ),
  taylorWithinEval f (n + 1) s x₀ x =
    taylorWithinEval f n s x₀ x +
      (((↑n + 1) * ↑n.factorial)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.coe_one : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : One M],
  ↑1 = Set.range fun r => r • 1
-- Mathlib.Topology.Filter
Filter.nhds_principal : ∀ {α : Type u_2} (s : Set α), nhds (Filter.principal s) = Filter.principal (Set.Iic (Filter.principal s))
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.laplacianCLM_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : AddCommGroup F] [inst_4 : Module ℂ F] [inst_5 : TopologicalSpace F]
  [inst_6 : IsTopologicalAddGroup F] [inst_7 : ContinuousConstSMul ℂ F] (f : TemperedDistribution E F),
  (LineDeriv.laplacianCLM ℂ E (TemperedDistribution E F)) f = Laplacian.laplacian f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₂ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.mt : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G},
  UniqueMul A B a0 b0 → ∀ ⦃a b : G⦄, a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a * b ≠ a0 * b0
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
/-- Given a positive linear functional `Λ` on continuous compactly supported functions on `X`
with values in `ℝ≥0`, for `K ⊆ X` compact define `λ(K) = inf {Λf | 1≤f on K}`.
When `X` is a locally compact T2 space, this will be shown to be a
content, and will be shown to agree with the Riesz measure on the compact subsets `K ⊆ X`.  -/
rieszContentAux : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    (CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) → TopologicalSpace.Compacts X → NNReal
-- Mathlib.Data.FunLike.Group
FunLike.coeMulHom_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Mul β]
  [inst_3 : IsMulApply F α β], Function.Injective ⇑(FunLike.coeMulHom F α β)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, 0 < n → (orderOf x = n ↔ x ^ n = 1 ∧ ∀ m < n, 0 < m → x ^ m ≠ 1)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure.below : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {α : Type t} →
        {J : α → Type u'} →
          [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] →
            {motive : (a : C) → P.colimitsClosure J a → Prop} → {a : C} → P.colimitsClosure J a → Prop