mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} {l : List α} {k : α}
  {h : k ∈ m.insertManyIfNewUnit l}, (m.insertManyIfNewUnit l)[k] = ()
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.inv_comp : ∀ {M : Type u_2} {N : Type u_3} {G : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommGroup G]
  (φ : N →* G) (ψ : M →* N), φ⁻¹.comp ψ = (φ.comp ψ)⁻¹
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] (t t_1 : Std.DTreeMap α β cmp),
  t = t_1 → ∀ (a : α) [inst_1 : Inhabited (β a)], t.get! a = t_1.get! a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_eq_some_get!_of_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} [inst_3 : Inhabited (β a)], m.contains a = true → m.get? a = some (m.get! a)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_left_of_neg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightMono R]
  [AddRightReflectLE R] {a b c : R}, c < 0 → (c * a ≤ c * b ↔ b ≤ a)
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
/-- The natural isomorphism between `nerveFunctor` and `nerveFunctor₂ ⋙ Truncated.cosk 2` whose
components `nerve C ≅ (Truncated.cosk 2).obj (nerveFunctor₂.obj C)` shows that nerves of categories
are 2-coskeletal.  -/
CategoryTheory.Nerve.cosk₂Iso : CategoryTheory.nerveFunctor ≅ CategoryTheory.Nerve.nerveFunctor₂.comp (SSet.Truncated.cosk 2)
-- Init.Data.String.Lemmas.Iterate
String.toList_revChars : ∀ {s : String}, s.revChars.toList = s.toList.reverse
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.IsPullback.map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {sq : CategoryTheory.Square C},
  sq.IsPullback →
    ∀ (F : CategoryTheory.Functor C D)
      [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F], (sq.map F).IsPullback
