mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Config
/-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search.  -/
Lean.Grind.Config.splitMatch : Lean.Grind.Config → Bool
-- Mathlib.CategoryTheory.Pi.Basic
/-- Assemble an `I`-indexed family of natural transformations into a single natural transformation.
 -/
CategoryTheory.NatTrans.pi' : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {E : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} E] →
          {F G : CategoryTheory.Functor E ((i : I) → C i)} →
            ((i : I) → F.comp (CategoryTheory.Pi.eval C i) ⟶ G.comp (CategoryTheory.Pi.eval C i)) → (F ⟶ G)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α} {v : β k}, (m.insert k v).getKeyD k fallback = k
-- Mathlib.Analysis.Calculus.Deriv.Prod
HasStrictDerivAt.finCons : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : F' 0} {φs' : (i : Fin n) → F' i.succ},
  HasStrictDerivAt φ φ' x →
    HasStrictDerivAt φs φs' x → HasStrictDerivAt (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.separatingLeft_congr_iff : ∀ {R : Type u_1} {M : Type u_5} {Mₗ₁ : Type u_9} {Mₗ₁' : Type u_10} {Mₗ₂ : Type u_11} {Mₗ₂' : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid Mₗ₁]
  [inst_4 : AddCommMonoid Mₗ₂] [inst_5 : AddCommMonoid Mₗ₁'] [inst_6 : AddCommMonoid Mₗ₂'] [inst_7 : Module R Mₗ₁]
  [inst_8 : Module R Mₗ₂] [inst_9 : Module R Mₗ₁'] [inst_10 : Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M}
  (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'),
  ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft ↔ B.SeparatingLeft
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_lt_lift : ∀ {x : Cardinal.{v}} {m : ℕ∞}, ↑m < Cardinal.lift.{u, v} x ↔ ↑m < x
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.rightOfAdd.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (a b : M) (hu : a + b = ↑u) (hc : AddCommute a b),
  u.rightOfAdd a b hu hc = u.leftOfAdd b a ⋯ ⋯
-- Lean.Util.Diff
Lean.Diff.Action.skip.sizeOf_spec : sizeOf Lean.Diff.Action.skip = 1
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_prod_list_swap : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {l : List (Equiv.Perm α)},
  (∀ g ∈ l, g.IsSwap) → Equiv.Perm.sign l.prod = (-1) ^ l.length
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.neg : ∀ {p x : ℝ}, LiouvilleWith p x → LiouvilleWith p (-x)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.symm_image_target_inter_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set Y), ↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' (e.target ∩ s)
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
/-- If the exponential comparison transformation (at `A`) is an isomorphism, then the Frobenius morphism
at `A` is an isomorphism.
 -/
CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.MonoidalClosed D]
  [inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  (h : L ⊣ F) (A : C) [i : CategoryTheory.IsIso (CategoryTheory.expComparison F A).natTrans],
  CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A).natTrans
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar : ∀ {k : Type u_1} {K : Type u_2} {R : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  [inst_3 : CommRing R] [inst_4 : Algebra k R] [IsPurelyInseparable k K] (q : ℕ) [ExpChar k q]
  (x : TensorProduct k R K), ∃ n, x ^ q ^ n ∈ (algebraMap R (TensorProduct k R K)).range
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardCongr₂_hom_app_val_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S)
  {ψ : T ⟶ (F.sheafPushforwardContinuous RingCat J K).obj S} (e : F ≅ G)
  (he :
    CategoryTheory.CategoryStruct.comp φ
        ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans e.hom RingCat J K).app S) =
      ψ)
  (X : SheafOfModules S) (x : Cᵒᵖ) (x_1 : ↑(((SheafOfModules.pushforward φ).obj X).val.obj x)),
  (ModuleCat.Hom.hom (((SheafOfModules.pushforwardCongr₂ φ e he).hom.app X).val.app x)) x_1 =
    (((SheafOfModules.pushforwardCongr he).hom.app X).val.app x).hom'
      ((((SheafOfModules.pushforwardNatTrans φ e.hom).app X).val.app x).hom' x_1)
-- Mathlib.Topology.ContinuousMap.Basic
/-- The composition of continuous maps, as a continuous map.  -/
ContinuousMap.comp : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] → [inst_2 : TopologicalSpace γ] → C(β, γ) → C(α, β) → C(α, γ)
-- Init.Data.List.Nat.Modify
List.modifyHead_modifyHead : ∀ {α : Type u_1} {l : List α} {f g : α → α}, List.modifyHead g (List.modifyHead f l) = List.modifyHead (g ∘ f) l
-- Mathlib.Order.IsNormal
Order.IsNormal.of_succ_lt : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : SuccOrder α]
  [inst_3 : LinearOrder β],
  (∀ (a : α), f a < f (Order.succ a)) →
    (∀ {a : α}, Order.IsSuccLimit a → IsLUB (f '' Set.Iio a) (f a)) → Order.IsNormal f
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFree.mono : ∀ {α : Type u_1} {G : SimpleGraph α} {m n : ℕ}, m ≤ n → G.CliqueFree m → G.CliqueFree n
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- Any discrete space is completely metrizable.  -/
TopologicalSpace.IsCompletelyMetrizableSpace.discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] [DiscreteTopology X], TopologicalSpace.IsCompletelyMetrizableSpace X
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.le_one_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (a : A), autoParam (p a) CFC.le_one_iff._auto_1 → (a ≤ 1 ↔ ∀ x ∈ spectrum R a, x ≤ 1)
-- Mathlib.Order.CountableSupClosed
countableSupClosed_preimage_ofDual : ∀ {α : Type u_2} [inst : LE α] {s : Set α}, CountableSupClosed (⇑OrderDual.ofDual ⁻¹' s) ↔ CountableInfClosed s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Clz
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastClz : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (xc : aig.RefVec w)
  (x : BitVec w) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx) →
    ∀ (idx : ℕ) (hidx : idx < w),
      ⟦assign,
          { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastClz aig xc).aig,
            ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastClz aig xc).vec.get idx hidx }⟧ =
        (x.clzAuxRec (w - 1)).getLsbD idx
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.instMonoidalTransportedFunctorSymmEquivalenceTransported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          (e : C ≌ D) → (CategoryTheory.Monoidal.equivalenceTransported e).symm.functor.Monoidal
-- Lean.Parser.Command
Lean.Parser.Command.structCtor.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.closure_mono : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {t s : Set α},
  s ⊆ t → BooleanSubalgebra.closure s ≤ BooleanSubalgebra.closure t
