mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable.  -/
ConditionallyCompleteLinearOrder.toDecidableEq : {α : Type u_5} → [self : ConditionallyCompleteLinearOrder α] → DecidableEq α
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_congr : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f g : α → β}, f =ᵐ[μ] g → MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g μ
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
/-- The Cech construction for `FormalCoproduct` is isomorphic
to the general `Arrow.augmentedCechNerve` construction applied to the morphism
to the terminal object.  -/
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      (U : CategoryTheory.Limits.FormalCoproduct C) →
        {T : C} →
          (hT : CategoryTheory.Limits.IsTerminal T) →
            U.cech.augmentOfIsTerminal (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT) ≅
              (CategoryTheory.Arrow.mk
                  ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).augmentedCechNerve
-- Mathlib.SetTheory.Cardinal.Aleph
Order.cof_cardinal : Order.cof Cardinal.{u} = Cardinal.univ.{u, u + 1}
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.eq_def : ∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (acc : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn assignments acc l =
    match acc with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth =>
      Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty =>
      match assignments[↑l.1]! with
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos =>
        if l.2 = true then Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l
        else Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg =>
        if (!l.2) = true then Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l
        else Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both =>
        Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned =>
        Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l' =>
      match assignments[↑l.1]! with
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos =>
        if l.2 = true then Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit
        else Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l'
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg =>
        if (!l.2) = true then Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit
        else Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l'
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both =>
        Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned =>
        Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit =>
      Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit
-- Batteries.CodeAction.Misc
/-- Returns all of the arguments given a type. The second argument of this
function is an accumulator.  -/
Batteries.CodeAction.getAllArgs : Lean.Expr → Array Lean.Name → Array Lean.Name
-- Mathlib.Algebra.Algebra.Defs
/-- An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`.

See the implementation notes in this file for discussion of the details of this definition.
 -/
Algebra : (R : Type u) → (A : Type v) → [CommSemiring R] → [Semiring A] → Type (max u v)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_lt_ulift : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.lift.{v, u} (Ordinal.type fun x1 x2 => x1 < x2)
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.hasCardinalLT_arrow_op_iff : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}),
  HasCardinalLT (CategoryTheory.Arrow Cᵒᵖ) κ ↔ HasCardinalLT (CategoryTheory.Arrow C) κ
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Expect.inst : Std.Http.Header Std.Http.Header.Expect
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_union_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α} (contains_right : m₂.contains k = true),
  (m₁.union m₂).get k ⋯ = m₂.get k contains_right
-- Lean.DocString.Types
Lean.Doc.Inline.footnote.inj : ∀ {i : Type u} {name : String} {content : Array (Lean.Doc.Inline i)} {name_1 : String}
  {content_1 : Array (Lean.Doc.Inline i)},
  Lean.Doc.Inline.footnote name content = Lean.Doc.Inline.footnote name_1 content_1 →
    name = name_1 ∧ content = content_1
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `M` is finite free over a PID `R`, then any submodule `N` is free
and we can find a basis for `M` and `N` such that the inclusion map is a diagonal matrix
in Smith normal form.

See `Submodule.smithNormalFormOfLE` for a version of this theorem that returns
a `Basis.SmithNormalForm`.

This is a strengthening of `Submodule.basisOfPidOfLE`.
 -/
Submodule.exists_smith_normal_form_of_le : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsDomain R] [IsPrincipalIdealRing R] [Finite ι] (b : Module.Basis ι R M) (N O : Submodule R M),
  N ≤ O → ∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we let `S.z` be any element such that `S.a + η ^ 2 * S.b = λ * S.z`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.z : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution✝ hζ → NumberField.RingOfIntegers K
-- Mathlib.Data.W.Constructions
WType.leftInverse_nat : Function.LeftInverse WType.ofNat WType.toNat
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Receiver.mk.injEq : ∀ {α : Type} (inner inner_1 : Std.Bounded.Receiver✝ α), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Lean.Expr
/-- Apply the given arguments to `f`, beta-reducing if `f` is a
lambda expression. See docstring for `betaRev` for examples.
 -/
Lean.Expr.beta : Lean.Expr → Array Lean.Expr → Lean.Expr
-- Init.Internal.Order.Basic
Lean.Order.instMonoBindEST : ∀ {ε σ : Type} [inst : Nonempty ε], Lean.Order.MonoBind (EST ε σ)
-- Mathlib.Order.Std
Preorder.OfStdArgs.mk : {α : Type u_1} →
  (le : autoParam (LE α) Preorder.OfStdArgs.le._autoParam) →
    (lt :
        autoParam
          (let this := le;
          LT α)
          Preorder.OfStdArgs.lt._autoParam) →
      autoParam
          (let this := le;
          let this_1 := lt;
          Std.LawfulOrderLT α)
          Preorder.OfStdArgs.lawfulOrderLT._autoParam →
        autoParam
            (let this := le;
            Std.IsPreorder α)
            Preorder.OfStdArgs.isPreorder._autoParam →
          Preorder.OfStdArgs α
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePointWeightsWithCircumcenter.eq_1 : ∀ (n : ℕ) (a : Fin (n + 2 + 1)),
  Affine.Simplex.mongePointWeightsWithCircumcenter n (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a) =
    (↑(n + 1))⁻¹
-- Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory
/-- The strict bicategory of quasicategories extracted from `QCat.CatEnrichedOrdinaryCat`.  -/
SSet.QCat.strictBicategory : CategoryTheory.Bicategory.Strict SSet.QCat
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_eq_iff' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'}
  [inst_3 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_4 : CategoryTheory.ConcreteCategory A FC]
  {P : CategoryTheory.Functor Cᵒᵖ A}
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)]
  [CategoryTheory.LocallySmall.{w, v, u} C] (X : C) (x : Φ.fiber.obj X)
  (z₁ z₂ : CategoryTheory.ToType (P.obj (Opposite.op X))),
  (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₁ =
      (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) z₂ ↔
    ∃ Y f y,
      (CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) y = x ∧
        (CategoryTheory.ConcreteCategory.hom (P.map f.op)) z₁ = (CategoryTheory.ConcreteCategory.hom (P.map f.op)) z₂
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instZero : {α : Type u_1} → {x : MeasurableSpace α} → Zero (MeasureTheory.Measure α)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.namespaceId : Lean.Syntax → Lean.Elab.CompletionInfo
-- Mathlib.Control.Traversable.Instances
_private.Mathlib.Control.Traversable.Instances.0.Option.instDecidableEq.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : Unit → motive none)
  (h_2 : (val : α) → motive (some val)),
  (match some val with
    | none => h_1 ()
    | some val => h_2 val) =
    h_2 val
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.map_germ_eq_Γgerm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {i : U ⟶ ⊤} (x : ↑X) (hx : x ∈ U) {Z : C}
  (h : F.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map i.op) (CategoryTheory.CategoryStruct.comp (F.germ U x hx) h) =
    CategoryTheory.CategoryStruct.comp (F.Γgerm x) h
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_mono : ∀ {a b : ENNReal}, b ≠ ⊤ → a ≤ b → a.toReal ≤ b.toReal
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instIsMultiplicativeFullSubcategoryWeakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {P : CategoryTheory.ObjectProperty C} [(HomotopicalAlgebra.weakEquivalences C).IsMultiplicative],
  (HomotopicalAlgebra.weakEquivalences P.FullSubcategory).IsMultiplicative
-- Mathlib.Algebra.Category.Ring.Basic
/-- The forgetful functor from `CommRingCat` to `RingCat` is fully faithful.  -/
CommRingCat.fullyFaithfulForget₂ToRingCat : (CategoryTheory.forget₂ CommRingCat RingCat).FullyFaithful
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.one_lt_cof_iff : ∀ {α : Type u} [inst : Preorder α] [Nonempty α], 1 < Order.cof α ↔ NoTopOrder α
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.rectVandermonde_apply : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} {α : Type u_3} {v w : α → R} {i : α} {j : Fin n},
  Matrix.rectVandermonde v w n i j = v i ^ ↑j * w i ^ ↑j.rev
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Characterization of `C^n` functions into a vector bundle.
Version at a point within a set.  -/
Bundle.contMDiffWithinAt_totalSpace : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7}
  [inst_5 : NormedAddCommGroup EB] [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM]
  {HM : Type u_11} [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M},
  ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f s x₀ ↔
    ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x₀ ∧
      ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuous_restrict_iff : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] (F : ι → β → α) {S : Set β},
  UniformEquicontinuous (S.domRestrict ∘ F) ↔ UniformEquicontinuousOn F S
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.mk_left : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] {P : CategoryTheory.MorphismProperty D}
  (Q : CategoryTheory.MorphismProperty C) {F : CategoryTheory.Functor C D} {X : D} {A : C} (f : F.obj A ⟶ X) (hf : P f),
  (CategoryTheory.MorphismProperty.CostructuredArrow.mk Q f hf).left = A
-- Mathlib.Data.NNReal.Defs
NNReal.instSMulNNRat : SMul ℚ≥0 NNReal
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.coe_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A], ↑⊥ = {0}
-- Mathlib.Topology.Algebra.Group.Torsor
/-- `Equiv.pointReflection` as a homeomorphism  -/
Homeomorph.pointReflection : {V : Type u_4} →
  {P : Type u_5} →
    [inst : AddGroup V] →
      [inst_1 : TopologicalSpace V] →
        [inst_2 : AddTorsor V P] → [inst_3 : TopologicalSpace P] → [IsTopologicalAddTorsor P] → P → P ≃ₜ P
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivRight_apply : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (a : MvPolynomial (Option S₁) R),
  (MvPolynomial.optionEquivRight R S₁) a =
    (MvPolynomial.aeval fun o => o.elim (MvPolynomial.C Polynomial.X) MvPolynomial.X) a
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.smul_nonpos : ∀ {Ω : Type u_1} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m0} {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : PartialOrder F]
  [inst_3 : NormedSpace ℝ F] [CompleteSpace F] [IsOrderedModule ℝ F] [IsOrderedAddMonoid F] {f : ι → Ω → F} {c : ℝ},
  c ≤ 0 → MeasureTheory.Supermartingale f ℱ μ → MeasureTheory.Submartingale (c • f) ℱ μ
-- Mathlib.Combinatorics.Graph.Simple
Graph.instSimpleNoEdge : ∀ {α : Type u_1} {β : Type u_2} (V : Set α), (Graph.noEdge V β).Simple
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.triangle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.associator X (⊥_ C) Y).hom
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X)
        (CategoryTheory.Limits.coprod.leftUnitor Y).hom) =
    CategoryTheory.Limits.coprod.map (CategoryTheory.Limits.coprod.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.id Y)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
/-- Given a symbolic bound `b`, returns `-b + 1`  -/
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.mkIntNegSucc : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneLift_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {t₁ t₂ : CategoryTheory.Limits.Cone K} (f : t₁ ⟶ t₂),
  (CategoryTheory.WithTerminal.coneLift✝.map f).hom = CategoryTheory.Over.Hom.left f.hom
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.mk.congr_simp : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (hom hom_1 : u.right ⟶ v.left) (e_hom : hom = hom_1)
  (comm :
    CategoryTheory.Arrow.Hom.left f - CategoryTheory.Arrow.Hom.left g = CategoryTheory.CategoryStruct.comp u.hom hom),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- The evaluation map is not generally multiplicative when the coefficient ring is noncommutative,
but nevertheless any polynomial of the form `p * (X - C r)` is sent to zero when evaluated at `r`.

This is the key step in our proof of the Cayley-Hamilton theorem.
 -/
Polynomial.eval_mul_X_sub_C : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} (r : R), Polynomial.eval r (p * (Polynomial.X - Polynomial.C r)) = 0
-- Init.Data.Iterators.PostconditionMonad
/-- A version of `bind` that provides a proof of the previous postcondition to the mapping function.
 -/
Std.Iterators.PostconditionT.pbind : {m : Type w → Type w'} →
  [Monad m] →
    {α β : Type w} →
      (x : Std.Iterators.PostconditionT m α) →
        (Subtype x.Property → Std.Iterators.PostconditionT m β) → Std.Iterators.PostconditionT m β
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mk_surjective : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : T} (X : CategoryTheory.Under S),
  ∃ Y f, CategoryTheory.Under.mk f = X
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.hasTrivialRadical_iff_no_solvable_ideals : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable ↥I → I = ⊥
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.SMulAntidiagonal.congr_simp : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s s_1 : Set G} (e_s : s = s_1) {t t_1 : Set P} (e_t : t = t_1)
  (a a_1 : P) (e_a : a = a_1) (h : (s.smulAntidiagonal t a).Finite),
  Finset.SMulAntidiagonal a h = Finset.SMulAntidiagonal a_1 ⋯
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.Gamma_two : Real.Gamma 2 = 1
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_add' : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f g : α → G},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → ∫ (a : α), (f + g) a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Matrix.charpoly.univ.eq_1 : ∀ (R : Type u_1) (n : Type u_3) [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  Matrix.charpoly.univ R n = (Matrix.mvPolynomialX n n R).charpoly
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.mono_iff_injective : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ⟶ Y),
  CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.GroupWithZero.Action.Units
Units.instMulDistribMulAction : {M : Type u_3} →
  {α : Type u_4} → [inst : Monoid M] → [inst_1 : Monoid α] → [MulDistribMulAction M α] → MulDistribMulAction Mˣ α
-- Mathlib.Analysis.Calculus.AddTorsor.Coord
smooth_barycentric_coord : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : AffineBasis ι 𝕜 E) (i : ι),
  ContDiff 𝕜 ⊤ ⇑(b.coord i)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanCompIso_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.spanCompIso F f g).app CategoryTheory.Limits.WalkingSpan.zero =
    CategoryTheory.Iso.refl (((CategoryTheory.Limits.span f g).comp F).obj CategoryTheory.Limits.WalkingSpan.zero)
-- Init.Data.Int.Order
Int.one_nonneg : 0 ≤ 1
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.tprod_of_nat_of_neg : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℤ → G},
  (Multipliable fun n => f ↑n) →
    (Multipliable fun n => f (-↑n)) → ∏' (n : ℤ), f n = ((∏' (n : ℕ), f ↑n) * ∏' (n : ℕ), f (-↑n)) / f 0
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The (strict) image of a `MorphismProperty C` by a functor `C ⥤ D`  -/
CategoryTheory.MorphismProperty.strictMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.MorphismProperty C → CategoryTheory.Functor C D → CategoryTheory.MorphismProperty D
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.maxKeyD_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).isEmpty = false →
        ∀ {fallback : α},
          (Std.DTreeMap.Raw.Const.alter t k f).maxKeyD fallback = k ↔
            (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Algebra.Module.FinitePresentation
instFinitePresentationTensorProduct : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] [Module.FinitePresentation R M],
  Module.FinitePresentation A (TensorProduct R A M)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.arrow_intersect : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
  (f : Y ⟶ X) (S R : CategoryTheory.Sieve X), J.Covers S f → J.Covers R f → J.Covers (S ⊓ R) f
-- Mathlib.Topology.Instances.Real.Lemmas
/-- The limit of a monotone, bounded above function `f : ι → ℝ` is a least upper bound
of the function.  -/
Real.isLUB_of_tendsto_monotone_bddAbove : ∀ {ι : Type u_1} [inst : Preorder ι] [Nonempty ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] {f : ι → ℝ} {x : ℝ},
  Filter.Tendsto f Filter.atTop (nhds x) → Monotone f → BddAbove (Set.range f) → IsLUB (Set.range f) x
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.neg_root_mem : ∀ {ι : 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] (P : RootPairing ι R M N) (i : ι),
  -P.root i ∈ Set.range ⇑P.root
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorObj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (I₂ : Type u_8) (I₃ : Type u_9) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃) (x : I₁ × I₂ × I₃),
  ((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃ x =
    ((F.obj (X₁ x.1)).obj (X₂ x.2.1)).obj (X₃ x.2.2)