-- Mathlib.RingTheory.Localization.FractionRing
/-- An algebra isomorphism of rings induces an algebra isomorphism of fraction fields.  -/
IsFractionRing.fieldEquivOfAlgEquiv : {A : Type u_8} →
  {B : Type u_9} →
    {C : Type u_10} →
      [inst : CommRing A] →
        [inst_1 : CommRing B] →
          [inst_2 : CommRing C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra A C] →
                (FA : Type u_12) →
                  (FB : Type u_13) →
                    (FC : Type u_14) →
                      [inst_5 : Field FA] →
                        [inst_6 : Field FB] →
                          [inst_7 : Field FC] →
                            [inst_8 : Algebra A FA] →
                              [inst_9 : Algebra B FB] →
                                [inst_10 : Algebra C FC] →
                                  [IsFractionRing A FA] →
                                    [IsFractionRing B FB] →
                                      [IsFractionRing C FC] →
                                        [inst_14 : Algebra A FB] →
                                          [IsScalarTower A B FB] →
                                            [inst_16 : Algebra A FC] →
                                              [IsScalarTower A C FC] →
                                                [inst_18 : Algebra FA FB] →
                                                  [IsScalarTower A FA FB] →
                                                    [inst_20 : Algebra FA FC] →
                                                      [IsScalarTower A FA FC] → (B ≃ₐ[A] C) → FB ≃ₐ[FA] FC
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.Q.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ),
  AlgebraicTopology.DoldKan.Q q =
    CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X) - AlgebraicTopology.DoldKan.P q
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y`. (See
`Orientation.inner_mul_areaForm_sub` for the "applied" form.)  -/
Orientation.inner_mul_areaForm_sub' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (a x : E),
  inner ℝ a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_add : ∀ {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] (m₁ m₂ : M) (s : ↥S),
  IsLocalizedModule.mk' f (m₁ + m₂) s = IsLocalizedModule.mk' f m₁ s + IsLocalizedModule.mk' f m₂ s
-- Init.Data.List.Int.Prod
List.prod_reverse_int : ∀ (xs : List ℤ), xs.reverse.prod = xs.prod
-- Mathlib.Algebra.Group.Pi.Basic
uniqueOfSurjectiveOne.eq_1 : ∀ (α : Type u_4) {β : Type u_5} [inst : One β] (h : Function.Surjective 1),
  uniqueOfSurjectiveOne α h = Function.Surjective.uniqueOfSurjectiveConst α 1 h
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc).left =
    CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc
-- Mathlib.RingTheory.QuasiFinite.Basic
Ideal.Fiber.lift_residueField_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal S) [inst_5 : q.IsPrime] [inst_6 : q.LiesOver p]
  [Algebra.QuasiFiniteAt R q] [inst_8 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_9 : Localization.AtPrime.IsLiesOverAlgebra p q],
  Function.Surjective
    ⇑(Algebra.TensorProduct.lift (Algebra.ofId p.ResidueField q.ResidueField)
        (IsScalarTower.toAlgHom R S q.ResidueField) ⋯)
-- Init.Data.Array.Lemmas
Array.map_id : ∀ {α : Type u_1} (xs : Array α), Array.map id xs = xs
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.not_noRepetition_append_of_right : ∀ {α : Type u} {a : α} {l m : List α}, ¬NoRepetition✝ a m → ¬NoRepetition✝ a (l ++ m)
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanIleanInfoParams.mk.inj : ∀ {version : ℕ} {references : Lean.Lsp.ModuleRefs} {decls : Lean.Lsp.Decls} {version_1 : ℕ}
  {references_1 : Lean.Lsp.ModuleRefs} {decls_1 : Lean.Lsp.Decls},
  { version := version, references := references, decls := decls } =
      { version := version_1, references := references_1, decls := decls_1 } →
    version = version_1 ∧ references = references_1 ∧ decls = decls_1
-- Mathlib.CategoryTheory.Limits.Types.Filtered
CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [CategoryTheory.IsFilteredOrEmpty J] [inst_2 : CategoryTheory.Limits.HasColimit F] {i j : J} {xi : F.obj i}
  {xj : F.obj j},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i)) xi =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) xj ↔
    ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
-- Mathlib.Data.Fintype.Order
Finite.map_iSup_of_monotoneOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β},
  MonotoneOn g s → (∀ (i : ι), f i ∈ s) → g (⨆ i, f i) = ⨆ i, g (f i)
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ici_disjoint_Iic : ∀ {α : Type v} [inst : Preorder α] {a b : α}, Disjoint (Set.Ici a) (Set.Iic b) ↔ ¬a ≤ b
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The maximal reduction of a word. It is computable
iff `α` has decidable equality.  -/
FreeGroup.reduce : {α : Type u_1} → [DecidableEq α] → List (α × Bool) → List (α × Bool)
-- Mathlib.Data.Finset.Lattice.Prod
Finset.sup_prodMap : ∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  [inst_2 : OrderBot α] [inst_3 : OrderBot β] {s : Finset ι} {t : Finset κ},
  s.Nonempty → t.Nonempty → ∀ (f : ι → α) (g : κ → β), (s ×ˢ t).sup (Prod.map f g) = (s.sup f, t.sup g)
-- Mathlib.Topology.Algebra.Group.Basic
discreteTopology_of_isOpen_singleton_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G],
  IsOpen {0} → DiscreteTopology G
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.closure_univ : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], NonUnitalSubring.closure Set.univ = ⊤
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
CategoryTheory.LocalizerMorphism.instIsIsoFunctorRightDerivedFunctorComparison : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₁ : Type u₄}
  {D₂ : Type u₅} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂] (F : CategoryTheory.Functor C₂ H)
  (F₁ : CategoryTheory.Functor D₁ H) (α₁ : Φ.functor.comp F ⟶ L₁.comp F₁) (F₂ : CategoryTheory.Functor D₂ H)
  (α₂ : F ⟶ L₂.comp F₂) [inst_7 : F₁.IsRightDerivedFunctor α₁ W₁] [Φ.IsRightDerivabilityStructure]
  [(Φ.functor.comp F).HasPointwiseRightDerivedFunctor W₁] [F₂.IsRightDerivedFunctor α₂ W₂],
  CategoryTheory.IsIso (Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂)
-- Init.Data.List.Control
List.instForIn'InferInstanceMembershipOfMonad : {m : Type u_1 → Type u_2} → {α : Type u_3} → [Monad m] → ForIn' m (List α) α inferInstance
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.factorₐ_refl : ∀ {R : Type u_5} {A : Type u_6} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I : Ideal A),
  Ideal.Quotient.factorₐ R ⋯ = AlgHom.id R (A ⧸ I)
-- Std.Do.WP.Monad
Std.Do.ExceptT.instWPMonad : {m : Type u → Type v} →
  {ps : Std.Do.PostShape} →
    {ε : Type u} →
      [inst : Monad m] → [Std.Do.WPMonad m ps] → Std.Do.WPMonad (ExceptT ε m) (Std.Do.PostShape.except ε ps)
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `wbtw_sub_const_iff`. -/
Wbtw.sub_const : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Wbtw R x y z → Wbtw R (x - v) (y - v) (z - v)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabSeqRight : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.nhds_eq_map_structureMap : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ (x : (i : ι) → ↑(A i)),
      nhds (RestrictedProduct.structureMap R A Filter.cofinite x) =
        Filter.map (RestrictedProduct.structureMap R A Filter.cofinite) (nhds x)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `F ⋙ G` preserves limits for `K`, and `G` reflects limits for `K ⋙ F`,
then `F` preserves limits for `K`.  -/
CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃}
  [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.PreservesLimit K (F.comp G)] [CategoryTheory.Limits.ReflectsLimit (K.comp F) G],
  CategoryTheory.Limits.PreservesLimit K F
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.neg_iso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (e : X ≅ Y), (-e).hom = -e.hom
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.ae_le_trim_iff : ∀ {α : Type u_1} {E : Type u_5} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : TopologicalSpace E] [inst_1 : Preorder E] [OrderClosedTopology E] [TopologicalSpace.PseudoMetrizableSpace E]
  (hm : m ≤ m₀),
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → (f ≤ᵐ[μ.trim hm] g ↔ f ≤ᵐ[μ] g)
-- Mathlib.Order.CompleteLattice.Basic
Prod.snd_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : SupSet α] [inst_1 : SupSet β] (f : ι → α × β),
  (iSup f).2 = ⨆ i, (f i).2
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.isBase_of_indep : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Spanning I → M.Indep I → M.IsBase I
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.size_updateAllBuckets : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} {self : Array (Std.DHashMap.Internal.AssocList α β)}
  {f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α δ},
  (Std.DHashMap.Internal.updateAllBuckets self f).size = self.size
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.brecOn.go : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K : CategoryTheory.Precoverage C} →
      {ι : C → Type w} →
        {motive : (a : C) → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι a → Sort u_1} →
          {a : C} →
            (t : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι a) →
              ((a : C) →
                  (t : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι a) →
                    CategoryTheory.Precoverage.SmallConstruction.Witness.below✝ t → motive a t) →
                motive a t ×' CategoryTheory.Precoverage.SmallConstruction.Witness.below✝ t
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β} {h : k' ∈ m.modify k f},
  (m.modify k f)[k'] = if heq : (k == k') = true then f m[k] else m[k']
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.Balanced) (x_2 : ℕ) (x_3 : x_2 < x.size),
  x.entryAtIdx x_1 x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | Std.DTreeMap.Internal.Impl.inner size k v l' r', hl, n, h =>
      match h_1 : compare n l'.size with
      | Ordering.lt => l'.entryAtIdx ⋯ n ⋯
      | Ordering.eq => ⟨k, v⟩
      | Ordering.gt => r'.entryAtIdx ⋯ (n - l'.size - 1) ⋯
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_unit : Ordinal.type emptyRelation = 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_11.eq_1 : ∀ (w : ℕ) (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (motive : Std.Tactic.BVDecide.BVExpr.Return aig w → Sort u_1)
  (aig_1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (rhs : aig_1.RefVec w)
  (hraig : aig.decls.size ≤ { aig := aig_1, vec := rhs }.aig.decls.size)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_1, vec := rhs }, hraig⟩).aig)
  (h_1 :
    (aig_2 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
      (rhs : aig_2.RefVec w) →
        (hraig : aig.decls.size ≤ { aig := aig_2, vec := rhs }.aig.decls.size) →
          (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_2, vec := rhs }, hraig⟩).aig) →
            motive { result := ⟨{ aig := aig_2, vec := rhs }, hraig⟩, cache := cache }),
  (match { result := ⟨{ aig := aig_1, vec := rhs }, hraig⟩, cache := cache } with
    | { result := ⟨{ aig := aig_2, vec := rhs }, hraig⟩, cache := cache } => h_1 aig_2 rhs hraig cache) =
    h_1 aig_1 rhs hraig cache
-- Aesop.Search.SearchM
Aesop.SearchM.Context.mk.injEq : ∀ (ruleSet : Aesop.LocalRuleSet) (normSimpContext : Aesop.NormSimpContext) (options : Aesop.Options')
  (ruleSet_1 : Aesop.LocalRuleSet) (normSimpContext_1 : Aesop.NormSimpContext) (options_1 : Aesop.Options'),
  ({ ruleSet := ruleSet, normSimpContext := normSimpContext, options := options } =
      { ruleSet := ruleSet_1, normSimpContext := normSimpContext_1, options := options_1 }) =
    (ruleSet = ruleSet_1 ∧ normSimpContext = normSimpContext_1 ∧ options = options_1)
-- Mathlib.Data.Num.ZNum
Num.toZNumNeg_succ : ∀ (n : Num), n.succ.toZNumNeg = n.toZNumNeg.pred
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasPluralDefaults.mk : {α : Sort u_1} → α → (α → α) → Lean.HasPluralDefaults✝ α
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.set_range_inclusion' : ∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X), Set.range ⇑(CategoryTheory.ConcreteCategory.hom U.inclusion') = ↑U
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
/-- The rank of a morphism `f : X ⟶ S` of schemes at a point `s : S`, when `S` is affine.
This is used as an auxiliary definition to define `AlgebraicGeometry.finrank`.  -/
_private.Mathlib.AlgebraicGeometry.Morphisms.FlatRank.0.AlgebraicGeometry.IsAffine.finrank : {X S : AlgebraicGeometry.Scheme} → [AlgebraicGeometry.IsAffine S] → (X ⟶ S) → ↥S → ℕ
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.toLpLinAlgEquiv_apply_apply_ofLp : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] (p : ENNReal)
  (a : Matrix n n R) (x : WithLp p (n → R)) (a_1 : n), (((Matrix.toLpLinAlgEquiv p) a) x).ofLp a_1 = a.mulVec x.ofLp a_1
-- Mathlib.Tactic.NormNum.Core
/-- Elaborator for `norm_num` conv tactic.  -/
Mathlib.Tactic.elabNormNumConv : Lean.Elab.Tactic.Tactic
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.weak_invMulSubgroup_bound : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G},
  ↑(A * A).card < 3 / 2 * ↑A.card → (A⁻¹ * A).card < 2 * A.card
-- Std.Time.Format
/-- Converts a date in the Lean format (`uuuu-MM-dd`) into a `String`.
 -/
Std.Time.PlainDate.toLeanDateString : Std.Time.PlainDate → String
-- Mathlib.Data.Set.Card.Arithmetic
Set.ncard_iUnion_of_finite : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] {s : ι → Set α},
  (∀ (i : ι), (s i).Finite) → Pairwise (Function.onFun Disjoint s) → (⋃ i, s i).ncard = ∑ᶠ (i : ι), (s i).ncard
-- Init.Data.UInt.Lemmas
UInt64.add_right_neg : ∀ (a : UInt64), a + -a = 0
-- Aesop.Forward.Match
/-- Convert forward rule matches to unsafe rules. Fails if any of the matches
is not an unsafe rule match.  -/
Aesop.forwardRuleMatchesToUnsafeRules? : Array Aesop.ForwardRuleMatch → Option (Array Aesop.UnsafeRule)
-- Mathlib.Tactic.Simproc.FinsetInterval
/-- Simproc to compute `Finset.Iic b` where `b` is a numeral.

**Warnings**:
* With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
* Make sure to exclude `Finset.insert_eq_of_mem` from your simp call when using this simproc. This
  avoids a quadratic time performance hit.  -/
Finset.Iic_ofNat : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_singleton`.

