mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Range
_private.Init.Data.Array.Range.0.Array.ofFn.go.eq_1 : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (acc : Array α) (i_1 : ℕ) (h : i_1 + 1 ≤ n),
  Array.ofFn.go✝ f acc i_1.succ h = Array.ofFn.go✝ f (acc.push (f ⟨n - i_1 - 1, ⋯⟩)) i_1 ⋯
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_pf_zero_add : ∀ {R : Type u_1} [inst : CommSemiring R] (b : R), 0 + b = b
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_iSizeToBitVec : ∀ (x : ISize), Int32.ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.mem_inv_pointwise_smul_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] {a : α}
  {S : Subgroup G} {x : G}, x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.NumberTheory.Divisors
Nat.pairwise_divisorsAntidiagonalList_fst : ∀ {n : ℕ}, List.Pairwise (fun x1 x2 => x1.1 < x2.1) n.divisorsAntidiagonalList
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.termα_ : Lean.ParserDescr
-- Aesop.Search.Expansion.Norm
Aesop.runNormSteps : Lean.MVarId → (steps : Array Aesop.NormStep) → 0 < steps.size → Aesop.NormM Aesop.NormSeqResult
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity holds if and only if all distances are proportional with a positive real ratio.  -/
similar_iff_exists_pos_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ ↔ ∃ r, 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
-- Mathlib.Topology.Sets.Opens
/-- the coercion `Opens α → Set α` applied to a pair is the same as taking the first component  -/
TopologicalSpace.Opens.coe_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U : Set α} {hU : IsOpen U}, ↑{ carrier := U, is_open' := hU } = U
-- Init.Data.NeZero
NeZero.mk : ∀ {R : Type u_1} [inst : Zero R] {n : R}, n ≠ 0 → NeZero n
-- Std.Data.ExtDTreeMap.Lemmas
/-- Variant of `get_map` that holds without `LawfulEqCmp`.  -/
Std.ExtDTreeMap.Const.get_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtDTreeMap.map f t},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.map f t) k h' = f (t.getKey k ⋯) (Std.ExtDTreeMap.Const.get t k ⋯)
-- Mathlib.Order.Sublocale
Sublocale.instCoframe : {X : Type u_1} → [inst : Order.Frame X] → Order.Coframe (Sublocale X)
-- Mathlib.Algebra.DirectSum.Ring
/-- Multiplication from the left between graded components distributes with respect to
addition.  -/
DirectSum.GNonUnitalNonAssocSemiring.add_mul : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : Add ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a b : A i) (c : A j),
  GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, ∅.contains k = false
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_smul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S₁ : Type u_2} [inst_1 : SMulZeroClass S₁ R] {a : S₁}
  {f : MvPolynomial σ R}, (a • f).support ⊆ f.support
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Multiplying the first vector passed to `oangle` by a real multiplies the sign of the angle by
the sign of the real.  -/
Orientation.oangle_sign_smul_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ), (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- **Alias** of the reverse direction of `Module.End.hasEigenvalue_iff_mem_spectrum`. -/
Module.End.HasEigenvalue.of_mem_spectrum : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {f : Module.End K V} {μ : K}, μ ∈ spectrum K f → f.HasEigenvalue μ
-- Mathlib.Data.Set.Image
/-- A variant of `image_id`  -/
Set.image_id' : ∀ {α : Type u_1} (s : Set α), (fun x => x) '' s = s
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
_private.Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin.0.ContinuousAlternatingMap.alternatizeUncurryFinCLM.aux : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → {n : ℕ} → (E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) →ₗ[𝕜] E [⋀^Fin (n + 1)]→ₗ[𝕜] F
-- Mathlib.Topology.Maps.Proper.Basic
/-- If the composition of two continuous functions `g ∘ f` is proper and `f` is surjective,
then `g` is proper.  -/
isProperMap_of_comp_of_surj : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z},
  Continuous f → Continuous g → IsProperMap (g ∘ f) → Function.Surjective f → IsProperMap g
