mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Perm
List.Perm.append : ∀ {α : Type u_1} {l₁ l₂ t₁ t₂ : List α}, l₁.Perm l₂ → t₁.Perm t₂ → (l₁ ++ t₁).Perm (l₂ ++ t₂)
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.frobeniusMorphism_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {A B : C} (f : A ⟶ B)
  (A' : CategoryTheory.Subobject A) (B' : CategoryTheory.Subobject B),
  CategoryTheory.IsPullback (CategoryTheory.Regular.frobeniusMorphism f A' B')
    ((A' ⊓ (CategoryTheory.Subobject.pullback f).obj B').ofLE A' ⋯)
    (((CategoryTheory.Subobject.exists f).obj A' ⊓ B').ofLE ((CategoryTheory.Subobject.exists f).obj A') ⋯)
    (CategoryTheory.Subobject.imageFactorisation f A').F.e
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapRingEquiv_trans : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : AddMonoid M] (e₁ : R ≃+* S) (e₂ : S ≃+* T),
  AddMonoidAlgebra.mapRingEquiv M (e₁.trans e₂) =
    (AddMonoidAlgebra.mapRingEquiv M e₁).trans (AddMonoidAlgebra.mapRingEquiv M e₂)
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitude_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)),
  (s.map f.toAffineMap ⋯).altitude i = AffineSubspace.map f.toAffineMap (s.altitude i)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.g_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [inst_3 : CategoryTheory.Epi S.g],
  CategoryTheory.CategoryStruct.comp S.g (hS.desc k hk) = k
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'_star : ∀ {α : Type u_1} (P : RegularExpression α), P.star.matches' = KStar.kstar P.matches'
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIco_comp_apply : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] {α : Type u_3} {β : Type u_4} {f : 𝕜 → α} {g : α → β} {a : 𝕜}
  {x : AddCircle p}, AddCircle.liftIco p a (g ∘ f) x = g (AddCircle.liftIco p a f x)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- Composition of morphisms of `PresheafedSpace`s.  -/
AlgebraicGeometry.PresheafedSpace.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : AlgebraicGeometry.PresheafedSpace C} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.instNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (S : C),
  Nonempty (J.OneHypercover S)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field contains the ring's 0.  -/
IntermediateField.zero_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  0 ∈ S
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.toList_intermediateDropWhile_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} {dropping : Bool} [Std.Iterators.Finite α Id]
  {it : Std.Iter β},
  (Std.Iter.Intermediate.dropWhile P dropping it).toList =
    if dropping = true then List.dropWhile P it.toList else it.toList
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.mk.inj : ∀ {m : Type w → Type w'} {α : Type v} {Property : α → Prop} {small : Std.Internal.Small (Subtype Property)}
  {operation : m (Std.Internal.USquash (Subtype Property))} {Property_1 : α → Prop}
  {small_1 : Std.Internal.Small (Subtype Property_1)} {operation_1 : m (Std.Internal.USquash (Subtype Property_1))},
  { Property := Property, small := small, operation := operation } =
      { Property := Property_1, small := small_1, operation := operation_1 } →
    Property = Property_1 ∧ operation ≍ operation_1
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instSemilatticeInfOpenNormalSubgroup : {G : Type u} → [inst : Group G] → [inst_1 : TopologicalSpace G] → SemilatticeInf (OpenNormalSubgroup G)
-- Mathlib.SetTheory.ZFC.Class
Class.iota_val : ∀ (A : Class.{u_1}) (x : ZFSet.{u_1}), (∀ (y : ZFSet.{u_1}), A y ↔ y = x) → A.iota = ↑x
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.rightOp_functor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ D) (X : C), e.rightOp.functor.obj X = Opposite.op (e.functor.obj (Opposite.op X))
-- Lean.Structure
Lean.instInhabitedStructureFieldInfo : Inhabited Lean.StructureFieldInfo
-- Std.Internal.Do.WP.Conjunctive
/-- `ReaderT` lifts conjunctivity from its base monad.  -/
Std.Internal.Do.ReaderT.instWPConjunctive : ∀ {m : Type u → Type v} {ρ : Type u} {Pred : Type w} {EPred : Type z} {α : Type u} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [Std.Internal.Do.WPConjunctive (m α) α Pred EPred],
  Std.Internal.Do.WPConjunctive (ReaderT ρ m α) α (ρ → Pred) EPred
