mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            h)
  (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β)
  (x_2 : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false),
  x = Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r →
    x_1 ≍ x_2 →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
        | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
          h_3 => h_2 size k v l size_1 k_1 v_1 l_1 r h r_1 h_3) ≍
        h_1 size k v r x_2
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.map_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D), P.isoClosure.map F = P.map F
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprExpr_mathlib.toExpr : Lean.Expr → Lean.Expr
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.lift_apply_apply : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] (b : FreeAddGroupBasis ι G)
  (a : ι → H) (x : G), (b.lift a) x = (FreeAddGroup.lift a) (b.repr x)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ), MeasureTheory.IsStoppingTime f π → MeasurableSet {ω | τ ω ≤ π ω}
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_eq_some_getValueCast! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  [inst_2 : Inhabited (β a)],
  Std.Internal.List.containsKey a l = true →
    Std.Internal.List.getValueCast? a l = some (Std.Internal.List.getValueCast! a l)
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.fold.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.node c l v r with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v r => h_2 c l v r) =
    h_2 c l v r
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_iff_le_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b c : α}, a - c ≤ b ↔ a ≤ b + c
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toNonempty : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : TopologicalSpace.NonemptyCompacts α}, Nonempty ↥s
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_arrow_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F]
  (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobjectIso f).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow) x
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.rawIdentNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Server.AsyncList
Lean.AsyncList.delayed.injEq : ∀ {ε : Type u} {α : Type v} (tl tl_1 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))),
  (Lean.AsyncList.delayed tl = Lean.AsyncList.delayed tl_1) = (tl = tl_1)
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.divX 0 = 0
-- Init.Control.Lawful.Instances
StateT.run_control : ∀ {m : Type u → Type u_1} {σ α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m (stM m (StateT σ m) α)) (s : σ),
  (control f).run s = f fun {β} x => x.run s
-- Mathlib.Algebra.Group.Action.Opposite
AddOpposite.instVAddAssocClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M N] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddAssocClass M N α], VAddAssocClass M N αᵃᵒᵖ
-- Mathlib.CategoryTheory.Pi.Basic
/-- Two functors to a product category are equal iff they agree on every coordinate.  -/
CategoryTheory.Functor.pi_ext : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (f f' : CategoryTheory.Functor A ((i : I) → C i)),
  (∀ (i : I), f.comp (CategoryTheory.Pi.eval C i) = f'.comp (CategoryTheory.Pi.eval C i)) → f = f'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- A point on an elliptic curve `W` over `R`.  -/
WeierstrassCurve.Affine.Point.mk : {R : Type r} →
  [inst : CommRing R] →
    {W' : WeierstrassCurve.Affine R} →
      [Nontrivial R] → [WeierstrassCurve.IsElliptic W'] → {x y : R} → W'.Equation x y → W'.Point
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
_private.Init.Data.Float.Model.Unpacked.Pack.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.eq_3 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (s : Float.Model.UnpackedFloat.Sign)
  (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)),
  (match Float.Model.UnpackedFloat.zero s with
    | Float.Model.UnpackedFloat.notANumber => h_1 ()
    | Float.Model.UnpackedFloat.infinity s => h_2 s
    | Float.Model.UnpackedFloat.zero s => h_3 s
    | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) =
    h_3 s
-- Init.Data.String.Defs
/-- Returns a slice that contains the entire string.
 -/
String.toSlice : String → String.Slice
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.instIsSupportedOfIsStrictlySupported : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [K.IsStrictlySupported e], K.IsSupported e
-- Mathlib.Order.BoundedOrder.Basic
/-- **Alias** of `ne_bot_of_gt`. -/
LT.lt.ne_bot : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a b : α}, b < a → a ≠ ⊥
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.mvarId : Lean.Meta.SimpAll.State → Lean.MVarId
-- Mathlib.LinearAlgebra.Dimension.Finite
Set.finrank.eq_1 : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  Set.finrank R s = Module.finrank R ↥(Submodule.span R s)
-- Mathlib.Analysis.Complex.Basic
Complex.hasSum_re : ∀ {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ}, HasSum f x L → HasSum (fun x => (f x).re) x.re L
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instZeroHom : (X Y : AddMonCat) → Zero (X ⟶ Y)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.divLeft.eq_1 : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (x : G),
  Homeomorph.divLeft x = { toEquiv := Equiv.divLeft x, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.instUnitizationNormedAlgebra : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] → [inst_4 : SMulCommClass 𝕜 A A] → NormedAlgebra 𝕜 (WithLp 1 (Unitization 𝕜 A))
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
/-- A variant of `ContinuousMapZero.hasFiniteIntegral_mkD_of_bound` for a family of
functions which are continuous on a compact set.  -/
ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] {s : Set Y} [inst_3 : CompactSpace ↑s] [inst_4 : Zero ↑s]
  (f : X → Y → E) (g : ContinuousMapZero (↑s) E),
  (∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s) →
    (∀ᵐ (x : X) ∂μ, f x ↑0 = 0) →
      ∀ (bound : X → ℝ),
        MeasureTheory.HasFiniteIntegral bound μ →
          (∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x) →
            MeasureTheory.HasFiniteIntegral (fun x => ContinuousMapZero.mkD (s.domRestrict (f x)) g) μ
-- Mathlib.GroupTheory.OrderOfElement
/-- Every finite right cancellative additive monoid is an additive group.  -/
AddRightCancelMonoid.addGroupOfFinite : {H : Type u_6} → [AddRightCancelMonoid H] → [Finite H] → AddGroup H
-- Mathlib.Analysis.Normed.Group.Ultra
/-- All triangles are isosceles in an ultrametric normed group.  -/
IsUltrametricDist.norm_div_eq_max_of_norm_div_ne_norm_div : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] (x y z : S),
  ‖x / y‖ ≠ ‖y / z‖ → ‖x / z‖ = max ‖x / y‖ ‖y / z‖
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.var.sizeOf_spec : ∀ (a : ℕ), sizeOf (Mathlib.Tactic.ITauto.IProp.var a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.instIsMultiplicativePathsPaths : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C),
  W.paths.IsMultiplicative
