mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_iff_forall_nat_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : ℕ∞}, ContDiffOn 𝕜 (↑n) f s ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiffOn 𝕜 (↑m) f s
-- Mathlib.Order.BooleanAlgebra.Basic
le_iff_disjoint_sdiff : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], z ≤ y → x ≤ y → (z ≤ x ↔ Disjoint z (y \ x))
-- Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
CategoryTheory.Abelian.instIsStableUnderRetractsEpiWithInjectiveKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.Abelian.epiWithInjectiveKernel.IsStableUnderRetracts
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Any morphism `k : W ⟶ X` satisfying `k ≫ f = 0` induces a morphism `l : W ⟶ kernel f` such that
`l ≫ kernel.ι f = k`.  -/
CategoryTheory.Limits.kernel.lift' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            {W : C} →
              (k : W ⟶ X) →
                CategoryTheory.CategoryStruct.comp k f = 0 →
                  { l // CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.kernel.ι f) = k }
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.associator_map_inl_inl : ∀ (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] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.sum.associator C D E).map
      ((CategoryTheory.Sum.inl_ (C ⊕ D) E).map ((CategoryTheory.Sum.inl_ C D).map f)) =
    (CategoryTheory.Sum.inl_ C (D ⊕ E)).map f
-- Mathlib.Algebra.Algebra.Equiv
LinearEquiv.algEquivOfRing_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (e : R ≃ₗ[R] A)
  (a : R), e.algEquivOfRing a = (↑↑(Algebra.ofId R A).toRingHom).toFun a
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.le_linearGrowthInf_iff : ∀ {u : ℕ → EReal} {a : EReal}, a ≤ LinearGrowth.linearGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in Filter.atTop, b * ↑n ≤ u n
-- Lean.Meta.Transform
_private.Lean.Meta.Transform.0.Lean.Meta.unfoldIfArgIsAppOf.isInterestingArg : Array Lean.Name → ℕ → Lean.Expr → Bool
-- Std.Http.Protocol.H1.Config
/-- Whether to enable keep-alive connections by default.
 -/
Std.Http.Protocol.H1.Config.enableKeepAlive : Std.Http.Protocol.H1.Config → Bool
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.Over.coreHomEquivToOverSections_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (I : C) [inst_2 : CategoryTheory.Closed I]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)]
  [inst_4 : CategoryTheory.BraidedCategory C] (A : C) (X : CategoryTheory.Over I),
  (CategoryTheory.Over.coreHomEquivToOverSections I).homEquiv A X =
    { toFun := CategoryTheory.Over.sectionsCurry, invFun := CategoryTheory.Over.sectionsUncurry, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Order.SuccPred.Basic
Order.not_isMax_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [Nontrivial α] (a : α), ¬IsMax (Order.pred a)
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr.exportEntry? : {α σ : Type} → Lean.SimpleScopedEnvExtension.Descr α σ → Lean.Environment → α → Lean.OLeanEntries (Option α)
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.triangleRotation_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  (CategoryTheory.Pretriangulated.triangleRotation C).functor = CategoryTheory.Pretriangulated.rotate C
-- Lean.Meta.Match.Match
/-- Returns the index of the first pattern in the first alternative that is refutable
(i.e. not a variable or inaccessible pattern). We want to handle these first
so that the generated code branches in the order suggested by the user's code.
 -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.firstRefutablePattern : Lean.Meta.Match.Problem → Option ℕ
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.instCompactSpaceCarrierObjTopCatCompHausLikeToTop : ∀ (P : TopCat → Prop) (X : CompHausLike P), CompactSpace ↑((CompHausLike.compHausLikeToTop P).obj X)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppMatchState.mk.sizeOf_spec : ∀ (info : Lean.Meta.MatcherInfo) (matcherTy : Lean.SubExpr) (motive : Option (Lean.Term × Lean.Expr))
  (motiveNamed : Bool) (discrs : Array Lean.Term) (hNames? : Array (Option Lean.Name)) (alts : Array Lean.SubExpr)
  (varNames : Array (Array Lean.Name)) (rhss : Array Lean.Term),
  sizeOf
      { info := info, matcherTy := matcherTy, motive := motive, motiveNamed := motiveNamed, discrs := discrs,
        hNames? := hNames?, alts := alts, varNames := varNames, rhss := rhss } =
    1 + sizeOf info + sizeOf matcherTy + sizeOf motive + sizeOf motiveNamed + sizeOf discrs + sizeOf hNames? +
          sizeOf alts +
        sizeOf varNames +
      sizeOf rhss
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedSemiring : Inhabited Lean.Meta.Sym.Arith.Semiring
-- Mathlib.Order.Filter.CountableInter
Filter.EventuallyLE.countable_iUnion : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → ⋃ i, s i ≤ᶠ[l] ⋃ i, t i
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.mem_map : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {x : M₂},
  x ∈ Submodule.map f p ↔ ∃ y ∈ p, f y = x
-- Init.Data.Fin.Lemmas
Fin.addNat_zero : ∀ (n : ℕ) (i : Fin n), i.addNat 0 = i
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.IsMonoidalDistrib.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [toIsMonoidalLeftDistrib : CategoryTheory.IsMonoidalLeftDistrib C]
  [toIsMonoidalRightDistrib : CategoryTheory.IsMonoidalRightDistrib C], CategoryTheory.IsMonoidalDistrib C
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.eq_bot_iff_card : ∀ {M : Type u_1} [inst : AddMonoid M] {S : AddSubmonoid M} [inst_1 : Fintype ↥S], S = ⊥ ↔ Fintype.card ↥S = 1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.diagram.eq_1 : ∀ (G : AddGrpCat),
  ProfiniteAddGrp.ProfiniteCompletion.diagram G =
    (ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram G).comp
      (CategoryTheory.forget₂ FiniteAddGrp.{u} ProfiniteAddGrp.{u})
-- Mathlib.Tactic.Widget.StringDiagram
/-- The horizontal position of the node in the string diagram, counting strings in codomains.  -/
Mathlib.Tactic.Widget.StringDiagram.IdNode.hPosTar : Mathlib.Tactic.Widget.StringDiagram.IdNode → ℕ
-- Mathlib.Algebra.Algebra.Operations
Submodule.one_eq_span : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A], 1 = R ∙ 1
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.Tendsto.subseq_mem : ∀ {α : Type u_3} {F : Filter α} {V : ℕ → Set α},
  (∀ (n : ℕ), V n ∈ F) → ∀ {u : ℕ → α}, Filter.Tendsto u Filter.atTop F → ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), u (φ n) ∈ V n
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The operator norm of the projection is `0` if the subspace is dense.  -/
AddSubgroup.norm_trivial_quotient_mk : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M),
  ↑S.topologicalClosure = Set.univ → ‖S.normedMk‖ = 0
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.category_comp_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Square C} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).τ₃ = CategoryTheory.CategoryStruct.comp f.τ₃ g.τ₃
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.ker_dualMap_eq_dualAnnihilator_range : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M₁ →ₗ[R] M₂),
  f.dualMap.ker = f.range.dualAnnihilator
