mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Floor.Ring
/-- a variant of `Nat.ceil_lt_add_one` with its condition `0 ≤ a` generalized to `-1 < a`  -/
Nat.ceil_lt_add_one_of_gt_neg_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsStrictOrderedRing R] {a : R},
  -1 < a → ↑⌈a⌉₊ < a + 1
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.Prod.upMulHom.eq_1 : ∀ (G : Type u) (H : Type v) [inst : Mul G] [inst_1 : Mul H],
  Prod.upMulHom✝ G H = { toFun := fun x t => Bool.rec { down := x.1 } { down := x.2 } t, map_mul' := ⋯ }
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.instIsEquivalenceModuleCatMonoidAlgebraOfModuleMonoidAlgebra : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G], Rep.ofModuleMonoidAlgebra.IsEquivalence
-- Mathlib.AlgebraicGeometry.Scheme
/-- forgetful functor to `Scheme` is the same as coercion  -/
AlgebraicGeometry.Scheme.forget_obj_eq_coe : AlgebraicGeometry.Scheme → Prop
-- Mathlib.Analysis.Normed.Field.Basic
NontriviallyNormedField.mk : {α : Type u_5} → [toNormedField : NormedField α] → (∃ x, 1 < ‖x‖) → NontriviallyNormedField α
-- Mathlib.Topology.Algebra.Group.Basic
continuousWithinAt_inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] {s : Set G} {x : G},
  ContinuousWithinAt Inv.inv s x
-- Mathlib.NumberTheory.FactorisationProperties
Nat.not_deficient_zero : ¬Nat.Deficient 0
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inlₗ_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (a : α), (OrderAddMonoidHom.inlₗ α β) a = toLex (a, 0)
-- Mathlib.Analysis.Complex.Exponential
Real.exp_pos : ∀ (x : ℝ), 0 < Real.exp x
-- Lean.Meta.Tactic.Grind.PP
/-- Result for helper function `isArithOfCastLike`  -/
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Result : Type
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The morphisms between the `obj` fields of descent data.  -/
CategoryTheory.Pseudofunctor.DescentData.Hom.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} → {f : (i : ι) → X i ⟶ S} → {D₁ D₂ : F.DescentData f} → D₁.Hom D₂ → (i : ι) → D₁.obj i ⟶ D₂.obj i
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- Interpret `fun f : α →₀ M ↦ f a` as a linear map.  -/
Finsupp.lapply : {α : Type u_1} →
  {M : Type u_2} →
    {R : Type u_5} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → α → (α →₀ M) →ₗ[R] M
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.cgf_const : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsProbabilityMeasure μ]
  (c : ℝ), ProbabilityTheory.cgf (fun x => c) μ t = t * c
-- Mathlib.Data.List.Flatten
/-- Taking only the first `i+1` elements in a list, and then dropping the first `i` ones, one is
left with a list of length `1` made of the `i`-th element of the original list.  -/
List.drop_take_succ_eq_cons_getElem : ∀ {α : Type u_1} (L : List α) (i : ℕ) (h : i < L.length), List.drop i (List.take (i + 1) L) = [L[i]]
-- Mathlib.Data.Num.Basic
PosNum.bit1.sizeOf_spec : ∀ (a : PosNum), sizeOf a.bit1 = 1 + sizeOf a
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If one adds to a vector `m'` another vector `m`, but only for coordinates in a finset `t`, then
the image under a multilinear map `f` is the sum of `f (s.piecewise m m')` along all subsets `s` of
`t`. This is mainly an auxiliary statement to prove the result when `t = univ`, given in
`map_add_univ`, although it can be useful in its own right as it does not require the index set `ι`
to be finite.  -/
MultilinearMap.map_piecewise_add : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m m' : (i : ι) → M₁ i) (t : Finset ι),
  f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v : β k') → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v l r => h_2 size k' v l r) =
    h_1 ()
-- Mathlib.Topology.Algebra.Module.Complement
/-- Two submodules `p` and `q` are *topological complements* if they are algebraic complements and
the projection on `p` along `q` is continuous.  -/
Submodule.IsTopCompl : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_2} →
      [TopologicalSpace M] → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → Submodule R M → Submodule R M → Prop
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.hasBinaryCoproduct_zero_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasZeroMorphisms C] (X : C), CategoryTheory.Limits.HasBinaryCoproduct 0 X
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- **Equational criterion for flatness**, backward direction, alternate form.

