mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.TaylorSeries
/-- A function that is complex differentiable on the open ball of radius `r` around `c`
is given by evaluating its Taylor series at `c` on this open ball.  -/
Complex.hasSum_taylorSeries_on_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ℝ⦄,
  DifferentiableOn ℂ f (Metric.ball c r) →
    ∀ ⦃z : ℂ⦄, z ∈ Metric.ball c r → HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
-- Mathlib.Data.UInt
UInt16.instNonUnitalCommRing : NonUnitalCommRing UInt16
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- A variant of `finsuppTensorFinsupp` where the first module is the ground ring.  -/
finsuppTensorFinsuppLid : (R : Type u_1) →
  (N : Type u_4) →
    (ι : Type u_5) →
      (κ : Type u_6) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid N] → [inst_2 : Module R N] → TensorProduct R (ι →₀ R) (κ →₀ N) ≃ₗ[R] ι × κ →₀ N
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- The external product of subcomplexes of simplicial sets.  -/
SSet.Subcomplex.prod : {X Y : SSet} → X.Subcomplex → Y.Subcomplex → (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).Subcomplex
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.Internal.Meta.toStringWithSep.maybeEscape : Bool → String → Bool → String
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coe_lpSubmodule : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)],
  (lpSubmodule 𝕜 E p).toAddSubgroup = lp E p
-- Mathlib.RingTheory.Morita.Matrix
/-- The linear equiv induced by the equality `toModuleCat (toMatrixModCat M) = Eᵢᵢ • Mⁿ`.  -/
fromModuleCatToModuleCatLinearEquivtoModuleCatObj : (R : Type u) →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] →
          (M : Type u_1) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                (i : ι) →
                  ↑(((ModuleCat.toMatrixModCat R ι).comp (MatrixModCat.toModuleCat R i)).obj (ModuleCat.of R M)) ≃ₗ[R]
                    ↥(MatrixModCat.toModuleCatObj R (ι → M) i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.Comon.Hom.mk'.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (f f_1 : M.X ⟶ N.X) (e_f : f = f_1)
  (f_counit : CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit)
  (f_comul :
    CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.comul =
      CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)),
  CategoryTheory.Comon.Hom.mk' f f_counit f_comul = CategoryTheory.Comon.Hom.mk' f_1 ⋯ ⋯
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Around the image of a point in the source, `(extChartAt I x).target` and `range I`
coincide locally.  -/
extChartAt_target_eventuallyEq' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x y : M},
  y ∈ (extChartAt I x).source → (extChartAt I x).target =ᶠ[nhds (↑(extChartAt I x) y)] Set.range ↑I
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.cons_zero_eq_div_of_eq_div : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (e : M) {t t_n t_d : Mathlib.Tactic.FieldSimp.NF M},
  t.eval = t_n.eval / t_d.eval → ((0, e) ::ᵣ t).eval = ((1, e) ::ᵣ t_n).eval / ((1, e) ::ᵣ t_d).eval
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_conj : ∀ (x : ℂ), Complex.cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.cosh x)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.coe_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (K : Subgroup G),
  ↑(Subgroup.map f K) = ⇑f '' ↑K
-- Mathlib.Algebra.Lie.Basis.Basic
/-- Lemma 4.4 from [Geck](Geck2017).  -/
LieAlgebra.Basis.borelLower_le_biSup : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] [IsDomain R]
  [CharZero R], b.borelLower ≤ ⨆ n, ⨆ (_ : n ≠ 0), LieAlgebra.rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.projRestricts_eq_comp : ∀ {I : Type u} (C : Set (I → Bool)) {J K L : I → Prop} [inst : (i : I) → Decidable (J i)]
  [inst_1 : (i : I) → Decidable (K i)] [inst_2 : (i : I) → Decidable (L i)] (hJK : ∀ (i : I), J i → K i)
  (hKL : ∀ (i : I), K i → L i),
  Profinite.NobelingProof.ProjRestricts C hJK ∘ Profinite.NobelingProof.ProjRestricts C hKL =
    Profinite.NobelingProof.ProjRestricts C ⋯
-- Mathlib.RingTheory.DualNumber
DualNumber.instIsPrincipalIdealRing : ∀ {K : Type u_2} [inst : DivisionRing K], IsPrincipalIdealRing (DualNumber K)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.toList_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)},
  (Std.ExtDTreeMap.filterMap f t).toList =
    List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toBitVec = BitVec.ofNat 16 n
