mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Taking the divisor of a meromorphic function commutes with restriction.
 -/
MeromorphicOn.divisor_restrict : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {V : Set 𝕜},
  MeromorphicOn f U → ∀ (hV : V ⊆ U), (MeromorphicOn.divisor f U).restrict hV = MeromorphicOn.divisor f V
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.eval_surjective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : M), Function.Surjective ⇑(smoothSheafCommRing.eval IM I M R x)
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverBind : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        [inst_2 : P.IsStableUnderComposition] →
          {X : AlgebraicGeometry.Scheme} →
            (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
              (𝒱 : (x : 𝒰.I₀) → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) (𝒰.X x)) →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [(x : 𝒰.I₀) → AlgebraicGeometry.Scheme.Cover.Over S (𝒱 x)] →
                      AlgebraicGeometry.Scheme.Cover.Over S (CategoryTheory.Precoverage.ZeroHypercover.bind 𝒰 𝒱)
-- Init.Core
/-- Places an element of a type into the quotient that equates terms according to an equivalence
relation.

The equivalence relation is found by synthesizing a `Setoid` instance. `Quotient.mk` instead expects
the instance to be provided explicitly.

Given `v : α`, `Quotient.mk' v : Quotient s` is like `v`, except all observations of `v`'s value
must respect `s.r`. `Quotient.lift` allows values in a quotient to be mapped to other types, so long
as the mapping respects `s.r`.

 -/
Quotient.mk' : {α : Sort u} → [s : Setoid α] → α → Quotient s
-- Mathlib.Topology.Neighborhoods
isOpen_setOfPred_eventually_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, IsOpen {x | ∀ᶠ (y : X) in nhds x, p y}
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.iInter_of_orderTop : ∀ {α : Type v} [inst : LinearOrder α] {ι : Type u_1} {f : ι → Set α} [OrderTop α],
  (∀ (i : ι), IsClub (f i)) → IsClub (⋂ i, f i)
-- Mathlib.Algebra.Group.Subgroup.Order
Subgroup.isCoatom_comap_of_surjective : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] {φ : G →* H},
  Function.Surjective ⇑φ → ∀ {M : Subgroup H}, IsCoatom M → IsCoatom (Subgroup.comap φ M)
