mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Field.Basic
one_div_strictAntiOn : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α],
  StrictAntiOn (fun x => 1 / x) (Set.Ioi 0)
-- Mathlib.CategoryTheory.ComposableArrows.Three
/-- The morphism `mk₂ f₁ f₂₃ ⟶ mk₂ f₁₂ f₃` when `f₁ ≫ f₂ = f₁₂` and `f₂ ≫ f₃ = f₂₃`.  -/
CategoryTheory.ComposableArrows.threeδ₂Toδ₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {i j k l : C} →
      (f₁ : i ⟶ j) →
        (f₂ : j ⟶ k) →
          (f₃ : k ⟶ l) →
            (f₁₂ : i ⟶ k) →
              (f₂₃ : j ⟶ l) →
                autoParam (CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
                    CategoryTheory.ComposableArrows.threeδ₂Toδ₁._auto_1 →
                  autoParam (CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃)
                      CategoryTheory.ComposableArrows.threeδ₂Toδ₁._auto_3 →
                    (CategoryTheory.ComposableArrows.mk₂ f₁ f₂₃ ⟶ CategoryTheory.ComposableArrows.mk₂ f₁₂ f₃)
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_real_apply_of_mem_of_notMem : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s → x ∈ s → y ∉ s → (ProbabilityTheory.bernoulliMeasure x y p).real s = ↑p
-- Batteries.Classes.Order
Std.LawfulLTCmp.toOrientedCmp : ∀ {α : Type u_1} {inst : LT α} {cmp : α → α → Ordering} [self : Std.LawfulLTCmp cmp], Std.OrientedCmp cmp
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.coe_subtype : ∀ {M : Type u_1} {A : Type u_3} [inst : MulOneClass M] [inst_1 : SetLike A M] [hA : SubmonoidClass A M] (S' : A),
  ⇑(SubmonoidClass.subtype S') = Subtype.val
-- Init.Core
Std.Irrefl.mk : ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a : α), ¬r a a) → Std.Irrefl r
-- Mathlib.Order.RelIso.Basic
RelEmbedding.ofMonotone_coe : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : Std.Trichotomous r] [inst_1 : Std.Asymm s]
  (f : α → β) (H : ∀ (a b : α), r a b → s (f a) (f b)), ⇑(RelEmbedding.ofMonotone f H) = f
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_ker : ∀ {R : Type u_1} {M : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {B : M →ₗ[R] M →ₗ[R] R}, B.IsSymm → ∀ {W : Submodule R M}, IsCompl W B.ker → (B.domRestrict₁₂ W W).Nondegenerate
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- A square matrix is row stochastic if each element is non-negative and row sums to one.  -/
Matrix.mem_rowStochastic_iff_sum : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.rowStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ ∀ (i : n), ∑ j, M i j = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sum_cos : ∀ (n : ℕ) {a : ℂ},
  (∀ (k : ℤ), a ≠ ↑k * (2 * ↑Real.pi)) →
    ∀ (b : ℂ),
      ∑ i ∈ Finset.range n, Complex.cos (a * ↑i + b) =
        Complex.sin (↑n * a / 2) * Complex.cos ((↑n - 1) * a / 2 + b) / Complex.sin (a / 2)
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryExtensive C]
  {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))}
  (self : CategoryTheory.coherentTopology.struct✝ F) (n : ℕ),
  (CategoryTheory.ConcreteCategory.hom
        ((F.map (CategoryTheory.homOfLE ⋯).op).hom.app
          (Opposite.op (CategoryTheory.coherentTopology.struct.X✝ self (n + 1)))))
      (CategoryTheory.coherentTopology.struct.x✝ self (n + 1)) =
    (CategoryTheory.ConcreteCategory.hom
        ((F.obj (Opposite.op n)).obj.map (CategoryTheory.coherentTopology.struct.map✝ self n).op))
      (CategoryTheory.coherentTopology.struct.x✝ self n)
-- Mathlib.Order.Hom.Lattice
SupHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] (f : SupHom α β) (f' : α → β) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.SetTheory.Ordinal.Notation
/-- Subtraction of ordinal notations  -/
NONote.instSub : Sub NONote
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_nonneg_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalSemiring R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A]
  [inst_18 : NonUnitalContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] {a : A} (ha : p a)
  {f : ContinuousMapZero (↑(quasispectrum R a)) R}, 0 ≤ (cfcₙHom ha) f ↔ 0 ≤ f
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- `pointsWithCircumcenter`, applied to `circumcenterIndex`, equals the
circumcenter.  -/
Affine.Simplex.pointsWithCircumcenter_eq_circumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
  s.pointsWithCircumcenter Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex = s.circumcenter
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If a function applied at a point is 0, a sum is unchanged by
removing that point, if present, from a `Finset`.  -/
Finset.sum_erase : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) {f : ι → M} {a : ι},
  f a = 0 → ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x