-- Lean.Data.Name
_private.Lean.Data.Name.0.Lean.Name.quickCmpImpl : Lean.Name → Lean.Name → Ordering
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_le' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a b : α}, |a|ₘ ≤ b ↔ a ≤ b ∧ a⁻¹ ≤ b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.instFunLikeSubtypeForallVMemSubmoduleCocycles₁ : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → {A : Rep.{u_1, u, u} k G} → FunLike (↥(groupCohomology.cocycles₁ A)) G ↑A
-- Init.Data.String.Iterator
String.mkIterator : String → String.Legacy.Iterator
-- Mathlib.Tactic.NormNum.GCD
/-- Evaluates the `Nat.lcm` function.  -/
Mathlib.Meta.NormNum.evalNatLCM : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- The values of a multiplicative character of order `n` are contained in `ℤ[μ]` when
`μ` is a primitive `n`th root of unity.  -/
MulChar.apply_mem_algebraAdjoin : ∀ {F : Type u_1} [inst : Field F] [Finite F] {R : Type u_2} [inst_2 : CommRing R] [IsDomain R] {χ : MulChar F R}
  {μ : R}, IsPrimitiveRoot μ (orderOf χ) → ∀ (a : F), χ a ∈ ℤ[μ]
-- Init.Data.Iterators.Basic
Std.Iterators.ProductivenessRelation.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        (Rel : Std.IterM m β → Std.IterM m β → Prop) →
          WellFounded Rel →
            (∀ {it it' : Std.IterM m β}, it'.IsPlausibleSkipSuccessorOf it → Rel it' it) →
              Std.Iterators.ProductivenessRelation α m
-- Mathlib.Data.Setoid.Partition
IndexedPartition.proj_some_index : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α),
  hs.proj (hs.some (hs.index x)) = hs.proj x
-- Mathlib.Algebra.Homology.Single
CochainComplex.toSingle₀Equiv.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V),
  C.toSingle₀Equiv X =
    { toFun := fun f => f.f 0, invFun := fun f => HomologicalComplex.mkHomToSingle f ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.norm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : NormedAddCommGroup γ] [OpensMeasurableSpace γ],
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.IdentDistrib (fun x => ‖f x‖) (fun x => ‖g x‖) μ ν
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.ScopedEntries : Type → Type
-- Std.Http.Data.URI.Config
/-- Maximum length of the host `reg-name` component, in bytes.
 -/
Std.Http.URI.Config.maxHostLength : Std.Http.URI.Config → ℕ
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_hom_app : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D] {X Y : CategoryTheory.Functor W.Localization D} (f : X ⟶ Y) (X_1 : C),
  ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).map f).hom.app X_1 =
    f.app (W.Q.obj X_1)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The adjunction given by an equivalence of categories. (To obtain the opposite adjunction,
simply use `e.symm.toAdjunction`.)  -/
CategoryTheory.Equivalence.toAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (e : C ≌ D) → e.functor ⊣ e.inverse
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.mk.injEq : ∀ {R : Type u_3} [inst : CommSemiring R] {A : Type u_4} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_5} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (toAlgHom : A →ₐ[R] B) (cont : autoParam (Continuous (↑↑toAlgHom.toRingHom).toFun) ContinuousAlgHom.cont._autoParam)
  (toAlgHom_1 : A →ₐ[R] B)
  (cont_1 : autoParam (Continuous (↑↑toAlgHom_1.toRingHom).toFun) ContinuousAlgHom.cont._autoParam),
  ({ toAlgHom := toAlgHom, cont := cont } = { toAlgHom := toAlgHom_1, cont := cont_1 }) = (toAlgHom = toAlgHom_1)
-- Mathlib.Order.MinMax
/-- **Alias** of `max_left_comm`. -/
Max.left_comm : ∀ {α : Type u_1} [inst : LinearOrder α] (a b c : α), max a (max b c) = max b (max a c)
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one : ∀ {n : ℕ} [inst : NeZero n] (K : Type u) {L : Type v} [inst_1 : Field K] [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n),
  (IsPrimitiveRoot.powerBasis K hζ).gen ∈ K[ζ - 1]
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.preSEval : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.instHasProjectiveDimensionLTHAddNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ)
  [CategoryTheory.HasProjectiveDimensionLT X n] (k : ℕ), CategoryTheory.HasProjectiveDimensionLT X (n + k)
-- Init.Data.List.Lemmas
List.exists_of_mem_flatten : ∀ {α : Type u_1} {L : List (List α)} {a : α}, a ∈ L.flatten → ∃ l ∈ L, a ∈ l
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.graphEquiv₂_apply : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] (f : Fin n → α) (i : Fin n),
  (Tuple.graphEquiv₂ f) i = (Tuple.graphEquiv₁ f) ((Tuple.sort f) i)
