mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.take.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (n : ℕ) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (n : ℕ) → motive n.succ []) (h_3 : (n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)),
  (match n.succ, [] with
    | 0, x => h_1 x
    | n.succ, [] => h_2 n
    | n.succ, a :: as => h_3 n a as) =
    h_2 n
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- Composition of `OrderMonoidWithZeroHom`s as an `OrderMonoidWithZeroHom`.  -/
OrderMonoidWithZeroHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : Preorder γ] →
            [inst_3 : MulZeroOneClass α] →
              [inst_4 : MulZeroOneClass β] → [inst_5 : MulZeroOneClass γ] → (β →*₀o γ) → (α →*₀o β) → α →*₀o γ
-- Mathlib.RingTheory.Finiteness.Basic
/-- The range of a linear map from a finite module is finite.  -/
Module.Finite.range : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [Module.Finite R M] (f : M →ₗ[R] N), Module.Finite R ↥f.range
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Ioc_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x y : (i : ι) → α i) [Nonempty ι],
  (Set.univ.pi fun i => Set.Ioc (x i) (y i)) ⊆ Set.Ioc x y
-- Init.Data.SInt.Lemmas
Int64.toInt_add : ∀ (a b : Int64), (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 64)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.add_linMulLin : ∀ {R : Type u_3} {M : Type u_4} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] (f g h : M →ₗ[R] A),
  QuadraticMap.linMulLin (f + g) h = QuadraticMap.linMulLin f h + QuadraticMap.linMulLin g h
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- This is the same as `ValuativeRel.ValueGroupWithZero.embed_mk`, where `embed` is upgraded to
`orderMonoidIso`.  -/
ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible] (x : R) (s : ↥(ValuativeRel.posSubmonoid R)),
  (ValuativeRel.ValueGroupWithZero.orderMonoidIso v) (ValuativeRel.ValueGroupWithZero.mk x s) =
    (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) x /
      (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) ↑s
-- Init.Control.StateCps
/-- Runs a stateful computation that's represented using continuation passing style by providing it with
an initial state and a continuation.
 -/
StateCpsT.runK : {α σ : Type u} → {m : Type u → Type v} → {β : Type u} → StateCpsT σ m α → σ → (α → σ → m β) → m β
-- Mathlib.Data.NNRat.Defs
NNRat.instNontrivial : Nontrivial ℚ≥0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functorialityEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D),
  CategoryTheory.Limits.Cone.functorialityEquivalence F e =
    { functor := CategoryTheory.Limits.Cone.functoriality F e.functor,
      inverse :=
        (CategoryTheory.Limits.Cone.functoriality (F.comp e.functor) e.inverse).comp
          (CategoryTheory.Limits.Cone.postcomposeEquivalence
              (F.associator e.functor e.inverse ≪≫ F.isoWhiskerLeft e.unitIso.symm ≪≫ F.rightUnitor)).functor,
      unitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun c =>
            CategoryTheory.Limits.Cone.ext
              (e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj c).1) ⋯)
          ⋯,
      counitIso :=
        CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cone.ext (e.counitIso.app c.pt) ⋯) ⋯,
      functor_unitIso_comp := ⋯ }
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.merge.eq_1 : ∀ {α : Type u_1} (ys : List α) (le : α → α → Bool), [].merge ys le = ys
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushoutComp_inv_app_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : P.IsStableUnderCobaseChangeAlong f]
  [inst_3 : P.IsStableUnderCobaseChangeAlong g] [inst_4 : P.HasPushoutsAlong f] [inst_5 : P.HasPushoutsAlong g]
  [inst_6 : Q.RespectsIso] [inst_7 : Q.IsStableUnderCobaseChange]
  (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g))
  (hfg :
    autoParam (fg = CategoryTheory.CategoryStruct.comp f g) CategoryTheory.MorphismProperty.Under.pushoutComp._auto_1)
  (X_1 : P.Under Q X),
  ((CategoryTheory.MorphismProperty.Under.pushoutComp f g fg hfg).inv.app X_1).right =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso X_1.hom f g).hom
      (CategoryTheory.Limits.pushout.map X_1.hom (CategoryTheory.CategoryStruct.comp f g) X_1.hom fg
        (CategoryTheory.CategoryStruct.id X_1.right) (CategoryTheory.CategoryStruct.id Z)
        (CategoryTheory.CategoryStruct.id X) ⋯ ⋯)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The centroid of a face of a simplex as the centroid of a subset of
