mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.SeparableDegree
IntermediateField.finSepDegree_top : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Field.finSepDegree F ↥⊤ = Field.finSepDegree F K
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- The type of simplices of `X : SSet.{u}` identifies to the type
of elements of `X` considered as a functor `SimplexCategoryᵒᵖ ⥤ Type u`.
(Note that this is not an (anti)equivalence of categories,
see `S.le_iff_nonempty_hom`.)  -/
SSet.S.equivElements : {X : SSet} → X.S ≃ CategoryTheory.Functor.Elements X
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Poly.denoteN.match_1.splitter : (motive : Lean.Grind.Linarith.Poly → Sort u_1) →
  (p : Lean.Grind.Linarith.Poly) →
    (Unit → motive Lean.Grind.Linarith.Poly.nil) →
      ((k : ℤ) →
          (v : Lean.Grind.Linarith.Var) →
            (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)) →
        motive p
-- Init.Data.SInt.Lemmas
ISize.ofIntTruncate_bitVecToInt : ∀ (n : BitVec System.Platform.numBits), ISize.ofIntClamp n.toInt = ISize.ofBitVec n
-- Init.Data.SInt.Lemmas
Int64.sub_left_inj : ∀ {a b : Int64} (c : Int64), a - c = b - c ↔ a = b
-- Mathlib.Order.Fin.Tuple
strictMono_vecCons : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α},
  StrictMono (Matrix.vecCons a f) ↔ a < f 0 ∧ StrictMono f
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.norm_setToL1_le : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  0 ≤ C → ‖MeasureTheory.L1.setToL1 hT‖ ≤ C
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p n : ℕ} [inst_2 : ExpChar R p] {f : Polynomial R}
  [inst_3 : PerfectRing R p],
  ((Polynomial.expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.map_spanIntNorm : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] (I : Ideal S) {T : Type u_4} [inst_9 : Semiring T] (f : R →+* T),
  Ideal.map f (Ideal.spanNorm R I) = Ideal.span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RcoSliceData.mk : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      (Std.DTreeMap.Internal.Impl α fun x => β) → Std.Rco α → Std.DTreeMap.Internal.Const.RcoSliceData α β
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.edist_toSnowflaking_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : EDist X] (x y : X),
  edist (Metric.Snowflaking.toSnowflaking x) (Metric.Snowflaking.toSnowflaking y) = edist x y ^ α
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.Value.n : Fin.Value✝ → ℕ
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.bitwise.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
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_zero_right : ∀ {x : NNReal}, x.agm 0 = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
HomotopyCategory.instCommShiftIntUpMapHomotopyCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.Additive] → (F.mapHomotopyCategory (ComplexShape.up ℤ)).CommShift ℤ
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.differentiableAt_rpow_const_of_ne : ∀ (p : ℝ) {x : ℝ}, x ≠ 0 → DifferentiableAt ℝ (fun x => x ^ p) x
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The iteration on a limit element identifies to the colimit of the
value on smaller elements, see `Iteration.isColimit`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.arrowMap_limit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J} (self : Φ.Iteration j)
  (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
  CategoryTheory.SmallObject.SuccStruct.arrowMap self.F k i ⋯ hij =
    CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT self.F hij) hi k hk
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldr_eq_foldr_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w}
  {f : (a : α) → β a → δ → δ} {init : δ},
  Std.DTreeMap.foldr f init t = Array.foldr (fun a b => f a.fst a.snd b) init t.toArray
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.nnnorm_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A] (a : A), ‖↑a‖₊ = ‖a‖₊
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- To prove a property on morphisms of a path category, it suffices to prove it for the identity
and prove that the property is preserved under composition on the left with length 1 paths.  -/
CategoryTheory.Paths.induction' : ∀ {V : Type u₁} [inst : Quiver V] (P : {a b : CategoryTheory.Paths V} → (a ⟶ b) → Prop),
  (∀ {v : V}, P (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of V).obj v))) →
    (∀ {u v w : V} (p : u ⟶ v) (q : (CategoryTheory.Paths.of V).obj v ⟶ (CategoryTheory.Paths.of V).obj w),
        P q → P (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of V).map p) q)) →
      ∀ {a b : CategoryTheory.Paths V} (f : a ⟶ b), P f
-- Lean.Parser.Syntax
Lean.Parser.Syntax.atom.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.FP.Basic
FP.Float.inf.sizeOf_spec : ∀ [C : FP.FloatCfg] (a : Bool), sizeOf (FP.Float.inf a) = 1 + sizeOf a
-- Mathlib.Topology.LocallyFinsupp
/-- A proof that the support of `toFun` is contained in `U`  -/
Function.locallyFinsuppWithin.supportWithinDomain' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y]
  (self : Function.locallyFinsuppWithin U Y), Function.support self.toFun ⊆ U
-- Mathlib.Order.Minimal
Maximal.not_prop_of_ssuperset : ∀ {α : Type u_2} {P : Set α → Prop} {s t : Set α}, Maximal P s → s ⊂ t → ¬P t
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.principalUnitGroup_injective : ∀ {K : Type u} [inst : Field K], Function.Injective ValuationSubring.principalUnitGroup
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_sdiff_Ioo_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b < a → Set.Ioc b a \ Set.Ioo b a = {a}
-- Init.Data.Int.Basic
Int.negSucc.inj : ∀ {a a_1 : ℕ}, Int.negSucc a = Int.negSucc a_1 → a = a_1
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.ne_zero_of_surjective : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} [Nontrivial M₂] {f : M →ₛₗ[σ₁₂] M₂}, Function.Surjective ⇑f → f ≠ 0
-- Mathlib.Order.MinMax
min_le_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, min b c ≤ a ↔ b ≤ a ∨ c ≤ a
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_inj : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {A : Matrix n l α} {B : Matrix n m α}
  {C : Matrix o l α} {D : Matrix o m α} {A' : Matrix n l α} {B' : Matrix n m α} {C' : Matrix o l α} {D' : Matrix o m α},
  Matrix.fromBlocks A B C D = Matrix.fromBlocks A' B' C' D' ↔ A = A' ∧ B = B' ∧ C = C' ∧ D = D'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.leftUnitor_inv_left_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : A),
  φ.leftUnitor.inv.left.app X = CategoryTheory.CategoryStruct.id (φ.left.obj X)
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.instGeometricallyIrreducibleSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyIrreducible f],
  AlgebraicGeometry.GeometricallyIrreducible (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Data.Multiset.Defs
Multiset.mem_coe : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ ↑l ↔ a ∈ l
-- Mathlib.Data.Fin.Tuple.Basic
/-- A `HEq` version of `Fin.removeNth_removeNth_eq_swap`.  -/
Fin.removeNth_removeNth_heq_swap : ∀ {n : ℕ} {α : Fin (n + 2) → Sort u_3} (m : (i : Fin (n + 2)) → α i) (i : Fin (n + 1)) (j : Fin (n + 2)),
  i.removeNth (j.removeNth m) ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m)
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R), (Polynomial.taylor r) f = 0 ↔ f = 0
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.hasPullback_of_pullbackCone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2))
  (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)), CategoryTheory.Limits.HasPullback f g
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_forget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) [CategoryTheory.Presheaf.IsLocallyInjective J φ],
  CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget D))
-- Mathlib.Data.Multiset.Filter
Multiset.countP_map : ∀ {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) (p : β → Prop) [inst : DecidablePred p],
  Multiset.countP p (Multiset.map f s) = (Multiset.filter (fun a => p (f a)) s).card
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.whiskerLeft_iso_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b)
  (x_1 x_2 : b ⟶ c) (f : x_1 ⟶ x_2),
  (CategoryTheory.Bicategory.whiskerLeft x f).iso.hom = CategoryTheory.Bicategory.whiskerLeft x.of f.iso.hom
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_div_two : ∀ {a b : ℕ}, (a &&& b) / 2 = a / 2 &&& b / 2
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.revMatchesAt_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat (pos.cast hst) ↔ String.Slice.Pattern.Model.RevMatchesAt pat pos
-- Mathlib.Data.UInt
/-- To use this instance, use `open scoped UInt32.CommRing`.