-- Mathlib.Condensed.Basic
Condensed.comp_hom : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] {X Y Z : Condensed C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
/-- Hölder's inequality, as an inequality on the `ℒp` seminorm of a scalar product `φ • f`.  -/
MeasureTheory.eLpNorm_smul_le_mul_eLpNorm : ∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E]
  {p q r : ENNReal} {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {φ : α → 𝕜},
      MeasureTheory.AEStronglyMeasurable φ μ →
        ∀ [hpqr : p.HolderTriple q r],
          MeasureTheory.eLpNorm (φ • f) r μ ≤ MeasureTheory.eLpNorm φ p μ * MeasureTheory.eLpNorm f q μ
-- Aesop.RuleTac.Basic
Aesop.instInhabitedRuleTacOutput : Inhabited Aesop.RuleTacOutput
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.mapPower_powerMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V)
  {α β : Type t} [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C]
  [inst_2 : CategoryTheory.Limits.HasProductsOfShape β C] (g : α → β),
  CategoryTheory.CategoryStruct.comp (U.mapPower g) (CategoryTheory.Limits.FormalCoproduct.powerMap f α) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f β) (V.mapPower g)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_7 : ∀ {C : Type u} (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv x) =
    id (CategoryTheory.Discrete.natTrans fun x_1 => CategoryTheory.CategoryStruct.id (x.normalizeObj'.obj x_1))
-- Init.Data.String.Lemmas.Order
String.Pos.sliceFrom_lt_sliceFrom_iff : ∀ {s : String} {p₀ q r : s.Pos} {h₁ : p₀ ≤ q} {h₂ : p₀ ≤ r}, p₀.sliceFrom q h₁ < p₀.sliceFrom r h₂ ↔ q < r
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.isOrtho_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} {x y : M}, B.IsOrtho x y ↔ (B x) y = 0
-- Init.Data.SInt.Lemmas
ISize.toInt8_toInt64 : ∀ (n : ISize), n.toInt64.toInt8 = n.toInt8
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termι'_1 : Lean.ParserDescr
-- Mathlib.Data.Finmap
Finmap.lookup_eq_some_iff : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s : Finmap β} {a : α} {b : β a},
  Finmap.lookup a s = some b ↔ ⟨a, b⟩ ∈ s.entries
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algHom_ext : ∀ {R : Type u} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Algebra R B]
  {f g : Polynomial R →ₐ[R] B}, f Polynomial.X = g Polynomial.X → f = g
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.e_comp_id : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eId V Y))
        (CategoryTheory.eComp V X Y Y)) =
    CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_le_add_mk_of_archimedean : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) (x : R) (y : S),
  ArchimedeanClass.mk x ≤ ArchimedeanClass.mk x + ArchimedeanClass.mk (f y)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.symm : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M}, a ≡ b [PMOD p] → b ≡ a [PMOD p]
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.isDiscrete : ∀ (C : Type u_1), CategoryTheory.IsDiscrete (CategoryTheory.Discrete C)
-- Init.Data.Iterators.Basic
Std.Shrink.inflate_inj : ∀ {α : Type u_1} {x y : Std.Shrink α}, x.inflate = y.inflate ↔ x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The pushout of an epimorphism is an epimorphism  -/
CategoryTheory.Limits.pushout.inr_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Epi f],
  CategoryTheory.Epi (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.Algebra.Order.Positive.Ring
Positive.instDistribSubtypeLtOfNat : {R : Type u_2} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Distrib { x // 0 < x }
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minEntry?_cons : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (e : (a : α) × β a) (l : List ((a : α) × β a)),
  Std.Internal.List.minEntry? (e :: l) =
    some
      (match Std.Internal.List.minEntry? l with
      | none => e
      | some w => e ⊓ w)
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.ofArray : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Aesop.OrderedHashSet α
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal mono category is a category in which every monomorphism is normal.  -/
CategoryTheory.IsNormalMonoCategory : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Batteries.Data.List.Perm
List.Subperm.refl : ∀ {α : Type u_1} (l : List α), l.Subperm l
-- Std.Data.Internal.List.Associative
/-- Returns the smallest key in an associative list or panics if the list is empty.  -/
Std.Internal.List.minKey! : {α : Type u} → {β : α → Type v} → [Ord α] → [Inhabited α] → List ((a : α) × β a) → α
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.ciInf_mem_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι},
  (∃ x ∈ s, f x ≤ sInf ∅) → ⨅ i ∈ s, f i ∈ Finset.image f s
-- Mathlib.CategoryTheory.Action.Basic
/-- Auxiliary definition for `functorCategoryEquivalence`.  -/
Action.FunctorCategoryEquivalence.inverse : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] → CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (Action V G)
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : α → β)
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.smul_def : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : SMul M X] (c : M) (x : UniformSpace.Completion X),
  c • x = UniformSpace.Completion.map (fun x => c • x) x