Let $M$ be a module over a commutative ring $R$. Suppose that for all finite free modules $R^l$,
all $f \in R^l$, and all linear maps $x \colon R^l \to M$ such that $x(f) = 0$, there
exist a finite free module $R^k$ and linear maps $a \colon R^l \to R^k$ and
$y \colon R^k \to M$ such that $x = y \circ a$ and $a(f) = 0$. Then $M$ is flat.  -/
Module.Flat.of_forall_exists_factorization : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0) → Module.Flat R M
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.filteredClosure.max : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  {f : α → C} {j j' : C},
  CategoryTheory.IsFiltered.filteredClosure f j →
    CategoryTheory.IsFiltered.filteredClosure f j' →
      CategoryTheory.IsFiltered.filteredClosure f (CategoryTheory.IsFiltered.max j j')
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback a `CompleteDistribLattice.MinimalAxioms` along an injection.  -/
Function.completeDistribLatticeMinimalAxioms : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  CompleteDistribLattice.MinimalAxioms β →
    ∀ (f : α → β),
      (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
        (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
          (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
            (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
              (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) → CompleteDistribLattice.MinimalAxioms α
-- Mathlib.Analysis.Complex.ReImTopology
IsClosed.reProdIm : ∀ {s t : Set ℝ}, IsClosed s → IsClosed t → IsClosed (s ×ℂ t)
-- Init.Data.Function
Function.Injective.ne : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ {a₁ a₂ : α}, a₁ ≠ a₂ → f a₁ ≠ f a₂
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- The preferred chart at each point in the charted space.  -/
ChartedSpace.chartAt : {H : Type u_5} →
  {inst : TopologicalSpace H} →
    {M : Type u_6} → {inst_1 : TopologicalSpace M} → [self : ChartedSpace H M] → M → OpenPartialHomeomorph M H
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.eq_bot_iff_forall : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H = ⊥ ↔ ∀ x ∈ H, x = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  (forIn t init fun a d => f a.1 d) = forIn t.keysArray init f
-- Mathlib.Order.Heyting.Basic
Codisjoint.himp_eq_right : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → b ⇨ a = a
-- Mathlib.Algebra.Algebra.Equiv
/-- Each element of the group defines an algebra equivalence.

This is a stronger version of `MulSemiringAction.toRingAut` and
`DistribMulAction.toModuleEnd`.  -/
MulSemiringAction.toAlgAut : (G : Type u_2) →
  (R : Type u_3) →
    (A : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Group G] → [inst_4 : MulSemiringAction G A] → [SMulCommClass G R A] → G →* A ≃ₐ[R] A
-- Lean.CoreM
/-- Option for capturing output to stderr during elaboration.  -/
Lean.Core.stderrAsMessages : Lean.Option Bool
-- Lean.Util.Diff
Lean.Diff.instBEqAction.beq : Lean.Diff.Action → Lean.Diff.Action → Bool
-- Std.Data.DTreeMap.Raw.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw`.
The `insertMany` function on `TreeSet` and `TreeSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.DTreeMap.Raw.Const.insertMany : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      {ρ : Type u_1} →
        [ForIn Id ρ (α × β)] → Std.DTreeMap.Raw α (fun x => β) cmp → ρ → Std.DTreeMap.Raw α (fun x => β) cmp
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Two compatible families on the sieve generated by a presieve `R` are equal if and only if they are
equal when restricted to `R`.
 -/
CategoryTheory.Presieve.restrict_inj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X}
  {x₁ x₂ : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows},
  x₁.Compatible →
    x₂.Compatible →
      CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₁ = CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₂ →
        x₁ = x₂
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The range of a semigroup homomorphism is a subsemigroup. See Note [range copy pattern].  -/
MulHom.srange : {M : Type u_1} → {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → Subsemigroup N
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.instCoeSortType.eq_1 : FiniteGrp.instCoeSortType = { coe := fun G => ↑G.toGrp }
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rankD_eq : ∀ {arr : Array Batteries.UFNode} {i : ℕ} (h : i < arr.size), Batteries.UnionFind.rankD arr i = arr[i].rank
-- Mathlib.Order.PartialSups
partialSups_monotone : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  (f : ι → α), Monotone ⇑(partialSups f)
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_1.eq_7 : ∀ (motive : Lean.Expr → Sort u_1) (e : Lean.Expr) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (e : Lean.Expr) → motive e),
  (∀ (a : Lean.Literal), e = Lean.Expr.lit a → False) →
    (∀ (mvarId : Lean.MVarId), e = Lean.Expr.mvar mvarId → False) →
      (∀ (deBruijnIndex : ℕ), e = Lean.Expr.bvar deBruijnIndex → False) →
        (∀ (fvarId : Lean.FVarId), e = Lean.Expr.fvar fvarId → False) →
          (∀ (declName : Lean.Name) (us : List Lean.Level), e = Lean.Expr.const declName us → False) →
            (∀ (u : Lean.Level), e = Lean.Expr.sort u → False) →
              (match e with
                | Lean.Expr.lit a => h_1 a
                | Lean.Expr.mvar mvarId => h_2 mvarId
                | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
                | Lean.Expr.fvar fvarId => h_4 fvarId
                | Lean.Expr.const declName us => h_5 declName us
                | Lean.Expr.sort u => h_6 u
                | e => h_7 e) =
                h_7 e
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_subset_range : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s t : Set β},
  s ⊆ Set.range ⇑m → t ⊆ Set.range ⇑m → s - t ⊆ Set.range ⇑m
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_mono_ae : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f g : X → E}
  {s : Set X} [ClosedIciTopology E],
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ → f ≤ᵐ[μ] g → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.surjective_domRestrict_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M},
  Function.Surjective ⇑f → (Function.Surjective ⇑(f.domRestrict S) ↔ Codisjoint S f.ker)
-- Init.Data.Vector.Count
Vector.not_mem_of_count_eq_zero : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a : α} {xs : Vector α n}, Vector.count a xs = 0 → a ∉ xs
-- Lean.Data.Name
/-- Returns true if this a part of name that is internal or dynamically
generated so that it may easily be changed.

Generally, user code should not explicitly use internal names.
 -/
Lean.Name.isInternalDetail : Lean.Name → Bool
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The `AddMonoidHom` from the preimage of an `AddSubmonoid` to itself.  -/
AddMonoidHom.addSubmonoidComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → (f : M →+ N) → (N' : AddSubmonoid N) → ↥(AddSubmonoid.comap f N') →+ ↥N'
-- Mathlib.Topology.Category.Stonean.Basic
/-- The morphism from `presentation X` to `X`.  -/
CompHaus.presentation.π : (X : CompHaus) → Stonean.toCompHaus.obj X.presentation ⟶ X
-- Mathlib.Order.Closure
/-- An element `x` is closed for `l : LowerAdjoint u` if it is a fixed point: `u (l x) = x`  -/
LowerAdjoint.closed : {α : Type u_1} → {β : Type u_4} → [inst : Preorder α] → [inst_1 : Preorder β] → {u : β → α} → LowerAdjoint u → Set α
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.addEquiv_apply : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V] (self : WithLp p V), (WithLp.addEquiv p V) self = self.ofLp
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.trivial_addGrp_neg : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrpObj.neg = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (X_1 : (TopologicalSpace.Opens ↑↑(Y.restrict ⋯))ᵒᵖ),
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict f).hom.c.app X_1 =
    CategoryTheory.CategoryStruct.comp
      (f.c.app
        (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj (Opposite.unop X_1))))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯))