-- Mathlib.Algebra.Ring.Subsemiring.Defs
AddSubmonoidWithOneClass.mk : ∀ {S : Type u_1} {R : outParam (Type u_2)} [inst : AddMonoidWithOne R] [inst_1 : SetLike S R]
  [toAddSubmonoidClass : AddSubmonoidClass S R] [toOneMemClass : OneMemClass S R], AddSubmonoidWithOneClass S R
-- Mathlib.Algebra.Field.Rat
NNRat.num_inv_of_ne_zero : ∀ {q : ℚ≥0}, q ≠ 0 → q⁻¹.num = q.den
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prod_of_not_isSFiniteKernel_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} (η : ProbabilityTheory.Kernel α γ),
  ¬ProbabilityTheory.IsSFiniteKernel κ → κ.prod η = 0
-- Mathlib.Order.Circular
/-- The circular preorder obtained from "looping around" a preorder.
See note [reducible non-instances].  -/
Preorder.toCircularPreorder : (α : Type u_1) → [Preorder α] → CircularPreorder α
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer : ∀ (R : Type u_4) {A : Type u_5} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : StarRing A] [inst_5 : Module R A] [inst_6 : IsSemitopologicalSemiring A]
  [inst_7 : ContinuousStar A] [inst_8 : ContinuousConstSMul R A] [inst_9 : IsScalarTower R A A]
  [inst_10 : SMulCommClass R A A] [inst_11 : StarModule R A] [T2Space A] (s : Set A),
  (NonUnitalStarAlgebra.adjoin R s).topologicalClosure ≤
    NonUnitalStarSubalgebra.centralizer R ↑(NonUnitalStarSubalgebra.centralizer R s)
-- Mathlib.Analysis.Complex.Trigonometric
/-- **De Moivre's formula**  -/
Complex.cos_add_sin_mul_I_pow : ∀ (n : ℕ) (z : ℂ),
  (Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I
-- Mathlib.Data.Set.Image
Set.image.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α), f '' s = {x | ∃ a ∈ s, f a = x}
-- Mathlib.Algebra.Regular.Basic
IsAddLeftRegular.nsmul : ∀ {R : Type u_1} [inst : AddMonoid R] {a : R} (n : ℕ), IsAddLeftRegular a → IsAddLeftRegular (n • a)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.comp_c : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).c =
    CategoryTheory.CategoryStruct.comp g.c ((TopCat.Presheaf.pushforward CommRingCat g.base).map f.c)
-- Mathlib.Analysis.Normed.Group.Continuity
Filter.Tendsto.enorm : ∀ {α : Type u_1} {E : Type u_4} [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] {a : E} {l : Filter α}
  {f : α → E}, Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => ‖f x‖ₑ) l (nhds ‖a‖ₑ)
-- Mathlib.Order.Cofinal
isCofinal_iff_iUnion_Iic_eq_univ : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsCofinal s ↔ ⋃ i ∈ s, Set.Iic i = Set.univ
-- Std.Async.Process
/-- A process identifier, represented by a numeric ID in UNIX systems (e.g. 1000).
 -/