-- Mathlib.ModelTheory.Syntax
/-- Applies a unary relation to a term as a formula.  -/
FirstOrder.Language.Relations.formula₁ : {L : FirstOrder.Language} → {α : Type u'} → L.Relations 1 → L.Term α → L.Formula α
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_apply_right : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) (i : ι) (m : M), (b.toDual (b i)) m = (b.repr m) i
-- Mathlib.Algebra.GroupWithZero.Units.Basic
inv_mul_eq_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, a ≠ 0 → (a⁻¹ * b = 1 ↔ a = b)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.isZero_of_subsingleton : ∀ (V : SemiNormedGrp₁) [Subsingleton V.carrier], CategoryTheory.Limits.IsZero V
-- Mathlib.Topology.Sober
genericPoints.component_surjective : ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSober α], Function.Surjective genericPoints.component
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The inverse function of a measurable equivalence is measurable.  -/
MeasurableEquiv.measurable_invFun : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (self : α ≃ᵐ β),
  Measurable ⇑self.symm
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.arrowCongr_apply : ∀ {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [inst : Mul P] [inst_1 : Mul Q] (f : M ≃ N)
  (g : P ≃* Q) (h : M → P) (n : N), (MulEquiv.arrowCongr f g) h n = g (h (f.symm n))
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_singleton : ∀ {α : Type u_1} {G : SimpleGraph α} (a : α), G.IsClique {a}
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.pow_vle_pow : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {a b : R}, a ≤ᵥ b → ∀ (n : ℕ), a ^ n ≤ᵥ b ^ n
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.getNumIndices : Lean.MVarId → Lean.MetaM ℕ
-- Std.Async.System
Std.Async.System.CPUInfo.mk : String → ℕ → Std.Async.System.CPUTimes → Std.Async.System.CPUInfo
-- Lean.Parser.Term
Lean.Parser.Term.num : Lean.Parser.Parser
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x`, `0 x = 0`, and
`(n • f) x = n • f x` is a left cancel additive monoid if `β` is a left cancel additive monoid.  -/
FunLike.addLeftCancelMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : AddLeftCancelMonoid β] →
                [IsZeroApply F α β] → [IsAddApply F α β] → [IsSMulApply ℕ F α β] → AddLeftCancelMonoid F
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_sup : ∀ {M : Type u_2} [inst : AddZeroClass M] (S₁ S₂ : AddSubmonoid M), (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
-- Aesop.RuleTac.Basic
/-- If the rule has a pattern, the pattern substitutions that were found in
the goal. Each substitution is a list of expressions which were found by
matching the pattern against expressions in the goal. For example, if `h : max
a b = max a c` appears in the goal and the rule has pattern `max x y`, there
will be two substitutions `{x ↦ a, y ↦ b}`) and `{x ↦ a, y ↦ c}`.

If the rule does not have a pattern, this is `none`. Otherwise it is
guaranteed to be `some xs` with `xs` non-empty and duplicate-free.  -/
Aesop.RuleTacInput.patternSubsts? : Aesop.RuleTacInput → Option (Array Aesop.Substitution)
-- Mathlib.Condensed.Light.Functors
/-- The functor from `LightProfinite` to `LightCondSet` preserves countable limits.
 -/
instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory : ∀ {J : Type} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J],
  CategoryTheory.Limits.PreservesLimitsOfShape J lightProfiniteToLightCondSet
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E}, Meromorphic f → Meromorphic g → Meromorphic (f + g)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).minKey? = t.minKey? ↔ ∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.Data.Finset.Sort
Finset.sort_eq : ∀ {α : Type u_1} (s : Finset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], ↑(s.sort r) = s.val
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.struct.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.struct = 1
-- Init.Core
/-- Right injection into the sum type `α ⊕' β`.  -/
PSum.inr : {α : Sort u} → {β : Sort v} → β → α ⊕' β
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
one_lt_zpow : ∀ {G : Type u_2} [inst : DivInvMonoid G] [inst_1 : Preorder G] [MulLeftMono G] {x : G},
  1 < x → ∀ {n : ℤ}, 0 < n → 1 < x ^ n
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- A matrix ring is isomorphic to the opposite of an endomorphism ring.  -/
matrixRingEquivEndVecMulOpposite : {ι : Type u_1} →
  [inst : Fintype ι] →
    [DecidableEq ι] → {A : Type u_3} → [inst_2 : Semiring A] → Matrix ι ι A ≃+* (Module.End A (ι → A))ᵐᵒᵖ
-- Aesop.Forward.Match.Types
Aesop.instOrdCompleteMatch : Ord Aesop.CompleteMatch
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorHomMk_app_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  (A B : CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C))
  (hom₁ : A.comp CategoryTheory.Pretriangulated.Triangle.π₁ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₁)
  (hom₂ : A.comp CategoryTheory.Pretriangulated.Triangle.π₂ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₂)
  (hom₃ : A.comp CategoryTheory.Pretriangulated.Triangle.π₃ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₃)
  (comm₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂) hom₂ =
        CategoryTheory.CategoryStruct.comp hom₁ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂))
      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_1)
  (comm₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃) hom₃ =
        CategoryTheory.CategoryStruct.comp hom₂ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃))
      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_3)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)
          (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
        CategoryTheory.CategoryStruct.comp hom₃ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁))
      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_5)
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorHomMk A B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₃ = hom₃.app j
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.isZero_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → S.f = 0 → S.g = 0 → CategoryTheory.Limits.IsZero S.X₂
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.eq_comp_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {α : Type u_9} (e : M ≃* N) (f : N → α) (g : M → α),
  f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mk_eq_bot_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : Submodule R M}
  {h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier}, { toSubmodule := N, lie_mem := h } = ⊥ ↔ N = ⊥
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_alter_le_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, (t.alter k f).size ≤ t.size + 1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonMonoidHom_apply : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : MulOneClass α] (a : α), Finset.singletonMonoidHom a = {a}
-- Mathlib.Data.ZMod.Basic
ZMod.val_add : ∀ {n : ℕ} [NeZero n] (a b : ZMod n), (a + b).val = (a.val + b.val) % n
-- Mathlib.Data.Matrix.Basic
Matrix.diag_sum : ∀ {n : Type u_3} {α : Type u_11} {ι : Type u_14} [inst : AddCommMonoid α] (s : Finset ι) (f : ι → Matrix n n α),
  (∑ i ∈ s, f i).diag = ∑ i ∈ s, (f i).diag
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.sub_one_left_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, y ∣ x → IsRelPrime (x - 1) y
-- Init.Data.Nat.Lemmas
Nat.add_le_mul : ∀ {a : ℕ}, 2 ≤ a → ∀ {b : ℕ}, 2 ≤ b → a + b ≤ a * b
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- For a subgroup `𝒢` of `GL(2, R)`, this is the additive group of `x : R` such that
`[1, x; 0, 1] ∈ 𝒢`.  -/
Subgroup.strictPeriods : {R : Type u_1} → [inst : Ring R] → Subgroup (GL (Fin 2) R) → AddSubgroup R
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insert_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {fallback v : β},
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl k fallback = v
-- Lean.DocString.Parser
/-- Replaces any error from `p` at the initial position with `expected msg`. This ensures that
each sub-parser of `delimitedInline` contributes a clear expected-token name, and clears
unhelpful generic "unexpected" messages from inner parsers so that the more informative message
from `inlineTextChar` survives error merging via `<|>`.
 -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.expectedFn : String → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → k ∉ m₁ ∩ m₂
