mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Float32
/-- Obtains a `Float32` whose value is near the given `ISize`.

It will be exactly the value of the given `ISize` if such a `Float32` exists. If no such `Float32`
exists, the returned value will either be the smallest `Float32` that is larger than the given
value, or the largest `Float32` that is smaller than the given value.

This function does not reduce in the kernel.
 -/
ISize.toFloat32 : ISize → Float32
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_le_one_of_subsingleton : ∀ {V : Type u} (G : SimpleGraph V) [Subsingleton V], G.chromaticNumber ≤ 1
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.StronglyMeasurable.stronglyMeasurableAtFilter : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {l : Filter α} {f : α → β}
  {μ : MeasureTheory.Measure α}, MeasureTheory.StronglyMeasurable f → StronglyMeasurableAtFilter f l μ
-- Mathlib.Order.WithBot
WithBot.map₂_coe_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithBot α) (b : β),
  WithBot.map₂ f a ↑b = WithBot.map (fun x => f x b) a
-- Mathlib.Order.Category.BddLat
BddLat.hom_id : ∀ {X : Lat}, Lat.Hom.hom (CategoryTheory.CategoryStruct.id X) = LatticeHom.id ↑X
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_ofList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α}, (Std.DHashMap.ofList l).contains k = (List.map Sigma.fst l).contains k
-- Mathlib.Order.SupIndep
iSupIndep_def : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α},
  iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- A helper structure that bundles the necessary data to
construct a `StrictlyUnitaryLaxFunctor` without specifying the redundant
field `mapId`.  -/
CategoryTheory.StrictlyUnitaryLaxFunctorCore : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Mathlib.Data.Int.Log
Int.log_natCast : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b n : ℕ), Int.log b ↑n = ↑(Nat.log b n)
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- `rightRetraction` splits `g`  -/
CategoryTheory.IsSplitEqualizer.bottom_rightRetraction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (self : CategoryTheory.IsSplitEqualizer f g ι),
  CategoryTheory.CategoryStruct.comp g self.rightRetraction = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instSMulCommClass : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)]
  [inst_1 : (i : ι) → SMul N (α i)] [∀ (i : ι), SMulCommClass M N (α i)], SMulCommClass M N ((i : ι) × α i)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMap'_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.LeftHomologyData)
  (h₂ : S₂.LeftHomologyData) (h₃ : S₃.LeftHomologyData),
  CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ₁ h₁ h₂)
      (CategoryTheory.ShortComplex.leftHomologyMap' φ₂ h₂ h₃)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {km : α}, t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map_id : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f], (IsLocalizedModule.map S f f) LinearMap.id = LinearMap.id
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_iUnion_measurableSet : ∀ {α : Type u_1} {ι : Sort u_6} (m : ι → MeasurableSpace α),
  MeasurableSpace.generateFrom (⋃ n, {t | MeasurableSet t}) = ⨆ n, m n
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
/-- The discrete uniformity  -/
DiscreteUniformity : (X : Type u_1) → [u : UniformSpace X] → Prop
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrable_indicatorConstLp : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_7} [inst : NormedAddCommGroup E]
  {p : ENNReal} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E),
  MeasureTheory.Integrable (↑↑(MeasureTheory.indicatorConstLp p hs hμs c)) μ