-- Mathlib.Analysis.Normed.Lp.LpEquiv
/-- The canonical map between `lp (fun _ : α ↦ A) ∞` and `α →ᵇ A` as an `AlgEquiv`.  -/
AlgEquiv.lpBCF : (α : Type u_1) →
  {A : Type u_4} →
    (𝕜 : Type u_5) →
      [inst : TopologicalSpace α] →
        [DiscreteTopology α] →
          [inst_2 : NormedRing A] →
            [inst_3 : NormOneClass A] →
              [inst_4 : NontriviallyNormedField 𝕜] →
                [inst_5 : NormedAlgebra 𝕜 A] → ↥(lp (fun x => A) ⊤) ≃ₐ[𝕜] BoundedContinuousFunction α A
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_add_closure_zero : ∀ {G : Type u_1} [inst : AddZeroClass G] [inst_1 : TopologicalSpace G] (s : Set G), s ⊆ s + closure {0}
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_filterMapₘ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Option (δ a)},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑(m.filterMapₘ f)
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.failed.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (err : Std.Http.Protocol.H1.Error),
  sizeOf (Std.Http.Protocol.H1.Event.failed err) = 1 + sizeOf err
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_zero : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2], ⇑0 = 0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isCocycle₂_of_mem_cocycles₂ : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  ∀ f ∈ groupCohomology.cocycles₂ (Rep.ofDistribMulAction k G A), groupCohomology.IsCocycle₂ f
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsNontrivial.mk : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀},
  (∃ x, v x ≠ 0 ∧ v x ≠ 1) → v.IsNontrivial