-- Mathlib.Algebra.Order.Group.Ideal
/-- In a canonically ordered and well-quasi-ordered additive monoid, any semigroup
ideal is finitely generated.  -/
AddSemigroupIdeal.fg_of_wellQuasiOrderedLE : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedAdd M]
  (I : AddSemigroupIdeal M), I.FG
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.diff_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ → (m₁ \ m₃).Equiv (m₂ \ m₃)
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
PiLp.hasStrictFDerivAt_ofLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [Finite ι] (p : ENNReal)
  [Fact (1 ≤ p)] (f : PiLp p E), HasStrictFDerivAt WithLp.ofLp (↑(PiLp.continuousLinearEquiv p 𝕜 E)) f
-- Init.Data.List.Monadic
/-- Auxiliary lemma for `mapM_eq_reverse_foldlM_cons`.  -/
List.foldlM_cons_eq_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} {as : List α}
  {b : β} {bs : List β},
  List.foldlM (fun acc a => (fun x => x :: acc) <$> f a) (b :: bs) as =
    (fun x => x ++ b :: bs) <$> List.foldlM (fun acc a => (fun x => x :: acc) <$> f a) [] as
-- Mathlib.Combinatorics.Matroid.Basic
_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.mem_ground_of_mem_of_subset : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α}, X ⊆ M.E → e ∈ X → e ∈ M.E
-- Std.Http.Data.Method
/-- Copy a resource to a new URI.
Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.8
 -/
Std.Http.Method.copy : Std.Http.Method
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Hover.range? : Lean.Lsp.Hover → Option Lean.Lsp.Range
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.sizeOf_spec : sizeOf Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned = 1
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_inv_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.valid_pack : ∀ {spec : Float.Model.Format} {f : Float.Model.UnpackedFloat}, spec.Valid (Float.Model.UnpackedFloat.pack spec f)
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.epi_homologyMap_shortComplexTruncLE_g : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE] (i' : ι'),
  CategoryTheory.Epi (HomologicalComplex.homologyMap (K.shortComplexTruncLE e).g i')
-- Mathlib.Topology.Category.Profinite.Extend
/-- If the projection maps in the cone are epimorphic and the cone is limiting, then
`Profinite.Extend.functor` is initial.

TODO: investigate how to weaken the assumption `∀ i, Epi (c.π.app i)` to
`∀ i, ∃ j (_ : j ⟶ i), Epi (c.π.app j)`.
 -/
Profinite.Extend.functor_initial : ∀ {I : Type u} [inst : CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I]
  {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite))
  (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)],
  (Profinite.Extend.functor c).Initial
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.replaceₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.ModelTheory.Syntax
/-- `iExsUnique f φ` transforms a `L.Formula (α ⊕ β)` into a `L.Formula α` by existentially
quantifying over all variables `Sum.inr _` and asserting that the solution should be unique  -/
FirstOrder.Language.Formula.iExsUnique : {L : FirstOrder.Language} → {α : Type u'} → (β : Type v') → [Finite β] → L.Formula (α ⊕ β) → L.Formula α