the points.  -/
Affine.Simplex.face_centroid_eq_centroid : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1),
  Finset.centroid k Finset.univ (s.face h).points = Finset.centroid k fs s.points
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeResult.mk.inj : ∀ {capabilities : Lean.Lsp.ServerCapabilities} {serverInfo? : Option Lean.Lsp.ServerInfo}
  {capabilities_1 : Lean.Lsp.ServerCapabilities} {serverInfo?_1 : Option Lean.Lsp.ServerInfo},
  { capabilities := capabilities, serverInfo? := serverInfo? } =
      { capabilities := capabilities_1, serverInfo? := serverInfo?_1 } →
    capabilities = capabilities_1 ∧ serverInfo? = serverInfo?_1
-- Init.Data.ByteArray.Lemmas
ByteArray.data_extract : ∀ {a : ByteArray} {b e : ℕ}, (a.extract b e).data = a.data.extract b e
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, (Std.TreeSet.ofList l cmp).isEmpty = l.isEmpty
-- Init.Data.SInt.Lemmas
ISize.toInt_one : ISize.toInt 1 = 1
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The vertices in a copy of `⊤ : SimpleGraph β` are a `card β`-clique.  -/
SimpleGraph.isNClique_map_copy_top : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} [inst : Fintype β] (f : ⊤.Copy G),
  G.IsNClique (Fintype.card β) (Finset.map f.toEmbedding Finset.univ)
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomAddAct.mk_vadd_mk_aeeqFun : ∀ {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : VAdd M α] [inst_3 : MeasurableConstVAdd M α]
  [inst_4 : MeasureTheory.VAddInvariantMeasure M α μ] (c : M) (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ),
  DomAddAct.mk c +ᵥ MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk (fun x => f (c +ᵥ x)) ⋯
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvironmentHeader.mk.inj : ∀ {trustLevel : UInt32} {mainModule : Lean.Name} {isModule : Bool} {imports : Array Lean.Import}
  {regions : Array Lean.CompactedRegion} {modules : Array Lean.EffectiveImport}
  {moduleName2Idx : Std.HashMap Lean.Name Lean.ModuleIdx} {importAllModules : Array Lean.EffectiveImport}
  {moduleData : Array Lean.ModuleData} {trustLevel_1 : UInt32} {mainModule_1 : Lean.Name} {isModule_1 : Bool}
  {imports_1 : Array Lean.Import} {regions_1 : Array Lean.CompactedRegion} {modules_1 : Array Lean.EffectiveImport}
  {moduleName2Idx_1 : Std.HashMap Lean.Name Lean.ModuleIdx} {importAllModules_1 : Array Lean.EffectiveImport}
  {moduleData_1 : Array Lean.ModuleData},
  { trustLevel := trustLevel, mainModule := mainModule, isModule := isModule, imports := imports, regions := regions,
        modules := modules, moduleName2Idx := moduleName2Idx, importAllModules := importAllModules,
        moduleData := moduleData } =
      { trustLevel := trustLevel_1, mainModule := mainModule_1, isModule := isModule_1, imports := imports_1,
        regions := regions_1, modules := modules_1, moduleName2Idx := moduleName2Idx_1,
        importAllModules := importAllModules_1, moduleData := moduleData_1 } →
    trustLevel = trustLevel_1 ∧
      mainModule = mainModule_1 ∧
        isModule = isModule_1 ∧
          imports = imports_1 ∧
            regions = regions_1 ∧
              modules = modules_1 ∧
                moduleName2Idx = moduleName2Idx_1 ∧ importAllModules = importAllModules_1 ∧ moduleData = moduleData_1
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_forall_2 : ∀ {σs : List (Type u)} {α : Sort u_1} {φ : α → Prop}, ⌜∀ (x : α), φ x⌝ ⊢ₛ ∀ x, ⌜φ x⌝
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- `Proj A` is covered by `Spec (A_f)₀` for all homogeneous elements of positive degree.  -/
AlgebraicGeometry.Proj.affineOpenCover : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) → [inst_3 : GradedRing 𝒜] → (AlgebraicGeometry.Proj 𝒜).AffineOpenCover
-- Init.Internal.Order.Basic
Lean.Order.is_sup : {α : Sort u} → [Lean.Order.PartialOrder α] → (α → Prop) → α → Prop
-- Init.Core
/-- Construct a `q` if some proposition `p` is decidable, and both the truth and falsity of `p` are
sufficient to construct a `q`.

This is a synonym for `dite`, the dependent if-then-else operator.
 -/
