mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Join
convexJoin_singleton_segment : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (a b c : E),
  convexJoin 𝕜 {a} (segment 𝕜 b c) = (convexHull 𝕜) {a, b, c}
-- Init.Data.Option.Lemmas
Option.bind_id_eq_join : ∀ {α : Type u_1} {x : Option (Option α)}, x.bind id = x.join
-- Init.Data.SInt.Lemmas
Int16.lt_of_lt_of_le : ∀ {a b c : Int16}, a < b → b ≤ c → a < c
-- Init.Data.Vector.Lemmas
Vector.setIfInBounds_setIfInBounds : ∀ {α : Type u_1} {n i : ℕ} (a : α) {b : α} {xs : Vector α n},
  (xs.setIfInBounds i a).setIfInBounds i b = xs.setIfInBounds i b
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionRight_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) {d d' : D} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight (Opposite.op c) f.op =
    Opposite.op (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- A `FullyFaithful` structure can be obtained from the assumption the `F` is both
full and faithful.  -/
CategoryTheory.Functor.FullyFaithful.ofFullyFaithful : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → [F.Full] → [F.Faithful] → F.FullyFaithful
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_zero_left_eq_zero : Real.logb 0 = 0
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.guard.inj : ∀ {e e_1 : Lean.Expr},
  Lean.Meta.Grind.EMatchTheoremConstraint.guard e = Lean.Meta.Grind.EMatchTheoremConstraint.guard e_1 → e = e_1
-- Mathlib.AlgebraicGeometry.Sites.Etale
/-- The small étale site of a scheme is the Grothendieck topology on the
category of schemes étale over `X` induced from the étale topology on `Scheme.{u}`.  -/
AlgebraicGeometry.Scheme.smallEtaleTopology : (X : AlgebraicGeometry.Scheme) → CategoryTheory.GrothendieckTopology X.Etale
-- Mathlib.Order.GameAdd
Prod.gameAdd_mk_iff : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a₁ a₂ : α} {b₁ b₂ : β},
  Prod.GameAdd rα rβ (a₁, b₁) (a₂, b₂) ↔ rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂
-- Init.Data.Int.Order
Int.add_le_of_le_neg_add : ∀ {a b c : ℤ}, b ≤ -a + c → a + b ≤ c
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Given two lax monoidal, monoidally isomorphic functors, if one is lax braided, so is the other.
 -/
CategoryTheory.Functor.LaxBraided.ofNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F G : CategoryTheory.Functor C D} →
                  (i : F ≅ G) →
                    [inst_6 : F.LaxBraided] →
                      [inst_7 : G.LaxMonoidal] → [CategoryTheory.NatTrans.IsMonoidal i.hom] → G.LaxBraided
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Composing each term `pₙ` in a formal multilinear series with `(u, ..., u)` where `u` is a fixed
continuous linear map, gives a new formal multilinear series `p.compContinuousLinearMap u`.  -/
FormalMultilinearSeries.compContinuousLinearMap : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      {G : Type x} →
        [inst : Semiring 𝕜] →
          [inst_1 : AddCommMonoid E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : ContinuousAdd E] →
                  [inst_5 : ContinuousConstSMul 𝕜 E] →
                    [inst_6 : AddCommMonoid F] →
                      [inst_7 : Module 𝕜 F] →
                        [inst_8 : TopologicalSpace F] →
                          [inst_9 : ContinuousAdd F] →
                            [inst_10 : ContinuousConstSMul 𝕜 F] →
                              [inst_11 : AddCommMonoid G] →
                                [inst_12 : Module 𝕜 G] →
                                  [inst_13 : TopologicalSpace G] →
                                    [inst_14 : ContinuousAdd G] →
                                      [inst_15 : ContinuousConstSMul 𝕜 G] →
                                        FormalMultilinearSeries 𝕜 F G → (E →L[𝕜] F) → FormalMultilinearSeries 𝕜 E G
-- Mathlib.Algebra.Category.Ring.Limits
/-- We show that the forgetful functor `CommRingCat ⥤ RingCat` creates limits.

All we need to do is notice that the limit point has a `Ring` instance available,
and then reuse the existing limit.
 -/
RingCat.instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J RingCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] →
        CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ RingCat SemiRingCat)