-- Mathlib.GroupTheory.GroupAction.Basic
Equiv.swap_mem_stabilizer : ∀ {α : Type u_1} [inst : DecidableEq α] {S : Set α} {a b : α},
  Equiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) S ↔ (a ∈ S ↔ b ∈ S)
-- Batteries.Data.Array.Match
Array.Matcher.mk : {α : Type u_1} → (table : Array.PrefixTable α) → Fin (table.size + 1) → Array.Matcher α
-- Mathlib.GroupTheory.Congruence.Defs
/-- Given a type `M` with an addition, `x, y ∈ M`, and an additive congruence relation
`c` on `M`, `(x, y) ∈ M × M` iff `x` is related to `y` by `c`.  -/
AddCon.instMembershipProd : {M : Type u_1} → [inst : Add M] → Membership (M × M) (AddCon M)
-- Mathlib.Data.Finset.Empty
Finset.nonempty_def : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty ↔ ∃ x, x ∈ s
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mem_mul_span_singleton : ∀ {R : Type u} [inst : Semiring R] {x y : R} {I : Ideal R} [I.IsTwoSided], x ∈ I * Ideal.span {y} ↔ ∃ z ∈ I, z * y = x
-- Mathlib.Algebra.Algebra.Operations
Submodule.bot_smul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (N : Submodule R M), ⊥ • N = ⊥
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {a k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).getKey? a = if compare k a = Ordering.eq then some k else t.getKey? a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipPrefix?_eq_skipPrefix?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.skipPrefix? pat = Option.map String.Pos.ofToSlice (s.toSlice.skipPrefix? pat)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.arrowSucc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  {j : J} (F F_1 : CategoryTheory.Functor (↑(Set.Iic j)) C),
  F = F_1 →
    ∀ (i i_1 : J) (e_i : i = i_1) (hi : i < j),
      CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi = CategoryTheory.SmallObject.SuccStruct.arrowSucc F_1 i_1 ⋯