Decidable.byCases : {p : Prop} → {q : Sort u} → [dec : Decidable p] → (p → q) → (¬p → q) → q
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- When `v` is `valuation R`, in the following commutative diagram where the first row is the map `v`
factored through its image group (with zero),
```
                                 embedding
    R –––––––––––> ValueGroup₀ v –––––-–––> ValueGroupWithZero R
    │                ∧
    │               /
    │              / embed v
    ∨             /
ValueGroupWithZero R
```
the map from `ValueGroupWithZero R` to itself is identity.
 -/
ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] (γ : ValuativeRel.ValueGroupWithZero R),
  MonoidWithZeroHom.ValueGroup₀.embedding ((ValuativeRel.ValueGroupWithZero.embed (ValuativeRel.valuation R)) γ) = γ
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_idem : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α),
  normalize (normalize x) = normalize x
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Given submodules `p i ⊆ s i`, this is the natural map: `⨂[R] i, p i → ⨂[R] i, s i`.
This is `TensorProduct.mapIncl` for an arbitrary family of modules.
 -/
PiTensorProduct.mapIncl : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            (p : (i : ι) → Submodule R (s i)) → (PiTensorProduct R fun i => ↥(p i)) →ₗ[R] PiTensorProduct R fun i => s i
-- Init.Data.List.Lemmas
List.getElem_singleton : ∀ {α : Type u_1} {a : α} {i : ℕ} (h : i < 1), [a][i] = a
-- Aesop.Builder.Basic
Aesop.PhaseSpec.safe.inj : ∀ {info info_1 : Aesop.SafeRuleInfo}, Aesop.PhaseSpec.safe info = Aesop.PhaseSpec.safe info_1 → info = info_1
-- Mathlib.Order.Cover
Set.covBy_iff_exists_sdiff_singleton : ∀ {α : Type u_1} {s t : Set α}, s ⋖ t ↔ ∃ a ∈ t, t \ {a} = s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.subtype_injective : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P) [inst_4 : Nonempty ↥s], Function.Injective ⇑s.subtype
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsExtTangentAt.wbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  s₁.IsExtTangentAt s₂ p → Wbtw ℝ s₁.center p s₂.center
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.RingCat.Colimits.descFunLift.match_1.eq_2 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (motive : RingCat.Colimits.Prequotient F → Sort u_2)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (RingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive RingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive RingCat.Colimits.Prequotient.one)
  (h_4 : (x : RingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : RingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : RingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match RingCat.Colimits.Prequotient.zero with
    | RingCat.Colimits.Prequotient.of j x => h_1 j x
    | RingCat.Colimits.Prequotient.zero => h_2 ()
    | RingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_2 ()
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodμ_unitIso_inv_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] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] (X : (A × C) × D × E),
  (CategoryTheory.prod.prodμ C D E A).unitIso.inv.app X =
    CategoryTheory.Prod.mkHom
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1.1) (CategoryTheory.CategoryStruct.id X.1.2))
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.2.1) (CategoryTheory.CategoryStruct.id X.2.2))
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- Given a morphism `g : M →ₗ[R] A'`, lift this to a morphism of type `A →ₐ[R] A'` (where `A`
satisfies the universal property of the symmetric algebra of `M`)  -/
IsSymmetricAlgebra.lift : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_3} →
            [inst_3 : CommSemiring A] →
              [inst_4 : Algebra R A] →
                {f : M →ₗ[R] A} →
                  IsSymmetricAlgebra f →
                    {A' : Type u_4} → [inst_5 : CommSemiring A'] → [inst_6 : Algebra R A'] → (M →ₗ[R] A') → A →ₐ[R] A'
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.over_iff : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] {W : CategoryTheory.MorphismProperty T} {X : T}
  {Y Z : CategoryTheory.Over X} (f : Y ⟶ Z), W.over f ↔ W (CategoryTheory.Over.Hom.left f)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app : ∀ {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 : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F] (X : C),
  CategoryTheory.CategoryStruct.comp (F.toRightDerivedZero.app X) (F.rightDerivedZeroIsoSelf.hom.app X) =
    CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.cancel_left_div_gcd' : ∀ {m a b c d : ℕ}, 0 < m → c ≡ d [MOD m] → c * a ≡ d * b [MOD m] → a ≡ b [MOD m / m.gcd c]
-- Mathlib.LinearAlgebra.Pi
LinearMap.iInf_ker_proj_le_iSup_range_single : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] {I J : Set ι},
  I.Finite → Codisjoint I J → ⨅ i ∈ J, (LinearMap.proj i).ker ≤ ⨆ i ∈ I, (LinearMap.single R φ i).range