-- Lean.DocString.Types
Lean.Doc.instInhabitedPart.default : {i : Type u} → {b : Type v} → {p : Type w} → Lean.Doc.Part i b p
-- Aesop.Tree.State
Aesop.GoalRef.markProvenByNormalization : Aesop.GoalRef → BaseIO Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Subcomplex.toOfSimplex_ι_assoc : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.toOfSimplex x)
      (CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.ofSimplex x).ι h) =
    CategoryTheory.CategoryStruct.comp (SSet.yonedaEquiv.symm x) h
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpEquiv_inverse_obj : ∀ (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.Functor.leftOpRightOpEquiv C D).inverse.obj F = Opposite.op F.leftOp
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.toArrow_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C}
  (η : X ⟶ Y),
  (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).right =
    CategoryTheory.SimplicialObject.Augmented.point.map η
-- Mathlib.ModelTheory.Order
FirstOrder.Language.model_dlo : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LinearOrder M]
  [L.OrderedStructure M] [DenselyOrdered M] [NoTopOrder M] [NoBotOrder M], M ⊨ L.dlo
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_le_exponent : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α],
  0 < AddMonoid.exponent M → ∀ (m : M) (a : α), AddAction.period m a ≤ AddMonoid.exponent M
-- Mathlib.RingTheory.AdjoinRoot
/-- `R`-algebra homomorphism from `R[x]` to `AdjoinRoot f` sending `X` to the `root`.  -/
AdjoinRoot.mkₐ : {R : Type u_1} → [inst : CommRing R] → (f : Polynomial R) → Polynomial R →ₐ[R] AdjoinRoot f
-- Mathlib.Topology.LocallyFinsupp
/-- The negative part of a sum is less than or equal to the sum of the negative parts.
 -/
Function.locallyFinsuppWithin.negPart_add : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y]
  [inst_2 : LinearOrder Y] [IsOrderedAddMonoid Y] (f₁ f₂ : Function.locallyFinsuppWithin U Y), (f₁ + f₂)⁻ ≤ f₁⁻ + f₂⁻
-- Mathlib.GroupTheory.Subsemigroup.Lemmas
AddSubsemigroup.center_sum : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N],
  AddSubsemigroup.center (M × N) = (AddSubsemigroup.center M).prod (AddSubsemigroup.center N)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- **Alias** of `RingHom.IsIntegral.to_finite`. -/
RingHom.Finite.of_isIntegral_of_finiteType : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.IsIntegral → f.FiniteType → f.Finite
-- Mathlib.Order.Filter.NAry
Filter.map₂_swap : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α → β → γ) (f : Filter α) (g : Filter β),
  Filter.map₂ m f g = Filter.map₂ (fun a b => m b a) g f
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.whiskerHom_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.RightLift f g} (i : s ⟶ t) {x : B} (h : x ⟶ c),
  (CategoryTheory.Bicategory.RightLift.whiskerHom i h).left = CategoryTheory.Bicategory.whiskerLeft h i.left
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.exists_hom_ι_eq_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] [CategoryTheory.IsFilteredOrEmpty J]
  {D : CategoryTheory.Limits.Cocone F} (hD : CategoryTheory.Limits.IsColimit D) (x : CategoryTheory.ToType D.pt)
  (k : J), ∃ j x_1 y, (CategoryTheory.ConcreteCategory.hom (D.ι.app j)) y = x
-- Mathlib.RingTheory.Fintype
ZMod.orderOf_lt : ∀ {n : ℕ}, 1 < n → ∀ (a : ZMod n), orderOf a < n
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- If `i` witnesses that `D` is a reflective subcategory and an exponential ideal, then `D` is
itself Cartesian closed.