-- Mathlib.MeasureTheory.Function.Jacobian
/-- A version of Sard lemma in fixed dimension: given a differentiable function from `E` to `E` and
a set where the differential is not invertible, then the image of this set has zero measure.  -/
MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure], (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → (∀ x ∈ s, (f' x).det = 0) → μ (f '' s) = 0
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and unary `-` is an `NegZeroClass`, if it admits an
injective map that preserves `0` and unary `-` to an `NegZeroClass`.  -/
Function.Injective.negZeroClass : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Zero M₁] →
      [inst_1 : Neg M₁] →
        [inst_2 : NegZeroClass M₂] →
          (f : M₁ → M₂) → Function.Injective f → f 0 = 0 → (∀ (x : M₁), f (-x) = -f x) → NegZeroClass M₁
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.instIsMonoidalId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Adjunction.id.IsMonoidal
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
/-- A predicate that indicates whether a formula can soundly be passed into performRupAdd.  -/
Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd : {α : outParam (Type u)} →
  {β : outParam (Type v)} →
    {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} →
      {σ : Type w} →
        {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} →
          [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] → σ → Prop
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.add_apply : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  (p q : FormalMultilinearSeries 𝕜 E F) (n : ℕ), (p + q) n = p n + q n
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.range_liftHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (B : QuaternionAlgebra.Basis A c₁ c₂ c₃), B.liftHom.range = R[B.i, B.j, B.k]
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- Fréchet derivative of `compContinuousLinearMap f g` with respect to `g`.

Recall that `compContinuousLinearMap f g` is the pullback of `f : F [⋀^ι]→L[𝕜] G`
along `g : E →L[𝕜] F`.

This function is linear in `f`, so its derivative with respect to `f`
is given by `compContinuousLinearMapCLM f g`.

The derivative with respect to `g` is given by
`f.fderivCompContinuousLinearMap g dg v = ∑ i, f fun j ↦ Function.update (fun _ ↦ g) i dg j (v j)`,
see `fderivCompContinuousLinearMap_apply` below.
 -/
ContinuousAlternatingMap.fderivCompContinuousLinearMap : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {G : Type wG} →
        {ι : Type v} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : SeminormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        [Fintype ι] → [DecidableEq ι] → F [⋀^ι]→L[𝕜] G → (E →L[𝕜] F) → (E →L[𝕜] F) →L[𝕜] E [⋀^ι]→L[𝕜] G
-- Mathlib.Data.LawfulXor.Basic
xor_cancel_left : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] (a b : α), a ^^^ (a ^^^ b) = b
-- Init.Data.Vector.Lemmas
Vector.prod_mk : ∀ {α : Type u_1} {n : ℕ} [inst : Mul α] [inst_1 : One α] {xs : Array α} (h : xs.size = n),
  (Vector.mk xs h).prod = xs.prod
-- Std.Data.Iterators.Producers.Repeat
Std.Iterators.Types.RepeatIterator.instIteratorLoop : {α : Type w} →
  {f : α → α} → {n : Type w → Type w'} → [Monad n] → Std.IteratorLoop (Std.Iterators.Types.RepeatIterator α f) Id n
-- Mathlib.Algebra.Group.TransferInstance
Equiv.div_def : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Div β] (x y : α), x / y = e.symm (e x / e y)
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Algebra.TensorProduct.linearEquivIncludeRange_symm_tmul : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] (x : ↥Algebra.TensorProduct.includeLeft.range)
  (y : ↥Algebra.TensorProduct.includeRight.range),
  (Algebra.TensorProduct.linearEquivIncludeRange R S T).symm (x ⊗ₜ[R] y) = ↑x * ↑y
-- Mathlib.Data.Setoid.Basic
Setoid.lift_injective_iff_ker_eq_of_le : ∀ {α : Type u_1} {β : Type u_2} {r : Setoid α} {f : α → β} (hle : r ≤ Setoid.ker f),
  Function.Injective (Quotient.lift f hle) ↔ Setoid.ker f = r
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.IsSStronglyConnected.isStronglyConnected : ∀ (V : Type u_2) [inst : Quiver V], Quiver.IsSStronglyConnected V → Quiver.IsStronglyConnected V
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
/-- If `G` preserves limits, we have an isomorphism from the image of the limit of a functor `F`
to the limit of the functor `F ⋙ G`.
 -/
