mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instCommMonoid : CommMonoid ℕ
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instMonoidHomClassCircle : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A], MonoidHomClass (PontryaginDual A) A Circle
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_alter_eq_self_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {f : Option β → Option β},
      m.contains k = true →
        (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isSome = true →
          (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).size = (↑m).size
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instContinuousNeg : ∀ {X : Type u_3} {R : Type u_4} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R], ContinuousNeg (ContinuousMapZero X R)
-- Lean.Meta.Tactic.Rfl
/-- Helper theorem for `Lean.MVarId.liftReflToEq`.  -/
Lean.Meta.Rfl.rel_of_eq_and_refl : ∀ {α : Sort u_1} {R : α → α → Prop} {x y : α}, x = y → R x x → R x y
-- Mathlib.Order.Irreducible
not_infPrime_top : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderTop α], ¬InfPrime ⊤
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.coe_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.ElementaryEmbedding M N), ⇑f.toEmbedding = ⇑f
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- If a function is analytic at a point, then its second derivative is symmetric.  -/
ContDiffAt.isSymmSndFDerivAt_of_omega : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  ContDiffAt 𝕜 ⊤ f x → IsSymmSndFDerivAt 𝕜 f x
-- Init.Data.Array.Monadic
Array.foldlM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {xs : Array α} {f : β → α → m β} {init : β},
  Array.foldlM f init (wfParam xs) = Array.foldlM f init xs.attach.unattach
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.WeaklyRegular], μ.InnerRegularWRT IsClosed fun s => MeasurableSet s ∧ μ s ≠ ⊤
-- Mathlib.Analysis.Normed.Group.Continuity
closure_one_eq : ∀ {E : Type u_4} [inst : SeminormedGroup E], closure {1} = {x | ‖x‖ = 0}
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Notation for an `AddEquiv`.  -/
«term_≃+_» : Lean.TrailingParserDescr
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  {μa : autoParam (MeasureTheory.Measure α) MeasureTheory.MeasurePreserving._auto_1}
  {μb : autoParam (MeasureTheory.Measure β) MeasureTheory.MeasurePreserving._auto_3},
  MeasureTheory.MeasurePreserving f μa μb → Measurable f
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instContinuousLineDerivTopENat : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F],
  ContinuousLineDeriv E (TestFunction Ω F ⊤) (TestFunction Ω F ⊤)
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.piLpCongrLeft_single : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {ι' : Type u_7}
  [inst_3 : Fintype ι'] [inst_4 : DecidableEq ι'] (e : ι' ≃ ι) (i' : ι') (v : 𝕜),
  (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) (EuclideanSpace.single i' v) = EuclideanSpace.single (e i') v
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The singleton presieve.  -/
CategoryTheory.Presieve.singleton : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (Y ⟶ X) → CategoryTheory.Presieve X
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.InitResults.mk.inj : ∀ {α : Type} {tree : Lean.Meta.RefinedDiscrTree.PreDiscrTree α}
  {errors : Array Lean.Meta.RefinedDiscrTree.ImportFailure✝} {tree_1 : Lean.Meta.RefinedDiscrTree.PreDiscrTree α}
  {errors_1 : Array Lean.Meta.RefinedDiscrTree.ImportFailure✝},
  { tree := tree, errors := errors } = { tree := tree_1, errors := errors_1 } → tree = tree_1 ∧ errors = errors_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], (m₁.union! m₂).get! k = m₂.getD k (m₁.get! k)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_union_le_size_add_size : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ ∪ m₂).size ≤ m₁.size + m₂.size
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.instMeasurableMul₂ : MeasurableMul₂ ENNReal
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.StateStack : Type → Type → Type → Type
-- Lean.SubExpr
Lean.SubExpr.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (pos : Lean.SubExpr.Pos), sizeOf { expr := expr, pos := pos } = 1 + sizeOf expr + sizeOf pos
-- Mathlib.Data.List.SplitLengths
_private.Mathlib.Data.List.SplitLengths.0.List.splitLengths.match_3.eq_2 : ∀ {α : Type u_1} (motive : List ℕ → List α → Sort u_2) (n : ℕ) (ns : List ℕ) (x : List α)
  (h_1 : (x : List α) → motive [] x) (h_2 : (n : ℕ) → (ns : List ℕ) → (x : List α) → motive (n :: ns) x),
  (match n :: ns, x with
    | [], x => h_1 x
    | n :: ns, x => h_2 n ns x) =
    h_2 n ns x
-- Mathlib.Data.Seq.Computation
Computation.liftRelAux_inl_inl : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {a : α} {b : β},
  Computation.LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b
