mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertList_perm_insertSmallerList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      (Std.Internal.List.insertList l toInsert).Perm (Std.Internal.List.insertSmallerList l toInsert)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insert! : ∀ {α : Type u} {β : α → Type v} [instBEq : BEq α] [inst : Ord α] [Std.LawfulBEqOrd α] [Std.TransOrd α] {k : α} {v : β k}
  {l : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    l.Ordered →
      (Std.DTreeMap.Internal.Impl.insert! k v l).toListModel.Perm (Std.Internal.List.insertEntry k v l.toListModel)
-- Mathlib.Logic.Relation
Relation.TransGen.closed' : ∀ {α : Type u_1} {r : α → α → Prop} {P : α → Prop},
  (∀ {a b : α}, r a b → P b → P a) → ∀ {a b : α}, Relation.TransGen r a b → P b → P a
-- Init.PropLemmas
Decidable.imp_iff_right_iff : ∀ {a b : Prop} [Decidable a], (a → b ↔ b) ↔ a ∨ b
-- Mathlib.Data.Holor
Holor.cast_type : ∀ {α : Type} {ds₁ ds₂ : List ℕ} (eq : ds₁ = ds₂) (a : Holor α ds₁), cast ⋯ a = fun t => a (cast ⋯ t)
-- Mathlib.Topology.Order.LowerUpperTopology
sierpinskiSpace.eq_1 : sierpinskiSpace = TopologicalSpace.generateFrom {{True}}
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.homMk_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {a b c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c)
  [inst_2 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ]
  [inst_3 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) ψ],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Fiber.homMk p S φ)
      (CategoryTheory.Functor.Fiber.homMk p S ψ) =
    CategoryTheory.Functor.Fiber.homMk p S (CategoryTheory.CategoryStruct.comp φ ψ)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects limits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ D` reflects colimits
of shape `J`.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_of_rightOp : ∀ {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] (F : CategoryTheory.Functor Cᵒᵖ D)
  [CategoryTheory.Limits.ReflectsLimitsOfShape Jᵒᵖ F.rightOp], CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Mathlib.Topology.EMetricSpace.Weak
instEDistWithBot.eq_1 : ∀ {α : Type u} [inst : EDist α],
  instEDistWithBot =
    {
      edist := fun x x_1 =>
        match x, x_1 with
        | none, some x => ⊤
        | none, none => 0
        | some x, none => ⊤
        | some x, some y => edist x y }
-- Lean.Parser.Extra
Lean.Parser.strLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.Internal.List.Associative
Std.Internal.List.minEntry?_eq_head? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l → Std.Internal.List.minEntry? l = l.head?
-- Mathlib.Analysis.Calculus.FDeriv.Norm
HasStrictFDerivAt.hasStrictDerivAt_norm_smul_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : StrongDual ℝ E} {x : E} {t : ℝ},
  t < 0 → HasStrictFDerivAt (fun x => ‖x‖) f x → HasStrictFDerivAt (fun x => ‖x‖) (-f) (t • x)
-- Lean.Meta.AppBuilder
/-- Given `f : α → β` and `h : a = b`, returns a proof of `f a = f b`. -/
Lean.Meta.mkCongrArg : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂AssociatorInv : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
              [inst_2 : Mathlib.Tactic.BicategoryCoherence.LiftHom g] →
                [inst_3 : Mathlib.Tactic.BicategoryCoherence.LiftHom h] →
                  Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.associator f g h).inv
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- Cone morphisms from the cone corresponding to a `SieveCompatible` family to the natural
cone associated to a sieve `S` and a presheaf `P` are in 1-1 correspondence with amalgamations
of the family.  -/
CategoryTheory.Presheaf.homEquivAmalgamation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {P : CategoryTheory.Functor Cᵒᵖ A} →
          {X : C} →
            {S : CategoryTheory.Sieve X} →
              {E : Aᵒᵖ} →
                {x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows} →
                  (hx : x.SieveCompatible) → (hx.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // x.IsAmalgamation t }
-- Std.Http.Data.URI.Basic
/-- Adds a query parameter to the query string.
 -/
Std.Http.URI.Query.insert : Std.Http.URI.Query → String → String → Std.Http.URI.Query
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightMap_coweightEquiv_symm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (n : N),
  (↑e).coweightMap ((RootPairing.Equiv.coweightEquiv P Q e).symm n) = n
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.isScalarTower' : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {R₁ : Type u_5} {R₂ : Type u_6} {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
  [inst_4 : DistribMulAction R₁ R] [inst_5 : SMulCommClass R₁ R R] [inst_6 : Monoid R₂] [inst_7 : DistribMulAction R₂ R]
  [inst_8 : SMulCommClass R₂ R R] [inst_9 : SMul R₁ R₂] [IsScalarTower R₁ R₂ R],
  IsScalarTower R₁ R₂ (PiTensorProduct R fun i => s i)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_sup_edge_of_ne_iff : ∀ {α : Type u_1} {G : SimpleGraph α} {v w : α} {s : Set α},
  v ≠ w → ((G ⊔ SimpleGraph.edge v w).IsClique s ↔ G.IsClique (s \ {v}) ∧ G.IsClique (s \ {w}))
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The proof that the normalized expression is equal to the original expression.  -/
Mathlib.Tactic.BicategoryLike.Eval.Result.proof : Mathlib.Tactic.BicategoryLike.Eval.Result → Lean.Expr
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_dite_eq : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} [inst_2 : DecidableEq ι]
  (i : ι) (f : (j : ι) → i = j → M),
  (s.expect fun j => if h : i = j then f j h else 0) = if i ∈ s then (↑s.card)⁻¹ • f i ⋯ else 0
-- Mathlib.Algebra.MvPolynomial.Basic
/-- `fun s ↦ monomial s 1` as a homomorphism.  -/
MvPolynomial.monomialOneHom : (R : Type u) → (σ : Type u_1) → [inst : CommSemiring R] → Multiplicative (σ →₀ ℕ) →* MvPolynomial σ R
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- An undirected hypergraph with vertices of type `α` and edges of type `Set α`, as described by vertex
and edge sets `vertexSet : Set α` and `edgeSet : Set (Set α)`.

The requirement `subset_vertexSet_of_mem_edgeSet` ensures that all vertices in edges are part of
`vertexSet`, i.e., all edges are subsets of the `vertexSet`.
 -/
Hypergraph : Type u_4 → Type u_4
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.hom_ext_iff : ∀ {R S : RingCat} {f g : R ⟶ S}, f = g ↔ RingCat.Hom.hom f = RingCat.Hom.hom g
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.isCycle_pow_pos_of_lt_prime_order : ∀ {β : Type u_3} [Finite β] {f : Equiv.Perm β},
  f.IsCycle → Nat.Prime (orderOf f) → ∀ (n : ℕ), 0 < n → n < orderOf f → (f ^ n).IsCycle
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_nnnorm : ∀ {S' : Type u_4} [inst : SeminormedAddGroup S'], IsNonarchimedean nnnorm → IsUltrametricDist S'
-- Mathlib.Control.Traversable.Instances
Option.comp_traverse : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G] {α : Type u_1}
  {β γ : Type u} (f : β → F γ) (g : α → G β) (x : Option α),
  Option.traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) x =
    Functor.Comp.mk (Option.traverse f <$> Option.traverse g x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokens.resultId? : Lean.Lsp.SemanticTokens → Option String
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' ψ'' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  (η' : ψ' ⟶ ψ'') {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''},
  CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.CategoryStruct.comp η η') φ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ)
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η' φ)
-- Mathlib.Data.Finset.Functor
Finset.instMonad : [(P : Prop) → Decidable P] → Monad Finset
-- Init.Grind.Lemmas
Lean.Grind.Bool.not_eq_of_eq_false : ∀ {a : Bool}, a = false → (!a) = true
-- Mathlib.Topology.Algebra.Monoid.Defs
Continuous.fun_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M}, Continuous f → Continuous g → Continuous fun i => f i + g i
-- Init.Data.Vector.Range
Vector.range'.eq_1 : ∀ (start size step : ℕ), Vector.range' start size step = Vector.mk (Array.range' start size step) ⋯
-- Mathlib.MeasureTheory.Group.Measure
/-- Continuity of the measure of translates of a compact set: Given a compact set `k` in a
topological group, for `g` close enough to the origin, `μ (g • k \ k)` is arbitrarily small.  -/
MeasureTheory.eventually_nhds_one_measure_smul_sdiff_lt : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [μ.InnerRegularCompactLTTop] {k : Set G},
  IsCompact k → IsClosed k → ∀ {ε : ENNReal}, ε ≠ 0 → ∀ᶠ (g : G) in nhds 1, μ (g • k \ k) < ε
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_inverse_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T')),
  ((CategoryTheory.CostructuredArrow.mapIso i).inverse.obj X).left = X.left
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced)
  (hr_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr_2 : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size Std.DTreeMap.Internal.Impl.leaf.size),
  Std.DTreeMap.Internal.Impl.maxView k v l Std.DTreeMap.Internal.Impl.leaf hl hr_2 hlr_2 =
    { k := k, v := v, tree := { impl := l, balanced_impl := hl, size_impl := ⋯ } }
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_eq_iff_left : ∀ {α : Type u} [inst : Monoid α] {a b : α} [inst_1 : Invertible a], ⅟a = b ↔ b * a = 1
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_ne_zero : ∀ {M : Type u_4} {a : M}, WithZero.exp a ≠ 0
-- Mathlib.CategoryTheory.Skeletal
/-- The equivalence between the thin skeleton and the category itself.  -/
CategoryTheory.ThinSkeleton.equivalence : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [Quiver.IsThin C] → CategoryTheory.ThinSkeleton C ≌ C
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- A linear operator `T` on a Hilbert space is **positive** if it is symmetric and
`∀ x, 0 ≤ re ⟪T x, x⟫`.  -/
LinearMap.IsPositive : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → (E →ₗ[𝕜] E) → Prop
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {km : α}, t.max? = some km → t.get! km = km
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.originForm.inj : ∀ {path : Std.Http.URI.Path} {query : Option Std.Http.URI.Query} {path_1 : Std.Http.URI.Path}
  {query_1 : Option Std.Http.URI.Query},
  Std.Http.RequestTarget.originForm path query = Std.Http.RequestTarget.originForm path_1 query_1 →
    path = path_1 ∧ query = query_1
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularEpi.uniq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsRegularEpi f] (k : X ⟶ Z)
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.left f) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.right f) k)
  (m : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f m = k → m = CategoryTheory.IsRegularEpi.desc f k h
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Loop through all constants that appear in the modules with module index from `start` to `stop - 1`,
and add the entries generated by `act` to the `PreDiscrTree`.
 -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.createImportInitResults : {α : Type} →
  Lean.Core.Context →
    Lean.NameGenerator →
      Lean.Environment →
        (Lean.Name →
            Lean.ConstantInfo →
              Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
          ℕ → ℕ → ℕ → BaseIO (Lean.Meta.RefinedDiscrTree.InitResults✝ α)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.addHom_ext'_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {N : Type u_8} [inst_1 : AddZeroClass N]
  {f g : MonoidAlgebra R M →+ N},
  f = g ↔ ∀ (m : M), f.comp (MonoidAlgebra.singleAddHom m) = g.comp (MonoidAlgebra.singleAddHom m)
-- Mathlib.AlgebraicTopology.DoldKan.Faces
AlgebraicTopology.DoldKan.HigherFacesVanish.of_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y Z : C} {q n : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
    ∀ (f : Z ⟶ Y), AlgebraicTopology.DoldKan.HigherFacesVanish q (CategoryTheory.CategoryStruct.comp f φ)
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.ext : ∀ {ι : Type u_1} {x y : PreAbstractSimplicialComplex ι}, x.faces = y.faces → x = y
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidal : (M : Type u) → [AddMonoid M] → CategoryTheory.MonoidalCategory (CategoryTheory.Discrete M)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {P : Type u_7} [inst : NormedAddCommGroup P]
  {f : α → P}, MeasureTheory.Integrable f μ → ENNReal.ofReal (∫ (x : α), ‖f x‖ ∂μ) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.left_act_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} (self : M.Hom N),
  CategoryTheory.CategoryStruct.comp M.actLeft self.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.hom) N.actLeft
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedCodeDecl : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.CodeDecl a)
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRec'_eq : ∀ {motive : ℕ → Sort u} {zero : motive 0}
  {bit : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)} (b : Bool) (n : ℕ)
  (h : n = 0 → b = true), Nat.binaryRec' zero bit (Nat.bit b n) = bit b n h (Nat.binaryRec' zero bit n)
-- Mathlib.Analysis.Normed.Order.Lattice
Int.hasSolidNorm : HasSolidNorm ℤ
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isCodetecting_unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ),
  P.unop.IsCodetecting ↔ P.IsDetecting
-- Batteries.Data.Float.Basic
/-- The floating point value "positive infinity", also used to represent numerical computations
which produce finite values outside of the representable range of `Float`.
 -/
Float.inf : Float
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.mk : {V : Type u_1} → (V → V → Prop) → Digraph V
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.mk_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [inst_1 : Nontrivial R] {X Y : R}
  (h : W'.NonsingularLift ⟦![X, Y, 1]⟧), { point := ⟦![X, Y, 1]⟧, nonsingular := h } ≠ 0
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_le_pow_left_iff : ∀ {a b : ENNReal} {n : ℕ}, n ≠ 0 → (a ^ n ≤ b ^ n ↔ a ≤ b)
-- Mathlib.Data.EReal.Operations
EReal.sub_mul_of_nonneg_of_ne_top : ∀ {a b c : EReal}, 0 ≤ a → a ≠ ⊤ → (b - c) * a = b * a - c * a
-- Mathlib.CategoryTheory.Join.Basic
/-- An induction principle for morphisms in a join of categories: a morphism is either of the form
`(inclLeft _ _).map _`, `(inclRight _ _).map _`, or is `edge _ _`.  -/
CategoryTheory.Join.homInduction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {P : {x y : CategoryTheory.Join C D} → (x ⟶ y) → Sort u_1} →
          ((x y : C) → (f : x ⟶ y) → P ((CategoryTheory.Join.inclLeft C D).map f)) →
            ((x y : D) → (f : x ⟶ y) → P ((CategoryTheory.Join.inclRight C D).map f)) →
              ((c : C) → (d : D) → P (CategoryTheory.Join.edge c d)) →
                {x y : CategoryTheory.Join C D} → (f : x ⟶ y) → P f
-- Init.Data.SInt.Lemmas
Int16.ofNat_div : ∀ {a b : ℕ}, a < 2 ^ 15 → b < 2 ^ 15 → Int16.ofNat (a / b) = Int16.ofNat a / Int16.ofNat b
-- Init.Data.Vector.Lemmas
Vector.reverse_eq_push_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α (n + 1)} {ys : Vector α n} {a : α},
  xs.reverse = ys.push a ↔ xs = Vector.cast ⋯ (#v[a] ++ ys.reverse)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.cancel_iso_inv_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
  (g' : X' ⟶ Y) (h : Z ≅ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h.inv) =
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h.inv) ↔
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
-- Mathlib.Order.Bounds.Basic
nonempty_of_not_bddBelow : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [ha : Nonempty α], ¬BddBelow s → s.Nonempty
-- Mathlib.NumberTheory.NumberField.ExistsRamified
/-- If `K` is a number field with positive rank, then some prime is ramified in `K`.  -/
NumberField.exists_not_isUnramifiedIn : ∀ {K : Type u_1} {𝒪 : Type u_2} [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsIntegralClosure 𝒪 ℤ K], Module.finrank ℚ K ≠ 1 → ∃ p, Nat.Prime p ∧ ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, k ∈ m₂ → (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f g : β → α},
  s₁ = s₂ → (∀ a ∈ s₂, f a = g a) → s₁.sup f = s₂.sup g
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.map_rev_map_op_apply : ∀ {n d d' : ℕ} (f : { len := d } ⟶ { len := d' })
  (g : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d' })) (i : Fin (d + 1)),
  ((CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplex.obj { len := n }).map (SimplexCategory.rev.map f).op)) g) i =
    g ((CategoryTheory.ConcreteCategory.hom f) i.rev).rev
-- Mathlib.Order.TypeTags
WithTop.top.eq_1 : ∀ {α : Type u_1}, WithTop.top = { top := none }
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.ex.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)), φ.ex = φ.not.all.not
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C) (T : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj T
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.LaxMonoidal.μ F X Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)) h) =
    h
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.Boundary.fst : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} {ac : e₁.AreComplementary e₂} {i₁ : ι₁} {i₂ : ι₂},
  ac.Boundary i₁ i₂ → e₁.BoundaryLE i₁
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.tendsto_meas_vadd_symmDiff_vadd : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X}
  [MeasureTheory.VAddInvariantMeasure G X μ],
  IsAddFoelner G μ (↑u) F →
    ∀ (g h : G), Filter.Tendsto (fun i => μ (symmDiff (g +ᵥ F i) (h +ᵥ F i)) / μ (F i)) (↑u) (nhds 0)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.lift_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂),
  (CategoryTheory.Quotient.functor r).comp (CategoryTheory.Quotient.lift r F H) = F
-- Aesop.Tree.Data
Aesop.TreeSpec.introMVarCluster : (self : Aesop.TreeSpec) → Aesop.MVarClusterData self.Goal self.Rapp → self.MVarCluster
-- Mathlib.CategoryTheory.Sites.Sieves
/-- If the identity arrow is in a sieve, the sieve is maximal.  -/
CategoryTheory.Sieve.id_mem_iff_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X},
  S.arrows (CategoryTheory.CategoryStruct.id X) ↔ S = ⊤