mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₅ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  {φ φ' : f ⟶ g},
  CategoryTheory.ComposableArrows.app' φ 0 _proof_449✝ = CategoryTheory.ComposableArrows.app' φ' 0 _proof_449✝ →
    CategoryTheory.ComposableArrows.app' φ 1 _proof_450✝ = CategoryTheory.ComposableArrows.app' φ' 1 _proof_450✝ →
      CategoryTheory.ComposableArrows.app' φ 2 _proof_451✝ = CategoryTheory.ComposableArrows.app' φ' 2 _proof_451✝ →
        CategoryTheory.ComposableArrows.app' φ 3 _proof_452✝ = CategoryTheory.ComposableArrows.app' φ' 3 _proof_452✝ →
          CategoryTheory.ComposableArrows.app' φ 4 _proof_453✝ = CategoryTheory.ComposableArrows.app' φ' 4 _proof_453✝ →
            CategoryTheory.ComposableArrows.app' φ 5 _proof_454✝ =
                CategoryTheory.ComposableArrows.app' φ' 5 _proof_454✝ →
              φ = φ'
-- Mathlib.Data.Rat.Init
NNRatCast.toCoeTail : {K : Type u_1} → [NNRatCast K] → CoeTail ℚ≥0 K
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.sub` -/
MeromorphicOn.fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → MeromorphicOn g U → MeromorphicOn (fun i => f i - g i) U
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.val_smul_of_tower : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : SMul M N] [inst_2 : SMul M α]
  [inst_3 : Monoid N] [inst_4 : MulAction N α] [inst_5 : SMulMemClass S N α] [inst_6 : IsScalarTower M N α] (s : S)
  (r : M) (x : ↥s), ↑(r • x) = r • ↑x
-- Mathlib.Analysis.Normed.Group.Defs
NNNorm.mk : {E : Type u_8} → (E → NNReal) → NNNorm E
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.completeSpace_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (e : α ≃ᵢ β),
  CompleteSpace α ↔ CompleteSpace β
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.splits : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [IsGalois F E] (x : E),
  (Polynomial.map (algebraMap F E) (minpoly F x)).Splits
-- Mathlib.LinearAlgebra.Dimension.Finrank
Module.finrank.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.finrank R M = Cardinal.toNat (Module.rank R M)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_eq_zero_of_ae_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {f : α → ε}, f =ᵐ[μ] 0 → MeasureTheory.eLpNorm f p μ = 0
-- Mathlib.RingTheory.Artinian.Ring
IsArtinianRing.isNilpotent_nilradical : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R], IsNilpotent (nilradical R)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_right_inj : ∀ {w : ℕ} (a b c : BitVec w), (c ^^^ a == c ^^^ b) = (a == b)
-- Mathlib.RingTheory.AlgebraTower
/-- `AlgHom`s from the top of a tower are equivalent to a pair of `AlgHom`s.  -/
algHomEquivSigma : {A : Type u_3} →
  {B : Type u_4} →
    {C : Type u_5} →
      {D : Type u_6} →
        [inst : CommSemiring A] →
          [inst_1 : CommSemiring C] →
            [inst_2 : CommSemiring D] →
              [inst_3 : Algebra A C] →
                [inst_4 : Algebra A D] →
                  [inst_5 : CommSemiring B] →
                    [inst_6 : Algebra A B] →
                      [inst_7 : Algebra B C] → [IsScalarTower A B C] → (C →ₐ[A] D) ≃ (f : B →ₐ[A] D) × (C →ₐ[B] D)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_inv_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.unmop =
    (CategoryTheory.MonoidalCategoryStruct.associator Z.unmop Y.unmop X.unmop).hom
-- Lean.Elab.Term.TermElabM
/-- Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`.
Example: Assume resolveName `v.head.bla.boo` produces `(v.head, ["bla", "boo"])`, then this method produces
`(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`.

See the comment there about `explicitLevels` and the meaning of the `List Level` component of the returned tuple.
 -/
Lean.Elab.Term.resolveName' : Lean.Syntax →
  List Lean.Level →
    optParam (Option Lean.Expr) none →
      Lean.Elab.TermElabM (Lean.Name × List (Lean.Expr × Lean.Syntax × List Lean.Syntax × List Lean.Level))
-- Init.Omega.Constraint
Lean.Omega.positivize_sat : ∀ {s : Lean.Omega.Constraint} {x v : Lean.Omega.Coeffs},
  s.sat' x v = true → (Lean.Omega.positivizeConstraint s x).sat' (Lean.Omega.positivizeCoeffs s x) v = true
-- Mathlib.Topology.Sheaves.CommRingCat
/-- The localization of a presheaf of `CommRing`s at locally non-zero-divisor sections.  -/
TopCat.Presheaf.totalQuotientPresheaf : {X : TopCat} → TopCat.Presheaf CommRingCat X → TopCat.Presheaf CommRingCat X
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `M`-equivariant functions `X → Y` with respect to the additive action of `M`.
This is the same as `X →ₑ[@id M] Y`.

We use the same notation as for multiplicative actions, as conflicts are unlikely.  -/
«AddActionHomIdLocal≺» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
IsDiscreteValuationRing.ringKrullDim_eq_one : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R], ringKrullDim R = 1
-- Init.Data.UInt.Lemmas
mod_usizeSize_uInt32Size : ∀ (n : ℕ), n % USize.size % UInt32.size = n % UInt32.size
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The morphism that is part of a morphism in `Over X`.  -/
CategoryTheory.Over.Hom.left : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] → {X : T} → {f g : CategoryTheory.Over X} → (f ⟶ g) → (f.left ⟶ g.left)
-- Mathlib.Algebra.Order.Sub.Basic
add_tsub_cancel_iff_le : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, a + (b - a) = b ↔ a ≤ b
-- Init.Data.Nat.Basic
Nat.eq_zero_or_eq_succ_pred : ∀ (n : ℕ), n = 0 ∨ n = n.pred.succ
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfOplax_toPrelaxFunctor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) (F' : F.PseudoCore),
  (CategoryTheory.Pseudofunctor.mkOfOplax F F').toPrelaxFunctor = F.toPrelaxFunctor
-- Mathlib.Data.List.Sort
List.SortedGT.getElem_lt_getElem_iff : ∀ {α : Type u_1} {l : List α} [inst : LinearOrder α],
  l.SortedGT → ∀ {i j : ℕ} {hi : i < l.length} {hj : j < l.length}, l[i] < l[j] ↔ j < i
-- Mathlib.Data.Stream.Init
_private.Mathlib.Data.Stream.Init.0.Stream'.cons.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → t.minKey? = t_1.minKey?
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instIsReducedToScheme : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} [AlgebraicGeometry.IsReduced X], AlgebraicGeometry.IsReduced ↑U
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.p_descQ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) {Z : C} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p (CategoryTheory.CategoryStruct.comp (h.descQ k hk) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.filterMap.go : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      ((a : α) → β a → Option (γ a)) →
        Std.DHashMap.Internal.AssocList α γ → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α γ
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A bounded variation function has a limit on its left within a set. Version with a general
filter, covering both left neighborhoods of points and `atTop`.  -/
BoundedVariationOn.exists_tendsto_left_of_filter : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E] {f : α → E}
  {s : Set α},
  BoundedVariationOn f s →
    ∀ (L : Filter α), (∀ y ∈ s, s ∩ Set.Ici y ∈ L) → s.Nonempty → ∃ l, Filter.Tendsto f L (nhds l)
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
/-- Empty graphs are strongly regular. Note that `ℓ` can take any value
for empty graphs, since there are no pairs of adjacent vertices.  -/
SimpleGraph.bot_strongly_regular : ∀ {V : Type u} [inst : Fintype V] {ℓ : ℕ}, ⊥.IsSRGWith (Fintype.card V) 0 ℓ 0
-- Mathlib.Topology.MetricSpace.PiNat
/-- Metric space structure on `ℕ → ℕ` where the distance is given by `dist x y = (1/2)^n`,
where `n` is the smallest index where `x` and `y` differ.
Not registered as a global instance by default.  -/
PiNat.metricSpaceNatNat : MetricSpace (ℕ → ℕ)
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.trivialFibrations_over_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C],
  HomotopicalAlgebra.trivialFibrations (CategoryTheory.Over S) = (HomotopicalAlgebra.trivialFibrations C).over
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.restrictPreimage_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty),
  (e.restrictPreimage hs).target = Prod.map Subtype.val id ⁻¹' e.toPretrivialization.target
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_natCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ), (↑n).imK = 0
-- Aesop.Search.SearchM
Aesop.getIteration : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Aesop.Iteration
-- Mathlib.Order.Bounds.Basic
/-- In a directed order, the union of two sets is bounded above if and only if both sets are.  -/
bddAbove_union : ∀ {α : Type u_1} [inst : Preorder α] [IsDirectedOrder α] {s t : Set α}, BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t
-- Mathlib.Topology.Constructions
isOpenMap_sigma : ∀ {X : Type u} {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] [inst_1 : TopologicalSpace X]
  {f : Sigma σ → X}, IsOpenMap f ↔ ∀ (i : ι), IsOpenMap fun a => f ⟨i, a⟩
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_sub_leadingTerm_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f : MvPolynomial σ R),
  m.toSyn (m.degree (f - m.leadingTerm f)) ≤ m.toSyn (m.degree f)
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.exists_eq_zpow_of_odd : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] (x : R) {k : ℤ}, Odd k → ∃ r, x = r ^ k
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_setWidth_of_le : ∀ {w pos v acc : ℕ} (x : BitVec w), pos ≤ v → (BitVec.setWidth v x).cpopNatRec pos acc = x.cpopNatRec pos acc
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.End_toOne_one : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A], 1 = BialgHom.id R A
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.instIsEmptySubtypeProductsIsGoodEmptyCollectionSetForallBool : ∀ {I : Type u} [inst : LinearOrder I], IsEmpty { l // Profinite.NobelingProof.Products.isGood ∅ l }
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode.eq_8 : ∀ (cf : Nat.Partrec.Code), cf.rfind'.encodeCode = 2 * (2 * cf.encodeCode + 1) + 1 + 4
-- Init.Data.UInt.Lemmas
UInt64.add_left_inj : ∀ {a b : UInt64} (c : UInt64), a + c = b + c ↔ a = b
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffVAdd.contMDiff_const_vadd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : VAdd G M] {n : WithTop ℕ∞}
  [ContMDiffVAdd I I' n G M] (g : G), ContMDiff I' I' n fun x => g +ᵥ x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `add_lt_add_of_lt_of_lt`. -/
add_lt_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b c d : α},
  a < b → c < d → a + c < b + d
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalCommSemiring α] [inst_1 : Fintype n] (A : Matrix m n α)
  (x : n → α), Matrix.vecMul x A.transpose = A.mulVec x
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m.insert k).contains k = true
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.two_mul_one_sub_le_norm_sub_one_sq : ∀ {A : Type u_1} [inst : CStarAlgebra A] {u : A},
  u ∈ unitary A → ∀ {z : ℂ}, z ∈ spectrum ℂ u → 2 * (1 - z.re) ≤ ‖u - 1‖ ^ 2
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.swap_mem_antidiagonal : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α},
  x.swap ∈ Finset.antidiagonal hs ht a ↔ x ∈ Finset.antidiagonal ht hs a