-- Std.Http.Protocol.H1.Parser
/-- Parses a status line and returns a fully-typed `Response.Head`.
`status-line = HTTP-version SP status-code SP [ reason-phrase ]`
Accepts only HTTP/1.1. For parsing where the version may be unrecognized and must be
mapped to an error event, use `parseStatusLineRawVersion`.
 -/
Std.Http.Protocol.H1.parseStatusLine : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.Response.Head
-- Mathlib.Algebra.Order.Floor.Div
gc_floorDiv_mul : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : FloorDiv α α] {a : α},
  0 < a → GaloisConnection (fun x => a * x) fun x => x ⌊/⌋ a
-- Mathlib.Computability.Primrec.Basic
Primcodable.sum : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → Primcodable (α ⊕ β)
-- Lean.Parser.Do
Lean.Parser.Term.doRepeat.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Pointwise.Set.Small
small_set_one : ∀ {α : Type u_1} [inst : One α], Small.{u, u_1} ↑1
-- Mathlib.CategoryTheory.Category.Cat.Colimit
/-- The category of small categories has all small colimits as a reflective subcategory of the
category of simplicial sets, which has all small colimits.  -/
CategoryTheory.Cat.instHasColimits : CategoryTheory.Limits.HasColimits CategoryTheory.Cat
-- Mathlib.Data.Num.Basic
/-- `castNum` casts a `Num` into any type which has `0`, `1` and `+`.  -/
castNum : {α : Type u_1} → [One α] → [Add α] → [Zero α] → Num → α
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.resRec.match_1.eq_2 : ∀ {w : ℕ} (s : ℕ) (motive : (s' : ℕ) → s' + 1 < w → 0 < s' + 1 → s = s'.succ → Sort u_1) (s'' : ℕ)
  (hs : s'' + 1 + 1 < w) (hslt : 0 < s'' + 1 + 1) (hs0 : s = (s'' + 1).succ)
  (h_1 : (hs : 0 + 1 < w) → (hslt : 0 < 0 + 1) → (hs0 : s = Nat.succ 0) → s''.succ = 0 → motive 0 hs hslt hs0)
  (h_2 :
    (s''_1 : ℕ) →
      (hs : s''_1 + 1 + 1 < w) →
        (hslt : 0 < s''_1 + 1 + 1) →
          (hs0 : s = (s''_1 + 1).succ) → s''.succ = s''_1.succ → motive s''_1.succ hs hslt hs0),
  (match hs' : s''.succ, hs, hslt, hs0 with
    | 0, hs, hslt, hs0 => h_1 hs hslt hs0 hs'
    | s''_1.succ, hs, hslt, hs0 => h_2 s''_1 hs hslt hs0 hs') =
    h_2 s'' hs hslt hs0 ⋯
-- Init.Data.BitVec.Lemmas
BitVec.toNat_mul : ∀ {n : ℕ} (x y : BitVec n), (x * y).toNat = x.toNat * y.toNat % 2 ^ n
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The second projection on a domain in a product is `C^∞`.  -/
contDiffOn_snd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {s : Set (E × F)}, ContDiffOn 𝕜 n Prod.snd s
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_algebraMap_map : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} {S : Type u_3} [inst_1 : CommSemiring A] [inst_2 : Algebra A R]
  [inst_3 : CommSemiring S] [inst_4 : Algebra A S] (φ : R →ₐ[A] S) (a : A) (f : PowerSeries R),
  (PowerSeries.rescale ((algebraMap A S) a)) ((PowerSeries.map ↑φ) f) =
    (PowerSeries.map ↑φ) ((PowerSeries.rescale ((algebraMap A R) a)) f)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.algebraMap_lift : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] {S : Type u_4} [inst_6 : CommRing S]
  [inst_7 : Algebra R S] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R S B] [inst_10 : Algebra R A]
  [inst_11 : IsScalarTower R A B] [isIntegral : Algebra.IsIntegral R S] (x : S),
  (algebraMap A B) ((IsIntegralClosure.lift R A B) x) = (algebraMap S B) x
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.isPushout_of_isLocalization : ∀ {R S Rₘ Sₘ : Type u} [inst : CommRing R] [inst_1 : CommRing Rₘ] [inst_2 : Algebra R Rₘ] [inst_3 : CommRing S]
  [inst_4 : CommRing Sₘ] [inst_5 : Algebra S Sₘ] (f : R →+* S) (fₘ : Rₘ →+* Sₘ),
  fₘ.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp f →
    ∀ (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (Submonoid.map f M) Sₘ],
      CategoryTheory.IsPushout (CommRingCat.ofHom f) (CommRingCat.ofHom (algebraMap R Rₘ))
        (CommRingCat.ofHom (algebraMap S Sₘ)) (CommRingCat.ofHom fₘ)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α], Topology.IsClosedEmbedding TopologicalSpace.NonemptyCompacts.toCompacts
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.Represents.smul : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι] {A : Matrix ι ι R} {f : Module.End R M},
  Matrix.Represents b A f → ∀ (r : R), Matrix.Represents b (r • A) (r • f)
