mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.trivializationAt_continuousLinearMapAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) {b₀ b : B},
  b ∈ (trivializationAt F Z.Fiber b₀).baseSet →
    Bundle.Trivialization.continuousLinearMapAt R (trivializationAt F Z.Fiber b₀) b =
      Z.coordChange (Z.indexAt b) (Z.indexAt b₀) b
-- Init.SimpLemmas
iff_congr : ∀ {p₁ p₂ q₁ q₂ : Prop}, (p₁ ↔ p₂) → (q₁ ↔ q₂) → ((p₁ ↔ q₁) ↔ (p₂ ↔ q₂))
-- Mathlib.Logic.IsEmpty.Defs
Quotient.instIsEmpty : ∀ {α : Sort u} [IsEmpty α] {s : Setoid α}, IsEmpty (Quotient s)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.map_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : B × F}, x ∈ e.target → ↑e.symm x ∈ e.source
-- Mathlib.Topology.Compactness.Lindelof
/-- A set `s` is Lindelöf if for every open cover of `s`, there exists a countable subcover.  -/
isLindelof_of_countable_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  (∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i) →
    IsLindelof s
-- Mathlib.Analysis.InnerProductSpace.PiL2
PiLp.inner_apply : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {ι : Type u_7} [inst_1 : Fintype ι] {f : ι → Type u_8}
  [inst_2 : (i : ι) → NormedAddCommGroup (f i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (f i)] (x y : PiLp 2 f),
  inner 𝕜 x y = ∑ i, inner 𝕜 (x.ofLp i) (y.ofLp i)
-- Mathlib.Data.Finset.Max
Finset.min_eq_top : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α}, s.min = ⊤ ↔ s = ∅
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.inter_sdiff_distrib_left`. -/
Set.inter_diff_distrib_left : ∀ {α : Type u_1} (s t u : Set α), s ∩ (t \ u) = (s ∩ t) \ (s ∩ u)
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the monadic predicate `p` returns `true` for
all element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are
examined in order of iteration.
 -/
Std.Iter.allM : {α β : Type w} →
  {m : Type → Type w'} →
    [Monad m] → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → (β → m Bool) → Std.Iter β → m Bool
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_st : ∀ {x : ℝ*}, x.st ≠ 0 → x.IsSt x.st
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.isoBaseOfIsPrincipal.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {I : Ideal R} [hprinc : Submodule.IsPrincipal I]
  (hI : I ≠ ⊥), Ideal.isoBaseOfIsPrincipal hI = Ideal.isoBaseOfIsPrincipal hI
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.integrableOn_rpowIntegrand₁₂ : ∀ {p x : ℝ},
  p ∈ Set.Ioo 1 2 →
    0 ≤ x → MeasureTheory.IntegrableOn (fun x_1 => p.rpowIntegrand₁₂ x_1 x) (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
        (CategoryTheory.CategoryStruct.id Y))
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.comp_right : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : Ring K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {v : V₂ →ₗ[K] V₃}, v.HasNoetherianRange → ∀ (u : V →ₗ[K] V₂), (v ∘ₗ u).HasNoetherianRange
-- Mathlib.Algebra.Ring.NegOnePow
/-- The cast of `negOnePow n` to a ring equals `(-1) ^ n.natAbs`.  -/
Int.coe_negOnePow : ∀ (R : Type u_1) [inst : Ring R] (n : ℤ), ↑↑n.negOnePow = (-1) ^ n.natAbs
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_filter_le_size : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool}, m.WF → (Std.HashSet.Raw.filter f m).size ≤ m.size
-- Mathlib.Data.Set.Piecewise
Set.piecewise_eqOn : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → β),
  Set.EqOn (s.piecewise f g) f s
-- Mathlib.Algebra.Regular.ULift
ULift.isRightRegular_up : ∀ {R : Type v} [inst : Mul R] {a : R}, IsRightRegular { down := a } ↔ IsRightRegular a
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instNeg : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Neg (WithVal v)
-- Init.Data.Array.Basic
/-- Constructs an array that contains all the numbers from `0` to `n`, exclusive.

Examples:
* `Array.range 5 := #[0, 1, 2, 3, 4]`
* `Array.range 0 := #[]`
* `Array.range 1 := #[0]`
 -/
