mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.whisker_right_id : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Std.Time.Date.Unit.Month
Std.Time.Internal.Bounded.LE.addTop.eq_1 : ∀ {n m : ℤ} (bounded : Std.Time.Internal.Bounded.LE n m) (num : ℤ) (h : num ≥ 0),
  bounded.addTop num h = ⟨↑bounded + num, ⋯⟩
-- Mathlib.Data.Matrix.Basic
Matrix.transpose_list_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : AddMonoid α] (l : List (Matrix m n α)),
  l.sum.transpose = (List.map Matrix.transpose l).sum
-- Init.Data.UInt.Bitwise
instCommutativeUInt8HAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Init.Data.BitVec.Lemmas
/-- A sign extension of `x : BitVec w` to a larger bitwidth `v ≥ w`
equals high bits of either `0` or `1` depending on `x.msb`, followed by `x`.  -/
BitVec.signExtend_eq_append_of_le : ∀ {w v : ℕ} {x : BitVec w} (h : w ≤ v),
  BitVec.signExtend v x = BitVec.cast ⋯ ((if x.msb = true then BitVec.allOnes (v - w) else 0#(v - w)) ++ x)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Icc_succ : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.Icc a.succ b.succ, f i = ∏ i ∈ Finset.Icc a b, f i.succ
-- Mathlib.Topology.UniformSpace.Equicontinuity
UniformEquicontinuous.uniformEquicontinuousOn : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α},
  UniformEquicontinuous F → ∀ (S : Set β), UniformEquicontinuousOn F S
-- Lean.Data.PrefixTree
Lean.PrefixTree.forMatchingM : {m : Type → Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} → {p : α → α → Ordering} → [Monad m] → Lean.PrefixTree α β p → List α → (β → m Unit) → m Unit
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_natCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoMod hp a (b + ↑m * p) = toIcoMod hp a b
-- Mathlib.Order.Birkhoff
OrderEmbedding.birkhoffSet_apply : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Fintype α] [inst_2 : DecidablePred SupIrred] [inst_3 : OrderBot α]
  (a : α), OrderEmbedding.birkhoffSet a = ↑(OrderIso.lowerSetSupIrred a)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasStrictFDerivAt.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) • f') x
-- Std.Http.Server.Connection
Std.Http.Server.Connection.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (socket : α)
  (machine : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving) (extensions : Std.Http.Extensions),
  sizeOf { socket := socket, machine := machine, extensions := extensions } =
    1 + sizeOf socket + sizeOf machine + sizeOf extensions
-- Init.Omega.Constraint
/-- It is convenient below to say that a constraint is satisfied at the dot product of two vectors,
so we make an abbreviation `sat'` for this.
 -/
Lean.Omega.Constraint.sat' : Lean.Omega.Constraint → Lean.Omega.Coeffs → Lean.Omega.Coeffs → Bool
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Disjoint union of two `0`-hypercovers.  -/
CategoryTheory.Precoverage.ZeroHypercover.sum : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S : C} → [J.IsStableUnderSup] → J.ZeroHypercover S → J.ZeroHypercover S → J.ZeroHypercover S
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.fromStructuredArrow_obj_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (c : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)),
  ((CategoryTheory.Limits.Cocone.fromStructuredArrow F).obj c).ι = c.hom
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.mem_top : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (x : M), x ∈ ⊤
-- Mathlib.Data.Vector.Basic
List.Vector.id_traverse : ∀ {n : ℕ} {α : Type u} (x : List.Vector α n), List.Vector.traverse pure x = pure x
-- Mathlib.Topology.Sheaves.Sheafify
/-- The prelocal predicate on functions into the stalks, asserting that the function is equal to a germ.
 -/