Std.IO.Process.PId : Type
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.sum_lt_lift_of_isRegular : ∀ {c : Cardinal.{max u v}} {ι : Type u} {f : ι → Cardinal.{max u v}},
  c.IsRegular → Cardinal.lift.{v, u} (Cardinal.mk ι) < c → (∀ (i : ι), f i < c) → Cardinal.sum f < c
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
/-- The tensor product of two quadratic maps, a shorthand for dot notation.  -/
QuadraticMap.tmul : {R : Type uR} →
  {A : Type uA} →
    {M₁ : Type uM₁} →
      {M₂ : Type uM₂} →
        {N₁ : Type uN₁} →
          {N₂ : Type uN₂} →
            [inst : CommRing R] →
              [inst_1 : CommRing A] →
                [inst_2 : AddCommGroup M₁] →
                  [inst_3 : AddCommGroup M₂] →
                    [inst_4 : AddCommGroup N₁] →
                      [inst_5 : AddCommGroup N₂] →
                        [inst_6 : Algebra R A] →
                          [inst_7 : Module R M₁] →
                            [inst_8 : Module A M₁] →
                              [inst_9 : Module R N₁] →
                                [inst_10 : Module A N₁] →
                                  [inst_11 : SMulCommClass R A M₁] →
                                    [IsScalarTower R A M₁] →
                                      [inst_13 : IsScalarTower R A N₁] →
                                        [inst_14 : Module R M₂] →
                                          [inst_15 : Module R N₂] →
                                            [Invertible 2] →
                                              QuadraticMap A M₁ N₁ →
                                                QuadraticMap R M₂ N₂ →
                                                  QuadraticMap A (TensorProduct R M₁ M₂) (TensorProduct R N₁ N₂)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : SizeOf C] (ι : Type) [fintype : Fintype ι] (X : ι → C),
  sizeOf { ι := ι, fintype := fintype, X := X } = 1 + sizeOf ι + sizeOf fintype
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
exists_one_le_mul_of_le : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : Preorder α] [ExistsMulOfLE α] {a b : α} [MulLeftReflectLE α],
  a ≤ b → ∃ c, 1 ≤ c ∧ a * c = b
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastJacobiSymAux.congr_simp : ∀ (a a_1 : ℕ) (e_a : a = a_1) (b b_1 : ℕ),
  b = b_1 →
    ∀ (flip flip_1 : Bool),
      flip = flip_1 → ∀ (ha0 : a > 0), fastJacobiSymAux✝ a b flip ha0 = fastJacobiSymAux✝ a_1 b_1 flip_1 ⋯
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
/-- Class of composing triples  -/
MonoidHom.CompTriple : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : Monoid M] → [inst_1 : Monoid N] → [inst_2 : Monoid P] → (M →* N) → (N →* P) → outParam (M →* P) → Prop
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.trySend : {α : Type} → Std.CloseableChannel.Unbounded✝ α → α → BaseIO Bool
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The set of all finite measures is a measurable set in the Giry monad.  -/
MeasureTheory.FiniteMeasure.measurableSet_isFiniteMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω], MeasurableSet {μ | MeasureTheory.IsFiniteMeasure μ}
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorRefVecBlastCpop : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop
-- Mathlib.CategoryTheory.Pi.Basic
_private.Mathlib.CategoryTheory.Pi.Basic.0.CategoryTheory.Pi.sumElimCategory.match_19.eq_1 : ∀ {I J : Type u_1} (motive : I ⊕ J → Sort u_2) (i : I) (h_1 : (i : I) → motive (Sum.inl i))
  (h_2 : (j : J) → motive (Sum.inr j)),
  (match Sum.inl i with
    | Sum.inl i => h_1 i
    | Sum.inr j => h_2 j) =
    h_1 i
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_eq_gcd_range_succ : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R),
  p.content = (Finset.range p.natDegree.succ).gcd p.coeff
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)] {f : Option (β k) → Option (β k)},
  (t.alter k f).get! k = (f (t.get? k)).get!
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.mapGL_injective : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [FaithfulSMul R S],
  Function.Injective ⇑(Matrix.SpecialLinearGroup.mapGL S)
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- A morphism of homological complexes `φ : F ⟶ G` has a homotopy fiber if for all
indices `i` and `j` such that `c.Rel i j`, the binary biproduct `F.X i ⊞ G.X j` exists.  -/
HomologicalComplex.HasHomotopyFiber : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} → {c : ComplexShape α} → {F G : HomologicalComplex C c} → (F ⟶ G) → Prop
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
groupCohomology.inhomogeneousCochains.ext_iff : ∀ {k G : Type u} [inst : CommRing k] {n : ℕ} [inst_1 : Group G] {A : Rep.{u, u, u} k G}
  {x y : ↑((groupCohomology.inhomogeneousCochains A).X n)}, x = y ↔ ∀ (g : Fin n → G), x g = y g
