mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_mul : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Mul M] (f : R →+* S)
  (x y : MonoidAlgebra R M), MonoidAlgebra.map (↑f) (x * y) = MonoidAlgebra.map (↑f) x * MonoidAlgebra.map (↑f) y
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast : ∀ (p q : Polynomial ℤ),
  p.IsPrimitive → (p ∣ q ↔ Polynomial.map (Int.castRingHom ℚ) p ∣ Polynomial.map (Int.castRingHom ℚ) q)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.sub : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr
-- Mathlib.Data.Set.Monotone
strictMonoOn_insert_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  StrictMonoOn f (insert a s) ↔ (∀ b ∈ s, b < a → f b < f a) ∧ (∀ b ∈ s, a < b → f a < f b) ∧ StrictMonoOn f s
-- Init.Data.List.Attach
List.filterMap_attachWith : ∀ {α : Type u_1} {β : Type u_2} {q : α → Prop} {l : List α} {f : { x // q x } → Option β} (H : ∀ x ∈ l, q x),
  List.filterMap f (l.attachWith q H) =
    List.filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      l.attach
-- Batteries.Data.Random.MersenneTwister
/-- Degree of recurrence (`n`).  -/
Batteries.Random.MersenneTwister.Config.stateSize : Batteries.Random.MersenneTwister.Config → ℕ
-- Std.Data.Internal.List.Associative
/-- Given a proof that the list is nonempty, returns the smallest key in an associative list.  -/
Std.Internal.List.minKey : {α : Type u} → {β : α → Type v} → [Ord α] → (xs : List ((a : α) × β a)) → xs.isEmpty = false → α
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_zero : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G}, ∫ᵛ (x : X), 0 ∂[B; μ] = 0
-- Mathlib.RingTheory.Polynomial.Nilpotent
/-- Let `P` be a polynomial over `R`. `P` is a unit if and only if all its coefficients are
nilpotent, except its constant term which is a unit.

See also `Polynomial.isUnit_iff'`.  -/
Polynomial.isUnit_iff_coeff_isUnit_isNilpotent : ∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R},
  IsUnit P ↔ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.piUnique_symm_apply : ∀ {ι : Type u_16} (M : ι → Type u_17) [inst : (j : ι) → Add (M j)] [inst_1 : Unique ι] (x : M default) (i : ι),
  (AddEquiv.piUnique M).symm x i = uniqueElim x i
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- The canonical `r + 1`-cliquefree Turán graph on `n` vertices.  -/
SimpleGraph.turanGraph : (n : ℕ) → ℕ → SimpleGraph (Fin n)
-- Mathlib.Order.Part
Antitone.partBind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] {f : α → Part β} {g : α → β → Part γ},
  Antitone f → Antitone g → Antitone fun x => (f x).bind (g x)
-- Mathlib.Geometry.Manifold.Diffeomorph
ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_9} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] (e : E ≃L[𝕜] E') (x : M),
  ↑(extChartAt (I.transContinuousLinearEquiv e) x).symm = ↑(extChartAt I x).symm ∘ ⇑e.symm
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- If `C` is a `V`-enriched ordinary category, and `C` has suitable limits,
then `J ⥤ C` is also a `J ⥤ V`-enriched ordinary category.  -/
CategoryTheory.Enriched.FunctorCategory.functorEnrichedOrdinaryCategory : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u₂) →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          (J : Type u₃) →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                [∀ (F₁ F₂ : CategoryTheory.Functor J C),
                      CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] →
                  [∀ (F₁ F₂ : CategoryTheory.Functor J C),
                        CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                    CategoryTheory.EnrichedOrdinaryCategory (CategoryTheory.Functor J V) (CategoryTheory.Functor J C)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.instInfiniteOfNatNat : Infinite (DihedralGroup 0)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addCHaar_mem_addHaarProduct : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G),
  MeasureTheory.Measure.haar.addCHaar K₀ ∈ MeasureTheory.Measure.haar.addHaarProduct ↑K₀
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_eq_zero_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, MeasureTheory.Measure.count s = 0 ↔ s = ∅
-- Mathlib.Algebra.Homology.Homotopy
dNext.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (i : ι),
  dNext i = AddMonoidHom.mk' (fun f => CategoryTheory.CategoryStruct.comp (C.d i (c.next i)) (f (c.next i) i)) ⋯