TopCat.Presheaf.Sheafify.isGerm : {X : TopCat} → (F : TopCat.Presheaf (Type v) X) → TopCat.PrelocalPredicate fun x => F.stalk x
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.toSMul_apply : ∀ {ι : Type u_1} {I₀ : WithTop (BoxIntegral.Box ι)} {E : Type u_4} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] (f : BoxIntegral.BoxAdditiveMap ι ℝ I₀) (I : BoxIntegral.Box ι) (x : E),
  (f.toSMul I) x = f I • x
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.tensorHom_def : ∀ (R : Type u) [inst : CommRing R] {X₁ Y₁ X₂ Y₂ : HopfAlgCat R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    HopfAlgCat.ofHom (Bialgebra.TensorProduct.map f.toBialgHom' g.toBialgHom')
-- Mathlib.LinearAlgebra.Complex.Module
Complex.selfAdjointEquiv_apply : ∀ (z : ↥(selfAdjoint ℂ)), Complex.selfAdjointEquiv z = (↑z).re
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Candidate component of units for the `LawfulDayConvolutionMonoidalCategoryStruct`,
this defaults to the ones deduced by `convolutions'` and `tensorObjIsoConvolution`.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    (V : Type u₂) →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  (d d' : D) →
                    (x y : C) →
                      CategoryTheory.MonoidalCategoryStruct.tensorObj
                          (((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                                    D).obj
                                d).obj
                            x)
                          (((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                                    D).obj
                                d').obj
                            y) ⟶
                        ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                                  D).obj
                              (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObj
                                C V d d')).obj
                          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.unmopMonObj_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : Cᴹᵒᵖ)
  [inst_2 : CategoryTheory.MonObj M], CategoryTheory.MonObj.one = CategoryTheory.MonObj.one.unmop
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.conjSqrt_monotone : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] {c : A}, Monotone ⇑(CFC.conjSqrt c)
-- Mathlib.Data.Rat.Lemmas
Rat.inv_ofNat_den : ∀ (a : ℕ) [a.AtLeastTwo], (OfNat.ofNat a)⁻¹.den = OfNat.ofNat a
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.comap_coe_nhds_infty : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  Filter.comap OnePoint.some (nhds OnePoint.infty) = Filter.coclosedCompact X
-- Mathlib.Topology.Compactness.Compact
/-- The disjoint union of two compact spaces is compact.  -/
instCompactSpaceSum : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] [CompactSpace Y],
  CompactSpace (X ⊕ Y)
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_replicate : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.Refl fun x1 x2 => x1 ≤ x2] {n : ℕ} {a : α}
  {f : α → β}, List.maxIdxOn? f (List.replicate n a) = if n = 0 then none else some 0
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.dropn_tail : ∀ {α : Type u} (s : Stream'.WSeq α) (n : ℕ), s.tail.drop n = s.drop (n + 1)
-- Mathlib.Tactic.FBinop
/-- Result returned by `analyze`.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.AnalyzeResult : Type
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerLeft_id' : ∀ {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] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E},
  F.whiskerLeft (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id (F.comp G)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.divRight_symm : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul Gᵐᵒᵖ G] (c : G),
  (IsometryEquiv.divRight c).symm = IsometryEquiv.mulRight c
-- Aesop.Stats.Basic
Aesop.instToJsonForwardStateStats.toJson : Aesop.ForwardStateStats → Lean.Json
-- Mathlib.Logic.Relation
/-- `EqvGen.setoid r` is the setoid generated by a relation `r`.

The motivation for this definition is that `Quot r` behaves like `Quotient (EqvGen.setoid r)`,
see for example `Quot.eqvGen_exact` and `Quot.eqvGen_sound`.  -/
Relation.EqvGen.setoid : {α : Type u_1} → (α → α → Prop) → Setoid α
-- Mathlib.RingTheory.Ideal.Basic
Ring.isField_iff_maximal_bot : ∀ {R : Type u_5} [inst : CommSemiring R] [Nontrivial R], IsField R ↔ ⊥.IsMaximal
-- Mathlib.LinearAlgebra.Matrix.Dual
LinearMap.toMatrix_transpose : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommSemiring K]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂]
  [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] [inst_7 : DecidableEq ι₁] [inst_8 : DecidableEq ι₂]
  {B₁ : Module.Basis ι₁ K V₁} {B₂ : Module.Basis ι₂ K V₂} (u : V₁ →ₗ[K] V₂),
  (LinearMap.toMatrix B₂.dualBasis B₁.dualBasis) (Module.Dual.transpose u) = ((LinearMap.toMatrix B₁ B₂) u).transpose
