mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- **Alias** of the reverse direction of `mdifferentiableWithinAt_insert`. -/
MDifferentiableWithinAt.insert' : ∀ {𝕜 : 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'] {f : M → M'} {x : M} {s : Set M}
  {y : M}, MDiffAt[s] f x → MDiffAt[insert y s] f x
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
/-- If `ω` is a closed `1`-form on a convex set `s`, then it admits a primitive,
a version stated in terms of `fderivWithin`.  -/
Convex.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {s : Set E} {ω : E → E →L[𝕜] F} [CompleteSpace F],
  Convex ℝ s →
    DifferentiableOn ℝ ω s →
      (∀ a ∈ s,
          ∀ x ∈ tangentConeAt ℝ s a,
            ∀ y ∈ tangentConeAt ℝ s a, ((fderivWithin ℝ ω s a) x) y = ((fderivWithin ℝ ω s a) y) x) →
        ∃ f, ∀ a ∈ s, HasFDerivWithinAt f (ω a) s a
-- Lean.SubExpr
Lean.SubExpr.Pos.asNat : Lean.SubExpr.Pos → ℕ
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.coe_projectionOnto_apply`. -/
Submodule.coe_linearProjOfIsCompl_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), ↑((p.projectionOnto q hpq) x) = (p.projection q hpq) x
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.SyntaxStack.raw : Lean.Parser.SyntaxStack → Array Lean.Syntax
-- Init.Data.Order.Lemmas
Std.max_self : ∀ {α : Type u} [inst : Max α] [Std.IdempotentOp max] {a : α}, a ⊔ a = a
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_eq_prod_of_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Set α} {t : Finset α},
  s ∩ Function.mulSupport f ⊆ ↑t → ↑t ⊆ s → ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.mergeSort_eq_merge_mkSlice : ∀ {α : Type u_1} {le : α → α → Bool} {xs : List α},
  xs.mergeSort le =
    if 1 < xs.length then
      ((Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...(xs.length + 1) / 2)).mergeSort le).merge
        ((Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs ((xs.length + 1) / 2)...*)).mergeSort le) le
    else xs
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] [inst_2 : Inhabited α] (h : t.WF) {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (↑(t.insertMany l ⋯)).getKey! k = t.getKey! k
-- Mathlib.CategoryTheory.Sites.InducedTopology
CategoryTheory.Functor.le_inducedTopology_iff : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D}
  {J : CategoryTheory.GrothendieckTopology C}, J ≤ F.inducedTopology K ↔ F.IsContinuous J K
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- the natural transformation induced by `unitUnit` exhibits
`(ι.obj <| 𝟙_ D).obj (𝟙_ C)` as a left Kan extension of `fromPUnit.{0} (𝟙_ V)` as a
along `fromPUnit.{0} (𝟙_ C)`.  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.isPointwiseLeftKanExtensionUnitUnit : (C : Type u₁) →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    (V : Type u₂) →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            (D : Type u₃) →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                {inst_5 : CategoryTheory.MonoidalCategoryStruct D} →
                  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] →
                    (CategoryTheory.Functor.LeftExtension.mk
                        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
                          (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
                        {
                          app := fun x =>
                            CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.unitUnit C V D,
                          naturality := ⋯ }).IsPointwiseLeftKanExtension
-- Mathlib.LinearAlgebra.Matrix.Module
Matrix.Module.diagonal_const_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (r : R) (v : ι → M), (Matrix.diagonal fun x => r) • v = r • v
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_mul_relrank_eq_inf_relrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E)
  {B C : IntermediateField F E}, B ≤ C → A.relrank B * B.relrank C = (A ⊓ B).relrank C
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
ChainComplex.isIso_iCycles₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : ChainComplex C ℕ) [inst_2 : HomologicalComplex.HasHomology K 0],
  CategoryTheory.IsIso (HomologicalComplex.iCycles K 0)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.val_inv_toRootsOfUnity_coe : ∀ {M : Type u_1} [inst : CommMonoid M] {μ : M} {n : ℕ} [inst_1 : NeZero n] (h : IsPrimitiveRoot μ n),
  ↑(↑h.toRootsOfUnity)⁻¹ = μ ^ (n - 1)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.mkHom_id : ∀ {M : Type u} [inst : SeminormedAddCommGroup M],
  SemiNormedGrp₁.mkHom (NormedAddGroupHom.id M) ⋯ = CategoryTheory.CategoryStruct.id { carrier := M, str := inst }
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.IsAllowedEncodedQueryChars.push : ∀ {r : UInt8 → Bool} {c : UInt8} {bs : ByteArray},
  Std.Http.URI.IsAllowedEncodedQueryChars r bs →
    Std.Http.URI.isEncodedQueryChar r c = true → Std.Http.URI.IsAllowedEncodedQueryChars r (bs.push c)
-- Mathlib.Analysis.Analytic.Uniqueness
/-- One-dimensional formal multilinear series representing the same function are equal.  -/
HasFPowerSeriesAt.eq_formalMultilinearSeries : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜},
  HasFPowerSeriesAt f p₁ x → HasFPowerSeriesAt f p₂ x → p₁ = p₂
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_self_sub_left : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddGroup N] (f g : α →₀ N),
  (f - g).neLocus f = g.support
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.classifier_χ₀ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (Y : CategoryTheory.Functor Cᵒᵖ (Type (max u v))),
  (CategoryTheory.Presheaf.classifier C).χ₀ Y =
    (CategoryTheory.Functor.isTerminalConst Cᵒᵖ CategoryTheory.Limits.Types.isTerminalPUnit).from Y
-- Mathlib.Data.Int.Log
Int.clog_of_one_le_right : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (b : ℕ) {r : R},
  1 ≤ r → Int.clog b r = ↑(Nat.clog b ⌈r⌉₊)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.rightUnitor_inv_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- If two simple functions are equal a.e., then their `lintegral`s are equal.  -/
MeasureTheory.SimpleFunc.lintegral_congr : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : MeasureTheory.SimpleFunc α ENNReal},
  ⇑f =ᵐ[μ] ⇑g → f.lintegral μ = g.lintegral μ
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_of_zero_dvd : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly),
  0 ∣ Int.Internal.Linear.Poly.denote' ctx p → Int.Internal.Linear.Poly.denote' ctx p = 0
-- Mathlib.CategoryTheory.Functor.FunctorHom
_private.Mathlib.CategoryTheory.Functor.FunctorHom.0.CategoryTheory.Functor.homObjEquiv.match_1.eq_1 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] (F A : CategoryTheory.Functor C (Type u_2)) (X : C)
  (motive : (CategoryTheory.MonoidalCategoryStruct.tensorObj F A).obj X → Sort u_4) (x : F.obj X) (y : A.obj X)
  (h_1 : (x : F.obj X) → (y : A.obj X) → motive (x, y)),
  (match (x, y) with
    | (x, y) => h_1 x y) =
    h_1 x y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ColorInformation.color : Lean.Lsp.ColorInformation → Lean.Lsp.Color
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.OuterRegular.smul_nnreal : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] (μ : MeasureTheory.Measure α) [μ.OuterRegular]
  (c : NNReal), (c • μ).OuterRegular
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.instInhabited : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → Inhabited (Monoid.CoprodI.Word M)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_eq_cons : ∀ {m n : ℤ}, m ≤ n → (m...=n).toList = m :: ((m + 1)...=n).toList
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The orbits of a normal subgroup form a block system  -/
AddAction.IsBlockSystem.of_normal : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {N : AddSubgroup G} [N.Normal],
  AddAction.IsBlockSystem G (Set.range fun a => AddAction.orbit (↥N) a)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.exists_bucket_of_update : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Array (Std.DHashMap.Internal.AssocList α β))
  (h : 0 < m.size) (k : α) (f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β),
  ∃ l,
    (Std.DHashMap.Internal.toListModel m).Perm ((Std.DHashMap.Internal.bucket m h k).toList ++ l) ∧
      (Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.updateBucket m h k f)).Perm
          ((f (Std.DHashMap.Internal.bucket m h k)).toList ++ l) ∧
        ∀ [LawfulHashable α],
          Std.DHashMap.Internal.IsHashSelf m → ∀ (k' : α), hash k = hash k' → Std.Internal.List.containsKey k' l = false
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stepAux.match_1.eq_5 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4}
  (motive : Turing.TM2.Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Sort u_5) (f : σ → Bool)
  (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) (v : σ) (S : (k : K) → List (Γ k))
  (h_1 :
    (k : K) →
      (f : σ → Γ k) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.push k f q) v S)
  (h_2 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.peek k f q) v S)
  (h_3 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.pop k f q) v S)
  (h_4 :
    (a : σ → σ) →
      (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.load a q) v S)
  (h_5 :
    (f : σ → Bool) →
      (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) →
        (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.branch f q₁ q₂) v S)
  (h_6 : (f : σ → Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.goto f) v S)
  (h_7 : (v : σ) → (S : (k : K) → List (Γ k)) → motive Turing.TM2.Stmt.halt v S),
  (match Turing.TM2.Stmt.branch f q₁ q₂, v, S with
    | Turing.TM2.Stmt.push k f q, v, S => h_1 k f q v S
    | Turing.TM2.Stmt.peek k f q, v, S => h_2 k f q v S
    | Turing.TM2.Stmt.pop k f q, v, S => h_3 k f q v S
    | Turing.TM2.Stmt.load a q, v, S => h_4 a q v S
    | Turing.TM2.Stmt.branch f q₁ q₂, v, S => h_5 f q₁ q₂ v S
    | Turing.TM2.Stmt.goto f, v, S => h_6 f v S
    | Turing.TM2.Stmt.halt, v, S => h_7 v S) =
    h_5 f q₁ q₂ v S
-- Lean.Meta.Basic
Lean.Meta.DefEqContext.rhs : Lean.Meta.DefEqContext → Lean.Expr
-- Lean.Meta.Sym.SymM
/-- Returns `true` if `e` is the internalized `False` expression.   -/
Lean.Meta.Sym.isFalseExpr : Lean.Expr → Lean.Meta.Sym.SymM Bool
-- Mathlib.RingTheory.Morita.Matrix
MatrixModCat.fromMatrixLinear_apply_coe : ∀ {R : Type u} {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module (Matrix ι ι R) M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R (Matrix ι ι R) M] {N : Type u_2} [inst_7 : AddCommGroup N]
  [inst_8 : Module (Matrix ι ι R) N] (i : ι) [inst_9 : Module R N] [inst_10 : IsScalarTower R (Matrix ι ι R) N]
  (f : M →ₗ[Matrix ι ι R] N) (c : ↥(MatrixModCat.toModuleCatObj R M i)), ↑((MatrixModCat.fromMatrixLinear i f) c) = f ↑c
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.restrictScalars_coe_root : ∀ {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field L] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module L M] [inst_4 : Module L N] (P : RootPairing ι L M N) (K : Type u_5)
  [inst_5 : Field K] [inst_6 : Algebra K L] [inst_7 : Module K M] [inst_8 : Module K N] [inst_9 : IsScalarTower K L M]
  [inst_10 : IsScalarTower K L N] [inst_11 : P.IsBalanced] [inst_12 : P.IsValuedIn K] (i : ι),
  ↑((P.restrictScalars' K).root i) = P.root i
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.expr.injEq : ∀ (a a_1 : Lean.Widget.CodeWithInfos), (Lean.Widget.MsgEmbed.expr a = Lean.Widget.MsgEmbed.expr a_1) = (a = a_1)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_I₀ : ∀ {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : s → X.Opens) (hU : TopologicalSpace.IsOpenCover U),
  (X.openCoverOfIsOpenCover U hU).I₀ = s
-- Lean.Data.Iterators.Producers.PersistentHashMap
/-- Counts the total entries in an entries array starting at index `i`.  -/
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Node.measure.measureEntries : {α : Type u_1} → {β : Type u_2} → Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → ℕ → ℕ
-- Lean.ParserCompiler
/-- Replace all references of `Parser` with `tyName`  -/
Lean.ParserCompiler.replaceParserTy : {α : Type} → Lean.ParserCompiler.Context α → Lean.Expr → Lean.Expr
-- Init.Data.SInt.Basic
/-- Truncating division for 16-bit signed integers, rounding towards zero. Usually accessed via the `/`
operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int16.div 10 3 = 3`
* `Int16.div 10 (-3) = (-3)`
* `Int16.div (-10) (-3) = 3`
* `Int16.div (-10) 3 = (-3)`
* `Int16.div 10 0 = 0`
 -/
Int16.div : Int16 → Int16 → Int16
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Nat.Iio_zero : Finset.Iio 0 = ∅
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Right.self_le_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : Preorder α] [MulRightMono α] {a : α}, a ≤ 1 → a ≤ a⁻¹
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.support_add : ∀ {X : Type u_1} (a b : FreeAbelianGroup X), (a + b).support ⊆ a.support ∪ b.support
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.Forall.match_1.splitter : {α : Type u_2} →
  (motive : (x : ℕ) → ((Fin x → α) → Prop) → Sort u_1) →
    (x : ℕ) →
      (x_1 : (Fin x → α) → Prop) →
        ((P : (Fin 0 → α) → Prop) → motive 0 P) →
          ((n : ℕ) → (P : (Fin (n + 1) → α) → Prop) → motive n.succ P) → motive x x_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- `varMap` before variables were reordered.  -/
