mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- If a `J`-shaped diagram in `FullSubcategory P` has a limit in `C` whose cone point lives in the
full subcategory, then this defines a limit in the full subcategory.  -/
CategoryTheory.Limits.createsLimitFullSubcategoryInclusion : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {P : CategoryTheory.ObjectProperty C} →
          (F : CategoryTheory.Functor J P.FullSubcategory) →
            [inst_2 : CategoryTheory.Limits.HasLimit (F.comp P.ι)] →
              P (CategoryTheory.Limits.limit (F.comp P.ι)) → CategoryTheory.CreatesLimit F P.ι
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsRight.postcomp : ∀ {C : Type u} {inst : CategoryTheory.CategoryStruct.{v, u} C} {P Q : CategoryTheory.MorphismProperty C}
  [self : P.RespectsRight Q] {X Y Z : C} (i : Y ⟶ Z),
  Q i → ∀ (f : X ⟶ Y), P f → P (CategoryTheory.CategoryStruct.comp f i)
-- Mathlib.Geometry.Manifold.HasGroupoid
StructureGroupoid.compatible_of_mem_maximalAtlas_right : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e' : OpenPartialHomeomorph M H} {x : M},
  e' ∈ StructureGroupoid.maximalAtlas M G → (chartAt H x).symm.trans e' ∈ G
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_eq_getLastD_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {fallback : α}, t.maxKeyD fallback = t.keys.getLastD fallback
-- Mathlib.Data.PNat.Find
PNat.find_eq_iff : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) {m : ℕ+}, PNat.find h = m ↔ p m ∧ ∀ n < m, ¬p n
-- Aesop.Forward.LevelIndex
Aesop.instBEqLevelIndex : BEq Aesop.LevelIndex
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.isBasis_subset : ∀ {α : Type u_1} {M : Matroid α} {I X Y : Set α}, M.IsBasis I X → I ⊆ Y → Y ⊆ X → M.IsBasis I Y
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Context.mk.inj : ∀ {letFVars letFVars_1 : List Lean.FVarId},
  { letFVars := letFVars } = { letFVars := letFVars_1 } → letFVars = letFVars_1
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instUniformSpace : {𝕜 : 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 : UniformSpace F] → [IsUniformAddGroup F] → UniformSpace (ContinuousMultilinearMap 𝕜 E F)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_inv_app_fst_app : ∀ {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₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (U : CategoryTheory.Functor X Y) (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x : X),
  ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).inv.app
            X_1).fst.app
      x =
    CategoryTheory.CategoryStruct.id (ψ.left.obj (X_1.fst.obj (U.obj x)))
-- Mathlib.Algebra.Group.Defs
/-- A monoid is Dedekind-finite if every left inverse is also a right inverse.
It is more common to talk about Dedekind-finite rings, but https://arxiv.org/abs/2102.01598
does define Dedekind-finite monoids in §2.2.  -/
IsDedekindFiniteMonoid : (M : Type u_2) → [MulOne M] → Prop
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.sup_def : ∀ {M : Type u_1} [inst : AddZeroClass M] {s₁ s₂ : SaturatedAddSubmonoid M},
  s₁ ⊔ s₂ = (s₁.toAddSubmonoid ⊔ s₂.toAddSubmonoid).saturation
-- Mathlib.Tactic.Convert
/-- Elaborates `term` ensuring the expected type, allowing stuck metavariables.
Returns stuck metavariables as additional goals.
 -/
Mathlib.Tactic.elabTermForConvert : Lean.Syntax → Option Lean.Expr → Lean.Elab.Tactic.TacticM (Lean.Expr × List Lean.MVarId)
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opFunctorCompOpFunctorIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C],
  SimplicialObject.opFunctorCompOpFunctorIso =
    (SimplexCategory.rev.op.whiskeringLeftObjCompIso SimplexCategory.rev.op).symm ≪≫
      (CategoryTheory.Functor.whiskeringLeft SimplexCategoryᵒᵖ SimplexCategoryᵒᵖ C).mapIso
          ((CategoryTheory.Functor.opHom SimplexCategory SimplexCategory).mapIso
            SimplexCategory.revCompRevIso.symm.op) ≪≫
        CategoryTheory.Functor.whiskeringLeftObjIdIso