-- Init.Grind.Ordered.Order
Lean.Grind.Preorder.lt_trans : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α}, a < b → b < c → a < c
-- Init.Meta.Defs
/-- Additional version description like "nightly-2018-03-11"  -/
Lean.version.getSpecialDesc : Unit → String
-- Init.Data.SInt.Lemmas
Int8.le_antisymm : ∀ {a b : Int8}, a ≤ b → b ≤ a → a = b
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.tendsto_sigmoid_atTop : Filter.Tendsto unitInterval.sigmoid Filter.atTop (nhds 1)
-- Mathlib.Algebra.Ring.BooleanRing
toBoolRing_top : ∀ {α : Type u_1} [inst : BooleanAlgebra α], toBoolRing ⊤ = 1
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.IsClosed.cylinder : ∀ {ι : Type u_2} {α : ι → Type u_1} [inst : (i : ι) → TopologicalSpace (α i)] (s : Finset ι)
  {S : Set ((i : ↥s) → α ↑i)}, IsClosed S → IsClosed (MeasureTheory.cylinder s S)
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.instIsNontrivialWithZeroMultiplicativeIntInftyValuation : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)], (RatFunc.inftyValuation F).IsNontrivial
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).getKey? k = if (f (Std.DHashMap.Const.get? m k)).isSome = true then some k else none
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis'.mem_of_insert_indep : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α}, M.IsBasis' I X → e ∈ X → M.Indep (insert e I) → e ∈ I
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The Second-Derivative Test from calculus, minimum version.
Applies to functions like `x^2 + 1[x ≥ 0]` as well as twice differentiable
functions.  -/
isLocalMin_of_deriv_deriv_pos : ∀ {f : ℝ → ℝ} {x₀ : ℝ}, deriv (deriv f) x₀ > 0 → deriv f x₀ = 0 → ContinuousAt f x₀ → IsLocalMin f x₀
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.get! t.max! = t.max!
-- Mathlib.Analysis.Convex.Basic
Convex.midpoint_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : Invertible 2] {s : Set E} {x y : E},
  Convex 𝕜 s → x ∈ s → y ∈ s → midpoint 𝕜 x y ∈ s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.affineOpenCover_f : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (i : (i : ℕ+) × ↥(𝒜 ↑i)),
  (AlgebraicGeometry.Proj.affineOpenCover 𝒜).f i = AlgebraicGeometry.Proj.awayι 𝒜 ↑i.snd ⋯ ⋯
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.not_neg : ∀ {w : ℕ} (x : BitVec w), ~~~(~~~x + 1#w) = x + -1#w
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_succ : ∀ (a b : Ordinal.{u_4}), a * Order.succ b = a * b + a
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax right unity.  -/
CategoryTheory.LaxFunctor.map₂_rightUnitor_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b}
  (h : self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b))
        (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)) h))