CategoryTheory.preservesLimitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            [inst_2 : CategoryTheory.Category.{w', w} J] →
              (F : CategoryTheory.Functor J C) →
                [inst_3 : CategoryTheory.Limits.PreservesLimit F G] →
                  [inst_4 : CategoryTheory.Limits.HasLimit F] →
                    G.obj (CategoryTheory.Limits.limit F) ≅ CategoryTheory.Limits.limit (F.comp G)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_eq_nsmul_single : ∀ {ι : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {m : Multiset ι} {f : ι → M} [inst_1 : DecidableEq ι] (i : ι),
  (∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 0) → (Multiset.map f m).sum = Multiset.count i m • f i
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.eval.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (l : Profinite.NobelingProof.Products I),
  Profinite.NobelingProof.Products.eval C l = (List.map (Profinite.NobelingProof.e C) ↑l).prod
-- Mathlib.Algebra.Order.Group.Action.End
RelIso.smul_def : ∀ {α : Type u_1} {r : α → α → Prop} (f : r ≃r r) (a : α), f • a = f a
-- Mathlib.CategoryTheory.Core
/-- A functor from a groupoid to a category C factors through the core of C.  -/
CategoryTheory.Core.functorToCore : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : Type u₂} →
      [inst_1 : CategoryTheory.Groupoid G] →
        CategoryTheory.Functor G C → CategoryTheory.Functor G (CategoryTheory.Core C)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticDvdSequence.smul : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R}, IsEllipticDvdSequence W → ∀ (x : R), IsEllipticDvdSequence (x • W)
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressReport : Type
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isClosedEmbedding_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], Topology.IsClosedEmbedding fun x => {x}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ext_keys_unit : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtDTreeMap α (fun x => Unit) cmp},
  t₁.keys.Perm t₂.keys → t₁ = t₂
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Constructor for the constant functor  -/
MvPFunctor.const.mk : (n : ℕ) → {A : Type u} → A → {α : TypeVec.{u} n} → ↑(MvPFunctor.const n A) α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Hover.contents : Lean.Lsp.Hover → Lean.Lsp.MarkupContent
-- Mathlib.Data.Finset.Dedup
Finset.perm_toList : ∀ {α : Type u_1} {f₁ f₂ : Finset α}, f₁.toList.Perm f₂.toList ↔ f₁ = f₂
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.instInhabited.eq_1 : ∀ {M : Type u_4} [inst : Add M], AddEquiv.instInhabited = { default := AddEquiv.refl M }
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_le_coeff_tight_cert : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Poly → ℤ → Bool
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConst.mk.injEq : ∀ (constInfo : Lean.AsyncConstantInfo) (exts? : Option (Task (Array Lean.EnvExtensionState)))
  (aconstsImpl : Task Dynamic) (isRealized : Bool) (constInfo_1 : Lean.AsyncConstantInfo)
  (exts?_1 : Option (Task (Array Lean.EnvExtensionState))) (aconstsImpl_1 : Task Dynamic) (isRealized_1 : Bool),
  ({ constInfo := constInfo, exts? := exts?, aconstsImpl := aconstsImpl, isRealized := isRealized } =
      { constInfo := constInfo_1, exts? := exts?_1, aconstsImpl := aconstsImpl_1, isRealized := isRealized_1 }) =
    (constInfo = constInfo_1 ∧ exts? = exts?_1 ∧ aconstsImpl = aconstsImpl_1 ∧ isRealized = isRealized_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- Auxiliary definition for `SSet.Truncated.liftOfStrictSegal`.  -/
SSet.Truncated.liftOfStrictSegal.app : {X Y : SSet.Truncated 2} →
  (f₀ :
      X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
        Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })) →
    (f₁ :
        X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
          Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })) →
      (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
          f₀
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
                x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
              (f₁ x)) →
        (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
            f₀
                ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                  x) =
              (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                (f₁ x)) →
          Y.StrictSegal → (n : (SimplexCategory.Truncated 2)ᵒᵖ) → X.obj n ⟶ Y.obj n
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A collection of morphisms `f b ⟶ P` induces a morphism `∐ f ⟶ P`.  -/
CategoryTheory.Limits.Sigma.desc : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} → [inst_1 : CategoryTheory.Limits.HasCoproduct f] → {P : C} → ((b : β) → f b ⟶ P) → (∐ f ⟶ P)
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.basicOpen_eq_bot_iff : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))),
  X.basicOpen s = ⊥ ↔ s = 0
