mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Data.Method
/-- Lock a resource to prevent concurrent modifications.
Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.10
 -/
Std.Http.Method.lock : Std.Http.Method
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.TopSortM : Type → Type
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option β → Option β}, m.WF → k ∈ m → (f m[k]?).isSome = true → (m.alter k f).size = m.size
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.NoSuffixPatternModel.eq_empty : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.Model.PatternModel pat}
  [self : String.Slice.Pattern.Model.NoSuffixPatternModel pat] (s t : String),
  String.Slice.Pattern.Model.PatternModel.Matches pat t →
    String.Slice.Pattern.Model.PatternModel.Matches pat (s ++ t) → s = ""
-- Mathlib.Data.List.Lemmas
List.foldl_range_subset_of_range_subset : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → α} {g : α → γ → α},
  ((Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b) →
    ∀ (a : α), Set.range (List.foldl f a) ⊆ Set.range (List.foldl g a)
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_snd : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B),
  (CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso.hom.app X).2 =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Sum.inr_ A' A).associator (CategoryTheory.Sum.swap A' A) X).inv
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.Sum.swapCompInr A' A).hom X)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- This and `δ_map` are the preliminary results for the long exact sequence in Tate cohomology
induced by a short exact sequence of `G`-reps.  -/
TateCohomology.map_δ : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G]
  {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (n : ℤ),
  CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor n).map S.g) (TateCohomology.δ hS n) = 0
-- Mathlib.SetTheory.Cardinal.Defs
/-- Lift a function between `Type*`s to a function between `Cardinal`s.  -/
Cardinal.map : (f : Type u → Type v) → ((α β : Type u) → α ≃ β → f α ≃ f β) → Cardinal.{u} → Cardinal.{v}
-- Mathlib.CategoryTheory.Pi.Basic
/-- Reindexing a family of categories gives equivalent `Pi` categories.  -/
CategoryTheory.Pi.equivalenceOfEquiv : {I : Type w₀} →
  {J : Type w₁} →
    (C : I → Type u₁) →
      [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → (e : J ≃ I) → ((j : J) → C (e j)) ≌ (i : I) → C i
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Continuous IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_diagonal : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (d : n → R),
  (Matrix.diagonal d).charmatrix = Matrix.diagonal fun i => Polynomial.X - Polynomial.C (d i)
-- Mathlib.Tactic.Positivity.Finset
/-- Extension for `Finset.dens`. `s.dens` is positive if `s` is nonempty.

It calls `Mathlib.Meta.proveFinsetNonempty` to attempt proving that the finset is nonempty.  -/
Mathlib.Meta.Positivity.evalFinsetDens : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.mk.sizeOf_spec : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} [inst_4 : SizeOf E] [inst_5 : SizeOf F]
  (toFun : E → F) (contDiff' : ContDiff ℝ (↑n) toFun) (zero_on_compl' : Set.EqOn toFun 0 (↑K)ᶜ),
  sizeOf { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' } = 1 + sizeOf contDiff'
-- Init.Data.UInt.Lemmas
USize.toUInt8_toUInt32 : ∀ (n : USize), n.toUInt32.toUInt8 = n.toUInt8
-- Mathlib.Analysis.Convex.Star
StarConvex.segment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {s : Set E}, StarConvex 𝕜 x s → ∀ {y : E}, y ∈ s → segment 𝕜 x y ⊆ s
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_nat_mod : ∀ {ι : Type u_1} (s : Finset ι) (n : ℕ) (f : ι → ℕ), (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n
-- Mathlib.Algebra.Group.Prod
AddHom.fst_comp_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : M →ₙ+ N)
  (g : M →ₙ+ P), (AddHom.fst N P).comp (f.prod g) = f
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit.congr_simp : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cone K₁}
  (hc₁ hc₁_1 : CategoryTheory.Limits.IsLimit c₁),
  hc₁ = hc₁_1 →
    ∀ {c₂ : CategoryTheory.Limits.Cone K₂} (hc₂ hc₂_1 : CategoryTheory.Limits.IsLimit c₂),
      hc₂ = hc₂_1 →
        ∀
          {c₃ :
            CategoryTheory.Limits.Cone
              (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
          (hc₃ hc₃_1 : CategoryTheory.Limits.IsLimit c₃),
          hc₃ = hc₃_1 →
            CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃ =
              CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit G hc₁_1 hc₂_1 hc₃_1
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.trivializationAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B),
  trivializationAt F Z.Fiber b = Z.localTrivAt b
-- Batteries.Tactic.Lint.Frontend
/-- Formats a map of linter warnings using `print_warning`, sorted by line number.  -/
Batteries.Tactic.Lint.printWarnings : Std.HashMap Lean.Name Lean.MessageData →
  optParam System.FilePath default → optParam Bool false → Lean.CoreM Lean.MessageData
-- Lean.MetavarContext
Lean.getDelayedMVarAssignment? : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → m (Option Lean.DelayedMetavarAssignment)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.any_eq_true_iff_exists_mem_getKey_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → β → Bool},
  m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p (m.getKey a h) (Std.DHashMap.Const.get m a h) = true
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_eq_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {p : α → Prop} {f g : α →₀ M},
  (∀ x ∈ f.support, p x) → (∀ x ∈ g.support, p x) → (Finsupp.subtypeDomain p f = Finsupp.subtypeDomain p g ↔ f = g)