Unlike `cartesianClosedOfReflective'` this construction lifts exponential objects in `C` to
exponential objects in `D` by applying the reflector to them, even though they already lie in the
essential image of `i`; if you need better control over definitional equality, use
`cartesianClosedOfReflective'` instead.  -/
CategoryTheory.cartesianClosedOfReflective : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        (i : CategoryTheory.Functor D C) →
          [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
            [CategoryTheory.Reflective i] →
              [inst_4 : CategoryTheory.MonoidalClosed C] →
                [inst_5 : CategoryTheory.CartesianMonoidalCategory D] →
                  [CategoryTheory.ExponentialIdeal i] → CategoryTheory.MonoidalClosed D
-- Mathlib.RepresentationTheory.Subrepresentation
/-- A submodule of an `A[G]`-module `M` can be thought of as a subrepresentation of `ofModule M`.
 -/
Subrepresentation.ofSubmodule : {A : Type u_1} →
  {G : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module (MonoidAlgebra A G) M] →
              Submodule (MonoidAlgebra A G) M → Subrepresentation (Representation.ofModule M)
-- Mathlib.Algebra.Group.TypeTags.Basic
ofMul_toMul : ∀ {α : Type u} (x : Additive α), Additive.ofMul (Additive.toMul x) = x
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsUniversalColimit.precompose_isIso : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} (α : F ⟶ G) [CategoryTheory.IsIso α] {c : CategoryTheory.Limits.Cocone G},
  CategoryTheory.IsUniversalColimit c →
    CategoryTheory.IsUniversalColimit ((CategoryTheory.Limits.Cocone.precompose α).obj c)
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.memberSubfamily_image_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  Finset.memberSubfamily a (Finset.image (fun x => x.erase a) 𝒜) = ∅
-- Mathlib.Topology.MetricSpace.HausdorffDistance
IsClosed.exists_infDist_eq_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [ProperSpace α],
  IsClosed s → s.Nonempty → ∀ (x : α), ∃ y ∈ s, Metric.infDist x s = dist x y
-- Mathlib.Order.Filter.Prod
Filter.mem_coprod_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : Filter α} {g : Filter β},
  s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
/-- The stalks of the structure sheaf of a smooth manifold are local rings.  -/
smoothSheafCommRing.instLocalRing_stalk : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] (x : M),
  IsLocalRing ↑((smoothSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜).presheaf.stalk x)
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_mem_Icc' : ∀ {ι : Type u_1} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f g : (i : ι) → π i}
  [inst_1 : (i : ι) → Preorder (π i)], g ≤ f → s.piecewise f g ∈ Set.Icc g f
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.var.injEq : ∀ {L : FirstOrder.Language} {α : Type u'} (a a_1 : α),
  (FirstOrder.Language.var a = FirstOrder.Language.var a_1) = (a = a_1)
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, panicking if no such key exists.
 -/
Std.ExtDTreeMap.getKeyLE! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtDTreeMap α β cmp → α → α
-- Mathlib.CategoryTheory.Products.Basic
/-- The Cartesian product of two equivalences of categories.  -/
CategoryTheory.Equivalence.prod : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} → [inst_3 : CategoryTheory.Category.{v₄, u₄} D] → (A ≌ B) → (C ≌ D) → (A × C ≌ B × D)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_diff_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (t₁ \ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∈ t₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
SpectrumRestricts.eq_1 : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] [inst_4 : Algebra S A] [inst_5 : Algebra R S] (a : A) (f : S → R),
  SpectrumRestricts a f = QuasispectrumRestricts a f
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.compCreatesColimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {E : Type u₃} →
              [ℰ : CategoryTheory.Category.{v₃, u₃} E] →
                (F : CategoryTheory.Functor C D) →
                  (G : CategoryTheory.Functor D E) →
                    [CategoryTheory.CreatesColimitsOfShape J F] →
                      [CategoryTheory.CreatesColimitsOfShape J G] → CategoryTheory.CreatesColimitsOfShape J (F.comp G)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContinuousLinearEquiv.ofEq.congr_simp : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  {module_M : Module R M} (p q : Submodule R M) (h : p = q),
  ContinuousLinearEquiv.ofEq p q h = ContinuousLinearEquiv.ofEq p q h
-- Mathlib.Topology.Order.LeftRight
nhdsLE_sup_nhdsGE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Iic a) ⊔ nhdsWithin a (Set.Ici a) = nhds a