-- Aesop.RuleTac.Forward
Aesop.RuleTac.assertForwardHyp : Lean.MVarId → Lean.Meta.Hypothesis → ℕ → Aesop.ScriptM (Lean.FVarId × Lean.MVarId)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.A_mono : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} (L : F) (r : ℝ) {ε δ : ℝ},
  ε ≤ δ → RightDerivMeasurableAux.A f L r ε ⊆ RightDerivMeasurableAux.A f L r δ
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.forgetAdjToOver_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Z : C), (CategoryTheory.forgetAdjToOver X).counit.app Z = CategoryTheory.SemiCartesianMonoidalCategory.fst Z X
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.toLowerSet_ofLowerSet : ∀ {α : Type u_1} (a : Topology.WithLowerSet α),
  Topology.WithLowerSet.toLowerSet (Topology.WithLowerSet.ofLowerSet a) = a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α} {h_contains : (m₁.diff m₂).contains k = true},
  (m₁.diff m₂).get k h_contains = m₁.get k ⋯
-- Lean.Elab.InfoTree.Types
Lean.Elab.DelabTermInfo.mk.injEq : ∀ (toTermInfo : Lean.Elab.TermInfo) (location? : Option Lean.DeclarationLocation)
  (mkDocString? : Option (Lean.PPContext → IO String)) (explicit : Bool) (toTermInfo_1 : Lean.Elab.TermInfo)
  (location?_1 : Option Lean.DeclarationLocation) (mkDocString?_1 : Option (Lean.PPContext → IO String))
  (explicit_1 : Bool),
  ({ toTermInfo := toTermInfo, location? := location?, mkDocString? := mkDocString?, explicit := explicit } =
      { toTermInfo := toTermInfo_1, location? := location?_1, mkDocString? := mkDocString?_1,
        explicit := explicit_1 }) =
    (toTermInfo = toTermInfo_1 ∧ location? = location?_1 ∧ mkDocString? = mkDocString?_1 ∧ explicit = explicit_1)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- The right inclusion in the constructed pushout `Pushout f g`.  -/
CategoryTheory.Limits.Types.Pushout.inr : {S X₁ X₂ : Type u} → (f : S ⟶ X₁) → (g : S ⟶ X₂) → X₂ ⟶ CategoryTheory.Limits.Types.Pushout f g
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertMany_list_eq_empty_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, t.insertMany l = ∅ ↔ t = ∅ ∧ l = []
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_assoc : ∀ (a : ℤ) {b c : ℤ}, c ∣ b → (a * b).tdiv c = a * b.tdiv c
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.mk : {α : Type u_1} → {f : Filter α} → (σ : Type u_5) → (F : CFilter (Set α) σ) → F.toFilter = f → f.Realizer
-- Mathlib.ModelTheory.Satisfiability
/-- A theory is satisfiable if a structure models it.  -/
FirstOrder.Language.Theory.IsSatisfiable : {L : FirstOrder.Language} → L.Theory → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.instPreservesLimitsOfShapeOppositeOfIsGroupoid : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {I : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.IsGroupoid I]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape I F],
  CategoryTheory.Limits.PreservesLimitsOfShape Iᵒᵖ F
-- Mathlib.CategoryTheory.Limits.Final
/-- Given a cocone over `F ⋙ G`, we can construct a `Cocone G` with the same cocone point.
 -/
CategoryTheory.Functor.Final.extendCocone : {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.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  CategoryTheory.Functor (CategoryTheory.Limits.Cocone (F.comp G)) (CategoryTheory.Limits.Cocone G)
-- Mathlib.Util.Notation3
/-- If `pp.tagAppFns` is true and the head of the current expression is a constant,
then delaborates the head and uses it for the ref.
This causes tokens inside the syntax to refer to this constant.
A consequence is that docgen will linkify the tokens.
 -/
Mathlib.Notation3.withHeadRefIfTagAppFns : Lean.PrettyPrinter.Delaborator.Delab → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.basicOpenIsoSpecAway_hom_SpecMap_assoc : ∀ {R : CommRingCat} (f : ↑R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of ↑R) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.basicOpenIsoSpecAway f).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Opens.ι (PrimeSpectrum.basicOpen f)) h
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAdjointPair.mul : ∀ {R : Type u_1} {M : Type u_5} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃}
  {f g f' g' : Module.End R M},
  B.IsAdjointPair B ⇑f ⇑g → B.IsAdjointPair B ⇑f' ⇑g' → B.IsAdjointPair B ⇑(f * f') ⇑(g' * g)
-- Init.Data.String.Slice
/-- Removes leading whitespace from a slice by moving its start position to the first non-whitespace
character, or to its end position if there is no non-whitespace character.

“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.