-- Mathlib.GroupTheory.Coxeter.Length
/-- The proposition that `i` is a left descent of `w`; that is, $\ell(s_i w) < \ell(w)$.  -/
CoxeterSystem.IsLeftDescent : {B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → W → B → Prop
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.ExactAt.of_isZero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {i : ι},
  CategoryTheory.Limits.IsZero (K.X i) → K.ExactAt i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₂ → (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_lt_mul : ∀ {a b c d : ENNReal}, a < c → b < d → a * b < c * d
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.evalEval_polynomial_zero : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R}, Polynomial.evalEval 0 0 W.polynomial = -W.a₆
-- Mathlib.Analysis.Convex.Side
/-- The points `x` and `y` are strictly on the same side of `s`.  -/
AffineSubspace.SSameSide : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : PartialOrder R] →
          [IsStrictOrderedRing R] →
            [inst_3 : AddCommGroup V] →
              [inst_4 : Module R V] → [inst_5 : AddTorsor V P] → AffineSubspace R P → P → P → Prop
-- Mathlib.Order.OrderDual
/-- `toDual` is the identity function to the `OrderDual` of a linear order.  -/
OrderDual.toDual : {α : Type u_1} → α ≃ αᵒᵈ
-- Mathlib.Topology.Constructions.SumProd
IsOpenMap.sumMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace W] [inst_3 : TopologicalSpace Z] {f : X → Y} {g : Z → W},
  IsOpenMap f → IsOpenMap g → IsOpenMap (Sum.map f g)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.forall_mem_single : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {x : ι → ℝ} (p : (ι → ℝ) → BoxIntegral.Box ι → Prop) (hJ : J ≤ I)
  (h : x ∈ BoxIntegral.Box.Icc I),
  (∀ J' ∈ BoxIntegral.TaggedPrepartition.single I J hJ x h,
      p ((BoxIntegral.TaggedPrepartition.single I J hJ x h).tag J') J') ↔
    p x J
-- Init.Prelude
/-- Applies a function to each element of the list, returning the resulting list of values.

`O(|l|)`.

Examples:
* `[a, b, c].map f = [f a, f b, f c]`
* `[].map Nat.succ = []`
* `["one", "two", "three"].map (·.length) = [3, 3, 5]`
* `["one", "two", "three"].map (·.reverse) = ["eno", "owt", "eerht"]`
 -/
List.map : {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.isoOfIsoLift_inv_hom_id : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [inst_2 : p.IsHomLift f φ.hom],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsHomLift.isoOfIsoLift p f φ).inv f =
    CategoryTheory.CategoryStruct.id S
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_algebraMap : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  (r : R), D ((algebraMap R A) r) = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.maxKeyD fallback ∈ t
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.instQuasiSeparatedToNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.QuasiSeparated (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Mathlib.Data.Subtype
Subtype.coe_ne_coe : ∀ {α : Sort u_1} {p : α → Prop} {a b : Subtype p}, ↑a ≠ ↑b ↔ a ≠ b
-- Aesop.Tracing
Aesop.«doElemAesop_trace[_]__» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.lift_comp_map : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8}
  {M₂ : Type u_12} {N₂ : Type u_14} {P₃ : Type u_18} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid N₂] [inst_7 : AddCommMonoid P₃] [inst_8 : Module R M]
  [inst_9 : Module R N] [inst_10 : Module R₂ M₂] [inst_11 : Module R₂ N₂] [inst_12 : Module R₃ P₃]
  [inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (i : M₂ →ₛₗ[σ₂₃] N₂ →ₛₗ[σ₂₃] P₃) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂),
  TensorProduct.lift i ∘ₛₗ TensorProduct.map f g = TensorProduct.lift ((i ∘ₛₗ f).compl₂ g)
-- Mathlib.Analysis.Normed.Group.Basic
dist_eq_norm_neg_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), dist a b = ‖-a + b‖
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.unique : ∀ {α : Type u} (f : Ultrafilter α) {g : Filter α}, g ≤ ↑f → autoParam g.NeBot Ultrafilter.unique._auto_1 → g = ↑f
-- Mathlib.Order.Closure
ClosureOperator.ofCompletePred_apply : ∀ {α : Type u_1} [inst : CompleteLattice α] (p : α → Prop) (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) (a : α),
  (ClosureOperator.ofCompletePred p hsinf) a = ⨅ b, ↑b
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.union : ∀ {α : Type u_2} {𝒜 : Set (Set α)} (s t : Set α),
  MeasureTheory.generateSetAlgebra 𝒜 s →
    MeasureTheory.generateSetAlgebra 𝒜 t → MeasureTheory.generateSetAlgebra 𝒜 (s ∪ t)
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmoothOfRelativeDimension.out : ∀ {n : ℕ} {R : Type u} {S : Type v} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.IsStandardSmoothOfRelativeDimension n R S],
  ∃ ι σ, ∃ (x : Finite σ) (_ : Finite ι), ∃ P, P.dimension = n