-- Init.Data.BitVec.Lemmas
BitVec.reverse_eq_zero_iff : ∀ {w : ℕ} {x : BitVec w}, x.reverse = 0#w ↔ x = 0#w
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk'.inj : ∀ {X : SSet} {toS : X.S} {nonDegenerate : toS.simplex ∈ X.nonDegenerate toS.dim} {toS_1 : X.S}
  {nonDegenerate_1 : toS_1.simplex ∈ X.nonDegenerate toS_1.dim},
  { toS := toS, nonDegenerate := nonDegenerate } = { toS := toS_1, nonDegenerate := nonDegenerate_1 } → toS = toS_1
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The coproduct of elements in a complete lattice is the supremum.  -/
Preorder.isColimitISup : {C : Type u} →
  [inst : CompleteLattice C] →
    {ι : Type u_1} →
      (X : ι → C) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (⨆ i, X i) fun i => CategoryTheory.homOfLE ⋯)
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_X_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {m n : ℕ},
  m ≤ n → (Polynomial.X ^ m).homogenize n = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_whisker_left_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h)
  {Z : self.obj a ⟶ self.obj c} (h_1 : self.map (CategoryTheory.CategoryStruct.comp f h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) h_1 =
    CategoryTheory.CategoryStruct.comp (self.mapComp f g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
        (CategoryTheory.CategoryStruct.comp (self.mapComp f h).inv h_1))
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.eval.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Λ] [inst_1 : Inhabited Γ] [inst_2 : Inhabited σ]
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) (l : List Γ),
  Turing.TM1.eval M l = Part.map (fun c => c.Tape.right₀) (StateTransition.eval (Turing.TM1.step M) (Turing.TM1.init l))
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.RingObjCat C} [inst_3 : SizeOf C]
  (hom : R₁.X ⟶ R₂.X) [isRingHom : CategoryTheory.IsRingHom hom],
  sizeOf { hom := hom, isRingHom := isRingHom } = 1 + sizeOf hom + sizeOf isRingHom
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.instRespectsRightScheme : ∀ {W P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsRight Q],
  (AlgebraicGeometry.sourceLocalClosure W P).RespectsRight Q
-- Mathlib.Logic.Denumerable
/-- Returns the next natural in a set, according to the usual ordering of `ℕ`.  -/
Nat.Subtype.succ : {s : Set ℕ} → [Infinite ↑s] → [DecidablePred fun x => x ∈ s] → ↑s → ↑s
-- Mathlib.Topology.ClusterPt
Filter.HasBasis.clusterPt_iff_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X},
  (nhds x).HasBasis p s → (ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in F, x ∈ s i)
-- Init.Data.Ord.SInt
Int64.instOrd : Ord Int64
-- Mathlib.RingTheory.Ideal.GoingDown
Ideal.exists_ltSeries_of_hasGoingDown : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.HasGoingDown R S] (l : LTSeries (PrimeSpectrum R)) (P : Ideal S) [inst_4 : P.IsPrime]
  [lo : P.LiesOver (RelSeries.last l).asIdeal],
  ∃ L,
    L.length = l.length ∧
      RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = RelSeries.toList l
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_bot : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A), M * ⊥ = ⊥
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.associator.injEq : ∀ (e : Lean.Expr) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁) (e_1 : Lean.Expr)
  (f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  (Mathlib.Tactic.BicategoryLike.StructuralAtom.associator e f g h =
      Mathlib.Tactic.BicategoryLike.StructuralAtom.associator e_1 f_1 g_1 h_1) =
    (e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_none : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  a ∉ t → t[a]? = none
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.mul_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.Relation F (x.mul RingCat.Colimits.Prequotient.zero) RingCat.Colimits.Prequotient.zero
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.mem_toGrothendieck_iff : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Precoverage C} {X : C}
  {S : CategoryTheory.Sieve X}, S ∈ J.toGrothendieck X ↔ J.Saturate X S
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.coe_bot : ∀ {M : Type u_1} [inst : MulOneClass M], ↑⊥ = {1}
-- Lean.LocalContext
Lean.LocalContext.mkBinding : Bool → Lean.LocalContext → Array Lean.Expr → Lean.Expr → optParam Bool true → optParam Bool false → Lean.Expr
-- Mathlib.Order.Defs.Unbundled
Equivalence.stdSymm : ∀ {α : Sort u_1} (r : α → α → Prop), Equivalence r → Std.Symm r
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.norm_div_natCast : ∀ {p : ℝ} [hp : Fact (0 < p)] {m n : ℕ}, ‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.instMonoidalTransportedInverseEquivalenceTransported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          (e : C ≌ D) → (CategoryTheory.Monoidal.equivalenceTransported e).inverse.Monoidal
-- Mathlib.Topology.FiberPartition
TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant : ∀ {S : Type u_1} {Y : Type u_2} [inst : TopologicalSpace S] (l : LocallyConstant S Y) [CompactSpace S],
  Finite (Function.Fiber ⇑l)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.not_connected_sum : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} [Nonempty V] [Nonempty W], ¬(G ⊕g H).Connected
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.continue.injEq : ∀ (ref ref_1 : Lean.Syntax),
  (Lean.Elab.Term.Do.Code.continue ref = Lean.Elab.Term.Do.Code.continue ref_1) = (ref = ref_1)
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.exists_vecMul_eq_zero_iff : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : CommRing A] [IsDomain A] {M : Matrix n n A}
  [inst_3 : DecidableEq n], (∃ v, v ≠ 0 ∧ Matrix.vecMul v M = 0) ↔ M.det = 0
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_app_comp_π_assoc : ∀ {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]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) {G' H' : CategoryTheory.Functor C V}
  (f : G ⟶ G') (ℌ' : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G' H') (c j : C) {Z : V}
  (h : F.obj j ⟹ G'.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((ℌ.map f ℌ').app c) (CategoryTheory.CategoryStruct.comp (ℌ'.π c j) h) =
    CategoryTheory.CategoryStruct.comp (ℌ.π c j)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ihom (F.obj j)).map (f.app (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))) h)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_33 : HAdd Std.Time.Day.Offset Std.Time.Minute.Offset Std.Time.Minute.Offset