Array.range : ℕ → Array ℕ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.mk : Lean.Expr → Option ℤ → Lean.Meta.Grind.Arith.Cutsat.SymbolicBound
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousLinearMap.coe_symm_flipMultilinearEquiv : ∀ {𝕜 : 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 ι],
  ⇑(ContinuousLinearMap.flipMultilinearEquiv 𝕜 E G G').symm = ContinuousMultilinearMap.flipLinear
-- Init.Grind.Module.Basic
/-- Alternative constructor for `NoNatZeroDivisors` when we have an `IntModule`.  -/
Lean.Grind.NoNatZeroDivisors.mk' : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α],
  (∀ (k : ℕ) (a : α), k ≠ 0 → k • a = 0 → a = 0) → Lean.Grind.NoNatZeroDivisors α
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.span_gcd : ∀ {R : Type u} [inst : Ring R] (x y : R) [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})],
  Ideal.span {IsBezout.gcd x y} = Ideal.span {x, y}
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.singularPart_totalVariation : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
-- Mathlib.LinearAlgebra.Matrix.Invertible
Matrix.isUnit_transpose : ∀ {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring α]
  (A : Matrix n n α), IsUnit A.transpose ↔ IsUnit A
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.Ico_sdiff_Ioo_same`. -/
Set.Ico_diff_Ioo_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a < b → Set.Ico a b \ Set.Ioo a b = {a}
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- The isomorphism given by `Presheaf.representable.symmetry`.  -/
CategoryTheory.Functor.relativelyRepresentable.symmetryIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {Y : D} →
            {b : C} →
              {f' : F.obj b ⟶ Y} →
                (hf' : F.relativelyRepresentable f') →
                  {a : C} →
                    {g : F.obj a ⟶ Y} →
                      (hg : F.relativelyRepresentable g) → [F.Full] → [F.Faithful] → hf'.pullback g ≅ hg.pullback f'
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.AEStronglyMeasurable.compProd_mk_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {a : α} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {δ : Type u_5}
  [inst : TopologicalSpace δ] {f : β × γ → δ},
  MeasureTheory.AEStronglyMeasurable f ((κ.compProd η) a) →
    ∀ᵐ (x : β) ∂κ a, MeasureTheory.AEStronglyMeasurable (fun y => f (x, y)) (η (a, x))
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.sec.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z z_1 : S),
  z = z_1 → IsLocalization.sec M z = IsLocalization.sec M z_1
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.toNatIso_hom : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G), (CategoryTheory.Cat.Hom.toNatIso e).hom = e.hom.toNatTrans
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.ext₂' : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsTriangulatedClosed₂],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₃ → P.isoClosure T.obj₂
-- Mathlib.Order.Hom.Basic
OrderHom.comp_mono : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  ⦃g₁ g₂ : β →o γ⦄, g₁ ≤ g₂ → ∀ ⦃f₁ f₂ : α →o β⦄, f₁ ≤ f₂ → g₁.comp f₁ ≤ g₂.comp f₂
-- Mathlib.Order.ConditionallyCompleteLattice.Group
le_ciInf_mul : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : Group α] [MulRightMono α]
  {a : α} {g : ι → α} {h : α}, (∀ (i : ι), a ≤ g i * h) → a ≤ iInf g * h
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.trans_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z'),
  (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ
-- Mathlib.Algebra.Homology.FullSubcategory
HomologicalComplex.liftFunctorObjectProperty_map_f : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] {ι : Type u_2} {c : ComplexShape ι} {V : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} V] [inst_2 : CategoryTheory.Preadditive V]
  (P : CategoryTheory.ObjectProperty V) (F : CategoryTheory.Functor D (HomologicalComplex V c))
  (hF : ∀ (X : D) (n : ι), P ((F.obj X).X n)) {X Y : D} (f : X ⟶ Y) (n : ι),
  ((HomologicalComplex.liftFunctorObjectProperty P F hF).map f).f n =
    CategoryTheory.ObjectProperty.homMk ((F.map f).f n)
-- Mathlib.Data.TypeVec
/-- similar to `diag` but the target vector is a `Subtype_`
guaranteeing the equality of the components  -/
TypeVec.diagSub : {n : ℕ} → {α : TypeVec.{u} n} → α.Arrow (TypeVec.Subtype_ α.repeatEq)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The left dual of the object `X`.  -/
CategoryTheory.«termᘁ_» : Lean.ParserDescr
-- Mathlib.Data.TypeVec
TypeVec.toSubtype'_of_subtype' : ∀ {n : ℕ} {α : TypeVec.{u_1} n} (r : (α.prod α).Arrow (TypeVec.repeat n Prop)),
  TypeVec.comp (TypeVec.toSubtype' r) (TypeVec.ofSubtype' r) = TypeVec.id
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold.match_2.splitter : (n : ℕ) →
  {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u_2} →
    (motive : (x : ℕ) → x ≤ n → α (n - x) ⋯ → Sort u_1) →
      (x : ℕ) →
        (x_1 : x ≤ n) →
          (x_2 : α (n - x) ⋯) →
            ((h : 0 ≤ n) → (a : α (n - 0) ⋯) → motive 0 h a) →
              ((m : ℕ) → (h : m.succ ≤ n) → (a : α (n - m.succ) ⋯) → motive m.succ h a) → motive x x_1 x_2
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupAdd_sound : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ)
  (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd →
    f.performRupAdd c rupHints = (f', true) →
      Std.Tactic.BVDecide.LRAT.Internal.Liff (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f f'
-- Init.Data.Nat.ToString
Nat.e_eq_digitChar : ∀ {n : ℕ}, 'e' = n.digitChar ↔ n = 14
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_add_projection_eq_id`. -/
Submodule.IsCompl.projection_add_projection_eq_id : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), p.projection q hpq + q.projection p ⋯ = LinearMap.id
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.mem_dilatransvections_iff_finrank_quotient : ∀ {V : Type u_2} [inst : AddCommGroup V] {K : Type u_3} [inst_1 : DivisionRing K] [inst_2 : Module K V]
  [Module.Finite K V] {e : V ≃ₗ[K] V},
  e ∈ LinearEquiv.dilatransvections K V ↔ Module.finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.cyclesMap_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.cyclesMap (φ - φ') =
    CategoryTheory.ShortComplex.cyclesMap φ - CategoryTheory.ShortComplex.cyclesMap φ'
-- Mathlib.GroupTheory.Coprod.Basic
/-- Lift a monoid homomorphism `FreeMonoid (M ⊕ N) →* P` satisfying additional properties to
`M ∗ N →* P`. In many cases, `Coprod.lift` is more convenient.

Compared to `Coprod.lift`,
this definition allows a user to provide a custom computational behavior.
Also, it only needs `MulOneClass` assumptions while `Coprod.lift` needs a `Monoid` structure.
 -/
Monoid.Coprod.clift : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_5} →
      [inst : MulOneClass M] →
        [inst_1 : MulOneClass N] →
          [inst_2 : MulOneClass P] →
            (f : FreeMonoid (M ⊕ N) →* P) →
              f (FreeMonoid.of (Sum.inl 1)) = 1 →
                f (FreeMonoid.of (Sum.inr 1)) = 1 →
                  (∀ (x y : M),
                      f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y))) →
                    (∀ (x y : N),
                        f (FreeMonoid.of (Sum.inr (x * y))) =
                          f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y))) →
                      Monoid.Coprod M N →* P
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.toOption.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (currPos : s.Pos) (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)),
  String.Slice.SplitInclusiveIterator.toOption✝ (String.Slice.SplitInclusiveIterator.operating currPos s_1) = some s_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} {h' : k ∈ Std.ExtDTreeMap.filterMap f t},
  (Std.ExtDTreeMap.filterMap f t).getKey k h' = t.getKey k ⋯
-- Mathlib.Algebra.Group.Equiv.Defs
/-- See Note [custom simps projection]  -/
AddEquiv.Simps.symm_apply : {M : Type u_4} → {N : Type u_5} → [inst : Add M] → [inst_1 : Add N] → M ≃+ N → N → M
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_hom_left : ∀ {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.HasKernel f] [inst_6 : CategoryTheory.Limits.HasCokernel f]
  [inst_7 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_8 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_9 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_10 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_11 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_12 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_13 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))]
  [inst_14 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  (CategoryTheory.Abelian.PreservesCoimageImageComparison.iso F f).hom.left =
    (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatUInt16UintOfNatNat : Lean.Grind.ToInt.OfNat UInt16 (Lean.Grind.IntInterval.uint 16)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- The image of a family of points in affine space, under an injective affine transformation, is
affine-independent.  -/
AffineIndependent.map' : ∀ {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] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {p : ι → P},
  AffineIndependent k p → ∀ (f : P →ᵃ[k] P₂), Function.Injective ⇑f → AffineIndependent k (⇑f ∘ p)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.RingCompute.mk : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompare BaseType →
          ({x y : Q(«$α»)} →
              BaseType x →
                BaseType y →
                  Lean.MetaM
                    (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» + «$y») ×
                      Option Q(Mathlib.Meta.NormNum.IsNat («$x» + «$y») 0))) →
            ({x y : Q(«$α»)} →
                BaseType x → BaseType y → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» * «$y»))) →
              ((v : Lean.Level) →
                  (β : Q(Type v)) →
                    Q(CommSemiring «$β») →
                      (x : Q(SMul «$β» «$α»)) →
                        (x_1 : Q(«$β»)) →
                          Mathlib.Tactic.AtomM
                            ((y : Q(«$α»)) ×
                              Mathlib.Tactic.Ring.Common.ExSum BaseType sα q(«$y») ×
                                Q(∀ (a : «$α»), «$x_1» • a = «$y» * a))) →
                ({x : Q(«$α»)} →
                    (rα : Q(CommRing «$α»)) →
                      BaseType x → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(-«$x»))) →
                  ({x : Q(«$α»)} →
                      {b : Q(ℕ)} →
                        BaseType x →
                          Mathlib.Tactic.Ring.Common.ExProdNat q(«$b») →
                            OptionT Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» ^ «$b»))) →
                    ({x : Q(«$α»)} →
                        Option Q(CharZero «$α») →
                          (fα : Q(Semifield «$α»)) →
                            BaseType x →
                              Mathlib.Tactic.AtomM (Option (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x»⁻¹)))) →
                      ((x : Q(«$α»)) →
                          Lean.MetaM
                            (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum BaseType sα)
                              q(«$x»))) →
                        ({x : Q(«$α»)} → BaseType x → Option Q(Mathlib.Meta.NormNum.IsNat «$x» 1)) →
                          Mathlib.Tactic.Ring.Common.Result BaseType q(Nat.rawCast 1) →
                            Mathlib.Tactic.Ring.Common.RingCompute BaseType sα
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonCompIso.eq_1 : ∀ {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.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal],
  CategoryTheory.Functor.mapMonCompIso =
    CategoryTheory.NatIso.ofComponents
      (fun X => CategoryTheory.Mon.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapMon.obj X).X) ⋯ ⋯) ⋯