-- Init.Data.Array.Lemmas
/-- Variant of `any_reverse` with a side condition for the `stop` argument.  -/
Array.any_reverse' : ∀ {α : Type u_1} {stop : ℕ} {f : α → Bool} {xs : Array α}, stop = xs.size → xs.reverse.any f 0 stop = xs.any f
-- Mathlib.Algebra.Ring.Parity
Even.mul_right : ∀ {α : Type u_2} [inst : Add α] [inst_1 : Mul α] {a : α} [RightDistribClass α], Even a → ∀ (b : α), Even (a * b)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.not_monic_zero : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], ¬Polynomial.Monic 0
-- Mathlib.Data.Matrix.Reflection
_private.Mathlib.Data.Matrix.Reflection.0.Matrix.Forall.match_1.splitter : {α : Type u_1} →
  (motive : (x x_1 : ℕ) → (Matrix (Fin x) (Fin x_1) α → Prop) → Sort u_2) →
    (x x_1 : ℕ) →
      (x_2 : Matrix (Fin x) (Fin x_1) α → Prop) →
        ((x : ℕ) → (P : Matrix (Fin 0) (Fin x) α → Prop) → motive 0 x P) →
          ((n x : ℕ) → (P : Matrix (Fin (n + 1)) (Fin x) α → Prop) → motive n.succ x P) → motive x x_1 x_2
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.mulConst_inv_left : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : DecidableEq G] (A B : Finset G), A⁻¹.mulConst B = A.divConst B
-- Mathlib.Data.ENat.Lattice
ENat.sSup_add : ∀ {s : Set ℕ∞} {a : ℕ∞}, s.Nonempty → sSup s + a = ⨆ b ∈ s, b + a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.toPresheaf_obj_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (X : Cᵒᵖ), ↑(((PresheafOfModules.toPresheaf R).obj M).obj X) = ↑(M.obj X)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonLeanClientCapabilities : Lean.FromJson Lean.Lsp.LeanClientCapabilities
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If `prodComparison F A B` is an isomorphism for all `A B` then `F` preserves limits of shape
`Discrete (WalkingPair)`.  -/
CategoryTheory.CartesianMonoidalCategory.preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D)
  [∀ (A B : C), CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
instIsOpenImmersionLocallyRingedSpaceMapSubtypeMemOpensVal : ∀ {𝕜 : 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] (U : TopologicalSpace.Opens M),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.map_ret : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α), Stream'.WSeq.map f (Stream'.WSeq.ret a) = Stream'.WSeq.ret (f a)
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- The multiplicative version of an additivized monoid is mul-equivalent to itself.  -/
MulEquiv.toMultiplicative_toAdditive : {G : Type u_2} → [inst : MulOneClass G] → Multiplicative (Additive G) ≃* G
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Expr.denoteN.match_1.eq_1 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (a b : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)),
  (match a.sub b with
    | a.sub b => h_1 a b
    | a.neg => h_2 a
    | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
    | Lean.Grind.Linarith.Expr.zero => h_4 ()
    | Lean.Grind.Linarith.Expr.var v => h_5 v
    | a.add b => h_6 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) =
    h_1 a b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.alterKey.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (k : α) →
      (motive : Option (β k) → Sort u_2) →
        (x : Option (β k)) → (Unit → motive none) → ((v : β k) → motive (some v)) → motive x
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.cechConerve_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (f : CategoryTheory.Arrow C), CategoryTheory.CosimplicialObject.cechConerve.obj f = f.cechConerve
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
/-- `nearestPtInd e N x` is the index `k` such that `e k` is the nearest point to `x` among the
points `e 0`, ..., `e N`. If more than one point are at the same distance from `x`, then
`nearestPtInd e N x` returns the least of their indices.  -/
MeasureTheory.SimpleFunc.nearestPtInd : {α : Type u_1} →
  [inst : MeasurableSpace α] →
    [inst_1 : PseudoEMetricSpace α] → [OpensMeasurableSpace α] → (ℕ → α) → ℕ → MeasureTheory.SimpleFunc α ℕ