-- Mathlib.CategoryTheory.Limits.Over
/-- If `F` has a limit, then the cone `limit.toUnder F` with cone point `𝟙 (limit F)` is
also a limit cone.  -/
CategoryTheory.Limits.limit.isLimitToOver : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.limit.toUnder F)
-- Mathlib.SetTheory.ZFC.PSet
/-- A pre-set is a subset of another pre-set if every element of the first family is extensionally
equivalent to some element of the second family.  -/
PSet.Subset : PSet.{u_1} → PSet.{u_2} → Prop
-- Mathlib.Analysis.CStarAlgebra.Classes
CStarAlgebra.mk : {A : Type u_1} →
  [toNormedRing : NormedRing A] →
    [toStarRing : StarRing A] →
      [toCompleteSpace : CompleteSpace A] →
        [toCStarRing : CStarRing A] →
          [toNormedAlgebra : NormedAlgebra ℂ A] → [toStarModule : StarModule ℂ A] → CStarAlgebra A
-- Mathlib.Algebra.Order.Group.Abs
mabs_div_le_max_div : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b c : G},
  a ≤ b → b ≤ c → ∀ (d : G), |b / d|ₘ ≤ max (c / d) (d / a)
-- Mathlib.Data.Finsupp.Weight
Finsupp.weight_single_one_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : Semiring R] [inst_1 : DecidableEq σ] (s : σ) (f : σ →₀ R),
  (Finsupp.weight (Pi.single s 1)) f = f s
-- Mathlib.Order.Lattice.Nat
Nat.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot ℕ
-- Init.Meta.Defs
Lean.TSyntax.instCoeNumLitPrec : Coe Lean.NumLit Lean.Prec
-- Mathlib.Logic.Basic
forall_and_left : ∀ {α : Sort u_1} [Nonempty α] (q : Prop) (p : α → Prop), (∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableMul : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Mul (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableMul (α i)], MeasurableMul ((i : ι) → α i)
-- Mathlib.Data.FP.Basic
FP.Float.nan : [C : FP.FloatCfg] → FP.Float
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_eq' : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι),
  DFinsupp.filter (fun x => x = i) f = fun₀ | i => f i
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionUnitIso`, the structural isomorphism `- ⊙ᵣ 𝟙_ C  ≅ -`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.termρᵣ : Lean.ParserDescr
-- Init.Data.Array.Lemmas
/-- Variant of `any_eq_true` in terms of membership rather than an array index.  -/
Array.any_eq_true' : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.any p = true ↔ ∃ x ∈ as, p x = true
-- Mathlib.Order.RelClasses
instWellFoundedLTOrderDualOfWellFoundedGT : ∀ (α : Type u_1) [inst : LT α] [h : WellFoundedGT α], WellFoundedLT αᵒᵈ
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.linearIsometryBoundedOfCompact_apply_apply : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] {𝕜 : Type u_4} [inst_3 : NormedRing 𝕜] [inst_4 : Module 𝕜 E]
  [inst_5 : IsBoundedSMul 𝕜 E] (f : C(α, E)) (a : α), ((ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) f) a = f a
-- Mathlib.Analysis.Normed.Operator.Basic
/-- If a continuous linear map is constructed from a linear map via the constructor `mkContinuous`,
then its norm is bounded by the bound given to the constructor if it is nonnegative.  -/
LinearMap.mkContinuous_norm_le : ∀ {𝕜 : 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 →ₛₗ[σ₁₂] F) {C : ℝ},
  0 ≤ C → ∀ (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖), ‖f.mkContinuous C h‖ ≤ C
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.Stable.exists_pow_smul_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {F : I.Filtration M}, F.Stable → ∃ n₀, ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.prod_pow : ∀ {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : Monoid β] (s : Set α) (t : Set β) (n : ℕ),
  s ×ˢ t ^ n = (s ^ n) ×ˢ (t ^ n)
-- Mathlib.Data.List.Find
_private.Mathlib.Data.List.Find.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Data.Set.Card
Set.Finite.encard_lt_card : ∀ {α : Type u_1} {s : Set α}, s.Finite → s ≠ Set.univ → s.encard < ENat.card α
-- Std.Time.Format.DateFormat
/-- Full extended-day-period strings for the `B` pattern.
Order: midnight, night, morning, noon, afternoon, evening.
 -/
Std.Time.DateFormatSymbols.extendedDayPeriodLong : Std.Time.DateFormatSymbols → Vector String 6
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.mul_cpow_ofReal_nonneg : ∀ {a b : ℝ}, 0 ≤ a → 0 ≤ b → ∀ (r : ℂ), (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C (CategoryTheory.CommMon D)) (X : C),
  CategoryTheory.MonObj.mul.app X = CategoryTheory.MonObj.mul
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z),
  CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (P.π.f 0) = 0
-- Mathlib.Analysis.Normed.Module.TransferInstance
Equiv.normedCommGroup.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedCommGroup β] (e : α ≃ β),
  e.normedCommGroup =
    { toNorm := (NormedCommGroup.induced α β e.mulEquiv ⋯).toNorm,
      toCommGroup := (NormedCommGroup.induced α β e.mulEquiv ⋯).toCommGroup, toPseudoMetricSpace := e.pseudometricSpace,
      eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsert_fst_eq_containsₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced),
  t.Ordered → ∀ (a : α) (b : β a), (Std.DTreeMap.Internal.Impl.containsThenInsert a b t htb).1 = t.containsₘ a
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.quasiMeasurePreserving_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {r : ℝ},
  r ≠ 0 → MeasureTheory.Measure.QuasiMeasurePreserving (fun x => r • x) μ μ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Closed balls and spheres coincide when the radius is non-positive  -/
Metric.closedBall_eq_sphere_of_nonpos : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, ε ≤ 0 → Metric.closedBall x ε = Metric.sphere x ε
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.symm : {R : Type u} →
  [inst : Rack R] → {a b : Rack.PreEnvelGroup R} → Rack.PreEnvelGroupRel' R a b → Rack.PreEnvelGroupRel' R b a
-- Lean.ErrorExplanation
Lean.ErrorExplanation.declLoc? : Lean.ErrorExplanation → Option Lean.DeclarationLocation
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_tensorProduct_of_isScalarTower : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] {S : Type u_1} [inst_5 : CommRing S] [inst_6 : Algebra R S] (N : Type u_2)
  [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : Module S N] [inst_10 : IsScalarTower R S N]
  [Module.Finite S N] [Module.Flat S N] (p : PrimeSpectrum S),
  Module.rankAtStalk (TensorProduct R N M) p =
    Module.rankAtStalk N p * Module.rankAtStalk M (PrimeSpectrum.comap (algebraMap R S) p)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.fromLeftNeg_leftNegEquiv_symm : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S),
  S.fromLeftNeg ((S.leftNegEquiv hS).symm x) = x
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.HasPullbacks],
  (AlgebraicGeometry.Scheme.precoverage P).HasPullbacks
-- Mathlib.Order.Interval.Finset.Defs
/-- Given a finset on `α`, lift it to being a finset on `WithTop α`
using `WithTop.some` and then insert `⊤`.  -/
WithTop.insertTop : {α : Type u_1} → Finset α ↪o Finset (WithTop α)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.whiskerEquiv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C}
  (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [inst_1 : CategoryTheory.Limits.HasCoproduct f]
  [inst_2 : CategoryTheory.Limits.HasCoproduct g],
  (CategoryTheory.Limits.Sigma.whiskerEquiv e w).hom = CategoryTheory.Limits.Sigma.map' ⇑e fun j => (w j).inv
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.instFunLike : {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) → FunLike S.Splitting G E
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFinset.congr_simp : ∀ {α : Type u_1} (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ [inst : Fintype α] [inst_1 : DecidableEq α] {inst_2 : DecidableRel G.Adj} [inst_3 : DecidableRel G_1.Adj]
      (n n_1 : ℕ), n = n_1 → G.cliqueFinset n = G_1.cliqueFinset n_1
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toList_zip_of_finite_left : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {it₂ : Std.Iter β₂} [Std.Iterators.Finite α₁ Id] [Std.Iterators.Productive α₂ Id],
  (it₁.zip it₂).toList = it₁.toList.zip (Std.Iter.take it₁.toList.length it₂).toList
-- Init.Data.String.Bootstrap
String.mk : List Char → String
-- Lean.Meta.SynthInstance
/-- If the type of the metavariable `mvar` has unused argument, return a pair `(α, transformer)`
where `α` is a new type without the unused arguments and the `transformer` is a function for converting a
solution with type `α` into a value that can be assigned to `mvar`.
Example: suppose `mvar` has type `(a : A) → (b : B a) → (c : C a) → D a c`, the result is the pair
```
((a : A) → (c : C a) → D a c,
 fun (f : (a : A) → (c : C a) → D a c) (a : A) (b : B a) (c : C a) => f a c
)
```

This method is used to improve the effectiveness of the TC resolution procedure. It was suggested and prototyped by
Tomas Skrivan. It improves the support for instances of type `a : A → C` where `a` does not appear in class `C`.
When we look for such an instance it is enough to look for an instance `c : C` and then return `fun _ => c`.

Tomas' approach makes sure that instance of a type like `a : A → C` never gets tabled/cached. More on that later.
At the core is this method. it takes an expression E and does two things:

The modification to TC resolution works this way: We are looking for an instance of `E`, if it is tabled
just get it as normal, but if not first remove all unused arguments producing `E'`. Now we look up the table again but
for `E'`. If it exists, use the transformer to create E. If it does not exists, create a new goal `E'`.
 -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.SynthInstance.removeUnusedArguments? : Lean.MetavarContext → Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.withElaboratedLHS : {α : Type} →
  Array Lean.Elab.Term.PatternVarDecl →
    Array Lean.Syntax →
      Lean.Syntax →
        ℕ →
          Lean.Expr →
            (Lean.Meta.Match.AltLHS → Lean.Expr → Lean.Elab.TermElabM α) →
              ExceptT Lean.Elab.Term.PatternElabException Lean.Elab.TermElabM α
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Equality of the composition of the unit and counit with the identity `G ⟶ GFG ⟶ G = 𝟙`  -/
CategoryTheory.Adjunction.right_triangle_components_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : F ⊣ G) (Y : D) {Z : C} (h : G.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.unit.app (G.obj Y))
      (CategoryTheory.CategoryStruct.comp (G.map (self.counit.app Y)) h) =
    h