-- Mathlib.Topology.MetricSpace.Ultra.Basic
/-- All triangles are isosceles in an ultrametric space.  -/
IsUltrametricDist.dist_eq_max_of_dist_ne_dist : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x y z : X),
  dist x y ≠ dist y z → dist x z = max (dist x y) (dist y z)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.List.moveToFront : {α : Type u_1} → [Inhabited α] → List α → ℕ → List α
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.measure_prod_compl_eq_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set α} {t : Set β},
  μ sᶜ = 0 → ν tᶜ = 0 → (μ.prod ν) (s ×ˢ t)ᶜ = 0
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.instSubcanonicalCanonicalTopology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.Sheaf.canonicalTopology C).Subcanonical
-- Mathlib.Condensed.TopCatAdjunction
CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction : CategoryTheory.IsIso CondensedSet.compactlyGeneratedAdjunction.counit
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.zero_smul : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddCommMonoid X] [inst_3 : Module R X] (x : OreLocalization S X), 0 • x = 0
-- Std.Time.Format.Modifier
/-- Reserved for a future generic location format (`VVVV`). Currently formatted identically to `short`.
 -/
Std.Time.ZoneId.full : Std.Time.ZoneId
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instCoePolynomial : {K : Type u} → [inst : CommRing K] → [IsDomain K] → Coe (Polynomial K) (RatFunc K)
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.continuousOn_arcosh : ContinuousOn Real.arcosh (Set.Ici 1)
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.mul_polyOfInterest_aux1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  ∑ i ∈ Finset.range (n + 1), ↑p ^ i * WittVector.wittMul p i ^ p ^ (n - i) = WittVector.wittPolyProd p n
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- If `Y Y'` have an exact pairing,
then the functor `tensorLeft Y'` is left adjoint to `tensorLeft Y`.
 -/
CategoryTheory.tensorLeftAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (Y Y' : C) →
        [CategoryTheory.ExactPairing Y Y'] →
          CategoryTheory.MonoidalCategory.tensorLeft Y' ⊣ CategoryTheory.MonoidalCategory.tensorLeft Y
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_sub_self_left : ∀ {m n : ℕ}, m ≤ n → ((n - m).Coprime m ↔ n.Coprime m)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsFibrant Y],
  HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass =
    HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass
-- Lean.Elab.Level
Lean.Elab.Level.LevelElabM : Type → Type