-- Lean.Data.Lsp.Internal
/-- End line of the range of this location.  -/
Lean.Lsp.RefInfo.Location.endPosLine : Lean.Lsp.RefInfo.Location → ℕ
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- The general Leibniz rule for Lie derivatives.  -/
LieDerivation.iterate_apply_lie : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (D : LieDerivation R L L) (n : ℕ) (a b : L),
  (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
-- Mathlib.Data.Nat.Digits.Lemmas
/-- **Alias** of `Nat.length_digits_le_length_digits_succ`. -/
Nat.digits_len_le_digits_len_succ : ∀ (b n : ℕ), (b.digits n).length ≤ (b.digits (n + 1)).length
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_units_conj : ∀ {m : Type u_2} {R : Type u_6} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  (M : (Matrix m m R)ˣ) (N : Matrix m m R), (↑M * N * ↑M⁻¹).trace = N.trace
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_aci_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.AC.Expr) (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_aci_cert lhs rhs lhs' rhs' =
    (lhs.toSeq.erase0.sort.beq' lhs').and' (rhs.toSeq.erase0.sort.beq' rhs')
-- Lean.Expr
/-- Given `e` of the form `f a_1 ... a_n`, return `f`.
If `n` is greater than the number of arguments, then return `e.getAppFn`.
 -/
Lean.Expr.stripArgsN : Lean.Expr → ℕ → Lean.Expr
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ ∩ m₂},
  (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.Data.Sym.Sym2
Sym2.instRepr : {α : Type u_1} → [Repr α] → Repr (Sym2 α)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.mul_right : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {f g : MvPowerSeries τ R},
  PowerSeries.HasSubst f → PowerSeries.HasSubst (g * f)
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.instIsStableUnderCompositionFppfPrecoverage : AlgebraicGeometry.Scheme.fppfPrecoverage.IsStableUnderComposition
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.coe_subtype : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] (S' : A),
  ⇑(MulMemClass.subtype S') = Subtype.val
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k₁ k₂ : α} (h : (k₁ == k₂) = true) (h₁ : k₁ ∈ m), m.get k₁ h₁ = m.get k₂ ⋯
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- **Alias** of the reverse direction of `completeSpace_coe_iff_isComplete`. -/
IsComplete.completeSpace_coe : ∀ {α : Type u} [inst : UniformSpace α] {s : Set α}, IsComplete s → CompleteSpace ↑s
-- Init.Prelude
Lean.Macro.instInhabitedState.default : Lean.Macro.State
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ServerInfo.mk.injEq : ∀ (name : String) (version? : Option String) (name_1 : String) (version?_1 : Option String),
  ({ name := name, version? := version? } = { name := name_1, version? := version?_1 }) =
    (name = name_1 ∧ version? = version?_1)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Implementation detail for `widePullbackShapeEquiv`.  -/
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.widePullbackShapeEquivObj : {J : Type u_1} → CategoryTheory.Limits.WidePullbackShape J ≃ CategoryTheory.WithTerminal (CategoryTheory.Discrete J)
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_neg_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), inner 𝕜 (-x) y = -inner 𝕜 x y
-- Mathlib.Topology.Constructible
/-- [Stacks Tag 09YD](https://stacks.math.columbia.edu/tag/09YD) -/
Topology.IsConstructible.image_of_isOpenEmbedding : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  Topology.IsOpenEmbedding f →
    IsRetrocompact (Set.range f) → Topology.IsConstructible s → Topology.IsConstructible (f '' s)
-- Mathlib.RingTheory.Extension.Basic
/-- The identity map `P.Cotangent → P.ker.Cotangent` from the type synonym.  -/
Algebra.Extension.Cotangent.val : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {P : Algebra.Extension R S} → P.Cotangent → P.ker.Cotangent
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_eq_nat_iff : ∀ {α : Type u} {n : ℕ}, Cardinal.mk α = ↑n ↔ Nonempty (α ≃ Fin n)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.branch.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (a : σ → Bool) (a_1 a_2 : Turing.TM2.Stmt Γ Λ σ),
  sizeOf (Turing.TM2.Stmt.branch a a_1 a_2) = 1 + sizeOf a_1 + sizeOf a_2
-- Mathlib.CategoryTheory.EpiMono
/-- All monos are split  -/
CategoryTheory.SplitMonoCategory.isSplitMono_of_mono : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.SplitMonoCategory C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.IsSplitMono f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.unitOfList_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α},
  (Std.DTreeMap.Const.unitOfList l cmp).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l)
-- Mathlib.GroupTheory.QuotientGroup.Finite
/-- If `F` and `coker(F →+ G)` are finite, then `G` is finite.  -/
AddGroup.fintypeOfDomOfCoker : {F : Type u_1} →
  {G : Type u_2} →
    [inst : AddGroup F] →
      [inst_1 : AddGroup G] → [Fintype F] → (f : F →+ G) → [f.range.Normal] → [Fintype (G ⧸ f.range)] → Fintype G
-- Mathlib.Combinatorics.Young.SemistandardTableau
/-- A semistandard Young tableau is a filling of the cells of a Young diagram by natural
numbers, such that the entries in each row are weakly increasing (left to right), and the entries
in each column are strictly increasing (top to bottom).

Here, a semistandard Young tableau is represented as an unrestricted function `ℕ → ℕ → ℕ` that, for
reasons of extensionality, is required to vanish outside `μ`.  -/
SemistandardYoungTableau : YoungDiagram → Type
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.coe_toHom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f : L.Equiv M N}, ⇑f.toHom = ⇑f
-- Mathlib.Algebra.Order.Group.Synonym
toLex_smul : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α), toLex (b • a) = b • toLex a
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.mul_def : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R},
  p * q = p.coeff.sum fun m a => q.coeff.sum fun n b => (MvPolynomial.monomial (m + n)) (a * b)