-- Mathlib.Tactic.Subsingleton
/-- Main loop for `addSubsingletonInsts`.  -/
_private.Mathlib.Tactic.Subsingleton.0.Mathlib.Tactic.elabSubsingletonInsts.go : List Lean.Term →
  Array (Lean.Term × Lean.Meta.AbstractMVarsResult) →
    Lean.Elab.TermElabM (Array (Lean.Term × Lean.Meta.AbstractMVarsResult))
-- Lean.Meta.Closure
Lean.Meta.Closure.collectLevelAux : Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_right_unitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
    CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b).hom)
        (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom)
-- Mathlib.RingTheory.Idempotents
_private.Mathlib.RingTheory.Idempotents.0.RingHom.prod_bijective_of_isIdempotentElem.match_1_1.splitter : (motive : Fin 2 → Sort u_1) → (i : Fin 2) → (Unit → motive 0) → (Unit → motive 1) → motive i
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeft_obj_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeft R l hl).obj X).right = X.right
-- Mathlib.Algebra.Homology.Single
/-- Morphisms from an `ℕ`-indexed chain complex `C`
to a single object chain complex with `X` concentrated in degree 0
are the same as morphisms `f : C.X 0 ⟶ X` such that `C.d 1 0 ≫ f = 0`.
 -/
ChainComplex.toSingle₀Equiv : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        (C : ChainComplex V ℕ) →
          (X : V) → (C ⟶ (ChainComplex.single₀ V).obj X) ≃ { f // CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0 }
-- Mathlib.Algebra.Field.Basic
OrderDual.instNNRatCast : {K : Type u_1} → [NNRatCast K] → NNRatCast Kᵒᵈ
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.instSmallPrecoverage : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.precoverage P).Small
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.sign_of_cycleType_eq_replicate : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {n : ℕ},
  0 < n →
    σ.cycleType = Multiset.replicate σ.cycleType.card n →
      Equiv.Perm.sign σ = if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)
-- Init.SimpLemmas
eq_false : ∀ {p : Prop}, ¬p → p = False
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeft_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (X x x_1 : CategoryTheory.Arrow C) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f =
    (CategoryTheory.MonoidalCategory.Arrow.pushoutProduct.obj X).map f
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpCacheKey.args : Lean.Elab.Tactic.Grind.DSimpCacheKey → Lean.Elab.Tactic.Grind.DSimpArgs
-- Init.Data.Order.Ord
Std.TransCmp.gt_of_gt_of_isGE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.gt → (cmp b c).isGE = true → cmp a c = Ordering.gt
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.const_obj_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.CosimplicialObject.Augmented.const.obj X).right = (CategoryTheory.CosimplicialObject.const C).obj X
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.instChartedSpaceM : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_4} →
        {H : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] →
                  {I : ModelWithCorners ℝ E H} → {s : SingularManifold X k I} → ChartedSpace H s.M
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- Constructor for `Equivalence.IsTriangulated`.  -/
CategoryTheory.Equivalence.IsTriangulated.mk' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (E : C ≌ D) [inst_12 : E.functor.CommShift ℤ]
  [inst_13 : E.inverse.CommShift ℤ] [E.CommShift ℤ], E.functor.IsTriangulated → E.IsTriangulated
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1AddEquivOfIsTrivial_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial]
  (a : ↑(groupHomology.H1 A)), (groupHomology.H1AddEquivOfIsTrivial A) a = (groupHomology.H1ToTensorOfIsTrivial A) a
-- Mathlib.Order.Hom.Basic
OrderHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] (f : γ →o δ) (g : β →o γ) (h : α →o β),
  (f.comp g).comp h = f.comp (g.comp h)