---

The extended diameter of a singleton vanishes  -/
EMetric.diam_singleton : ∀ {X : Type u_2} {x : X} [inst : PseudoEMetricSpace X], Metric.ediam {x} = 0
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.comp_isLocallySurjective_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
  [CategoryTheory.Presheaf.IsLocallySurjective J f₁],
  CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂) ↔
    CategoryTheory.Presheaf.IsLocallySurjective J f₂
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticTag.beq : Lean.Lsp.DiagnosticTag → Lean.Lsp.DiagnosticTag → Bool
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.neg_udiv_eq_intMin_iff_eq_intMin_eq_one_of_msb_eq_true : ∀ {w : ℕ} {x y : BitVec w}, x.msb = true → y.msb = false → (-x / y = BitVec.intMin w ↔ x = BitVec.intMin w ∧ y = 1#w)
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.addNamespace : Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Order.Sublocale
Sublocale.toNucleus_apply : ∀ {X : Type u_1} [inst : Order.Frame X] (S : Sublocale X) (x : X), S.toNucleus x = ↑(S.restrict x)
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_bind : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {a b : α} {P : Finpartition a} {Q : (i : α) → i ∈ P.parts → Finpartition i},
  b ∈ (P.bind Q).parts ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts
-- Lean.Parser.Syntax
Lean.Parser.Command.namedName.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.MvPolynomial.Derivation
/-- The derivation on `MvPolynomial σ R` that takes value `f i` on `X i`, as a linear map.
Use `MvPolynomial.mkDerivation` instead.  -/
MvPolynomial.mkDerivationₗ : {σ : Type u_1} →
  (R : Type u_2) →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] → [Module (MvPolynomial σ R) A] → (σ → A) → MvPolynomial σ R →ₗ[R] A
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconePrecompose.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : G ⟶ F} {c : CategoryTheory.Limits.Cocone F},
  H.mapCoconePrecompose =
    CategoryTheory.Limits.Cocone.extInv
      (CategoryTheory.Iso.refl (H.mapCocone ((CategoryTheory.Limits.Cocone.precompose α).obj c)).pt) ⋯
-- Mathlib.Analysis.Asymptotics.Defs
/-- Definition of `IsBigO` in terms of `IsBigOWith`. We record it in a lemma as `IsBigO` is
irreducible.  -/
Asymptotics.isBigO_iff_isBigOWith : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =O[l] g ↔ ∃ c, Asymptotics.IsBigOWith c l f g
-- Init.Data.List.Basic
/-- Erases repeated elements, using a given comparison function,
keeping the first element of each run.

`O(|l|)`.

Example:
* `[1, 3, 2, 2, 2, 3, 3, 7].eraseRepsBy (· % 4 == · % 5) = [1, 3, 2, 3]`
 -/
List.eraseRepsBy : {α : Type u_1} → (α → α → Bool) → List α → List α
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.map_pt : ∀ {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] {J : CategoryTheory.Limits.MultispanShape}
  {d : CategoryTheory.Limits.MultispanIndex J C} (c : CategoryTheory.Limits.Multicofork d)
  (F : CategoryTheory.Functor C D), (c.map F).pt = F.obj c.pt