mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Projective
/-- An R-module is projective if it is a direct summand of a free module, or equivalently
if maps from the module lift along surjections. There are several other equivalent
definitions.  -/
Module.Projective : (R : Type u_1) → [inst : Semiring R] → (P : Type u_2) → [inst_1 : AddCommMonoid P] → [Module R P] → Prop
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_neg : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F), ‖-f‖ = ‖f‖
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1`, `*` and `⁻¹` is a commutative group, if it admits an injective map that
preserves `1`, `*` and `⁻¹` to a commutative group. See note [reducible non-instances].  -/
Function.Injective.commGroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Inv M₁] →
            [inst_4 : Div M₁] →
              [inst_5 : Pow M₁ ℤ] →
                [inst_6 : CommGroup M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → CommGroup M₁
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
/-- `ContinuousMultilinearMap.restrictScalars` as a `ContinuousLinearMap`.  -/
ContinuousMultilinearMap.restrictScalarsLinear : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    {E : ι → Type u_3} →
      {F : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : (i : ι) → TopologicalSpace (E i)] →
            [inst_2 : (i : ι) → AddCommGroup (E i)] →
              [inst_3 : (i : ι) → Module 𝕜 (E i)] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      [inst_7 : IsTopologicalAddGroup F] →
                        [∀ (i : ι), ContinuousSMul 𝕜 (E i)] →
                          (𝕜' : Type u_5) →
                            [inst_9 : NontriviallyNormedField 𝕜'] →
                              [inst_10 : NormedAlgebra 𝕜' 𝕜] →
                                [inst_11 : (i : ι) → Module 𝕜' (E i)] →
                                  [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] →
                                    [inst_13 : Module 𝕜' F] →
                                      [inst_14 : IsScalarTower 𝕜' 𝕜 F] →
                                        [inst_15 : ContinuousConstSMul 𝕜' F] →
                                          ContinuousMultilinearMap 𝕜 E F →L[𝕜'] ContinuousMultilinearMap 𝕜' E F
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectR_mapId_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  (x : C),
  ((CategoryTheory.Bicategory.Prod.sectR b C).mapId x).inv =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x))
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.minpoly_coeff_zero_of_injective : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] {f : M →ₗ[R] M} [Nontrivial R], Function.Injective ⇑f → (minpoly R f).coeff 0 ≠ 0
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.tsum_G2Term_eq_tsum' : ∀ (z : UpperHalfPlane),
  ∑' (m : Fin 2 → ℤ), EisensteinSeries.G2Term✝ z m = ∑' (n : ℤ) (m : ℤ), EisensteinSeries.G2Term✝ z ![m, n]
-- Mathlib.Topology.Algebra.ConstMulAction
/-- A finite group action is always properly discontinuous.  -/
Finite.to_properlyDiscontinuousVAdd : ∀ {Γ : Type u_4} [inst : AddGroup Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : AddAction Γ T] [Finite Γ],
  ProperlyDiscontinuousVAdd Γ T
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.subtype_injective : ∀ {G : Type u_1} [inst : Group G] (s : Subgroup G), Function.Injective ⇑s.subtype
-- Mathlib.CategoryTheory.Core
CategoryTheory.CoreHom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : CategoryTheory.Core C}
  {x y : CategoryTheory.CoreHom X Y}, x.iso = y.iso → x = y
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.instSMulOfDistribMulAction : {ι : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommMonoid M] →
      {I₀ : WithTop (BoxIntegral.Box ι)} →
        {R : Type u_4} → [inst_1 : Monoid R] → [DistribMulAction R M] → SMul R (BoxIntegral.BoxAdditiveMap ι M I₀)
-- Init.Data.Nat.Gcd
Nat.gcd_gcd_self_right_right : ∀ (m n : ℕ), m.gcd (n.gcd m) = n.gcd m
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousMul.measurableMul : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [inst_3 : Mul γ]
  [SeparatelyContinuousMul γ], MeasurableMul γ
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_update_singleton_eq_filter_piFinset_eq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} [inst_2 : (a : α) → DecidableEq (δ a)]
  (s : (i : α) → Finset (δ i)) (i : α) {a : δ i},
  a ∈ s i → Fintype.piFinset (Function.update s i {a}) = {f ∈ Fintype.piFinset s | f i = a}
-- Mathlib.Algebra.Group.Action.Defs
IsLeftCancelSMul.left_cancel : ∀ {G : Type u_11} {P : Type u_12} [inst : SMul G P] [IsLeftCancelSMul G P] (a : G) (b c : P), a • b = a • c → b = c
-- Mathlib.Topology.Homotopy.Product
Path.Homotopic.prod_lift : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {a₁ a₂ : α} {b₁ b₂ : β}
  (p₁ : Path a₁ a₂) (p₂ : Path b₁ b₂),
  Path.Homotopic.prod (Path.Homotopic.Quotient.mk p₁) (Path.Homotopic.Quotient.mk p₂) =
    Path.Homotopic.Quotient.mk (p₁.prod p₂)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.map_π : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasEnd F'] (f : F ⟶ F')
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.map f) (CategoryTheory.Limits.end_.π F' j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F j) ((f.app (Opposite.op j)).app j)
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Client.mk.injEq : ∀ (shared shared_1 : Std.Http.Internal.Mock.SharedState✝),
  ({ shared := shared } = { shared := shared_1 }) = (shared = shared_1)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lift_comp_includeRight : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C)
  (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)),
  (AlgHom.restrictScalars R (Algebra.TensorProduct.lift f g hfg)).comp Algebra.TensorProduct.includeRight = g
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.le_radius_of_summable : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}, (Summable fun n => ‖p n‖ * ↑r ^ n) → ↑r ≤ p.radius
-- Mathlib.Order.GaloisConnection.Basic
/-- If `α` is a partial order with top element, then `WithTop.untop' ⊥` and
coercion form a Galois insertion.  -/
WithTop.giUntopDTop : {α : Type u} → [inst : Preorder α] → [inst_1 : OrderTop α] → GaloisCoinsertion WithTop.some (WithTop.untopD ⊤)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.liftCycles_ιChainComplex_homologyπ_homology₀ε : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C]
  (x : X.obj (Opposite.op { len := 0 })),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0
        SSet.liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (X.chainComplex R) 0) (X.homology₀ε R)) =
    CategoryTheory.CategoryStruct.id R