-- Mathlib.Data.Nat.MaxPowDiv
padicValNat_base_pow_mul : ∀ {p n : ℕ}, 1 < p → n ≠ 0 → ∀ (k : ℕ), padicValNat p (p ^ k * n) = padicValNat p n + k
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.stabilizerEquivStabilizer_symm_apply : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g • a)
  (x : ↥(MulAction.stabilizer G b)), ↑((MulAction.stabilizerEquivStabilizer hg).symm x) = (MulAut.conj g⁻¹) ↑x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ} {k : α},
  t.WF →
    (k ∈ Std.DTreeMap.Raw.filterMap f t ↔
      ∃ (h : k ∈ t), (f (t.getKey k h) (Std.DTreeMap.Raw.Const.get t k h)).isSome = true)
-- Mathlib.Analysis.Normed.Group.Constructions
nnnorm_le_pi_nnnorm' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i)
  (i : ι), ‖f i‖₊ ≤ ‖f‖₊
-- Mathlib.Order.CompleteLattice.Basic
iInf_sigma' : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {κ : β → Type u_8} (f : (i : β) → κ i → α),
  ⨅ i, ⨅ j, f i j = ⨅ x, f x.fst x.snd
-- Mathlib.Order.BooleanAlgebra.Basic
sup_inf_sdiff : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x y : α), x ⊓ y ⊔ x \ y = x
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.mul : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    {F : CategoryTheory.Functor J MonCat} →
      MonCat.Colimits.Prequotient F → MonCat.Colimits.Prequotient F → MonCat.Colimits.Prequotient F
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.Config.mk.inj : ∀ {toConfig : Mathlib.Tactic.AtomM.Recurse.Config} {ifUnchanged : Mathlib.Tactic.BehaviorIfUnchanged}
  {mode : Mathlib.Tactic.RingNF.RingMode} {toConfig_1 : Mathlib.Tactic.AtomM.Recurse.Config}
  {ifUnchanged_1 : Mathlib.Tactic.BehaviorIfUnchanged} {mode_1 : Mathlib.Tactic.RingNF.RingMode},
  { toConfig := toConfig, ifUnchanged := ifUnchanged, mode := mode } =
      { toConfig := toConfig_1, ifUnchanged := ifUnchanged_1, mode := mode_1 } →
    toConfig = toConfig_1 ∧ ifUnchanged = ifUnchanged_1 ∧ mode = mode_1
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
/-- [Stacks Tag 0951](https://stacks.math.columbia.edu/tag/0951) -/
AlgebraicGeometry.WeaklyEtale.instHasOfPostcompPropertyScheme : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.WeaklyEtale @AlgebraicGeometry.WeaklyEtale
-- Mathlib.MeasureTheory.Group.AEStabilizer
MulAction.aestabilizer.eq_1 : ∀ (G : Type u_1) {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ] (s : Set α),
  MulAction.aestabilizer G μ s = { carrier := {g | g • s =ᵐ[μ] s}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Order.CompleteBooleanAlgebra
Pi.instCompleteAtomicBooleanAlgebra : {ι : Type u_1} →
  {π : ι → Type u_2} → [(i : ι) → CompleteAtomicBooleanAlgebra (π i)] → CompleteAtomicBooleanAlgebra ((i : ι) → π i)
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.mk.sizeOf_spec : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] [inst_8 : SizeOf R] [inst_9 : SizeOf L] [inst_10 : SizeOf M]
  [inst_11 : SizeOf N] (toLieModuleHom : M →ₗ⁅R,L⁆ N) (invFun : N → M)
  (left_inv : Function.LeftInverse invFun (↑toLieModuleHom).toFun)
  (right_inv : Function.RightInverse invFun (↑toLieModuleHom).toFun),
  sizeOf { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    1 + sizeOf toLieModuleHom
-- Mathlib.Topology.Order.Basic
le_mem_nhds : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {a b : α},
  a < b → ∀ᶠ (x : α) in nhds b, a ≤ x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The canonical map `(X ⟶ Y) → Ext X Y 0`.  -/
CategoryTheory.Abelian.Ext.mk₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] → {X Y : C} → (X ⟶ Y) → CategoryTheory.Abelian.Ext X Y 0
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instCommRing : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → CommRing (AdicCompletion I R)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hurwitzZetaEven_residue_one : ∀ (a : UnitAddCircle), Filter.Tendsto (fun s => (s - 1) * HurwitzZeta.hurwitzZetaEven a s) (nhdsWithin 1 {1}ᶜ) (nhds 1)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.mem_extChartAt_source_of_eq_one : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s) {i : ι}
  {x : M}, ↑(fs.toFun i) x = 1 → x ∈ (extChartAt I (fs.c i)).source
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.congr : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X Y : T → Ω → E},
  ProbabilityTheory.IsAEKolmogorovProcess X P p q M →
    (∀ (t : T), X t =ᵐ[P] Y t) → ProbabilityTheory.IsAEKolmogorovProcess Y P p q M
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v : MeasureTheory.VectorMeasure α M) {i : Set α},
  MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i → 0 ≤ v i
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.instCommRingRingOfIntegers : (K : Type u_1) → [inst : Field K] → CommRing (NumberField.RingOfIntegers K)
-- Mathlib.Data.Set.SymmDiff
Set.subset_symmDiff_union_symmDiff_right : ∀ {α : Type u} {s t u : Set α}, Disjoint t u → s ⊆ symmDiff s t ∪ symmDiff s u
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isRetrocompact_zeroLocus_compl : ∀ {R : Type u} [inst : CommSemiring R] {s : Set R}, s.Finite → IsRetrocompact (PrimeSpectrum.zeroLocus s)ᶜ
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D)
  [inst_5 : F.Additive] {M N : CategoryTheory.Mat_ C} (f : M ⟶ N),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv (F.map f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j)))
      (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).inv
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_one_right' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a : α), Associated (gcd a 1) 1
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.InducingFunctorData.tensorHom_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategoryStruct D]
  {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) {X₁ Y₁ X₂ Y₂ : D}
  (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    CategoryTheory.CategoryStruct.comp (self.μIso X₁ X₂).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
        (self.μIso Y₁ Y₂).hom)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (t : CategoryTheory.Limits.Cone G) (w : F ≅ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift G t)
      (CategoryTheory.Limits.HasLimit.isoOfNatIso w).inv =
    CategoryTheory.Limits.limit.lift F ((CategoryTheory.Limits.Cone.postcompose w.inv).obj t)
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Section.mk.sizeOf_spec : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} [inst_3 : SizeOf N] [inst_4 : SizeOf E] [inst_5 : SizeOf G] (toFun : G → E)
  (rightInverse_rightHom : Function.RightInverse toFun ⇑S.rightHom),
  sizeOf { toFun := toFun, rightInverse_rightHom := rightInverse_rightHom } = 1