Examples:

* `"abc".toSlice.trimAsciiStart == "abc".toSlice`

* `"   abc".toSlice.trimAsciiStart == "abc".toSlice`

* `"abc \t  ".toSlice.trimAsciiStart == "abc \t  ".toSlice`

* `"  abc   ".toSlice.trimAsciiStart == "abc   ".toSlice`

* `"abc\ndef\n".toSlice.trimAsciiStart == "abc\ndef\n".toSlice`
 -/
String.Slice.trimAsciiStart : String.Slice → String.Slice
-- Mathlib.RingTheory.Ideal.Quotient.Index
/-- Let `N` be a finite index f.g. `R`-submodule, and `I` be a finite index ideal.
Then `I • N` also has finite index.  -/
Submodule.finite_quotient_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  {N : Submodule R M} [Finite (R ⧸ I)] [Finite (M ⧸ N)], N.FG → Finite (M ⧸ I • N)
-- Mathlib.Topology.Maps.Basic
isOpenMap_iff_image_interior : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f ↔ ∀ (s : Set X), f '' interior s ⊆ interior (f '' s)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- A map `incl(X) ⟶ Y` is specified by an element of `Y`'s indexing set, and then a morphism
`X ⟶ Y.obj i` in the original category.  -/
CategoryTheory.Limits.FormalCoproduct.Hom.asSigma : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {Y : CategoryTheory.Limits.FormalCoproduct C} →
        ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y) → (i : Y.I) × (X ⟶ Y.obj i)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables. If `f` has continuous derivative `f'` on `[a, b]`,
and `g` is continuous on `f '' [a, b]`, then we can substitute `u = f x` to get
`∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
Compared to `intervalIntegral.integral_comp_mul_deriv` we only require that `g` is continuous on
`f '' [a, b]`.
 -/
intervalIntegral.integral_comp_mul_deriv' : ∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    ContinuousOn f' (Set.uIcc a b) →
      ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_sup : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (S T : L.Substructure M) (f : L.Hom M N),
  FirstOrder.Language.Substructure.map f (S ⊔ T) =
    FirstOrder.Language.Substructure.map f S ⊔ FirstOrder.Language.Substructure.map f T
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceNe : Lean.Meta.Simp.Simproc
-- Mathlib.Order.Lattice
Subtype.semilatticeInf.eq_1 : ∀ {α : Type u} [inst : SemilatticeInf α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)),
  Subtype.semilatticeInf Psup =
    { toPartialOrder := Subtype.partialOrder fun x => P x, inf := fun x y => ⟨↑x ⊓ ↑y, ⋯⟩, inf_le_left := ⋯,
      inf_le_right := ⋯, le_inf := ⋯ }
-- Mathlib.Data.EReal.Operations
EReal.mul_sub_of_nonneg_of_ne_top : ∀ {a b c : EReal}, 0 ≤ a → a ≠ ⊤ → a * (b - c) = a * b - a * c
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
/-- Right unitor for the vertical composition of strong natural transformations
between pseudofunctors.  -/
CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.id G) ≅ η
-- Mathlib.MeasureTheory.Function.EssSup
essSup.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] {x : MeasurableSpace α} (f : α → β)
  (μ : MeasureTheory.Measure α), essSup f μ = Filter.limsup f (MeasureTheory.ae μ)
-- Mathlib.Topology.Order.DenselyOrdered
instNeBotNhdsWithinComplSetSingletonOfNontrivial : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] (x : α)
  [Nontrivial α], (nhdsWithin x {x}ᶜ).NeBot
-- Mathlib.Algebra.Group.Conj
isConj_iff_eq : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, IsConj a b ↔ a = b
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instAddCommMonoid : {R : Type u_1} → [inst : AddCommMonoid R] → AddCommMonoid (ArithmeticFunction R)
-- Mathlib.CategoryTheory.ObjectProperty.Comma
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsCommaComma : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (F₁ : CategoryTheory.Functor C₁ D) (F₂ : CategoryTheory.Functor C₂ D) (P₁ : CategoryTheory.ObjectProperty C₁)
  (P₂ : CategoryTheory.ObjectProperty C₂) [P₁.IsClosedUnderIsomorphisms] [P₂.IsClosedUnderIsomorphisms],
  (CategoryTheory.ObjectProperty.comma F₁ F₂ P₁ P₂).IsClosedUnderIsomorphisms
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
/-- The condition that a pairing only involves inner horns.  -/
SSet.Subcomplex.Pairing.IsInner : {X : SSet} → {A : X.Subcomplex} → (P : A.Pairing) → [P.IsProper] → Prop
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.mkD_of_continuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : α → β}
  {g : C(↑s, β)} (hf : ContinuousOn f s),
  ContinuousMap.mkD (s.domRestrict f) g = { toFun := s.domRestrict f, continuous_toFun := ⋯ }
-- Mathlib.Order.LiminfLimsup
Filter.frequently_lt_of_lt_limsSup : ∀ {α : Type u_1} {f : Filter α} [inst : ConditionallyCompleteLinearOrder α] {a : α},
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) Filter.frequently_lt_of_lt_limsSup._auto_1 →
    a < f.limsSup → ∃ᶠ (n : α) in f, a < n
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instNegOffset : Neg Std.Time.Minute.Offset
-- Init.Core
/-- If `r a b`, then `TransGen r a b`. This is the base case of the transitive closure.  -/
Relation.TransGen.single : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Relation.TransGen r a b
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.isValidForSlice' : ∀ {pat s : String.Slice} {needlePos stackPos : String.Pos.Raw},
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos →
    needlePos = 0 → String.Pos.Raw.IsValidForSlice s stackPos
-- Std.Time.DateTime.Timestamp
/-- Adds a `Week.Offset` to the given `Timestamp`.
 -/
Std.Time.Timestamp.addWeeks : Std.Time.Timestamp → Std.Time.Week.Offset → Std.Time.Timestamp
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_nsmul_eq_nsmul_val : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) (n : ℕ), ↑(n • a) = n • ↑a
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.IsCyclicallyReduced.singleton : ∀ {α : Type u} {x : α × Bool}, FreeAddGroup.IsCyclicallyReduced [x]
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_ne_nil_iff : ∀ {m n : ℕ}, (m<...=n).toList ≠ [] ↔ m < n
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- If `G` is generated by `S`, then the quotient by the center embeds into `S`-indexed sequences
of commutators.  -/
Subgroup.quotientCenterEmbedding : {G : Type u_1} →
  [inst : Group G] → {S : Set G} → Subgroup.closure S = ⊤ → G ⧸ Subgroup.center G ↪ ↑S → ↑(commutatorSet G)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.restrict_subset_loops_eq : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, X ⊆ M.loops → M.restrict X = Matroid.loopyOn X
-- Lean.Compiler.ModPkgExt
/-- Sets the package of the current module.  -/
Lean.Environment.setModulePackage : Option Lean.PkgId → Lean.Environment → Lean.Environment
-- Mathlib.Order.CompleteLattice.Defs
CompleteLattice.toInfSet : {α : Type u_8} → [self : CompleteLattice α] → InfSet α
-- Mathlib.Computability.StateTransition
StateTransition.reaches₀_eq : ∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ}, f a = f b → StateTransition.Reaches₀ f a b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_id_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} {f : Z ⟶ X},
  CategoryTheory.IsPushout f (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) f
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.hom_ext_iff : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_7}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {f g : PolynomialModule R M →ₗ[R] M'},
  f = g ↔ ∀ (a : ℕ), f ∘ₗ PolynomialModule.lsingle R a = g ∘ₗ PolynomialModule.lsingle R a
-- Mathlib.Topology.Instances.Matrix
/-- To show a function into matrices is continuous it suffices to show the coefficients of the
resulting matrix are continuous  -/
continuous_matrix : ∀ {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace α]
  {f : α → Matrix m n R}, (∀ (i : m) (j : n), Continuous fun a => f a i j) → Continuous f
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_of_isLocalized'_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Rₚ : ↑s → Type u_4) [inst_3 : (r : ↑s) → CommSemiring (Rₚ r)] [inst_4 : (r : ↑s) → Algebra R (Rₚ r)]
      [inst_5 : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)] (Mₚ : ↑s → Type u_5)
      [inst_6 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_7 : (r : ↑s) → Module R (Mₚ r)]
      [inst_8 : (r : ↑s) → Module (Rₚ r) (Mₚ r)] [inst_9 : ∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_10 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N P : Submodule R M},
      (∀ (r : ↑s),
          Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N =
            Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) P) →
        N = P
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableOn.comp : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {s : Set M} {g : M' → M''} {u : Set M'}, MDiff[u] g → MDiff[s] f → s ⊆ f ⁻¹' u → MDiff[s] (g ∘ f)
-- Mathlib.Topology.Algebra.Ring.Basic
Subsemiring.topologicalClosure_minimal : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [inst_2 : IsSemitopologicalSemiring R]
  (s : Subsemiring R) {t : Subsemiring R}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Init.Data.Array.Lemmas
Array.toList_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α}, (Array.replicate n a).toList = List.replicate n a
-- Mathlib.LinearAlgebra.LinearPMap
Prod.swap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (p : α × β), p.swap = (p.2, p.1)