-- Init.Data.Int.DivMod.Lemmas
Int.le_of_mul_le_mul_left : ∀ {a b c : ℤ}, a * b ≤ a * c → 0 < a → b ≤ c
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_ite_mem : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Module ℚ≥0 M]
  [inst_3 : DecidableEq ι] (s : Finset ι) (f : ι → M),
  (Finset.univ.expect fun i => if i ∈ s then f i else 0) = s.dens • s.expect fun i => f i
-- Init.Data.Array.Erase
Array.eraseIdx_set_lt : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {w : i < xs.size} {j : ℕ} {a : α} (h : j < i),
  (xs.set i a w).eraseIdx j ⋯ = (xs.eraseIdx j ⋯).set (i - 1) a ⋯
-- Lean.DocString.Types
Lean.Doc.instBEqBlock.beq : {i : Type u_1} → {b : Type u_2} → [BEq i] → [BEq b] → Lean.Doc.Block i b → Lean.Doc.Block i b → Bool
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccAboveEquiv_symm_apply_ne_last : ∀ {n : ℕ} {p : Fin (n + 1)} (h : p ≠ Fin.last n) (x : { x // x ≠ p }),
  (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioo_succ_right_eq_Ioc_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Finset.Ioo a (Order.succ b) = Finset.Ioc a b
-- Init.Data.Bool
Bool.instMax : Max Bool
-- Mathlib.Data.Set.Function
Set.surjOn_of_subsingleton' : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Subsingleton β] (f : α → β),
  (t.Nonempty → s.Nonempty) → Set.SurjOn f s t
-- Mathlib.LinearAlgebra.Ray
/-- Two vectors are in the same ray if either one of them is zero or some positive multiples of them
are equal (in the typical case over a field, this means one of them is a nonnegative multiple of
the other).  -/
SameRay : (R : Type u_1) →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [IsStrictOrderedRing R] → {M : Type u_2} → [inst_3 : AddCommMonoid M] → [Module R M] → M → M → Prop
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.grindPatternCnstr : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] (c c' : C) (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxLeftLinear.μₗ F (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
          (CategoryTheory.Functor.LaxLeftLinear.μₗ F c' d))
        (CategoryTheory.Functor.LaxLeftLinear.μₗ F c
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)))
-- Init.Data.Int.Order
Int.lt_neg_of_lt_neg : ∀ {a b : ℤ}, a < -b → b < -a
-- Mathlib.Order.Category.PartOrd
PartOrd.coe_id : ∀ {X : PartOrd}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem:
Weak convergence of probability measures implies that if the boundary of a Borel set
carries no probability mass under the limit measure, then the limit of the measures of the set
equals the measure of the set under the limit probability measure.

A version with coercions to ordinary `ℝ≥0∞`-valued measures is
`MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto'`.
 -/
MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto : ∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
  [inst_2 : OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω}
  {μs : ι → MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs L (nhds μ) → ∀ {E : Set Ω}, μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
fderivWithin_ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt ℂ f s x →
    UniqueDiffWithinAt ℂ s x →
      fderivWithin ℂ (fun x => Complex.cos (f x)) s x = -Complex.sin (f x) • fderivWithin ℂ f s x
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.prodComm_apply : ∀ (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R E] [inst_4 : Module R E₂] (a : E × E₂),
  (LinearIsometryEquiv.prodComm R E E₂) a = a.swap
-- Init.Data.Array.Lemmas
Array.filterMap_replicate : ∀ {α : Type u_1} {β : Type u_2} {stop n : ℕ} {a : α} {f : α → Option β},
  autoParam (stop = n) Array.filterMap_replicate._auto_7 →
    Array.filterMap f (Array.replicate n a) 0 stop =
      match f a with
      | none => #[]
      | some b => Array.replicate n b
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.nnRat_ofNat_smul_1 : ∀ {d : ℕ} {R : Type u_3} {A : Type u_4} [inst : Semifield R] [inst_1 : Semifield A] [inst_2 : Algebra R A] {a : A}
  [inst_3 : d.AtLeastTwo], (1 / OfNat.ofNat d) • a = 1 / OfNat.ofNat d * a
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_cancel : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → (a * b).fdiv b = a
-- Init.Meta.Defs
Lean.Meta.ApplyConfig.mk : Lean.Meta.ApplyNewGoals → Bool → Bool → Bool → Lean.Meta.ApplyConfig
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_le_of_le_log : ∀ {b x c : Ordinal.{u_1}}, c ≠ 0 → c ≤ Ordinal.log b x → b ^ c ≤ x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.DHashMap.Const.get? (Std.DHashMap.Const.ofList l) k' = some v
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_eq_update_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α), Finsupp.erase a f = f.update a 0
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyData_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology], S.rightHomologyData.H = S.rightHomology
-- Mathlib.Data.Set.Lattice
Set.compl_iInter₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α), (⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsInitial X)
  (c : CategoryTheory.Limits.BinaryCofan X Y), Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inr