-- Mathlib.Topology.Order.LiminfLimsup
BoundedGENhdsClass.of_closedIicTopology : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIicTopology α], BoundedGENhdsClass α
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.xgcd_val : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x y : R),
  EuclideanDomain.xgcd x y = (EuclideanDomain.gcdA x y, EuclideanDomain.gcdB x y)
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.toList_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α}, m₁.Equiv m₂ → m₁.toList.Perm m₂.toList
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry from an emetric space is an embedding  -/
Isometry.isEmbedding : ∀ {α : Type u} {β : Type v} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → Topology.IsEmbedding f
-- Mathlib.NumberTheory.AlmostPrime
Nat.Prime.mul_isAlmostPrime_two : ∀ {p q : ℕ}, Nat.Prime p → Nat.Prime q → Nat.IsAlmostPrime 2 (p * q)
-- Std.Data.TreeMap.Basic
Std.TreeMap.instGetElem?Mem : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → GetElem? (Std.TreeMap α β cmp) α β fun m a => a ∈ m
-- Mathlib.SetTheory.Cardinal.Order
/-- An embedding of any type to the set of cardinals in its universe.  -/
embeddingToCardinal : {α : Type u} → α ↪ Cardinal.{u}
-- Batteries.Data.Nat.Lemmas
Nat.testBit_ofBits : ∀ {n i : ℕ} (f : Fin n → Bool), (Nat.ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.comp.eq_1 : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  {D : Type u₂} {E : Type u₃} [inst_2 : CategoryTheory.EnrichedCategory V C]
  [inst_3 : CategoryTheory.EnrichedCategory V D] [inst_4 : CategoryTheory.EnrichedCategory V E]
  (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E),
  CategoryTheory.EnrichedFunctor.comp V F G =
    { obj := fun X => G.obj (F.obj X),
      map := fun x x_1 => CategoryTheory.CategoryStruct.comp (F.map x x_1) (G.map (F.obj x) (F.obj x_1)), map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurable.measurable' : ∀ {α : Type u_2} {β : Type u_3} [m : MeasurableSpace α] [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α}, MeasureTheory.NullMeasurable f μ → Measurable f
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.toSheaf_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) (M : SheafOfModules R), ((SheafOfModules.toSheaf R).obj M).obj = M.val.presheaf
-- Init.Prelude
/-- A region or slice of some underlying string.

A substring contains a string together with the start and end byte positions of a region of
interest. Actually extracting a substring requires copying and memory allocation, while many
substrings of the same underlying string may exist with very little overhead, and they are more
convenient than tracking the bounds by hand.

Using its constructor explicitly, it is possible to construct a `Substring` in which one or both of
the positions is invalid for the string. Many operations will return unexpected or confusing results
if the start and stop positions are not valid. For this reason, `Substring` will be deprecated in
favor of `String.Slice`, which always represents a valid substring.
 -/
Substring.Raw : Type
-- Aesop.Search.Main
_private.Aesop.Search.Main.0.Aesop.expandNextGoal.traceNewRapps : {Q : Type} → [inst : Aesop.Queue Q] → Array Aesop.RappRef → Aesop.SearchM Q Unit
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α}, k ∈ t → t.getKey? k = some k
-- Mathlib.GroupTheory.Exponent
AddGroup.exponent_dvd_card : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : Fintype G], AddMonoid.exponent G ∣ Fintype.card G
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.η_single : ∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k] (x : PUnit.{u + 1}),
  (Representation.LinearizeMonoidal.η k G) (MonoidAlgebra.single x 1) = 1