-- Mathlib.Computability.EpsilonNFA
εNFA.accepts.eq_1 : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ), M.accepts = {x | ∃ S ∈ M.accept, S ∈ M.eval x}
-- Mathlib.Algebra.Homology.TotalComplex
/-- The inclusion of a summand in the total complex.  -/
HomologicalComplex₂.ιTotal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                (K : HomologicalComplex₂ C c₁ c₂) →
                  (c₁₂ : ComplexShape I₁₂) →
                    [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                      [inst_3 : DecidableEq I₁₂] →
                        [inst_4 : K.HasTotal c₁₂] →
                          (i₁ : I₁) →
                            (i₂ : I₂) → (i₁₂ : I₁₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ (K.total c₁₂).X i₁₂)
-- Mathlib.CategoryTheory.Square
/-- the bottom-left morphism  -/
CategoryTheory.Square.Hom.τ₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {sq₁ sq₂ : CategoryTheory.Square C} → sq₁.Hom sq₂ → (sq₁.X₃ ⟶ sq₂.X₃)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.mul_dpow : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ},
  IsUnit ↑(n - 1).factorial →
    I ^ n = 0 →
      ∀ {m k : ℕ} {x : A},
        x ∈ I →
          DividedPowers.OfInvertibleFactorial.dpow I m x * DividedPowers.OfInvertibleFactorial.dpow I k x =
            ↑((m + k).choose m) * DividedPowers.OfInvertibleFactorial.dpow I (m + k) x
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.comp_onFunction : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (g : L' →ᴸ L'') (f : L →ᴸ L')
  (_n : ℕ) (F : L.Functions _n), (g.comp f).onFunction F = g.onFunction (f.onFunction F)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.unitOfList_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, Std.ExtTreeMap.unitOfList l cmp = ∅ ↔ l = []
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a < ArchimedeanClass.mk b → a ≤ 0 → a < b
-- Mathlib.FieldTheory.IsAlgClosed.Basic
_private.Mathlib.FieldTheory.IsAlgClosed.Basic.0.IsAlgClosed.FractionRing.isAlgebraic : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type v} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S] [Algebra.IsAlgebraic R S],
  Algebra.IsAlgebraic (FractionRing R) (FractionRing S)