-- Mathlib.Probability.Kernel.Disintegration.Basic
MeasureTheory.Measure.IsCondKernel.isProbabilityMeasure : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω))
  (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [MeasureTheory.IsFiniteMeasure ρ]
  [MeasurableSingletonClass α] {a : α}, ρ.fst {a} ≠ 0 → MeasureTheory.IsProbabilityMeasure (ρCond a)
-- Mathlib.Order.Basic
LE.ext : ∀ {α : Type u} {x y : LE α}, LE.le = LE.le → x = y
-- Init.Data.FloatArray.Basic
FloatArray.get! : FloatArray → ℕ → Float
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.intCast.injEq : ∀ (k k_1 : ℤ), (Lean.Grind.CommRing.Expr.intCast k = Lean.Grind.CommRing.Expr.intCast k_1) = (k = k_1)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.has_zero_object : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.NonPreadditiveAbelian C],
  CategoryTheory.Limits.HasZeroObject C
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Coercion of an `AddMonoidHom` into a function is itself
an `AddMonoidHom`.

See also `AddMonoidHom.eval`.  -/
AddMonoidHom.coeFn : (α : Type u_5) → (β : Type u_6) → [inst : AddZeroClass α] → [inst_1 : AddCommMonoid β] → (α →+ β) →+ α → β
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.iso_inv_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesImage.iso F f).inv
      (F.map (CategoryTheory.Abelian.image.ι f)) =
    CategoryTheory.Abelian.image.ι (F.map f)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
/-- In a Banach space `E` with a measure `μ`, then for any `f : α → E`, we have
`‖𝔼[f | m]‖ ≤ᵐ[μ] 𝔼[‖f‖ | m]`.  -/
norm_condExp_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2}
  {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → E),
  (fun x => ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun x => ‖f x‖ | m]