-- Mathlib.Data.Rel
SetRel.isTrans_univ : ∀ {α : Type u_1}, SetRel.IsTrans Set.univ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- If `P` is multiplicative and stable under base change, having the of-postcomp property
w.r.t. `Q` is equivalent to `Q` implying `P` on the diagonal.  -/
CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [P.IsMultiplicative]
  {Q : CategoryTheory.MorphismProperty C} [Q.IsStableUnderBaseChange], P.HasOfPostcompProperty Q ↔ Q ≤ P.diagonal
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Result.no : Lean.Meta.Grind.Result✝
-- Mathlib.Data.PEquiv
PEquiv.trans_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ),
  (f.trans g) a = some c ↔ ∃ b, f a = some b ∧ g b = some c
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- **Double counting** argument.

Considering `r` as a bipartite graph, the LHS is a strict lower bound on the number of edges while
the RHS is an upper bound.  -/
Finset.card_nsmul_lt_card_nsmul_of_lt_of_le' : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R]
  (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : R} [inst_3 : (a : α) → (b : β) → Decidable (r a b)],
  t.Nonempty →
    (∀ b ∈ t, n < ↑(Finset.bipartiteBelow r s b).card) →
      (∀ a ∈ s, ↑(Finset.bipartiteAbove r t a).card ≤ m) → t.card • n < s.card • m
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupAdd_result : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ)
  (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd → f.performRupAdd c rupHints = (f', true) → f' = f.insert c
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidates.candidates : Lean.Elab.Structural.RecArgCandidates → Array Lean.Elab.Structural.RecArgCandidate
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- Continuous alternating maps form a seminormed additive commutative group.
We override projection to `PseudoMetricSpace` to ensure that instances commute
in `with_reducible_and_instances`.  -/
ContinuousAlternatingMap.instSeminormedAddCommGroup : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {ι : Type v} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : NormedSpace 𝕜 F] → [Fintype ι] → SeminormedAddCommGroup (E [⋀^ι]→L[𝕜] F)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.root'_apply_apply_mem_of_mem_span : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : Module S N] [IsScalarTower S R N] [P.IsValuedIn S] {x : N},
  x ∈ Submodule.span S (Set.range ⇑P.coroot) → ∀ (i : ι), (P.root' i) x ∈ (Algebra.linearMap S R).range
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instMulOneClass.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MulOneClass Y],
  LocallyConstant.instMulOneClass = Function.Injective.mulOneClass DFunLike.coe ⋯ ⋯ ⋯
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffWithinAt.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₁} {s : Set M} {x : M},
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s x →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n f s x →
      ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n (fun x => g x ∘SL f x) s x
-- Mathlib.Order.WithBot
WithBot.le_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithTop α} {y : WithBot αᵒᵈ}, x ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual x
-- Mathlib.Algebra.Group.Commute.Units
Units.val_ofPowEqOne : ∀ {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ) (ha : a ^ n = 1) (hn : n ≠ 0), ↑(Units.ofPowEqOne a n ha hn) = a
-- Mathlib.Data.Rat.Lemmas
Rat.inv_intCast_den : ∀ (a : ℤ), (↑a)⁻¹.den = if a = 0 then 1 else a.natAbs
-- Init.Meta.Defs
Lean.Syntax.instCoeOutTSepArrayTSyntaxArray : {k : Lean.SyntaxNodeKinds} → {sep : String} → CoeOut (Lean.Syntax.TSepArray k sep) (Lean.TSyntaxArray k)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_mul_lt_iff₀'` for a version with multiplication on the other side.  -/
inv_mul_lt_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (c⁻¹ * b < a ↔ b < c * a)
-- Init.Data.Array.Lemmas
Array.any_empty : ∀ {α : Type u_1} [BEq α] {p : α → Bool}, #[].any p = false
-- Mathlib.Order.Concept
Concept.extent_ssubset_extent_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c.extent ⊂ d.extent ↔ c < d
-- Mathlib.Data.Finmap
Finmap.mem_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b' : β a'} {s : Finmap β},
  a ∈ Finmap.insert a' b' s ↔ a = a' ∨ a ∈ s
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyonedaForget_hom_app_app_hom_apply_hom : ∀ (X : AddCommMonCatᵒᵖ) (X_1 : AddCommMonCat) (f : ↑(Opposite.unop X) →+ ↑X_1),
  AddCommMonCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((AddCommMonCat.coyonedaForget.hom.app X).app X_1)) f) = f
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_two : Nat.fib 2 = 1
-- Mathlib.Topology.Instances.Matrix
Matrix.blockDiagonal_tsum : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} [inst_2 : DecidableEq p] [T2Space R] {f : X → p → Matrix m n R},
  Matrix.blockDiagonal (∑'[L] (x : X), f x) = ∑'[L] (x : X), Matrix.blockDiagonal (f x)