-- Mathlib.Data.Int.Cast.Lemmas
/-- If two `MonoidWithZeroHom`s agree on `-1` and the naturals then they are equal.  -/
MonoidWithZeroHom.ext_int : ∀ {M : Type u_5} [inst : MonoidWithZero M] {f g : ℤ →*₀ M},
  f (-1) = g (-1) → f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom → f = g
-- Mathlib.Algebra.Lie.Basis.Basic
/-- The nilpotent part of the "upper" Borel subalgebra associated to a basis.  -/
LieAlgebra.Basis.borelUpper : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] →
            [inst_3 : LieAlgebra R L] → {H : LieSubalgebra R L} → LieAlgebra.Basis ι H → LieSubmodule R (↥H) L
-- Mathlib.Order.Filter.Pointwise
Filter.coe_pureOneHom : ∀ {α : Type u_2} [inst : One α], ⇑Filter.pureOneHom = pure
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
BoundedContinuousFunction.innerProbChar_apply : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (t x : E),
  (BoundedContinuousFunction.innerProbChar t) x = Complex.exp (↑(inner ℝ x t) * Complex.I)
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_predAbove_succAbove : ∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), (j.predAbove i).predAbove (i.succAbove j) = j
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The canonical isomorphism of triangles `(triangleh φ).rotate ≅ (triangleh (inr φ))`.  -/
CochainComplex.mappingCone.rotateTrianglehIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (φ : K ⟶ L) →
            (CochainComplex.mappingCone.triangleh φ).rotate ≅
              CochainComplex.mappingCone.triangleh (CochainComplex.mappingCone.inr φ)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_ne_zero : ∀ (α : Type u) [Nonempty α], Cardinal.mk α ≠ 0
-- Mathlib.Data.ZMod.Units
/-- The unit of `ZMod m` associated with an integer prime to `n`.  -/
ZMod.unitOfIsCoprime : {m : ℕ} → (n : ℤ) → IsCoprime n ↑m → (ZMod m)ˣ
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- `Hσ` is null homotopic  -/
AlgebraicTopology.DoldKan.homotopyHσToZero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} → (q : ℕ) → Homotopy (AlgebraicTopology.DoldKan.Hσ q) 0
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {c d : E → 𝔸'},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 d x → fderiv 𝕜 (c * d) x = c x • fderiv 𝕜 d x + d x • fderiv 𝕜 c x
-- Init.Data.Repr
instReprAtomUInt64 : ReprAtom UInt64
-- Lean.Expr
Lean.Expr.mvar.inj : ∀ {mvarId mvarId_1 : Lean.MVarId}, Lean.Expr.mvar mvarId = Lean.Expr.mvar mvarId_1 → mvarId = mvarId_1
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.HasWeakSheafify J B]
  [inst_4 : CategoryTheory.HasWeakSheafify J A] [inst_5 : J.PreservesSheafification F]
  (X : CategoryTheory.Functor Cᵒᵖ A),
  (CategoryTheory.presheafToSheafCompComposeAndSheafifyIso J F).inv.app X =
    (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J X) F)