-- Mathlib.Tactic.Ring.Common
/-- Evaluate an expression as a potential coefficient.  -/
Mathlib.Tactic.Ring.Common.RingCompute.derive : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα →
          (x : Q(«$α»)) →
            Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum BaseType sα) q(«$x»))
-- Mathlib.NumberTheory.Divisors
Int.neg_mem_divisorsAntidiag : ∀ {xy : ℤ × ℤ} {z : ℤ}, -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerLeft_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f) =
    CategoryTheory.Limits.pullback.map R.hom S.hom R.hom T.hom (CategoryTheory.CategoryStruct.id R.left)
      (CategoryTheory.Over.Hom.left f) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isCircuit_rotate`. -/
SimpleGraph.Walk.IsCircuit.rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v} (hu : u ∈ c.support),
  c.IsCircuit → (c.rotate u hu).IsCircuit
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∪ t₂).get? k = t₁.get? k
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.eventually_constant_prod : ∀ {M : Type u_4} [inst : CommMonoid M] {u : ℕ → M} {N : ℕ},
  (∀ n ≥ N, u n = 1) → ∀ {n : ℕ}, N ≤ n → ∏ k ∈ Finset.range n, u k = ∏ k ∈ Finset.range N, u k
-- Aesop.Forward.Match.Types
Aesop.Match.instHashable : Hashable Aesop.Match
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.pull_end_proc : Lean.ParserDescr
-- Mathlib.Data.PFun
_private.Mathlib.Data.PFun.0.PFun.fix.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : β ⊕ α → Sort u_3) →
      (x : β ⊕ α) →
        ((b : β) → x = Sum.inl b → motive (Sum.inl b)) → ((a' : α) → x = Sum.inr a' → motive (Sum.inr a')) → motive x
-- Mathlib.GroupTheory.Congruence.Star
conGen_star : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : StarMul M] {r : M → M → Prop},
  (∀ (a b : M), r a b → r (star a) (star b)) → ∀ ⦃a b : M⦄, (conGen r) a b → (conGen r) (star a) (star b)
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.CommGrpCat.Hom.mk.inj : ∀ {A B : CommGrpCat} {hom' hom'_1 : ↑A →* ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Init.SimpLemmas
of_eq_true : ∀ {p : Prop}, p = True → p
-- Mathlib.Data.Sum.Order
Sum.inl_lt_inl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : α}, Sum.inl a < Sum.inl b ↔ a < b
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticForm.baseChange_tmul : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup M₂]
  [inst_3 : Algebra R A] [inst_4 : Module R M₂] [inst_5 : Invertible 2] (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂),
  (QuadraticForm.baseChange A Q) (a ⊗ₜ[R] m₂) = Q m₂ • (a * a)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `F : D ⥤ K ⥤ C` preserves the colimit of some `G : J ⥤ D` if it does for each `k : K`.  -/
CategoryTheory.Limits.preservesColimit_of_evaluation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor D (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor J D),
  (∀ (k : K), CategoryTheory.Limits.PreservesColimit G (F.comp ((CategoryTheory.evaluation K C).obj k))) →
    CategoryTheory.Limits.PreservesColimit G F
-- Mathlib.Algebra.Lie.CartanExists
/-- Let `x` and `y` be elements of a Lie `R`-algebra `L`, and `M` a Lie module over `L`.
Then the characteristic polynomials of the family of endomorphisms `⁅r • y + x, _⁆` of `M`
have coefficients that are polynomial in `r : R`.
In other words, we obtain a polynomial over `R[X]`
that specializes to the characteristic polynomial of `⁅r • y + x, _⁆` under the map `X ↦ r`.
This polynomial is captured in `lieCharpoly R M x y`.  -/
_private.Mathlib.Algebra.Lie.CartanExists.0.LieAlgebra.engel_isBot_of_isMin.lieCharpoly : (R : Type u_2) →
  {L : Type u_3} →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [LieModule R L M] →
                    [Module.Finite R L] →
                      [Module.Free R L] → [Module.Finite R M] → [Module.Free R M] → L → L → Polynomial (Polynomial R)
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app_assoc : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F]
  (X₁ X₂ : C) {Z : E} (h : ((CategoryTheory.MonoidalCategory.curriedTensorPost F).obj (L.obj X₁)).obj (L.obj X₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂)) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app X₁)
        ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app X₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G X₁ X₂)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Lifting.iso L W G F).inv.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂))
          (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.OplaxMonoidal.δ L X₁ X₂)) h)))
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Injective.hasSum_range_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {g : γ → β}, Function.Injective g → (HasSum (fun x => f ↑x) a ↔ HasSum (f ∘ g) a)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_Ω₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C)
  (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω)
  (isPullback :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth)
  (uniq :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] (χ' : X ⟶ Ω),
      CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m),
  (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω₀ = Ω₀
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- **Turán's theorem**, reverse direction.

Any graph isomorphic to `turanGraph n r` is itself Turán-maximal if `0 < r`.  -/
SimpleGraph.isTuranMaximal_of_iso : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n r : ℕ}
  (f : G ≃g SimpleGraph.turanGraph n r), 0 < r → G.IsTuranMaximal r
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.ColimitType.instZero : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → Zero (RingCat.Colimits.ColimitType F)
-- Mathlib.Data.Finset.Filter
Finset.monotone_filter_left : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], Monotone (Finset.filter p)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toAlgebra : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → (S : IntermediateField K L) → Algebra (↥S) L
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_list_prod : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (l : List (MvPolynomial σ R)),
  l.prod.totalDegree ≤ (List.map MvPolynomial.totalDegree l).sum
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.union : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t₁ t₂ : Set α},
  Absorbs M s t₁ → Absorbs M s t₂ → Absorbs M s (t₁ ∪ t₂)
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- A module `M` is Hausdorff with respect to an ideal `I` if `⋂ I^n M = 0`.  -/
IsHausdorff : {R : Type u_1} → [inst : CommRing R] → Ideal R → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.prod_mul_tprod_subtype_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] [CompleteSpace α]
  [T2Space α] {f : β → α},
  Multipliable f → ∀ (s : Finset β), (∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : β), f x
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instIsLeftCancelAdd : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Add α] [IsLeftCancelAdd α], IsLeftCancelAdd (Matrix m n α)
-- Mathlib.Logic.Relation
Relation.TransGen.stdSymm : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Std.Symm (Relation.TransGen r)
-- Mathlib.Analysis.Calculus.ImplicitContDiff
IsContDiffImplicitAt.mk : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  {E₂ : Type u_3} [inst_3 : NormedAddCommGroup E₂] [inst_4 : NormedSpace 𝕜 E₂] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E₁ × E₂ → F} {f' : E₁ × E₂ →L[𝕜] F}
  {u : E₁ × E₂},
  HasFDerivAt f f' u →
    ContDiffAt 𝕜 n f u →
      Function.Bijective ⇑(f' ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂) → n ≠ 0 → IsContDiffImplicitAt n f f' u
-- Mathlib.CategoryTheory.Generator.Basic
/-- An ingredient of the proof of the Special Adjoint Functor Theorem: a cocomplete well-copowered
category with a small separating set has a terminal object.

In fact, it follows from the Special Adjoint Functor Theorem that `C` is already complete, see
`hasLimits_of_hasColimits_of_isSeparating`.  -/
CategoryTheory.hasTerminal_of_isSeparating : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} Cᵒᵖ]
  [CategoryTheory.WellPowered.{w, v₁, u₁} Cᵒᵖ] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v₁, u₁} C]
  {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v₁, u₁} P],
  P.IsSeparating → CategoryTheory.Limits.HasTerminal C
-- Batteries.Data.List.Lemmas
List.idxOfNth_eq_length_iff : ∀ {α : Type u_1} {x : α} {n : ℕ} [inst : BEq α] {xs : List α}, List.idxOfNth x xs n = xs.length ↔ List.count x xs ≤ n
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.ins.eq_3 : ∀ {α : Type u_1} (x a : RBTree.RBNode α) (y : α) (parent : RBTree.RBNode.Path α),
  (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent).ins x =
    parent.ins (RBTree.RBNode.node RBTree.RBColor.red a y x)