-- Std.Data.DHashMap.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.

Note: this replacement behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insert` function on `HashSet` and `HashSet.Raw` behaves differently: it will return the set
unchanged if a matching key is already present.
 -/
Std.DHashMap.insert : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → (a : α) → β a → Std.DHashMap α β
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_sub_self_of_bmod_eq : ∀ {a : ℤ} {b : ℕ} {c : ℤ}, a.bmod b = c → ↑b ∣ c - a
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.hcomp_half : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ x₂ : X} {p₀ q₀ : Path x₀ x₁} {p₁ q₁ : Path x₁ x₂} (F : p₀.Homotopy q₀)
  (G : p₁.Homotopy q₁) (t : ↑unitInterval), (F.hcomp G) (t, ⟨1 / 2, ⋯⟩) = x₁
-- Mathlib.Topology.MetricSpace.Ultra.Pi
Pi.instIsUltrametricDist : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → PseudoMetricSpace (X i)]
  [∀ (i : ι), IsUltrametricDist (X i)], IsUltrametricDist ((i : ι) → X i)
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.killCompl_X : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} (i : σ),
  (MvPowerSeries.killCompl e) (MvPowerSeries.X (e i)) = MvPowerSeries.X i
-- Mathlib.Analysis.Convex.Join
convexJoin_singleton_left : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (t : Set E) (x : E), convexJoin 𝕜 {x} t = ⋃ y ∈ t, segment 𝕜 x y
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α},
  (m₁ ∩ m₂).getKeyD k fallback = if k ∈ m₂ then m₁.getKeyD k fallback else fallback
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Functor.toOver_obj_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} S]
  (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X)
  (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) (Y : S),
  ((F.toOver X f h).obj Y).left = F.obj Y
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
exists_isTranscendenceBasis_superset : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {s : Set A},
  AlgebraicIndepOn R id s → ∃ t, s ⊆ t ∧ IsTranscendenceBasis R Subtype.val
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_one_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] [inst_3 : One R],
  HahnSeries.cardSupp 1 ≤ 1
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand the square  -/
norm_add_mul_self_real : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * inner ℝ x y + ‖y‖ * ‖y‖
-- Mathlib.Algebra.Group.Units.Defs
/-- `inv` is the left inverse of `val` in the base `Monoid`.  -/
Units.inv_val : ∀ {α : Type u} [inst : Monoid α] (self : αˣ), self.inv * ↑self = 1
-- Mathlib.Topology.Instances.Matrix
IsCompact.matrix : ∀ {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] {S : Set R}, IsCompact S → IsCompact S.matrix
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of `Finset.apply_sup'_eq_sup'_comp`. -/
Finset.comp_inf'_eq_inf'_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup γ] {s : Finset β}
  (H : s.Nonempty) {f : β → α} (g : α → γ), (∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) → g (s.sup' H f) = s.sup' H (g ∘ f)
-- Mathlib.Algebra.Group.Indicator
Set.indicator_symmDiff : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (s t : Set α) (f : α → M),
  (symmDiff s t).indicator f = (s \ t).indicator f + (t \ s).indicator f
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- `A.IsDiag` means square matrix `A` is a diagonal matrix.  -/
Matrix.IsDiag : {α : Type u_1} → {n : Type u_4} → [Zero α] → Matrix n n α → Prop
-- Lean.Elab.Declaration
/-- Return true if all elements of the mutual-block are definitions/theorems/abbrevs.  -/
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.isMutualDefLike : Lean.Syntax → Bool
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq : ∀ {G : Type u_5} {α : Type u_6} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α} {s t : Set α}
  {μ : MeasureTheory.Measure α} (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g⁻¹ • x) μ μ → s =ᵐ[μ] t → g • s =ᵐ[μ] g • t
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
/-- The liftings of a commutative are in bijection with the liftings of its (left)
adjoint square.  -/
CategoryTheory.CommSq.leftAdjointLiftStructEquiv : {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] →
        {G : CategoryTheory.Functor C D} →
          {F : CategoryTheory.Functor D C} →
            {A B : C} →
              {X Y : D} →
                {i : B ⟶ A} →
                  {p : Y ⟶ X} →
                    {u : X ⟶ G.obj A} →
                      {v : Y ⟶ G.obj B} →
                        (sq : CategoryTheory.CommSq v p (G.map i) u) → (adj : F ⊣ G) → sq.LiftStruct ≃ ⋯.LiftStruct