-- Aesop.Forward.Substitution
/-- Given `rule` of type `∀ (x₁ : T₁) ... (xₙ : Tₙ), U` and a substitution `σ` for
the arguments `xᵢ`, specialise `rule` with the arguments given by `σ`. That is,
construct `U t₁ ... tₙ` where `tⱼ` is `σ(xⱼ)` if `xⱼ ∈ dom(σ)` and is otherwise
a fresh fvar, then λ-abstract the fresh fvars.  -/
Aesop.Substitution.specializeRule : Lean.Expr → Aesop.Substitution → Lean.MetaM Lean.Expr
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonMarkupContent : Lean.FromJson Lean.Lsp.MarkupContent
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimits F],
  CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.power_def : ∀ (α β : Type u), Cardinal.mk α ^ Cardinal.mk β = Cardinal.mk (β → α)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.prevn.eq_2 : ∀ (x : String.Legacy.Iterator) (n : ℕ), x.prevn n.succ = x.prev.prevn n
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.val_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M} (h : a ≠ 1),
  ↑(FiniteMulArchimedeanClass.mk a h) = MulArchimedeanClass.mk a
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.coe_top : ∀ {M : Type u_1} [inst : MulOneClass M], ↑⊤ = Set.univ
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_map_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {U V : N} (g : V ⟶ U) {X : C} (f : p.obj U ⟶ X),
  CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk (CategoryTheory.CategoryStruct.comp (p.map g) f) =
    CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk f
-- Init.Data.Option.Lemmas
Option.rel_some_some : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {r : α → β → Prop}, Option.Rel r (some a) (some b) ↔ r a b
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toArray_eq_toArray_rcc : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α], r.toArray = (Std.PRange.UpwardEnumerable.least...=r.upper).toArray
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.op_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g),
  h.op.i = CategoryTheory.Arrow.homMk (CategoryTheory.Arrow.Hom.right h.r).op (CategoryTheory.Arrow.Hom.left h.r).op ⋯
-- Mathlib.Algebra.BigOperators.Finprod
/-- Note that `b ∈ (s.filter (fun ab => Prod.fst ab = a)).image Prod.snd` iff `(a, b) ∈ s` so
we can simplify the right-hand side of this lemma. However the form stated here is more useful for
iterating this lemma, e.g., if we have `f : α × β × γ → M`.  -/
finprod_mem_finset_product' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] [inst_1 : DecidableEq α] [inst_2 : DecidableEq β]
  (s : Finset (α × β)) (f : α × β → M),
  ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- The canonical (semiring) equivalence between `WithAbs v` and `WithAbs w`, for any two