Lean.Meta.Grind.Arith.Cutsat.State.varMap' : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_emod_of_dvd : ∀ (n : ℤ) {m k : ℤ}, m ∣ k → n % k % m = n % m
-- Mathlib.Data.ULift
ULift.down_surjective : ∀ {α : Type u}, Function.Surjective ULift.down
-- Lean.Language.Lean.Types
/-- Next command, unless this is a terminal command.  -/
Lean.Language.Lean.CommandParsedSnapshot.nextCmdSnap? : Lean.Language.Lean.CommandParsedSnapshot → Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)
-- Init.Data.Sum.Basic
Sum.isLeft_inl : ∀ {α : Type u_1} {β : Type u_2} {x : α}, (Sum.inl x).isLeft = true
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- A `Cat`-enriched ordinary category comes with hom-categories `X ⟶[Cat] Y` whose underlying type
of objects is equivalent to the type `X ⟶ Y` defined by the category structure on `C`. The following
definition transfers the category structure to the latter type of objects.  -/
CategoryTheory.CatEnrichedOrdinary.instCategoryHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {X Y : CategoryTheory.CatEnrichedOrdinary C} → CategoryTheory.Category.{v', v} (X ⟶ Y)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.iSup_def : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_2} {f : ι → SaturatedSubmonoid M},
  iSup f = (⨆ i, (f i).toSubmonoid).saturation
-- Batteries.Data.Float.Lemmas
Float32.Model.mk.congr_simp : ∀ (toBits toBits_1 : UInt32) (e_toBits : toBits = toBits_1) (valid : Float.Model.Format.binary32.Valid toBits.toBitVec),
  { toBits := toBits, valid := valid } = { toBits := toBits_1, valid := ⋯ }
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.forget₂_algCat_map : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (f : A ⟶ B),
  (CategoryTheory.forget₂ (CommAlgCat R) (AlgCat R)).map f = AlgCat.ofHom (CommAlgCat.Hom.hom f)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeTop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], ⊤.IsClosedUnderColimitsOfShape J
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- An auxiliary lemma for manipulating sequence indices.  -/
PadicSeq.lift_index_left_left : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) (v2 v3 : ℕ),
  padicNorm p (↑f (PadicSeq.stationaryPoint hf)) = padicNorm p (↑f (max (PadicSeq.stationaryPoint hf) (max v2 v3)))
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.IsClosedUnderLimitsOfShape J ↔ P.limitsOfShape J ≤ P
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.tensorObj_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C),
  CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty D) [P.RespectsIso] (E : C ≌ D), P.inverseImage E.functor = P.map E.inverse
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- Differentiability on a set is equivalent to differentiability in the extended charts.  -/
mdifferentiableOn_iff_of_mem_maximalAtlas' : ∀ {𝕜 : 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'] {f : M → M'} {s : Set M}
  {e : OpenPartialHomeomorph M H} {e' : OpenPartialHomeomorph M' H'},
  e ∈ IsManifold.maximalAtlas I 1 M →
    e' ∈ IsManifold.maximalAtlas I' 1 M' →
      s ⊆ e.source →
        Set.MapsTo f s e'.source →
          (MDiff[s] f ↔ DifferentiableOn 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s))
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_zsmul_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocMod hp a (m • p + b) = toIocMod hp a b
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
Prove a degree bound for `sinPoly n` by induction. Note this is where we find the value in an
explicit description of `sinPoly`.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly_natDegree_le : ∀ (n : ℕ), (sinPoly✝ n).natDegree ≤ n
-- Mathlib.LinearAlgebra.Complex.Module
Complex.liftAux.congr_simp : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] (I' I'_1 : A) (e_I' : I' = I'_1) (hf : I' * I' = -1),
  Complex.liftAux I' hf = Complex.liftAux I'_1 ⋯
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regulator_ne_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.Units.regulator K ≠ 0
-- Batteries.Data.DList.Basic
/-- A difference List is a Function that, given a List, returns the original
contents of the difference List prepended to the given List.
This structure supports `O(1)` `append` and `push` operations on lists, making it
useful for append-heavy uses such as logging and pretty printing.
 -/
Batteries.DList : Type u → Type u
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In a commutative (possibly non-unital) semiring,
if `s₁` and `s₂` are sums of squares, then `s₁ * s₂` is a sum of squares.
 -/
IsSumSq.mul : ∀ {R : Type u_1} [inst : NonUnitalCommSemiring R] {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → IsSumSq (s₁ * s₂)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- A variant of `app_inv_app` that gives an `eqToHom` instead of `homOfLe`.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app' : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↑Y.toTopCat) (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U)) =
    Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Init.Data.Float.Model.Unpacked.Operations.Div
/-- Computes a `(mantissa, exponent)` pair for the quotient with enough bits to populate the mantissa
for the given specification. Also returns an `Accuracy` stating how the returned pair relates to
the infinitely precise quotient.
 -/
Float.Model.UnpackedFloat.divCore : Float.Model.Format → ℕ → ℤ → ℕ → ℤ → ℕ × ℤ × Float.Model.UnpackedFloat.Accuracy
-- Mathlib.Order.LatticeIntervals
Set.Ici.disjoint_iff : ∀ {α : Type u_1} [inst : SemilatticeInf α] {a : α} {x y : ↑(Set.Ici a)}, Disjoint x y ↔ ↑x ⊓ ↑y = a