-- Mathlib.Order.RelClasses
instIsStrictTotalOrderGt : ∀ {α : Type u} [inst : LinearOrder α], IsStrictTotalOrder α fun x1 x2 => x2 < x1
-- Mathlib.Order.SuccPred.Archimedean
/-- Induction principle on a type with a `PredOrder` for all elements below a given element `m`.  -/
Pred.rec : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α] {m : α} {P : (n : α) → n ≤ m → Prop},
  P m ⋯ → (∀ (n : α) (hmn : n ≤ m), P n hmn → P (Order.pred n) ⋯) → ∀ ⦃n : α⦄ (hmn : n ≤ m), P n hmn
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
DirectedOn.isGLB_csInf : ∀ {α : Type u_2} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.instRespectsRightOppositeOpOfRespectsLeft : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P Q : CategoryTheory.MorphismProperty C)
  [P.RespectsLeft Q], P.op.RespectsRight Q.op
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
/-- If `f` is an open partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
invertible derivative `f'` at `f.symm a`, then `f.symm` has the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
OpenPartialHomeomorph.hasFDerivAt_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F)
  {f' : E ≃L[𝕜] F} {a : F}, a ∈ f.target → HasFDerivAt (↑f) (↑f') (↑f.symm a) → HasFDerivAt (↑f.symm) (↑f'.symm) a
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_inf : ∀ {R : Type u_2} [inst : NonAssocRing R] (S₁ S₂ : Subring Rᵐᵒᵖ), (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Continuous.dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {f g : β → α},
  Continuous f → Continuous g → Continuous fun b => dist (f b) (g b)
-- Mathlib.Algebra.Exact.Basic
Function.Exact.of_ladder_addEquiv_of_exact' : ∀ {X₁ : Type u_8} {X₂ : Type u_9} {X₃ : Type u_10} {Y₁ : Type u_11} {Y₂ : Type u_12} {Y₃ : Type u_13}
  [inst : AddCommMonoid X₁] [inst_1 : AddCommMonoid X₂] [inst_2 : AddCommMonoid X₃] [inst_3 : AddCommMonoid Y₁]
  [inst_4 : AddCommMonoid Y₂] [inst_5 : AddCommMonoid Y₃] (e₁ : X₁ ≃+ Y₁) (e₂ : X₂ ≃+ Y₂) (e₃ : X₃ ≃+ Y₃)
  {f₁₂ : X₁ →+ X₂} {f₂₃ : X₂ →+ X₃} {g₁₂ : Y₁ →+ Y₂} {g₂₃ : Y₂ →+ Y₃},
  g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂ → g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃ → Function.Exact ⇑g₁₂ ⇑g₂₃ → Function.Exact ⇑f₁₂ ⇑f₂₃
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.hom_ext' : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f g : X ⊞ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl f =
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl g →
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr f =
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr g →
      f = g
-- Std.Time.Format
/-- The leanDateTimeWithZoneNoNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ssZZZZZ`
for representing date, time, and time zone. It uses the default value that can be parsed with the
notation of dates.
 -/
Std.Time.Formats.leanDateTimeWithZoneNoNanos : Std.Time.GenericFormat Std.Time.Awareness.any
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.proper.congr_simp : ∀ {s : String.Slice} (needle : String.Slice) (table table_1 : Vector ℕ needle.utf8ByteSize) (e_table : table = table_1)
  (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) (stackPos stackPos_1 : String.Pos.Raw),
  stackPos = stackPos_1 →
    ∀ (needlePos needlePos_1 : String.Pos.Raw) (e_needlePos : needlePos = needlePos_1)
      (hn : needlePos < needle.rawEndPos),
      String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =
        String.Slice.Pattern.ForwardSliceSearcher.proper needle table_1 ⋯ stackPos_1 needlePos_1 ⋯
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.darts_nodup_of_support_nodup : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.support.Nodup → p.darts.Nodup
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- The embedding has closed range if the domain (and therefore the codomain) is a ring,
see `PrimeSpectrum.isClosedEmbedding_comap_of_surjective`.
On the other hand, `comap (Nat.castRingHom (ZMod 2))` does not have closed range.  -/
PrimeSpectrum.isEmbedding_comap_of_surjective : ∀ {R : Type u} (S : Type v) [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  Function.Surjective ⇑f → Topology.IsEmbedding (PrimeSpectrum.comap f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The `CategoricalPullback F G` is the category of triples
`(a : A, c : C, F a ≅ G c)`.
Morphisms `(a, c, e) ⟶ (a', c', e')` are pairs of morphisms
`(f₁ : a ⟶ a', f₂ : c ⟶ c')` compatible with the specified
isomorphisms.  -/
CategoryTheory.Limits.CategoricalPullback : {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] →
            CategoryTheory.Functor A B → CategoryTheory.Functor C B → Type (max (max u₁ u₃) v₂)
-- Mathlib.ModelTheory.Ultraproducts
FirstOrder.Language.Ultraproduct.Product.instNonempty : ∀ {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} [∀ (a : α), Nonempty (M a)], Nonempty ((↑u).Product M)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.isClosed_subsets_of_isClosed : ∀ {α : Type u_1} [inst : UniformSpace α] {s : Set α}, IsClosed s → IsClosed {t | ↑t ⊆ s}
-- Init.Data.Nat.Coprime
Nat.Coprime.gcd_mul : ∀ {m n : ℕ} (k : ℕ), m.Coprime n → k.gcd (m * n) = k.gcd m * k.gcd n
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [inst_5 : F.Additive]
  [inst_6 : G.Additive] [inst_7 : H.Additive] {Z : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.up ℕ))}
  (h : H.rightDerivedToHomotopyCategory ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory β) h)