See the module docstring for an explanation -/
UInt32.instCommRing : CommRing UInt32
-- Mathlib.Algebra.Opposites
AddOpposite.unop_one : ∀ {α : Type u_1} [inst : One α], AddOpposite.unop 1 = 1
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_ringHom_injective : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  Function.Injective RingHomClass.toRingHom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl = true
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.ι_map_πQ_assoc : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {ι : CategoryTheory.Functor A C} {X₂ : A} {X₃ : C}
  (f₂ : ι.obj X₂ ⟶ X₃) {Q : A} (β : X₃ ⟶ ι.obj Q) [inst_2 : ι.Full] {Z : C} (h : ι.obj Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ι.map (CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β)) h =
    CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.CategoryStruct.comp β h)
-- Mathlib.Data.PNat.Prime
PNat.lcm_dvd : ∀ {m n k : ℕ+}, m ∣ k → n ∣ k → m.lcm n ∣ k
-- Mathlib.Topology.Basic
isClosed_imp : ∀ {X : Type u} [inst : TopologicalSpace X] {p q : X → Prop},
  IsOpen {x | p x} → IsClosed {x | q x} → IsClosed {x | p x → q x}
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_some_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {a : α}, a ∈ m → m.get? a = some (m.get! a)
-- Lean.Meta.Basic
/-- Returns `true` if another local declaration in the local context depends on `fvarId`.
 -/
Lean.FVarId.hasForwardDeps : Lean.FVarId → Lean.MetaM Bool
-- Mathlib.Order.WithBot
WithTop.instPartialOrder.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α],
  WithTop.instPartialOrder = { toPreorder := WithTop.instPreorder, le_antisymm := ⋯ }