-- Lean.Elab.PreDefinition.WF.Preprocess
_private.Lean.Elab.PreDefinition.WF.Preprocess.0.Lean.Elab.WF.processParamLet : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.List.Sublist
List.mem_of_cons_sublist : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist l₂ → a ∈ l₂
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Slot.pos : {α : Type} → Std.Slot✝ α → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.isoPushout.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl inl_1 : X ⟶ P}
  (e_inl : inl = inl_1) {inr inr_1 : Y ⟶ P} (e_inr : inr = inr_1) (h : CategoryTheory.IsPushout f g inl inr)
  [inst_1 : CategoryTheory.Limits.HasPushout f g], h.isoPushout = ⋯.isoPushout
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- A version of `Function.extend` for bounded continuous maps. We assume that the domain has
discrete topology, so we only need to verify boundedness.  -/
BoundedContinuousFunction.extend : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        {δ : Type u_2} →
          [inst_2 : TopologicalSpace δ] →
            [DiscreteTopology δ] →
              (α ↪ δ) → BoundedContinuousFunction α β → BoundedContinuousFunction δ β → BoundedContinuousFunction δ β
-- Init.Data.UInt.Lemmas
UInt16.neg_mul_neg : ∀ (a b : UInt16), -a * -b = a * b
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.keys.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : List ((a : α) × β a) → Sort u_3) →
      (x : List ((a : α) × β a)) →
        (Unit → motive []) → ((k : α) → (snd : β k) → (l : List ((a : α) × β a)) → motive (⟨k, snd⟩ :: l)) → motive x
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.linearEquivMapExtendScalars_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) [inst_5 : Module.FinitePresentation R M]
  (f : M →ₗ[R] N),
  (Module.FinitePresentation.linearEquivMapExtendScalars S) ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) =
    (IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
        (Localization S))
      f
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.homotopyOfEq.congr_simp : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} (f g : u ⟶ v)
  (w :
    (CategoryTheory.Preadditive.RightFreyd.quotient V).map f =
      (CategoryTheory.Preadditive.RightFreyd.quotient V).map g),
  CategoryTheory.Preadditive.RightFreyd.homotopyOfEq f g w = CategoryTheory.Preadditive.RightFreyd.homotopyOfEq f g w
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (h : x ⤳ x')
  (y : ↑(Y.presheaf.stalk ((TopCat.Hom.hom f.base) x'))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x))
      ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) y) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x')) y)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.open_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (self : PartialDiffeomorph I J M N n),
  IsOpen self.source
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_embedding_eq_zero_iff_lt : ∀ {α β : Type u}, Cardinal.mk (α ↪ β) = 0 ↔ Cardinal.mk β < Cardinal.mk α
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_eraseKey_of_key_beq_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {a : α} {l : List ((a : α) × β a)} (p : (a : α) × β a),
  (p.fst == a) = false → (p ∈ Std.Internal.List.eraseKey a l ↔ p ∈ l)
-- Init.Data.BitVec.Lemmas
BitVec.pos_of_msb : ∀ {w : ℕ} {x : BitVec w}, x.msb = true → 0#w < x
-- Mathlib.Data.Seq.Basic
Stream'.Seq.join_cons_nil : ∀ {α : Type u} (a : α) (S : Stream'.Seq (Stream'.Seq1 α)),
  (Stream'.Seq.cons (a, Stream'.Seq.nil) S).join = Stream'.Seq.cons a S.join
-- Mathlib.Order.Hom.Basic
RelEmbedding.toOrderHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β]
  (f : (fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2), Function.Injective ⇑f.toRelHom.toOrderHom
-- Mathlib.Data.Fin.SuccPred
Fin.val_sub_castPred_of_ge : ∀ {n : ℕ} {a b : Fin (n + 1)} (hb : b ≠ Fin.last n) (h : a ≤ b), ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1
-- Mathlib.RingTheory.Localization.Finiteness
Module.Finite.instAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] {P : Ideal R} [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [Module.Finite R S] [inst_4 : P.IsPrime],
  Module.Finite (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
-- Lean.DocString.Types
Lean.Doc.Part.mk.injEq : ∀ {i : Type u} {b : Type v} {p : Type w} (title : Array (Lean.Doc.Inline i)) (titleString : String)
  (metadata : Option p) (content : Array (Lean.Doc.Block i b)) (subParts : Array (Lean.Doc.Part i b p))
  (title_1 : Array (Lean.Doc.Inline i)) (titleString_1 : String) (metadata_1 : Option p)
  (content_1 : Array (Lean.Doc.Block i b)) (subParts_1 : Array (Lean.Doc.Part i b p)),
  ({ title := title, titleString := titleString, metadata := metadata, content := content, subParts := subParts } =
      { title := title_1, titleString := titleString_1, metadata := metadata_1, content := content_1,
        subParts := subParts_1 }) =
    (title = title_1 ∧
      titleString = titleString_1 ∧ metadata = metadata_1 ∧ content = content_1 ∧ subParts = subParts_1)
-- Init.Data.Char.Lemmas
Char.lt_asymm : ∀ {a b : Char}, a < b → ¬b < a
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.instNeZeroOfNonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  [Nonempty X], NeZero μ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
    (∀ a ∈ t, l.contains a = false) → (t.insertManyIfNewUnit l).size = t.size + l.length
-- Mathlib.Order.Defs.PartialOrder
Preorder.lt_iff_le_not_ge : ∀ {α : Type u_2} [self : Preorder α] (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_zpow_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle ((f ^ n) x) y ↔ f.SameCycle x y
-- Lean.Meta.Basic
Lean.Meta.resetCache : Lean.MetaM Unit
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_ofList_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (Std.HashMap.Raw.ofList l)[k']? = some v
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_denote_eq : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig cache →
    ∀ (idx : ℕ) (hidx : idx < w),
      ⟦assign.toAIGAssignment,
          { aig := (↑(Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache).result).aig,
            ref := (↑(Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache).result).vec.get idx hidx }⟧ =
        (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD idx
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.quasiIso_map_of_preservesRightHomology : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (F.mapShortComplex.obj S₁).HasHomology]
  [inst_8 : (F.mapShortComplex.obj S₂).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂]
  [CategoryTheory.ShortComplex.QuasiIso φ], CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ)
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.mk_dest : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : MvQPF.Fix F α),
  MvQPF.Fix.mk x.dest = x
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.Functor.FullyFaithful.hasShift.zero.eq_1 : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_2} D] [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift D A]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C)
  (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)),
  CategoryTheory.Functor.FullyFaithful.hasShift.zero hF s i =
    (hF.whiskeringRight C).preimageIso
      (i 0 ≪≫ F.isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A) ≪≫ F.rightUnitor ≪≫ F.leftUnitor.symm)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.instOne : {D : Type u_1} → {Q : Type u_2} → [Group D] → [Group Q] → One (D ≀ᵣ Q)