-- Mathlib.RingTheory.FiniteType
RingHom.FiniteType.of_surjective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] (f : A →+* B),
  Function.Surjective ⇑f → f.FiniteType
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_ofNat : ∀ (n : ℕ), Int16.ofBitVec (BitVec.ofNat 16 n) = Int16.ofNat n
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- A binary fan in `Over X` is a limit if its corresponding pullback cone to `X` is a limit.  -/
CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : Y ⟶ X} →
        {g : Z ⟶ X} →
          {c : CategoryTheory.Limits.PullbackCone f g} →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.pullbackConeEquivBinaryFan.functor.obj c)
-- Mathlib.Algebra.RingQuot
/-- The universal ring homomorphism from `RingQuot r` to `B ⧸ Ideal.ofRel r`.  -/
RingQuot.ringQuotToIdealQuotient : {B : Type uR} → [inst : CommRing B] → (r : B → B → Prop) → RingQuot r →+* B ⧸ Ideal.ofRel r
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.toColon_hom_left_colonπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (Φ.toColon Ψ).hom) (Φ.colonπ Ψ) = 0
-- Mathlib.Data.List.MinMax
List.maximum_of_length_pos_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} (h : 0 < l.length), List.maximum_of_length_pos h ∈ l
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMkSucc_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C (n + 1)}
  (α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯) (β : F.δ₀ ≅ G.δ₀)
  (w :
    CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)
        (CategoryTheory.ComposableArrows.app' β.hom 0 ⋯) =
      CategoryTheory.CategoryStruct.comp α.hom (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)),
  (CategoryTheory.ComposableArrows.isoMkSucc α β w).inv = CategoryTheory.ComposableArrows.homMkSucc α.inv β.inv ⋯
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.inner_def : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (x y : TensorProduct 𝕜 E F),
  inner 𝕜 x y =
    (((TensorProduct.lift (TensorProduct.mapBilinear (RingHom.id 𝕜) E F 𝕜 𝕜)).compr₂ (LinearMap.mul' 𝕜 𝕜) ∘ₛₗ
          TensorProduct.map (innerₛₗ 𝕜) (innerₛₗ 𝕜))
        x)
      y
-- Mathlib.Topology.Algebra.Order.Group
comap_abs_nhds_zero : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G], Filter.comap abs (nhds 0) = nhds 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.uniqueHomToTrivial : {D : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} D] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D] →
      (A : CategoryTheory.AddMon D) → Unique (A ⟶ CategoryTheory.AddMon.trivial D)
-- Mathlib.NumberTheory.Padics.PadicNumbers
_private.Mathlib.NumberTheory.Padics.PadicNumbers.0.PadicSeq.norm_eq_of_equiv : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p} (hf : ¬f ≈ 0) (hg : ¬g ≈ 0),
  f ≈ g → padicNorm p (↑f (PadicSeq.stationaryPoint hf)) = padicNorm p (↑g (PadicSeq.stationaryPoint hg))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_whiskerRight : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A₂]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B₂] [inst_8 : CategoryTheory.Category.{v₉, u₉} C₂]
  {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₇)
  [inst_9 : CategoryTheory.Category.{v₇, u₇} X] {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (α : ψ ⟶ ψ')
  (φ : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight α φ) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ φ).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map α)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj φ))
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ' φ).inv)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Zero α], Matrix.transpose 0 = 0