-- Mathlib.Topology.Order
nhds_mono : ∀ {α : Type u} {t₁ t₂ : TopologicalSpace α} {a : α}, t₁ ≤ t₂ → nhds a ≤ nhds a
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- The compact coherentification preserves the topology of k-spaces.  -/
CompactCoherentification.homeo : {X : Type u_1} → [inst : TopologicalSpace X] → [CompactlyCoherentSpace X] → X ≃ₜ CompactCoherentification X
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.merge.eq_3 : ∀ {α : Type u_1} (le : α → α → Bool) (x : α) (xs_2 : List α) (y : α) (ys_2 : List α),
  (x :: xs_2).merge (y :: ys_2) le =
    if le x y = true then x :: xs_2.merge (y :: ys_2) le else y :: (x :: xs_2).merge ys_2 le
-- Mathlib.FieldTheory.PrimitiveElement
AlgHom.natCard_of_splits : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  [Algebra.IsSeparable F E] (L : Type u_3) [inst_5 : Field L] [inst_6 : Algebra F L],
  (∀ (x : E), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) → Nat.card (E →ₐ[F] L) = Module.finrank F E
-- Mathlib.Algebra.Group.WithOne.Basic
AddEquiv.withZeroCongr.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β),
  e.withZeroCongr =
    { toFun := ⇑(WithZero.mapAddHom e.toAddHom), invFun := ⇑(WithZero.mapAddHom e.symm.toAddHom), left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }