mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.QPF.Univariate.Basic
QPF.corecF_eq : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (g : α → F α) (x : α),
  (QPF.corecF g x).dest = (QPF.P F).map (QPF.corecF g) (QPF.repr (g x))
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.measurable_densityProcess_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) {s : Set β} (a : α),
  MeasurableSet s → Measurable fun x => κ.densityProcess ν n a x s
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.IsHomLift.isoOfIsoLift.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p p_1 : CategoryTheory.Functor 𝒳 𝒮) (e_p : p = p_1) {R S : 𝒮} {a b : 𝒳} (f f_1 : R ⟶ S) (e_f : f = f_1)
  (φ φ_1 : a ≅ b) (e_φ : φ = φ_1) [inst_2 : p.IsHomLift f φ.hom],
  CategoryTheory.IsHomLift.isoOfIsoLift p f φ = CategoryTheory.IsHomLift.isoOfIsoLift p_1 f_1 φ_1
-- Mathlib.GroupTheory.Subsemigroup.Center
AddSubsemigroup.mem_center_iff : ∀ {M : Type u_1} [inst : AddSemigroup M] {z : M}, z ∈ AddSubsemigroup.center M ↔ ∀ (g : M), g + z = z + g
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft W)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso X₁ X₂).hom.right =
    (CategoryTheory.MonoidalCategoryStruct.associator W X₁.right X₂.right).inv
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- The quotient by the dual is isomorphic to its dual annihilator.  -/
Subspace.quotDualEquivAnnihilator : {K : Type u_1} →
  {V : Type u_2} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          [FiniteDimensional K V] →
            (W : Subspace K V) → (Module.Dual K V ⧸ W.dualLift.range) ≃ₗ[K] ↥(Submodule.dualAnnihilator W)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_ofNat_le_lift : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.beth (OfNat.ofNat n) ≤ Cardinal.lift.{v, u} c ↔ Cardinal.beth (OfNat.ofNat n) ≤ c
-- Mathlib.Topology.UniformSpace.Cauchy
/-- If the sequence `SequentiallyComplete.seq` converges to `a`, then `f ≤ 𝓝 a`.  -/
SequentiallyComplete.le_nhds_of_seq_tendsto_nhds : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α}
  (U_mem : ∀ (n : ℕ), U n ∈ uniformity α),
  (∀ s ∈ uniformity α, ∃ n, U n ⊆ s) →
    ∀ ⦃a : α⦄, Filter.Tendsto (SequentiallyComplete.seq hf U_mem) Filter.atTop (nhds a) → f ≤ nhds a
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃ObjObj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6)
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃),
  (CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂).obj F₃ =
    CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃
-- Mathlib.Order.Hom.Lattice
OrderIsoClass.toInfHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : SemilatticeInf α]
  [inst_2 : SemilatticeInf β] [OrderIsoClass F α β], InfHomClass F α β
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.coe_valMinAbs : ∀ {n : ℕ} (x : ZMod n), ↑x.valMinAbs = x
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCancelCommMonoidOfAddOpposite : {M : Type u_1} → [AddCancelCommMonoid Mᵃᵒᵖ] → AddCancelCommMonoid Mᵈᵃᵃ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintLabelPart.toJson : Lean.Lsp.InlayHintLabelPart → Lean.Json
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorComm_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (a b p : ℤ),
  ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p = (HomologicalComplex.XIsoOfEq K ⋯).hom
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_id : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G), Subgroup.map (MonoidHom.id G) K = K
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roc.forIn'_eq_match.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (x : Option α) → (x = none → motive none) → ((next : α) → x = some next → motive (some next)) → motive x
-- Lean.Meta.Tactic.Grind.Extension
/-- Grind patterns may have constraints associated with them.
 -/
Lean.Meta.Grind.EMatchTheoremConstraint : Type
-- Mathlib.Algebra.Order.IsBotOne
IsBotZeroClass.isBot_zero : ∀ {α : Type u_1} {inst : LE α} {inst_1 : Zero α} [self : IsBotZeroClass α], IsBot 0
-- Mathlib.Algebra.Group.WithOne.Defs
_private.Mathlib.Algebra.Group.WithOne.Defs.0.WithZero.unzero.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : WithZero α) → x ≠ 0 → Sort u_2) (x : α) (x_1 : ↑x ≠ 0)
  (h_1 : (x : α) → (x_2 : ↑x ≠ 0) → motive (some x) x_2),
  (match some x, x_1 with
    | some x, x_2 => h_1 x x_2) =
    h_1 x x_1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipPrefixWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.toSlice.skipPrefixWhile pat = (s.skipPrefixWhile pat).toSlice
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.instDecidableEqQuotientSubgroupOfDecidablePredMem.eq_1 : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) [inst_1 : DecidablePred fun x => x ∈ s],
  QuotientGroup.instDecidableEqQuotientSubgroupOfDecidablePredMem s = Quotient.decidableEq
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.coeff_erase_same : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α),
  ((SkewMonoidAlgebra.erase a) f).coeff a = 0
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- A connected object `X` of `C` is Galois if the quotient `X / Aut X` is terminal.  -/
CategoryTheory.PreGaloisCategory.IsGalois : {C : Type u₁} → [inst : CategoryTheory.Category.{u₂, u₁} C] → [CategoryTheory.GaloisCategory C] → C → Prop
-- Mathlib.Algebra.Group.Submonoid.Operations
AddEquiv.addSubmonoidMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M),
  e.addSubmonoidMap S = { toEquiv := (↑e).image ↑S, map_add' := ⋯ }
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_of_indep_of_le_right : ∀ {Ω : Type u_1} {m₁ m₂ m₃ _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.Indep m₁ m₂ μ → m₃ ≤ m₂ → ProbabilityTheory.Indep m₁ m₃ μ
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.preimage_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Set.preimage ⇑h.symm = Set.image ⇑h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.forM_eq_forM_toArray : ∀ {α : Type u} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Monad m]
  [LawfulMonad m] {f : α → β → m PUnit.{w + 1}},
  Std.DTreeMap.Internal.Impl.forM f t = Array.forM (fun a => f a.1 a.2) (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Init.Data.Int.Basic
Int.instLawfulBEq : LawfulBEq ℤ
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.congr_of_eventuallyEq_insert : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → f₁ =ᶠ[nhdsWithin x (insert x s)] f → ContDiffWithinAt 𝕜 n f₁ s x
-- Init.Data.BitVec.Lemmas
BitVec.not_lt_zero : ∀ {w : ℕ} {x : BitVec w}, ¬x < 0#w
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.continuous_iff : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] [Topology.IsGeneratedBy X Y] (g : Y → Z),
  Continuous g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous (g ∘ ⇑f)
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddCommGrpCat)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.eq_true_of_isValid : ∀ (ctx : Nat.Internal.Linear.Context) (c : Nat.Internal.Linear.ExprCnstr),
  c.toNormPoly.isValid = true → Nat.Internal.Linear.ExprCnstr.denote ctx c = True
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_eq_some_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.minKey? = some t.minKey!
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instMax.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E],
  AddGroupSeminorm.instMax = { max := fun p q => { toFun := ⇑p ⊔ ⇑q, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }
-- Mathlib.Data.Nat.PrimeFin
Nat.primeFactors_pow_succ : ∀ (n k : ℕ), (n ^ (k + 1)).primeFactors = n.primeFactors
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instEmptyCollection : {α : Type u} → EmptyCollection (Std.HashSet.Raw α)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Zipper.done.toList = []
-- Mathlib.Analysis.Complex.Basic
Complex.equivRealProd_apply_le' : ∀ (z : ℂ), ‖Complex.equivRealProd z‖ ≤ 1 * ‖z‖
-- Mathlib.Analysis.Convex.Function
ConvexOn.convex_strict_epigraph : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β} [ZeroLEOneClass 𝕜],
  ConvexOn 𝕜 s f → Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 < p.2}
-- Mathlib.Algebra.Ring.Defs
/-- A `Semiring` is a type with addition, multiplication, a `0` and a `1` where addition is
commutative and associative, multiplication is associative and left and right distributive over
addition, and `0` and `1` are additive and multiplicative identities.  -/
Semiring : Type u → Type u
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.snd_smul : ∀ {ι : Type u_1} {α : Type u_3} {A : ι → Type u_2} [inst : (i : ι) → SMul α (A i)] (a : α) (x : GradedMonoid A),
  (a • x).snd = a • x.snd
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
/-- The Yoneda embedding for preadditive categories sends an object `Y` to the presheaf sending an
object `X` to the `End Y`-module of morphisms `X ⟶ Y`.
 -/
CategoryTheory.preadditiveYonedaObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (Y : C) → CategoryTheory.Functor Cᵒᵖ (ModuleCat (CategoryTheory.End Y))
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsFragment.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (K : ℝ) (S A : Finset G),
  Finset.IsFragment✝ K S A = (Finset.expansion✝ K S A = Finset.connectivity✝ K S)
-- Mathlib.FieldTheory.Finite.GaloisField
instCharPGaloisField : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (n : ℕ), CharP (GaloisField p n) p
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_negative : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v w : Set α},
  MeasurableSet u →
    MeasurableSet v →
      MeasurableSet w →
        MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u →
          MeasureTheory.VectorMeasure.restrict s v ≤ MeasureTheory.VectorMeasure.restrict 0 v →
            s (symmDiff u v) = 0 → s (w ∩ u) = s (w ∩ v)
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toOplaxFunctor'_map : ∀ {I : Type u_1} {B : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} I] [inst_1 : CategoryTheory.Bicategory B]
  [inst_2 : CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B)
  {X Y : CategoryTheory.LocallyDiscrete I} (x : X ⟶ Y),
  F.toOplaxFunctor'.map x =
    match x with
    | { as := f } => F.map f
-- Mathlib.Algebra.GradedMonoid
/-- When all the indexed types are the same, the dependent product is just the regular product.  -/
List.dProd_monoid : ∀ (ι : Type u_1) {R : Type u_2} {α : Type u_3} [inst : AddMonoid ι] [inst_1 : Monoid R] (l : List α) (fι : α → ι)
  (fA : α → R), l.dProd fι fA = (List.map fA l).prod
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
_private.Mathlib.AlgebraicGeometry.Morphisms.Basic.0.AlgebraicGeometry.HasAffineProperty.pullback_fst_of_right : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q],
  Q.IsStableUnderBaseChange →
    ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [inst : AlgebraicGeometry.IsAffine S],
      Q g → P (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `UniqueMul` is preserved under embeddings that are multiplicative.

See `UniqueMul.mulHom_image_iff` for a version with swapped bundling.  -/
UniqueMul.mulHom_map_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] {A B : Finset G} {a0 b0 : G} (f : G ↪ H),
  (∀ (x y : G), f (x * y) = f x * f y) →
    (UniqueMul (Finset.map f A) (Finset.map f B) (f a0) (f b0) ↔ UniqueMul A B a0 b0)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_pos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀},
  0 < a → 0 < b → 0 < a / b
-- Mathlib.Analysis.Analytic.Constructions
formalMultilinearSeries_geometric_radius : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [NormOneClass A], (formalMultilinearSeries_geometric 𝕜 A).radius = 1
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mergeGrind? : Lean.TSyntax `tactic → Lean.TSyntax `tactic → Option (Lean.TSyntax `tactic)
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.right : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [CategoryTheory.MonoidalCoherence X Y] →
          CategoryTheory.MonoidalCoherence
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.mapPushoutAdj_unit_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushoutsAlong f] (X_1 : CategoryTheory.Under X),
  (CategoryTheory.Under.mapPushoutAdj f).unit.app X_1 =
    CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.inl X_1.hom f) ⋯
-- Aesop.Rule.Name
Aesop.BuilderName.unfold.sizeOf_spec : sizeOf Aesop.BuilderName.unfold = 1
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.UnfoldLift.read : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {ρ : Type u} [inst : MonadLift m n] [inst_1 : MonadReaderOf ρ m],
  MonadReaderOf.read = monadLift MonadReaderOf.read
-- Mathlib.Tactic.NormNum.Core
/-- Constructs a simp context from the simp argument syntax.  -/
Mathlib.Meta.NormNum.getSimpContext : Lean.Syntax → Lean.Syntax → optParam Bool false → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Context
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- the colimit of `F` identifies to `Y`  -/
CategoryTheory.TransfiniteCompositionOfShape.isColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {X Y : C} →
            {f : X ⟶ Y} →
              [inst_3 : SuccOrder J] →
                [inst_4 : WellFoundedLT J] →
                  (self : CategoryTheory.TransfiniteCompositionOfShape J f) →
                    CategoryTheory.Limits.IsColimit { pt := Y, ι := self.incl }
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instPartialOrderFiniteIndexNormalSubgroup : {G : Type u_1} → [inst : Group G] → PartialOrder (FiniteIndexNormalSubgroup G)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- In a Turán-maximal graph, non-adjacent vertices have the same degree.  -/
SimpleGraph.IsTuranMaximal.degree_eq_of_not_adj : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} {s t : V},
  G.IsTuranMaximal r → ¬G.Adj s t → G.degree s = G.degree t
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.of_fac : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S),
  f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp (p.map φ) (CategoryTheory.eqToHom hb)) →
    p.IsHomLift f φ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α} {k : α} {h : k ∈ Std.HashMap.Raw.unitOfList l},
  (Std.HashMap.Raw.unitOfList l)[k] = ()
-- Init.Data.String.Search
String.revFind : String → (Char → Bool) → Option String.Pos.Raw
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.isZero_single_obj_X : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : V) (i : ι), i ≠ j → CategoryTheory.Limits.IsZero (((HomologicalComplex.single V c j).obj A).X i)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_id : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat),
  AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (CategoryTheory.CategoryStruct.id X) x =
    CategoryTheory.CategoryStruct.id (X.presheaf.stalk x)
-- Batteries.Control.AlternativeMonad
AlternativeMonad.mk : {m : Type u_1 → Type u_2} → [toAlternative : Alternative m] → [toBind : Bind m] → AlternativeMonad m
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.subMulAction.eq_1 : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] (n : ℕ) [inst_2 : DecidableEq α],
  Set.powersetCard.subMulAction G α n = { carrier := Set.powersetCard α n, smul_mem' := ⋯ }
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map.id' : ∀ {α : Type u} (x : FreeGroup α), (FreeGroup.map fun z => z) x = x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.unit_smul_eq_zero : ∀ {K : Type u_1} [inst : Field K] (u : (NumberField.RingOfIntegers K)ˣ) (x : NumberField.mixedEmbedding.mixedSpace K),
  u • x = 0 ↔ x = 0
-- Init.Core
Lean.Name.str.inj : ∀ {pre : Lean.Name} {str : String} {pre_1 : Lean.Name} {str_1 : String},
  pre.str str = pre_1.str str_1 → pre = pre_1 ∧ str = str_1
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.instOrElseFormatterM : {α : Type} → OrElse (Lean.PrettyPrinter.FormatterM α)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.containsKey.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = (k == a || Std.Internal.List.containsKey a l)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.HasTwoOutOfThreeProperty
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instZero : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [Zero M] → Zero (l.Germ M)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.continuousOn_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ContinuousOn (↑e.symm) e.target
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_pow : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (x : ↥S) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.snd_orthogonalDecomposition_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (x : E),
  (K.orthogonalDecomposition x).snd = Kᗮ.orthogonalProjectionOnto x
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.Action.instAndThen : AndThen Lean.Meta.Grind.Action
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.mem_cocycles₁_of_addMonoidHom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} [A.IsTrivial] (f : Additive G →+ ↑A),
  ⇑f ∘ ⇑Additive.ofMul ∈ groupCohomology.cocycles₁ A
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
          k ∈ List.map Sigma.fst toInsert → Std.Internal.List.getKey! k' (Std.Internal.List.insertList l toInsert) = k
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_eq_top_iff : ∀ {x : ENNReal}, ↑x = ⊤ ↔ x = ⊤
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The canonical morphism `K.truncLE e ⟶ K` when `e` is an embedding of complex
shapes which satisfy `e.IsTruncLE`.  -/
HomologicalComplex.ιTruncLE : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncLE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      [inst_4 : CategoryTheory.Limits.HasZeroObject C] → K.truncLE e ⟶ K
-- Batteries.Data.List.Lemmas
List.disjoint_of_disjoint_append_left_right : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l → l₂.Disjoint l
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MeasurePreserving.integrable_comp : ∀ {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : MeasurableSpace δ] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε] {ν : MeasureTheory.Measure δ}
  {g : δ → ε} {f : α → δ},
  MeasureTheory.MeasurePreserving f μ ν →
    MeasureTheory.AEStronglyMeasurable g ν → (MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable g ν)