-- Lean.Meta.Tactic.Simp.Types
/-- Construct the `Expr` `cast h e`, from a `Simp.Result` with proof `h`.  -/
Lean.Meta.Simp.Result.mkCast : Lean.Meta.Simp.Result → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.ereal_toReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → EReal} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => (f x).toReal) μ
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- `X.AffineZariskiSite` is the small affine Zariski site of `X`, whose elements are affine open
sets of `X`, and whose arrows are basic open sets `D(f) ⟶ U` for any `f : Γ(X, U)`.

Note that this differs from the definition on stacks project where the arrows in the small affine
Zariski site are arbitrary inclusions.
 -/
AlgebraicGeometry.Scheme.AffineZariskiSite : AlgebraicGeometry.Scheme → Type u
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.many1NoAntiquot.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instIsScalarTower : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {S : Type u_5} {T : Type u_6}
  [inst_8 : DistribSMul S F] [inst_9 : SMulCommClass 𝕜₂ S F] [inst_10 : ContinuousConstSMul S F]
  [inst_11 : DistribSMul T F] [inst_12 : SMulCommClass 𝕜₂ T F] [inst_13 : ContinuousConstSMul T F] [inst_14 : SMul S T]
  [IsScalarTower S T F], IsScalarTower S T (E →SWOT[σ] F)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.faceOpposite_point_eq_point_zero : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Affine.Simplex k P 1) (n : Fin 1), (s.faceOpposite 1).points n = s.points 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Over.forget X.1) X.2),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse X).obj Y).left = Y.left.left
-- Mathlib.Topology.Order.Compact
compactSpace_Icc : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α] (a b : α),
  CompactSpace ↑(Set.Icc a b)
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
/-- Turn a group-like element `a` into a unit with inverse its antipode.  -/
GroupLike.toUnits : (R : Type u_1) →
  {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : HopfAlgebra R A] → GroupLike R A →* Aˣ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.mk_eq_mk_iff : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (s t : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) (f g : ℝ → ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.mk s f = Tactic.ComputeAsymptotics.MultiseriesExpansion.mk t g ↔
    s = t ∧ f = g
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Auxiliary for `List.splitWrtComposition`.  -/
List.splitWrtCompositionAux : {α : Type u_1} → List α → List ℕ → List (List α)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Left whiskering of a lax natural transformation and a modification.  -/
CategoryTheory.Lax.LaxTrans.whiskerLeft : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          (η : F ⟶ G) →
            {θ ι : G ⟶ H} → (θ ⟶ ι) → (CategoryTheory.CategoryStruct.comp η θ ⟶ CategoryTheory.CategoryStruct.comp η ι)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.awayι_toSpecZero : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.toSpecZero 𝒜) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f)))
-- Mathlib.Algebra.Order.Ring.Int
Int.add_two_le_iff_lt_of_even_sub : ∀ {m n : ℤ}, Even (n - m) → (m + 2 ≤ n ↔ m < n)
-- Init.Data.UInt.Lemmas
UInt32.sub_self : ∀ (a : UInt32), a - a = 0
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.ker_toSpanSingleton : ∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] {x : M}, x ≠ 0 → (LinearMap.toSpanSingleton R M x).ker = ⊥
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesOfIsCocycle₁_coe : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] {f : G → A} (hf : groupCohomology.IsCocycle₁ f)
  (a : G), ↑(groupCohomology.cocyclesOfIsCocycle₁ hf) a = f a
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.abs_le_one_iff : ∀ {a : ℤ}, |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inlₗ.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β],
  OrderAddMonoidHom.inlₗ α β =
    { toFun := (Prod.Lex.toLexOrderHom.comp ↑(OrderAddMonoidHom.inl α β)).toFun, map_zero' := ⋯, map_add' := ⋯,
      monotone' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt16.not_le : ∀ {a b : UInt16}, ¬a ≤ b ↔ b < a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.le_inf_div : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Div α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] {s t : Finset α} {f : α → β} {a : β}, a ≤ (s / t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x / y)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Waiter.consumerNode.inj : ∀ {a a_1 : Lean.Meta.SynthInstance.ConsumerNode},
  Lean.Meta.SynthInstance.Waiter.consumerNode a = Lean.Meta.SynthInstance.Waiter.consumerNode a_1 → a = a_1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
IsUnramifiedAtInfinitePlaces.mk : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K],
  (∀ (w : NumberField.InfinitePlace K), NumberField.InfinitePlace.IsUnramified k w) → IsUnramifiedAtInfinitePlaces k K