-- Mathlib.NumberTheory.Transcendental.Liouville.Residual
/-- The set of Liouville numbers in dense.  -/
dense_liouville : Dense {x | Liouville x}
-- Lean.MetavarContext
Lean.DelayedMetavarAssignment.mvarIdPending : Lean.DelayedMetavarAssignment → Lean.MVarId
-- Mathlib.Data.Finset.Basic
Equiv.piFinsetUnion_left : ∀ {ι : Type u_5} [inst : DecidableEq ι] (α : ι → Type u_4) {s t : Finset ι} (h : Disjoint s t) {f : (i : ↥s) → α ↑i}
  {g : (i : ↥t) → α ↑i} {i : ι} (hi : i ∈ s) (hi' : i ∈ s ∪ t), (Equiv.piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.mk_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (h : 1 ∈ Set.Ioc 0 1),
  ⟨1, h⟩ = 1
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- The composition of smooth morphisms is smooth.  -/
AlgebraicGeometry.smooth_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) [AlgebraicGeometry.Smooth f]
  [AlgebraicGeometry.Smooth g], AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.sub_left : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α},
  IsUpperSet t → IsLowerSet (s - t)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.instInhabited.eq_1 : MagmaCat.instInhabited = { default := MagmaCat.of PEmpty.{u_1 + 1} }
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
/-- Given a cyclic `f : Perm α`, generate the `Cycle α` in the order
of application of `f`. Implemented by finding an element `x : α`
in the support of `f` in `Finset.univ`, and iterating on using
`Equiv.Perm.toList f x`.
 -/
Equiv.Perm.toCycle : {α : Type u_1} → [Fintype α] → [DecidableEq α] → (f : Equiv.Perm α) → f.IsCycle → Cycle α
-- Init.Data.List.Nat.Basic
List.getElem_intersperse_two_mul : ∀ {α : Type u_1} {l : List α} {sep : α} {i : ℕ} (h : 2 * i < (List.intersperse sep l).length),
  (List.intersperse sep l)[2 * i] = l[i]
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.edist_eq_iSup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, edist f g = ⨆ x, edist (f x) (g x)
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetWRT' : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν],
  MeasureTheory.SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))
-- Mathlib.Order.LiminfLimsup
limsup_max : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) limsup_max._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) limsup_max._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) limsup_max._auto_5 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) limsup_max._auto_7 →
          Filter.limsup (fun a => max (u a) (v a)) f = max (Filter.limsup u f) (Filter.limsup v f)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.fibration_op_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C],
  HomotopicalAlgebra.Fibration f.op ↔ HomotopicalAlgebra.Cofibration f
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Presentation of `log⁺` in terms of `log`.  -/
Real.half_mul_log_add_log_abs : ∀ {x : ℝ}, 2⁻¹ * (Real.log x + |Real.log x|) = x.posLog
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- If two functions agree outside of a discrete set in the circle, then their averages agree.  -/
Real.circleAverage_congr_codiscreteWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f₁ f₂ : ℂ → E} {c : ℂ} {R : ℝ},
  f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂ →
    R ≠ 0 → Real.circleAverage f₁ c R = Real.circleAverage f₂ c R
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.mk : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} {h : S.RightHomologyData}
  {F : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F →
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair h.g' 0) F → h.IsPreservedBy F
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves limits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F : Cᵒᵖ ⥤ D`
preserves colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.preservesColimit_of_rightOp : ∀ {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.Limits.PreservesLimit K.leftOp F.rightOp],
  CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainBotCoeff_zero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (β : LieModule.Weight R L M),
  LieModule.chainBotCoeff 0 β = 0
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.isOpenQuotientMap_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G},
  IsOpenQuotientMap QuotientAddGroup.mk
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂ : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r : ℤ) (pq pq' : κ),
  (c r).Rel pq pq' →
    ∀ (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_16),
      self.i₀ r pq ⋯ = self.i₂ pq'
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toSubmodule_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Injective ⇑Subalgebra.toSubmodule
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.prodL_symm_apply : ∀ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) (G' : Type wG') [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (a : ContinuousMultilinearMap 𝕜 E (G × G')),
  (ContinuousMultilinearMap.prodL 𝕜 E G G').symm a = ContinuousMultilinearMap.prodEquiv.invFun a
-- Mathlib.Topology.Algebra.InfiniteSum.Group
cauchySeq_finset_iff_tprod_vanishing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] {f : β → α},
  (CauchySeq fun s => ∏ b ∈ s, f b) ↔ ∀ e ∈ nhds 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e