-- Mathlib.Data.List.Basic
List.length_injective_iff : ∀ {α : Type u}, Function.Injective List.length ↔ Subsingleton α
-- Mathlib.Algebra.Order.Kleene
IdemCommSemiring.add_eq_sup : ∀ {α : Type u_5} [self : IdemCommSemiring α] (a b : α), a + b = a ⊔ b
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_iCycles_pOpcycles_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  S.Exact ↔ CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles = 0
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso'_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C}
  (t : CategoryTheory.Limits.IsTerminal T),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' X i t).hom.left =
    CategoryTheory.CategoryStruct.comp
      (⋯.desc
        (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom I)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (i.to T)))
        (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom I)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (i.to T)))
        ⋯)
      (CategoryTheory.CategoryStruct.comp ⋯.isoPushout.inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left
            (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T))
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).hom))
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.Ioc_eq_empty_iff`. -/
Finset.Ioc_eq_empty : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], ¬a < b → Finset.Ioc a b = ∅
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.map_id : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  exteriorPower.map n LinearMap.id = LinearMap.id
-- Mathlib.Topology.Algebra.Order.Archimedean
Subgroup.dense_iff_ne_zpowers : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] {s : Subgroup G},
  Dense ↑s ↔ ∀ (a : G), s ≠ Subgroup.zpowers a
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Every map of arrows is right homotopic to itself.  -/
CategoryTheory.Arrow.RightHomotopy.refl : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} → (f : u ⟶ v) → CategoryTheory.Arrow.RightHomotopy f f
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_refl_of_refl_on : ∀ {α : Type u_1} {m : Multiset α} {r : α → α → Prop}, (∀ x ∈ m, r x x) → Multiset.Rel r m m
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.below.trans : ∀ {F : Type u → Type v} [q : QPF F] {motive : (a a_1 : (QPF.P F).W) → QPF.Wequiv a a_1 → Prop} (u v w : (QPF.P F).W)
  (a : QPF.Wequiv u v) (a_1 : QPF.Wequiv v w),
  QPF.Wequiv.below a → motive u v a → QPF.Wequiv.below a_1 → motive v w a_1 → QPF.Wequiv.below ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.mopAlgEquivOp_apply_coe : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (a : (↥S.toSubsemiring)ᵐᵒᵖ), ↑(S.mopAlgEquivOp a) = MulOpposite.op ↑(MulOpposite.unop a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insertIfNew k v).contains k = true
-- Init.Data.Nat.Lemmas
Nat.mod_two_eq_zero_or_one : ∀ (n : ℕ), n % 2 = 0 ∨ n % 2 = 1
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.apply_dualBasis_left : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate)
  (b : Module.Basis ι K V) (i j : ι), (B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [toHasLimitsOfShape : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) C],
  (∀ S ∈ J (⊤_ C), S = ⊤) → J.IsLocalSite
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.linearIndepOn : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (s : Set ι), LinearIndepOn R (⇑b) s
-- Init.Data.List.Lemmas
List.removeAll_cons : ∀ {α : Type u_1} [inst : BEq α] {xs : List α} {y : α} {ys : List α},
  xs.removeAll (y :: ys) = (List.filter (fun x => !x == y) xs).removeAll ys
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instMul.eq_1 : ∀ {α : Type u_1} [inst : Mul α], OrderDual.instMul = inst
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
/-- The pullback functor `PresheafOfModules S ⥤ PresheafOfModules R` induced by
a morphism of presheaves of rings `S ⟶ F.op ⋙ R`, defined as the left adjoint
functor to the pushforward, when it exists.  -/
PresheafOfModules.pullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor Dᵒᵖ RingCat} →
            {S : CategoryTheory.Functor Cᵒᵖ RingCat} →
              (φ : S ⟶ F.op.comp R) →
                [(PresheafOfModules.pushforward φ).IsRightAdjoint] →
                  CategoryTheory.Functor (PresheafOfModules S) (PresheafOfModules R)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- A (pre) inner product space is a vector space with an additional operation called inner product.
The (semi)norm could be derived from the inner product, instead we require the existence of a
seminorm and the fact that `‖x‖^2 = re ⟪x, x⟫` to be able to put instances on `𝕂` or product spaces.

Note that `NormedSpace` does not assume that `‖x‖=0` implies `x=0` (it is rather a seminorm).

To construct a seminorm from an inner product, see `PreInnerProductSpace.ofCore`.
 -/
InnerProductSpace : (𝕜 : Type u_4) → (E : Type u_5) → [RCLike 𝕜] → [SeminormedAddCommGroup E] → Type (max u_4 u_5)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  [inst_2 : Std.LawfulEqOrd α] {l : List ((a : α) × β a)} {k : α} [inst_3 : Inhabited (β k)],
  (List.map Sigma.fst l).contains k = false → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).get! k = default
-- 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),
  ‖MeasureTheory.L1.setToL1 hT‖ ≤ max C 0
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_ι_assoc : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U ≤ V) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.homOfLE e) (CategoryTheory.CategoryStruct.comp V.ι h) =
    CategoryTheory.CategoryStruct.comp U.ι h
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- If the topology of a space is induced by a countable family of seminorms, then the topology
is first countable.  -/
WithSeminorms.firstCountableTopology : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [Countable ι] {p : SeminormFamily 𝕜 E ι} [inst_4 : TopologicalSpace E],
  WithSeminorms p → FirstCountableTopology E
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.fold_eq_foldl_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {δ : Type w} {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  {f : δ → α → β → δ} {init : δ},
  m.WF → Std.DHashMap.Raw.fold f init m = Array.foldl (fun a b => f a b.1 b.2) init (Std.DHashMap.Raw.Const.toArray m)
-- Init.Data.List.Basic
List.tailD_cons : ∀ {α : Type u} {a : α} {l l' : List α}, (a :: l).tailD l' = l
-- Mathlib.Logic.Function.Basic
Function.apply_update₂ : ∀ {ι : Sort u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} {γ : ι → Sort u_4}
  (f : (i : ι) → α i → β i → γ i) (g : (i : ι) → α i) (h : (i : ι) → β i) (i : ι) (v : α i) (w : β i) (j : ι),
  f j (Function.update g i v j) (Function.update h i w j) = Function.update (fun k => f k (g k) (h k)) i (f i v w) j
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+ β) (h : Monotone (↑f).toFun), ⇑{ toAddMonoidHom := f, monotone' := h } = ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- `C` has coreflexive equalizers if it has equalizers for every coreflexive pair.  -/
CategoryTheory.Limits.HasCoreflexiveEqualizers : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.eq_1 : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] (f : α → β) (s : Set α) (a : α),
  IsLocalMaxOn f s a = IsMaxFilter f (nhdsWithin a s) a
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- A subgroup of `Perm α` is `⊤` if(f) it is `(Nat.card α - 1)`-pretransitive.  -/
Equiv.Perm.eq_top_of_isMultiplyPretransitive : ∀ {α : Type u_1} [Finite α] {G : Subgroup (Equiv.Perm α)},
  MulAction.IsMultiplyPretransitive (↥G) α (Nat.card α - 1) → G = ⊤
-- Mathlib.Algebra.Category.MonCat.Yoneda
/-- The `AddCommMonCat`-valued coyoneda embedding.  -/
AddCommMonCat.coyoneda : CategoryTheory.Functor AddCommMonCatᵒᵖ (CategoryTheory.Functor AddCommMonCat AddCommMonCat)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.degree_eq_zero_of_subsingleton : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) [inst : Fintype ↑(G'.neighborSet v)],
  G'.verts.Subsingleton → G'.degree v = 0
-- Init.Data.BitVec.Bitblast
BitVec.sshiftRightRec.eq_2 : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (s_1 : ℕ),
  x.sshiftRightRec y s_1.succ = (x.sshiftRightRec y s_1).sshiftRight' (y &&& BitVec.twoPow w₂ s_1.succ)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Sieves on an object `X` form a complete lattice.
We generate this directly rather than using the Galois insertion for nicer definitional properties.
 -/
CategoryTheory.Sieve.instCompleteLattice : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CompleteLattice (CategoryTheory.Sieve X)
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.zero_sub : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, 0 - μ = 0
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.Hom.toBialgHom_injective : ∀ {R : Type u} [inst : CommRing R] (V W : BialgCat R), Function.Injective BialgCat.Hom.toBialgHom
-- Mathlib.Computability.NFA
NFA.stepSet.eq_1 : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (a : α), M.stepSet S a = ⋃ s ∈ S, M.step s a
-- Init.Data.List.Range
List.range_ne_nil : ∀ {n : ℕ}, List.range n ≠ [] ↔ n ≠ 0
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.liftOn₂.eq_1 : ∀ {M : Type u_1} [inst : Add M] {β : Sort u_4} {c : AddCon M} (q r : c.Quotient) (f : M → M → β)
  (h : ∀ (a₁ a₂ b₁ b₂ : M), c a₁ b₁ → c a₂ b₂ → f a₁ a₂ = f b₁ b₂), AddCon.liftOn₂ q r f h = Quotient.liftOn₂' q r f h
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- The first projection `ROfRel ⟶ X`.  -/
TypeCat.p₁OfRel : {X : Type w} → (φ : X → X → Prop) → TypeCat.ROfRel φ ⟶ X
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.instLawfulToForwardSearcherModelCharDefaultForwardSearcherForallBoolBeq : ∀ {c : Char}, String.Slice.Pattern.Model.LawfulToForwardSearcherModel c
-- Init.Data.BitVec.Lemmas
BitVec.length_pos_of_lt : ∀ {w : ℕ} {b b' : BitVec w}, b < b' → 0 < w