-- Init.Data.SInt.Lemmas
Int8.toInt_sub_of_le : ∀ (a b : Int8), 0 ≤ b → b ≤ a → (a - b).toInt = a.toInt - b.toInt
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerSkip_flatMapM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α m β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ it₁' : Std.IterM m β},
  it₁.IsPlausibleStep (Std.IterStep.skip it₁') →
    (Std.IterM.flatMapAfterM f it₁ none).IsPlausibleStep (Std.IterStep.skip (Std.IterM.flatMapAfterM f it₁' none))
-- Mathlib.Data.Set.Function
/-- **Alias** of `Set.InjOn.image_sdiff_subset`. -/
Set.InjOn.image_diff_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {t : Set α},
  Set.InjOn f s → t ⊆ s → f '' (s \ t) = f '' s \ f '' t
-- Lean.Message
Lean.MessageDataContext.mk : Lean.Environment → Lean.MetavarContext → Lean.LocalContext → Lean.Options → Lean.MessageDataContext
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIdIso C).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
-- Mathlib.Algebra.Group.AddChar
AddChar.div_apply' : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : DivisionCommMonoid M] (ψ χ : AddChar A M) (a : A),
  (ψ / χ) a = ψ a / χ a
-- Mathlib.Topology.UniformSpace.Equicontinuity
EquicontinuousWithinAt.mono : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} {x₀ : X}
  {S T : Set X}, EquicontinuousWithinAt F T x₀ → S ⊆ T → EquicontinuousWithinAt F S x₀
-- Batteries.Recycling.RBTree.Basic
/-- A red-black tree. (This is an internal implementation detail of the `RBSet` type,
which includes the invariants of the tree.) This is a binary search tree augmented with
a "color" field which is either red or black for each node and used to implement
the re-balancing operations.
See: [Red–black tree](https://en.wikipedia.org/wiki/Red%E2%80%93black_tree)
 -/
RBTree.RBNode : Type u → Type u
-- Mathlib.CategoryTheory.Limits.Final
/-- Given a cone over `F ⋙ G`, we can construct a `Cone G` with the same cocone point.
 -/
CategoryTheory.Functor.Initial.extendCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  CategoryTheory.Functor (CategoryTheory.Limits.Cone (F.comp G)) (CategoryTheory.Limits.Cone G)
-- Mathlib.Analysis.Normed.Ring.Lemmas
NNReal.lipschitzWith_sub : LipschitzWith 2 fun p => p.1 - p.2
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.pathELength_mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b a' b' : ℝ} {γ : ℝ → M},
  a' ≤ a → b ≤ b' → Manifold.pathELength I γ a b ≤ Manifold.pathELength I γ a' b'
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.degree_eq_one_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial B],
  (minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.entryAtIdx?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.entryAtIdx? i = t₂.entryAtIdx? i
-- Mathlib.FieldTheory.Relrank
IntermediateField.rank_comap : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E)
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] (f : L →ₐ[F] E),
  Module.rank (↥(IntermediateField.comap f A)) L = A.relrank f.fieldRange
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.of_discrete : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F} [DiscreteMeasurableSpace α] [Finite α] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp f p μ
-- Mathlib.Order.Interval.Set.Nat
Set.ncard_Iic_nat : ∀ (b : ℕ), (Set.Iic b).ncard = b + 1
-- Init.Data.Array.Lemmas
Array.toArray_eq_append_iff : ∀ {α : Type u_1} {xs : List α} {as bs : Array α}, xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList
-- Mathlib.RingTheory.FiniteType
/-- A commutative algebra is finitely generated if and only if it is a quotient
of a polynomial ring whose variables are indexed by a finset.  -/
Algebra.FiniteType.iff_quotient_mvPolynomial : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.FiniteType R S ↔ ∃ s f, Function.Surjective ⇑f
-- Init.Data.UInt.Bitwise
UInt8.not_eq_comm : ∀ {a b : UInt8}, ~~~a = b ↔ a = ~~~b
-- Std.Sat.CNF.Basic
Std.Sat.CNF.VarMem_append : ∀ {α : Type u_1} {v : α} {f1 f2 : Std.Sat.CNF α},
  Std.Sat.CNF.VarMem v (f1 ++ f2) ↔ Std.Sat.CNF.VarMem v f1 ∨ Std.Sat.CNF.VarMem v f2
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_subtypeDomain_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {v : Π₀ (i : ι), β i} {p : ι → Prop}
  [inst_4 : DecidablePred p] {h : (i : ι) → β i → γ},
  (∀ x ∈ v.support, p x) → ((DFinsupp.subtypeDomain p v).sum fun i b => h (↑i) b) = v.sum h
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangle_obj₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), h.triangle.obj₃ = Z₂₃
-- Mathlib.LinearAlgebra.Prod
LinearMap.inr_injective : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Function.Injective ⇑(LinearMap.inr R M M₂)
-- Mathlib.Order.Nat
/-- `Nat.find` is the minimum element of a nonempty set of natural numbers.  -/
Set.Nonempty.isLeast_natFind : ∀ {s : Set ℕ} [inst : DecidablePred fun x => x ∈ s] (hs : s.Nonempty), IsLeast s (Nat.find hs)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instSemilatticeInf : {X : AlgebraicGeometry.Scheme} → SemilatticeInf X.IdealSheafData
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.mk.inj : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} {inst : NormedField 𝕜}
  {inst_1 : SeminormedAddCommGroup V} {inst_2 : NormedSpace 𝕜 V} {inst_3 : PseudoMetricSpace P}
  {inst_4 : NormedAddTorsor V P} {inst_5 : SeminormedAddCommGroup V₂} {inst_6 : NormedSpace 𝕜 V₂}
  {inst_7 : PseudoMetricSpace P₂} {inst_8 : NormedAddTorsor V₂ P₂} {toAffineMap : P →ᵃ[𝕜] P₂}
  {norm_map : ∀ (x : V), ‖toAffineMap.linear x‖ = ‖x‖} {toAffineMap_1 : P →ᵃ[𝕜] P₂}
  {norm_map_1 : ∀ (x : V), ‖toAffineMap_1.linear x‖ = ‖x‖},
  { toAffineMap := toAffineMap, norm_map := norm_map } = { toAffineMap := toAffineMap_1, norm_map := norm_map_1 } →
    toAffineMap = toAffineMap_1