-- Mathlib.Topology.Order.Monotone
/-- A monotone function `f` sending `top` to `top` and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set.  -/
Monotone.map_sInf_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α},
  ContinuousAt f (sInf s) → Monotone f → f ⊤ = ⊤ → f (sInf s) = sInf (f '' s)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.mul` -/
Meromorphic.fun_mul : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'}, Meromorphic f → Meromorphic g → Meromorphic fun i => f i * g i
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.order_C : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonAssocSemiring R] {r : R}, (HahnSeries.C r).order = 0
-- Mathlib.Topology.UniformSpace.Separation
eq_of_clusterPt_uniformity : ∀ {α : Type u} [inst : UniformSpace α] [T0Space α] {x y : α}, ClusterPt (x, y) (uniformity α) → x = y
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.mk.inj : ∀ {X : TopCat} {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {CC : C → Type v} {FC : C → C → Type w}
  {inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)} {inst_2 : CategoryTheory.ConcreteCategory C FC}
  {inst_3 : CategoryTheory.Limits.HasColimits C} {F : TopCat.Presheaf C X} {base : ↑X}
  {germ : CategoryTheory.ToType (F.stalk base)} {base_1 : ↑X} {germ_1 : CategoryTheory.ToType (F.stalk base_1)},
  { base := base, germ := germ } = { base := base_1, germ := germ_1 } → base = base_1 ∧ germ ≍ germ_1
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_typein_top : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (f : PrincipalSeg r s),
  Ordinal.lift.{u, v} ((Ordinal.typein s).toRelEmbedding f.top) = Ordinal.lift.{v, u} (Ordinal.type r)
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_singleton_univ : ∀ {G : Type u_1} [inst : Group G] {g : G}, Subgroup.IsComplement {g} Set.univ
-- Mathlib.Data.Quot
Quot.lift₂_mk : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} (f : α → β → γ)
  (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b)
  (a : α) (b : β), Quot.lift₂ f hr hs (Quot.mk r a) (Quot.mk s b) = f a b
-- Init.Data.UInt.Bitwise
UInt32.zero_or : ∀ {a : UInt32}, 0 ||| a = a
-- Init.Data.Subtype.Order
Subtype.instLawfulOrderMax : ∀ {α : Type u} [inst : LE α] [inst_1 : Max α] [inst_2 : Std.LawfulOrderMax α] {P : α → Prop},
  Std.LawfulOrderMax (Subtype P)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Option.getD.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (opt : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive opt
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.comap_iInf : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {ι : Sort u_1} (f : K →+* L)
  (s : ι → Subfield L), Subfield.comap f (iInf s) = ⨅ i, Subfield.comap f (s i)
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isColocal.homEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {Y Z : C}
  {g : Y ⟶ Z} (hg : P.isColocal g) (X : C) (hX : P X) (f : X ⟶ Y),
  (hg.homEquiv X hX) f = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Analysis.Convex.SpecificFunctions.Pow
NNReal.strictConcaveOn_sqrt : StrictConcaveOn NNReal Set.univ ⇑NNReal.sqrt
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddLocalization.addEquivOfQuotient_symm_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (x : M) (y : ↥S),
  (AddLocalization.addEquivOfQuotient f).symm (f.mk' x y) = (AddLocalization.addMonoidOf S).mk' x y
-- Init.Data.Nat.Basic
Nat.instAssociativeHMul : Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.termδ : Lean.ParserDescr
-- Lean.Meta.DiscrTree.Main
Lean.Meta.DiscrTree.insert : {α : Type} → [BEq α] → Lean.Meta.DiscrTree α → Lean.Expr → α → optParam Bool false → Lean.MetaM (Lean.Meta.DiscrTree α)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.to.eq_1 : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C),
  CategoryTheory.ForgetEnrichment.to W X = X
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_add_one : ∀ (o : Ordinal.{u_1}), Cardinal.aleph (o + 1) = Order.succ (Cardinal.aleph o)
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.add_algebraMap_isNat_zero : ∀ {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r s : R},
  r + s = 0 → Mathlib.Meta.NormNum.IsNat ((algebraMap R A) r + (algebraMap R A) s) 0
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.Pos.skipWhile.match_1.eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (h_1 : (nextCurr : s.Pos) → motive (some nextCurr))
  (h_2 : Unit → motive none),
  (match none with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_eq_natCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : NatCast α] {d : n → α} {m : ℕ},
  Matrix.diagonal d = ↑m ↔ d = ↑m
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.mul_right_iff : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, IsUnit b → (IsUnit (a * b) ↔ IsUnit a)
-- Mathlib.Order.Basic
max_def_lt : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), max a b = if a < b then b else a
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.scalarRestriction_hom`.