-- Init.Data.Array.Perm
Array.Perm.of_toList_perm : ∀ {α : Type u_1} {as bs : Array α}, as.toList.Perm bs.toList → as.Perm bs
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_sub_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a - x) '' Set.Iio b = Set.Ioi (a - b)
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_False : Set.Iic False = {False}
-- Mathlib.Topology.NhdsWithin
IsClosed.mem_of_nhdsWithin_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, IsClosed s → ∀ {x : α}, (nhdsWithin x s).NeBot → x ∈ s
-- Mathlib.Order.CompleteLattice.Group
iSup₂_add_le : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] [inst_1 : Add α] [AddLeftMono α]
  [AddRightMono α] (u v : (i : ι) → κ i → α), ⨆ i, ⨆ j, u i j + v i j ≤ (⨆ i, ⨆ j, u i j) + ⨆ i, ⨆ j, v i j
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α},
  Std.DTreeMap.Const.get? (Std.DTreeMap.map f t) k = Option.map (f k) (Std.DTreeMap.Const.get? t k)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ D` creates
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.createsLimitOfOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.CreatesColimit K.op F.op] → CategoryTheory.CreatesLimit K F
-- Mathlib.Topology.VectorBundle.Riemannian
/-- In a continuous Riemannian bundle, local changes of coordinates given by the trivialization at
a point distort the norm by a factor arbitrarily close to 1.  -/
eventually_norm_symmL_trivializationAt_self_comp_lt : ∀ {B : Type u_1} [inst : TopologicalSpace B] (F : Type u_2) [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  (E : B → Type u_3) [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E]
  [h : IsContinuousRiemannianBundle F E] (x : B) {r : ℝ},
  1 < r →
    ∀ᶠ (y : B) in nhds x,
      ‖Bundle.Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
            Bundle.Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
        r
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Iso.map_inv_hom_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y)
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D),
  CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) ((F.map e.hom).app Z) =
    CategoryTheory.CategoryStruct.id ((F.obj Y).obj Z)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.Trace.hasToJson : Lean.ToJson Lean.Lsp.Trace
-- Mathlib.Order.Category.BddLat
BddLat.ext_iff : ∀ {X Y : BddLat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X.toLat), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.isBasis_iff_forall_insert_dep : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.Indep I → I ⊆ X → (M.IsBasis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I))
-- Mathlib.Algebra.Free
FreeMagma.mul_eq : ∀ {α : Type u} (x y : FreeMagma α), x.mul y = x * y
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod.etaIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C × D),
  (CategoryTheory.prod.etaIso X).inv =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
-- Mathlib.CategoryTheory.Generator.Basic
/-- Given a category `C` that has a codetector (`HasCodetector C`), `codetector C` is an arbitrarily
chosen codetector of `C`.
 -/
CategoryTheory.codetector : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.HasCodetector C] → C
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_homothetyAffine : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1), ⇑(AffineMap.homothetyAffine c) = AffineMap.homothety c
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.BuiltinSimprocs.mk.sizeOf_spec : ∀ (keys : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey))
  (procs : Std.HashMap Lean.Name (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)),
  sizeOf { keys := keys, procs := procs } = 1 + sizeOf keys + sizeOf procs
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- If `f` belongs to `Lp` for the measure `μ.trim hm`, then it belongs to the subgroup
`lpMeasSubgroup F m p μ`.  -/
MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp F p (μ.trim hm))),
  MeasureTheory.MemLp.toLp ↑↑f ⋯ ∈ MeasureTheory.lpMeasSubgroup F m p μ
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cocone.ofCofork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (t :
    CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
      (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
  (j : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.Cocone.ofCofork t).ι.app j =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
-- Mathlib.Algebra.Algebra.Basic
Module.End.algebraMap_isUnit_inv_apply_eq_iff : ∀ {R : Type u} (S : Type v) {M : Type w} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass S R M] [inst_6 : SMul R S]
  [inst_7 : IsScalarTower R S M] {x : R} (h : IsUnit ((algebraMap R (Module.End S M)) x)) (m m' : M),
  ↑h.unit⁻¹ m = m' ↔ m = x • m'
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- Basic hypothesis to talk about a `C^n` (Lie) additive monoid or a `C^n` additive
semigroup. A `C^n` additive monoid over `G`, for example, is obtained by requiring both the
instances `AddMonoid G` and `ContMDiffAdd I n G`.

See also `ContMDiffVAdd I I' n G M` for `C^n` actions of `G` on a manifold `M`.  -/
ContMDiffAdd : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                WithTop ℕ∞ → (G : Type u_4) → [Add G] → [inst : TopologicalSpace G] → [ChartedSpace H G] → Prop
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.instSemigroup : {𝕜 : Type u_1} → [inst : NonUnitalSeminormedRing 𝕜] → Semigroup ↑(Metric.closedBall 0 1)
-- Mathlib.Algebra.Star.Basic
/-- `star` as a ring endomorphism, for commutative `R`. This is used to denote complex
conjugation, and is available under the notation `conj` in the scope `ComplexConjugate`.

Note that this is the preferred form (over `starRingAut`, available under the same hypotheses)
because the notation `E →ₗ⋆[R] F` for an `R`-conjugate-linear map (short for
`E →ₛₗ[starRingEnd R] F`) does not pretty-print if there is a coercion involved, as would be the
case for `(↑starRingAut : R →* R)`.  -/
ComplexConjugate.termConj : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.eq_sum_range_sub' : ∀ {G : Type u_3} [inst : AddCommGroup G] (f : ℕ → G) (n : ℕ),
  f n = ∑ i ∈ Finset.range (n + 1), if i = 0 then f 0 else f i - f (i - 1)
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasFDerivAt_exp_smul_const_of_mem_ball : ∀ (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [inst : NontriviallyNormedField 𝕂] [CharZero 𝕂]
  [inst_2 : NormedCommRing 𝕊] [inst_3 : NormedRing 𝔸] [inst_4 : NormedSpace 𝕂 𝕊] [inst_5 : NormedAlgebra 𝕂 𝔸]
  [inst_6 : Algebra 𝕊 𝔸] [inst_7 : ContinuousSMul 𝕊 𝔸] [inst_8 : IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊),
  t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    HasFDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) • ContinuousLinearMap.smulRight 1 x) t