absolute values `v` and `w` on `R`.  -/
WithAbs.equivWithAbs : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] →
      [inst_1 : PartialOrder S] → [inst_2 : Semiring R] → (v w : AbsoluteValue R S) → WithAbs v ≃+* WithAbs w
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If an affine subspace contains a set of points, it contains the affine span of that set.  -/
affineSpan_le_of_subset_coe : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {s₁ : AffineSubspace k P}, s ⊆ ↑s₁ → affineSpan k s ≤ s₁
-- Mathlib.Analysis.Convex.Visible
/-- If a point `x` sees a convex combination of points of a set `s` through `convexHull ℝ s ∌ x`,
then it sees all terms of that combination.

Note that the converse does not hold.  -/
IsVisible.of_convexHull_of_pos : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup V] [inst_4 : Module 𝕜 V] {s : Set V} {x : V} {ι : Type u_4} {t : Finset ι} {a : ι → V}
  {w : ι → 𝕜},
  (∀ i ∈ t, 0 ≤ w i) →
    ∑ i ∈ t, w i = 1 →
      (∀ i ∈ t, a i ∈ s) →
        x ∉ (convexHull 𝕜) s →
          IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i) →
            ∀ {i : ι}, i ∈ t → 0 < w i → IsVisible 𝕜 ((convexHull 𝕜) s) x (a i)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakPullback.lift_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C} (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.lift h k w)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.fst f g) h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Mathlib.CategoryTheory.SmallObject.Basic
CategoryTheory.MorphismProperty.isCardinalForSmallObjectArgument_smallObjectκ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C)
  [inst_1 : I.HasSmallObjectArgument], I.IsCardinalForSmallObjectArgument I.smallObjectκ
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_one : ∀ {𝕜 : Type u_1} {E : Type u_2} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G],
  ContinuousLinearMap.rTensor G 1 = 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.toAffineMap_inj : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂}, ↑e = ↑e' ↔ e = e'
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the reverse direction of `hasDerivWithinAt_Ioi_iff_Ici`. -/
HasDerivWithinAt.Ioi_of_Ici : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_3 : PartialOrder 𝕜],
  HasDerivWithinAt f f' (Set.Ici x) x → HasDerivWithinAt f f' (Set.Ioi x) x
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_iff_eq_or_gt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a < Order.succ b ↔ b = a ∨ a < b
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.trans : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ₁ μ₂ μ₃ : MeasureTheory.Measure α},
  μ₁.AbsolutelyContinuous μ₂ → μ₂.AbsolutelyContinuous μ₃ → μ₁.AbsolutelyContinuous μ₃
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.Hom.mk.eq_1 : ∀ {a b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)), SimplexCategory.Hom.mk f = f
-- Init.Data.Int.Pow
Int.pow_lt_pow_of_lt : ∀ {a : ℤ} {b c : ℕ}, 1 < a → b < c → a ^ b < a ^ c
-- Mathlib.Topology.Algebra.UniformConvergence
instModuleUniformOnFun : {α : Type u_1} →
  {β : Type u_2} →
    {R : Type u_4} →
      {𝔖 : Set (Set α)} →
        [inst : Semiring R] → [inst_1 : AddCommMonoid β] → [Module R β] → Module R (UniformOnFun α β 𝔖)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_union_add_inter' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ (t : Set α), μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
-- Std.Time.Date.Unit.Month
/-- Checks if a given day is valid for the specified month and year. For example, `29/02` is valid only
if the year is a leap year.
 -/
Std.Time.Month.Ordinal.Valid : Bool → Std.Time.Month.Ordinal → Std.Time.Day.Ordinal → Prop
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
/-- Bundle a subgroup with typeclass assumptions of normality and finite index.  -/
FiniteIndexNormalSubgroup.ofSubgroup : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → [H.Normal] → [H.FiniteIndex] → FiniteIndexNormalSubgroup G
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.insertMany_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {k : α}, t.insertMany [k] = t.insert k
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (I : FractionalIdeal (nonZeroDivisors R) K),
  FractionalIdeal.count K v I =
    if x : I = 0 then 0
    else
      have a := Classical.choose ⋯;
      have J := Classical.choose ⋯;
      ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
-- Mathlib.LinearAlgebra.Basis.Basic
Submodule.eq_top_iff_forall_basis_mem : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {p : Submodule R M}, p = ⊤ ↔ ∀ (i : ι), b i ∈ p
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.adjoin_algebra_injective : ∀ (n : ℕ) (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K],
  Function.Injective ⇑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))