---

If `g : M ⟶ N` is a `B`-linear morphism of `B`-modules, then it induces an
`A`-linear morphism when `M` and `N` have an `A`-module structure obtained
by restricting scalars along a monoid morphism `A ⟶ B`.  -/
CategoryTheory.Mod_.scalarRestriction_hom : ∀ {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.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.MonObj A] [inst_5 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsMonHom f] (M N : D) [inst_7 : CategoryTheory.ModObj B M]
  [inst_8 : CategoryTheory.ModObj B N] (g : M ⟶ N) [CategoryTheory.IsModHom B g], CategoryTheory.IsModHom A g
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_def : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]}, ‖z‖ = ‖↑z‖
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.ShortExact.ab_injective_f : ∀ {S : CategoryTheory.ShortComplex Ab}, S.ShortExact → Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom S.f)
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.StepResult.mk : {dir : Std.Http.Protocol.H1.Direction} →
  Array (Std.Http.Protocol.H1.Event dir) → Std.Http.Internal.ChunkedBuffer → Std.Http.Protocol.H1.StepResult dir
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_δ_μ : ∀ {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] {C' : Type u₁'}
  [inst_4 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal]
  (G : CategoryTheory.Functor D C') (X Y : C),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.δ F X Y))
      (G.map (CategoryTheory.Functor.LaxMonoidal.μ F X Y)) =
    CategoryTheory.CategoryStruct.id (G.obj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)))
-- Mathlib.Algebra.MvPolynomial.Basic
/-- Infer base ring for `MvPolynomial _ R`. Used by the `polynomial` tactic.  -/
MvPolynomial.mvPolynomialInferBaseImpl : Mathlib.Tactic.Polynomial.PolynomialExt
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.e_comp_id_assoc : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (X Y : C) {Z : V} (h : (X ⟶[V] Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eId V Y))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Y) h)) =
    h
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- The trivial monoid algebra is the base ring.  -/
AddMonoidAlgebra.uniqueLinearEquiv : (R : Type u_1) →
  {S : Type u_2} →
    (M : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Module R S] → [Zero M] → [Subsingleton M] → AddMonoidAlgebra S M ≃ₗ[R] S
-- Init.Data.UInt.Lemmas
UInt32.ofInt_mul : ∀ (x y : ℤ), UInt32.ofInt (x * y) = UInt32.ofInt x * UInt32.ofInt y
-- Mathlib.Topology.Category.Profinite.CofilteredLimit
Profinite.exists_locallyConstant_fin_two : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J]
  {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) (hC : CategoryTheory.Limits.IsLimit C)
  (f : LocallyConstant (↑C.pt.toTop) (Fin 2)), ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
-- Std.Http.Data.Status
/-- 307 Temporary Redirect
 -/
Std.Http.Status.temporaryRedirect : Std.Http.Status
-- Init.Data.Vector.Lemmas
Vector.findSomeM?_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m]
  {f : α → m (Option β)} {xs : Vector α n}, List.findSomeM? f xs.toList = Vector.findSomeM? f xs
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.SL_neg_smul : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane), -g • z = g • z