-- Init.Data.Option.Lemmas
Option.mem_map_of_mem : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {a : α} (g : α → β), a ∈ x → g a ∈ Option.map g x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → γ a} {k : α},
  t.WF → (Std.DTreeMap.Internal.Impl.map f t).get? k = Option.map (f k) (t.get? k)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.quasiIso_opFunctor_map_iff : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L)
  [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i],
  QuasiIso ((HomologicalComplex.opFunctor V c).map φ.op) ↔ QuasiIso φ
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.localEpi_antitone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C], Antitone CategoryTheory.ObjectProperty.localEpi
-- Mathlib.Topology.MetricSpace.Gluing
/-- Given two maps `Φ` and `Ψ` intro metric spaces `X` and `Y` such that the distances between
`Φ p` and `Φ q`, and between `Ψ p` and `Ψ q`, coincide up to `2 ε` where `ε > 0`, one can almost
glue the two spaces `X` and `Y` along the images of `Φ` and `Ψ`, so that `Φ p` and `Ψ p` are
at distance `ε`.  -/
Metric.glueMetricApprox : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : MetricSpace X] →
        [inst_1 : MetricSpace Y] →
          [Nonempty Z] →
            (Φ : Z → X) →
              (Ψ : Z → Y) →
                (ε : ℝ) → 0 < ε → (∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε) → MetricSpace (X ⊕ Y)
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_eq_top_iff : ∀ {x : EReal}, x.exp = ⊤ ↔ x = ⊤
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec.map_apply : ∀ {R S : CommRingCat} (f : R ⟶ S) (x : ↥(AlgebraicGeometry.Spec S)),
  (AlgebraicGeometry.Spec.map f) x = PrimeSpectrum.comap (CommRingCat.Hom.hom f) x
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `Ring` instance along a surjective function.  -/
Function.Surjective.ring : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : Neg S] →
                  [inst_5 : Sub S] →
                    [inst_6 : SMul ℕ S] →
                      [inst_7 : SMul ℤ S] →
                        [inst_8 : Pow S ℕ] →
                          [inst_9 : NatCast S] →
                            [inst_10 : IntCast S] →
                              [inst_11 : Ring R] →
                                f 0 = 0 →
                                  f 1 = 1 →
                                    (∀ (x y : R), f (x + y) = f x + f y) →
                                      (∀ (x y : R), f (x * y) = f x * f y) →
                                        (∀ (x : R), f (-x) = -f x) →
                                          (∀ (x y : R), f (x - y) = f x - f y) →
                                            (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                              (∀ (n : ℤ) (x : R), f (n • x) = n • f x) →
                                                (∀ (x : R) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                  (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → Ring S
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.equivElements_apply_fst : ∀ {X : SSet} (s : X.S), (SSet.S.equivElements s).fst = Opposite.op { len := s.dim }
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.mem_toList_insert_of_mem : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {y : α × β} {k : α} (v : β) {t : RBTree.RBMap α β cmp},
  y ∈ t.toList → y ∈ (t.insert k v).toList ∨ cmp k y.1 = Ordering.eq
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.instPreservesColimitsOfSizeFreeFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat],
  CategoryTheory.Limits.PreservesColimitsOfSize.{v₂, u₂, u, max u u₁, u + 1, max (max (u + 1) u₁) v₁}
    SheafOfModules.freeFunctor
-- Mathlib.Topology.Algebra.Monoid.AddChar
DenseRange.addChar_eq_of_eval_one_eq : ∀ {A : Type u_1} {M : Type u_2} [inst : TopologicalSpace A] [inst_1 : AddMonoidWithOne A] [inst_2 : Monoid M]
  [inst_3 : TopologicalSpace M] [T2Space M],
  DenseRange Nat.cast → ∀ {κ₁ κ₂ : AddChar A M}, Continuous ⇑κ₁ → Continuous ⇑κ₂ → κ₁ 1 = κ₂ 1 → κ₁ = κ₂
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_le_sum : ∀ {α : Type u_5} {f : Filter α} {R : Type u_6} [inst : Preorder R] {κ : Type u_7} [inst_1 : AddCommMonoid R]
  [AddLeftMono R] [AddRightMono R] {u : κ → α → R} (s : Finset κ),
  (∀ k ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u k)) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (∑ k ∈ s, u k)
-- Mathlib.Condensed.Epi
Condensed.epi_iff_locallySurjective_on_compHaus : ∀ (A : Type u') [inst : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type v'}
  [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_2 : CategoryTheory.ConcreteCategory A FA]
  [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] {X Y : Condensed A} (f : X ⟶ Y)
  [(CategoryTheory.coherentTopology CompHaus).WEqualsLocallyBijective A]
  [CategoryTheory.HasSheafify (CategoryTheory.coherentTopology CompHaus) A]
  [(CategoryTheory.coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)]
  [CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) A)]
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)],
  CategoryTheory.Epi f ↔
    ∀ (S : CompHaus) (y : CategoryTheory.ToType (Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x =
              (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_comp_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₂ : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom)
  {f₁'' : CategoryTheory.Arrow C₁} (sq₁₂'' : F.PushoutObjObj f₁''.hom f₂.hom) (sq : f₁ ⟶ f₁') (sq' : f₁' ⟶ f₁'')
  {Z : CategoryTheory.Arrow C₃} (h : CategoryTheory.Arrow.mk sq₁₂''.ι ⟶ Z),
  CategoryTheory.CategoryStruct.comp (sq₁₂.mapArrowLeft sq₁₂' sq)
      (CategoryTheory.CategoryStruct.comp (sq₁₂'.mapArrowLeft sq₁₂'' sq') h) =
    CategoryTheory.CategoryStruct.comp (sq₁₂.mapArrowLeft sq₁₂'' (CategoryTheory.CategoryStruct.comp sq sq')) h
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- Polar sets of neighborhoods of the origin are bounded in the weak dual.  -/
WeakDual.isBounded_polar : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, s ∈ nhds 0 → Bornology.IsBounded (WeakDual.polar 𝕜 s)
-- Lean.DocString.Extension
Lean.ElabInline.deferred.sizeOf_spec : ∀ (index : ℕ), sizeOf (Lean.ElabInline.deferred index) = 1 + sizeOf index
-- Mathlib.RingTheory.LocalProperties.Semilocal
/-- A semilocal ring `R` is Noetherian if
its localization at every maximal ideal is a Noetherian ring.  -/
IsNoetherianRing.of_isLocalization_maximal : ∀ {R : Type u_1} [inst : CommSemiring R] [Finite (MaximalSpectrum R)] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3)
  [inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)]
  [inst_3 : (P : Ideal R) → [inst_3 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P],
  (∀ (P : Ideal R) [inst : P.IsMaximal], IsNoetherianRing (Rₚ P)) → IsNoetherianRing R
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The condition that ensures associated elements are normalized to the same element.  -/
NormalizationMonoid.normUnit_mul_units : ∀ {α : Type u_2} {inst : MonoidWithZero α} [self : NormalizationMonoid α] {a : α} (u : αˣ),
  a ≠ 0 → normUnit (a * ↑u) = u⁻¹ * normUnit a
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_13 : HAdd Std.Time.Second.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Homology.Homotopy
/-- homotopy is a transitive relation.  -/
Homotopy.trans : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} → {e f g : C ⟶ D} → Homotopy e f → Homotopy f g → Homotopy e g
-- Lean.Elab.ParseImportsFast
Lean.PrintImportResult.mk.injEq : ∀ (result? : Option Lean.ModuleHeader) (errors : Array String) (result?_1 : Option Lean.ModuleHeader)
  (errors_1 : Array String),
  ({ result? := result?, errors := errors } = { result? := result?_1, errors := errors_1 }) =
    (result? = result?_1 ∧ errors = errors_1)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Equivalence.isRightAdjoint_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.inverse.IsRightAdjoint
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiff_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞}, ContMDiff I I n id
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst_k.eq_1 : ∀ (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulConst_k k p =
    Bool.rec
      (Bool.rec
        (Lean.Grind.CommRing.Poly.rec (fun k' => Lean.Grind.CommRing.Poly.num (k.mul k'))
          (fun k' m x ih => Lean.Grind.CommRing.Poly.add (k.mul k') m ih) p)
        p (k.beq' 1))
      (Lean.Grind.CommRing.Poly.num 0) (k.beq' 0)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- `ContDiffMapSupportedInClass B E F n K` states that `B` is a type of bundled `n`-times
continuously differentiable functions with support in the compact set `K`.  -/
ContDiffMapSupportedInClass : Type u_5 →
  (E : outParam (Type u_6)) →
    (F : outParam (Type u_7)) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedAddCommGroup F] →
          [NormedSpace ℝ E] →
            [NormedSpace ℝ F] → outParam ℕ∞ → outParam (TopologicalSpace.Compacts E) → Type (max (max u_5 u_6) u_7)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget.lhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget aig w → aig.RefVec w
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Let `e` be a trivialization of a `C^n` vector bundle `E₁` over `B`. Then `m ↦ e.symmL 𝕜 m`
defines a section of the bundle of continuous linear maps `F₁ →L[𝕜] E₁` over `B`, and this section
is `C^n` at any point in `e.baseSet`.  -/
Bundle.Trivialization.contMDiffAt_symmL : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {EB : Type u_4}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_5} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B] {E₁ : B → Type u_6}
  [inst_6 : (x : B) → AddCommGroup (E₁ x)] [inst_7 : (x : B) → Module 𝕜 (E₁ x)] [inst_8 : NormedAddCommGroup F₁]
  [inst_9 : NormedSpace 𝕜 F₁] [inst_10 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_11 : (x : B) → TopologicalSpace (E₁ x)] [inst_12 : ∀ (x : B), IsTopologicalAddGroup (E₁ x)]
  [inst_13 : ∀ (x : B), ContinuousSMul 𝕜 (E₁ x)] [inst_14 : FiberBundle F₁ E₁] [inst_15 : VectorBundle 𝕜 F₁ E₁]
  [ContMDiffVectorBundle n F₁ E₁ IB] (e : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  [inst_17 : MemTrivializationAtlas e] {x : B},
  x ∈ e.baseSet →
    ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₁))) n (fun m => ⟨m, Bundle.Trivialization.symmL 𝕜 e m⟩)
      x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrp_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.Grp C} (ψ : G ⟶ H) (Y : Cᵒᵖ),
  (CategoryTheory.yonedaGrp.map ψ).app Y = GrpCat.ofHom (MonCat.Hom.hom ((CategoryTheory.yonedaMon.map ψ.hom).app Y))