-- Mathlib.Analysis.Matrix.Order
/-- A positive semi-definite matrix is positive definite if and only if it is invertible.  -/
Matrix.PosSemidef.posDef_iff_isUnit : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {x : Matrix n n 𝕜},
  x.PosSemidef → (x.PosDef ↔ IsUnit x)
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mkAux.eq_def : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0)
  (x : ℕ),
  ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ x =
    match x with
    | 0 => { X₁ := X₂, X₂ := X₁, X₃ := X₀, f := d₁, g := d₀, zero := s }
    | n.succ =>
      { X₁ := (succ (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).fst,
        X₂ := (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₁, X₃ := (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₂,
        f := (succ (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst,
        g := (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f, zero := ⋯ }
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_interval_add_Ioi' : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b →
    MeasureTheory.IntegrableOn f (Set.Ioi b) μ →
      ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Set.Ioi b, f x ∂μ = ∫ (x : ℝ) in Set.Ioi a, f x ∂μ
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_iff : ∀ {n : ℤ}, Odd n ↔ n % 2 = 1
-- Mathlib.RingTheory.Morita.Matrix
MatrixModCat.toModuleCatObj.congr_simp : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (M : Type u_1)
  [inst_3 : AddCommGroup M] [inst_4 : Module (Matrix ι ι R) M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R (Matrix ι ι R) M] (i i_1 : ι),
  i = i_1 → MatrixModCat.toModuleCatObj R M i = MatrixModCat.toModuleCatObj R M i_1
-- Std.Time.Time.Unit.Nanosecond
/-- Creates an `Ordinal` from a `Fin`, ensuring the value is within bounds.
 -/
Std.Time.Nanosecond.Ordinal.ofFin : Fin 1000000000 → Std.Time.Nanosecond.Ordinal
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph0_le_aleph : ∀ (o : Ordinal.{u_1}), Cardinal.aleph0 ≤ Cardinal.aleph o
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) (X : C),
  ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).obj X =
    Opposite.op ((Opposite.unop F).obj (Opposite.op X))
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.Integrable.inner_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {f : α → E},
  MeasureTheory.Integrable f μ → ∀ (c : E), MeasureTheory.Integrable (fun x => inner 𝕜 (f x) c) μ
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNonUnitalCommRing : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [NonUnitalCommRing Y] → NonUnitalCommRing (LocallyConstant X Y)
-- Aesop.Forward.State
Aesop.instInhabitedVariableMap.default : Aesop.VariableMap
-- Plausible.Random
/-- A monad to generate random objects using the generator type `g`.  -/
Plausible.RandG : Type → Type u_1 → Type u_1
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.comp_eq_id : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.LeftInverse f g → f ∘ g = id
-- Init.Sym.Lemmas
Lean.Sym.Int.dvd_eq_true : ∀ (a b : ℤ), decide (a ∣ b) = true → (a ∣ b) = True
-- Mathlib.Order.Filter.Extr
isMinOn_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMinOn f s a ↔ ∀ x ∈ s, f a ≤ f x
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.EStateM.tryCatch.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) →
        ((ok : EStateM.Result ε σ α) → (∀ (e : ε) (s : σ), ok = EStateM.Result.error e s → False) → motive ok) →
          motive x
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.IsAffineOpen.fromSpecStalk_isPreimmersion : ∀ {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↥X} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥X)
  (hx : x ∈ U), AlgebraicGeometry.IsPreimmersion (hU.fromSpecStalk hx)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ NumberField.mixedEmbedding.fundamentalCone K → 0 < NumberField.mixedEmbedding.norm x
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_one_add_of_lt : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R}, v x < 1 → v (1 + x) = 1
-- Init.Data.NeZero
instNeZeroNatHMul : ∀ {n m : ℕ} [hn : NeZero n] [hm : NeZero m], NeZero (n * m)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.mdifferentiable' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] (s : ContMDiffSection I F n V),
  n ≠ 0 → MDiff fun x => ⟨x, s x⟩
-- Batteries.Data.Array.Pairwise
Array.pairwise_extract : ∀ {α : Type u_1} {R : α → α → Prop} {as : Array α},
  Array.Pairwise R as → ∀ (start stop : ℕ), Array.Pairwise R (as.extract start stop)
-- Mathlib.Data.Rel
SetRel.cod_inv : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.inv.cod = R.dom
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign.eq_1 : ∀ (θ : Real.Angle), θ.sign = SignType.sign θ.sin
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppCategory : Lean.Name → Lean.Syntax → Lean.CoreM Std.Format