-- Mathlib.RingTheory.Spectrum.Maximal.Basic
/-- The prime spectrum is in bijection with the set of prime ideals.  -/
MaximalSpectrum.equivSubtype : (R : Type u_1) → [inst : CommSemiring R] → MaximalSpectrum R ≃ { I // I.IsMaximal }
-- Mathlib.Computability.Ackermann
not_primrec_ack_self : ¬Primrec fun n => ack n n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- To give an isomorphism between cocones, it suffices to give an
isomorphism between their vertices which commutes with the cocone
maps.  -/
CategoryTheory.Limits.BinaryBicones.ext : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        {c c' : CategoryTheory.Limits.BinaryBicone P Q} →
          (φ : c.pt ≅ c'.pt) →
            autoParam (CategoryTheory.CategoryStruct.comp c.inl φ.hom = c'.inl)
                CategoryTheory.Limits.BinaryBicones.ext._auto_1 →
              autoParam (CategoryTheory.CategoryStruct.comp c.inr φ.hom = c'.inr)
                  CategoryTheory.Limits.BinaryBicones.ext._auto_3 →
                autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.fst = c.fst)
                    CategoryTheory.Limits.BinaryBicones.ext._auto_5 →
                  autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.snd = c.snd)
                      CategoryTheory.Limits.BinaryBicones.ext._auto_7 →
                    (c ≅ c')
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The ring homomorphism from a given commutative ring in the diagram to the colimit commutative
ring.  -/
CommRingCat.Colimits.coconeMorphism : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → (j : J) → F.obj j ⟶ CommRingCat.Colimits.colimit F
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.brecOn.go : {motive : Turing.ToPartrec.Cont → Sort u} →
  (t : Turing.ToPartrec.Cont) →
    ((t : Turing.ToPartrec.Cont) → Turing.ToPartrec.Cont.below t → motive t) → motive t ×' Turing.ToPartrec.Cont.below t
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.mk_comp_liftRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  [inst_2 : IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (n : ℕ),
  (Ideal.Quotient.mk (I ^ n)).comp (IsAdicComplete.liftRingHom I f ⋯) = f n
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompInlCompAssociator.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E],
  CategoryTheory.sum.inrCompInlCompAssociator C D E =
    (CategoryTheory.Sum.inr_ C D).isoWhiskerLeft (CategoryTheory.sum.inlCompAssociator C D E) ≪≫
      (CategoryTheory.Sum.inl_ C (D ⊕ E)).inrCompSum'
        ((CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E)))
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_C : ∀ {R : Type u_1} [inst : Semiring R] (r : R), (HahnSeries.ofPowerSeries ℤ R) (PowerSeries.C r) = HahnSeries.C r
-- Mathlib.Tactic.Linarith.Preprocessing
/-- If `pf` is a proof of a strict inequality `(a : ℤ) < b`,
`mkNonstrictIntProof pf` returns a proof of `a + 1 ≤ b`,
and similarly if `pf` proves a negated weak inequality.
 -/
Mathlib.Tactic.Linarith.mkNonstrictIntProof? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.stabilizerEquivStabilizer_neg : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a b : α} (hg : b = -g +ᵥ a),
  AddAction.stabilizerEquivStabilizer hg = (AddAction.stabilizerEquivStabilizer ⋯).symm
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_containsThenInsert : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  (htb : t.Balanced), t.Ordered → (Std.DTreeMap.Internal.Impl.containsThenInsert k v t htb).2.impl.Ordered
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.id_mem_of_src : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d : C} {f : c ⟶ d},
  f ∈ S.arrows c d → CategoryTheory.CategoryStruct.id c ∈ S.arrows c c
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.smul_apply : ∀ {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : Module S V] [inst_5 : AddCommMonoid W]
  [inst_6 : Module R W] [inst_7 : Module S W] [inst_8 : SMulCommClass R S W] [inst_9 : SMul S R]
  [inst_10 : IsScalarTower S R V] [inst_11 : IsScalarTower S R W] (α : Sˣ) (e : V ≃ₗ[R] W) (x : V), (α • e) x = ↑α • e x
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- If `c` and `G.mapCone c` are limit cones and the projection maps in `c` are epimorphic,
then `cone G c.pt` is a limit cone.
 -/
LightProfinite.Extend.isLimitCone : {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} →
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        (G : CategoryTheory.Functor LightProfinite C) →
          CategoryTheory.Limits.IsLimit c →
            [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] →
              CategoryTheory.Limits.IsLimit (G.mapCone c) →
                CategoryTheory.Limits.IsLimit (LightProfinite.Extend.cone G c.pt)
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.defaultExpansion_Carrier : ∀ {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective)
  [inst : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => φ.onFunction f)]
  [inst_1 : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => φ.onRelation r)] (M : T.ModelType)
  [inst_2 : Inhabited ↑M], ↑(FirstOrder.Language.Theory.ModelType.defaultExpansion h M) = ↑M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).getKey? k = some k
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_restrict_of_subset : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  s ⊆ t → (μ.restrict t).restrict s = μ.restrict s
-- Mathlib.CategoryTheory.Action.Limits
Action.smul_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {R : Type u_3} [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R V]
  {X Y : Action V G} (r : R) (f : X ⟶ Y), (r • f).hom = r • f.hom
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instInhabited.eq_1 : ∀ (M : Type u_4) [inst : MulOne M], Monoid.End.instInhabited M = { default := 1 }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.mono_snd_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    autoParam (CategoryTheory.Mono f) CategoryTheory.IsPullback.mono_snd_of_mono._auto_1 → CategoryTheory.Mono snd