mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.star_mul_le_algebraMap_norm_sq : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A},
  star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
-- Batteries.Tactic.Lint.Simp
_private.Batteries.Tactic.Lint.Simp.0.Batteries.Tactic.Lint.Expr.eqOrIff? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Lean.Elab.Util
Lean.Elab.addMacroStack : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → Lean.MessageData → Lean.Elab.MacroStack → m Lean.MessageData
-- Mathlib.Order.Monotone.Defs
Antitone.comp_antitoneOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α}, Antitone g → AntitoneOn f s → MonotoneOn (g ∘ f) s
-- Mathlib.Condensed.TopCatAdjunction
condensedSetToTopCat_map : ∀ {X Y : CondensedSet} (f : X ⟶ Y), condensedSetToTopCat.map f = CondensedSet.toTopCatMap f
-- Lean.Data.Json.Elab
/-- Json number negation syntax for scientific numbers.  -/
Lean.Json.«json-__1» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom Y)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.center_toSubsemiring : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (Subalgebra.center R A).toSubsemiring = Subsemiring.center A
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_singleton_eq_span_singleton : ∀ {R : Type u_8} {M : Type u_9} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.IsTorsionFree R M] {x y : M}, R ∙ x = R ∙ y ↔ ∃ z, z • x = y
-- Mathlib.Algebra.Order.Interval.Basic
instDivInterval : {α : Type u_2} → [inst : Preorder α] → [inst_1 : CommGroup α] → [MulLeftMono α] → Div (Interval α)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] [inst_3 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDTreeMap.Const.insertMany t l).getKey! k = t.getKey! k
-- Mathlib.InformationTheory.Hamming
/-- The Hamming weight function to the naturals.  -/
hammingNorm : {ι : Type u_2} →
  {β : ι → Type u_3} → [Fintype ι] → [(i : ι) → DecidableEq (β i)] → [(i : ι) → Zero (β i)] → ((i : ι) → β i) → ℕ
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.le_stabilizer_vadd_right : ∀ {α : Type u_2} {β : Type u_3} {G' : Type u_4} [inst : AddGroup G'] [inst_1 : VAdd α β] [inst_2 : AddAction G' β]
  [VAddCommClass G' α β] (a : α) (b : β), AddAction.stabilizer G' b ≤ AddAction.stabilizer G' (a +ᵥ b)
-- Init.Data.Int.Gcd
Int.dvd_mul : ∀ {a b c : ℤ}, c ∣ a * b ↔ ∃ c₁ c₂, c₁ ∣ a ∧ c₂ ∣ b ∧ c₁ * c₂ = c
-- Mathlib.CategoryTheory.Limits.Over
/-- `Over.liftCocone` is limiting if the original cocone is.  -/
CategoryTheory.Over.isColimitLiftCocone : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) →
            {X : C} →
              (f : c.pt ⟶ X) →
                CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsColimit (CategoryTheory.Over.liftCocone c f)
-- Mathlib.Topology.Algebra.UniformField
/-- The value of `hat_inv` at zero is not really specified, although it's probably zero.
Here we explicitly enforce the `inv_zero` axiom.
 -/
UniformSpace.Completion.instInvCompletion : {K : Type u_1} → [Field K] → [inst : UniformSpace K] → Inv (UniformSpace.Completion K)
-- Mathlib.Tactic.CrossRefAttribute
/-- `stacksTag` is the node kind of Stacks Project Tags: a sequence of digits and
uppercase letters.  -/
Mathlib.CrossRef.stacksTagKind : Lean.SyntaxNodeKind
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- `@[simp]`-normal form of `FGModuleCatEvaluation_apply`, where the carriers have been unfolded.
 -/
FGModuleCat.FGModuleCatEvaluation_apply' : ∀ (K : Type u) [inst : Field K] (V : FGModuleCat K) (f : ↑(FGModuleCat.FGModuleCatDual K V)) (x : ↑V),
  (ModuleCat.Hom.hom (FGModuleCat.FGModuleCatEvaluation K V).hom) (f ⊗ₜ[K] x) = f.toFun x
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.comp_assoc : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Semiring D] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Algebra R C] [inst_8 : Algebra R D] [inst_9 : CoalgebraStruct R A]
  [inst_10 : CoalgebraStruct R B] [inst_11 : CoalgebraStruct R C] [inst_12 : CoalgebraStruct R D] (φ₁ : C →ₐc[R] D)
  (φ₂ : B →ₐc[R] C) (φ₃ : A →ₐc[R] B), (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
-- Mathlib.Topology.Constructions.SumProd
continuous_sum_swap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Sum.swap
-- Init.Data.Float.Float32
/-- Computes the base-10 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`log10f`.
 -/
Float32.log10 : Float32 → Float32
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapDomainAlgHom_comp : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} {O : Type u_9} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] [inst_5 : Monoid O] (f : M →* N)
  (g : N →* O),
  MonoidAlgebra.mapDomainAlgHom R A (g.comp f) =
    (MonoidAlgebra.mapDomainAlgHom R A g).comp (MonoidAlgebra.mapDomainAlgHom R A f)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has filtered colimits is said to have `AB5` provided that
filtered colimits are exact.
 -/
CategoryTheory.AB5 : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasFilteredColimits C] → Prop
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from groups to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.  -/
GrpCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget GrpCat)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.sec_snd_ne_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] [Nontrivial R],
  M ≤ nonZeroDivisors R → ∀ (x : S), ↑(IsLocalization.sec M x).2 ≠ 0
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {F : I.Filtration M}, F.Stable → ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
-- Lean.CoreM
Lean.Core.Context.currRecDepth : Lean.Core.Context → ℕ
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.nest_denest : ∀ (p : DyckWord) (hn : p.IsNested), (p.denest hn).nest = p
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.algebraMap_presheafObj : ∀ {R : CommRingCat} {X : AlgebraicGeometry.Scheme} [inst : X.Over (AlgebraicGeometry.Spec R)]
  [inst_1 : AlgebraicGeometry.IsAffine X],
  algebraMap ↑R ↑(X.presheaf.obj (Opposite.op ⊤)) =
    CommRingCat.Hom.hom
      (AlgebraicGeometry.Spec.fullyFaithful.preimage
          (CategoryTheory.CategoryStruct.comp X.isoSpec.inv (X ↘ AlgebraicGeometry.Spec R))).unop
-- Mathlib.Analysis.Normed.Group.Uniform
Real.isometry_intCast : Isometry Int.cast
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.prod_natCast : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] (s : Finset ι) (f : ι → ℕ), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basis_ne_zero : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  Set.InjOn v ↑s → i ∈ s → Lagrange.basis s v i ≠ 0
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Submodule.powSMulQuotInclusion.eq_1 : ∀ {R : Type u_3} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b c : ℕ} (h : c = b + a) (N : Submodule R M),
  Submodule.powSMulQuotInclusion I M h N = (I ^ b • ⊤).mapQ (I ^ c • N) (I ^ a • N).subtype ⋯
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balanced_one_leaf_leaf : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf).Balanced
-- Std.Data.Internal.List.Associative
Std.Internal.List.distinctKeys_of_sublist_keys : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × γ a)},
  (Std.Internal.List.keys l').Sublist (Std.Internal.List.keys l) →
    Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys l'
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.ofAlgEquiv.eq_1 : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) [inst_1 : IsAdicComplete I S],
  AdicCompletion.ofAlgEquiv I =
    { toFun := (↑(AdicCompletion.ofLinearEquiv I S)).toFun, invFun := (AdicCompletion.ofLinearEquiv I S).invFun,
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Init.Data.Array.Lemmas
Array.length_toList : ∀ {α : Type u_1} {xs : Array α}, xs.toList.length = xs.size
-- Batteries.Data.Vector.Basic
_private.Batteries.Data.Vector.Basic.0.Vector.scanrMFast : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} → {n : ℕ} → [Monad m] → (α → β → m β) → β → Vector α n → n < USize.size → m (Vector β (n + 1))
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinForm.tensorDistribEquiv_apply : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Module.Free R M₁]
  [inst_6 : Module.Finite R M₁] [inst_7 : Module.Free R M₂] [inst_8 : Module.Finite R M₂]
  (B : TensorProduct R (LinearMap.BilinForm R M₁) (LinearMap.BilinForm R M₂)),
  (LinearMap.BilinForm.tensorDistribEquiv R) B = (LinearMap.BilinForm.tensorDistrib R R) B
-- Mathlib.RingTheory.Congruence.Basic
RingCon.coe_iInf : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {ι : Sort u_5} (f : ι → RingCon R), ⇑(iInf f) = ⨅ i, ⇑(f i)
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Group α] {a b : α}, a⁺ᵐ < b ↔ a < b ∧ 1 < b
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_inter_add_sdiff`. -/
MeasureTheory.measure_inter_add_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasurableSet t → μ (s ∩ t) + μ (s \ t) = μ s
-- Mathlib.Data.Set.Basic
Set.subset_inter_iff : ∀ {α : Type u} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedInfo : Inhabited Lean.Elab.Info
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
coe_basisOfTopLeSpanOfCardEqFinrank : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : OrzechProperty R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {ι : Type u_3} [inst_4 : Fintype ι] (b : ι → M) (le_span : ⊤ ≤ Submodule.span R (Set.range b))
  (card_eq : Fintype.card ι = Module.finrank R M), ⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b
-- Mathlib.Analysis.Convex.Basic
AntitoneOn.convex_gt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, AntitoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ r < f x}
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- If `v` is a linearly independent family of vectors (indexed by a linearly ordered type),
then the family of its `n`-fold exterior products is also linearly independent.  -/
exteriorPower.ιMulti_family_linearIndependent_field : ∀ {K : Type u_2} {E : Type u_4} (n : ℕ) [inst : Field K] [inst_1 : AddCommGroup E] [inst_2 : Module K E] {I : Type u_5}
  [inst_3 : LinearOrder I] {v : I → E},
  LinearIndependent K v → LinearIndependent (ι := ↑(Set.powersetCard I n)) K (exteriorPower.ιMulti_family K n v)
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- **Alias** of `Ultrafilter.exists_le`.

---

The ultrafilter lemma: Any proper filter is contained in an ultrafilter.  -/
Filter.exists_ultrafilter_le : ∀ {α : Type u} (f : Filter α) [h : f.NeBot], ∃ u, ↑u ≤ f
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.instAssociativeSigmaMinOfTransOrd_std : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α], Std.Associative min
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
IsRegularCardinalOrder.mk : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  (Ordinal.type fun x1 x2 => x1 < x2) ≤ (Order.cof α).ord → IsRegularCardinalOrder α
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.prodMap.eq_1 : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [inst : AddMonoid A] [inst_1 : AddMonoid B]
  [inst_2 : AddMonoid C] [inst_3 : AddMonoid D] [inst_4 : TopologicalSpace A] [inst_5 : TopologicalSpace B]
  [inst_6 : TopologicalSpace C] [inst_7 : TopologicalSpace D] (f : A →ₜ+ C) (g : B →ₜ+ D),
  f.prodMap g = { toAddMonoidHom := f.prodMap g.toAddMonoidHom, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Category.Ring.EqualizerPushout
/-- Any map `f : R ⟶ S` in `CommRingCat` with faithfully flat `f.hom : R ⟶ S` is a regular
monomorphism.  -/
CommRingCat.isRegularMono_of_faithfullyFlat : ∀ {R S : CommRingCat} (f : R ⟶ S), (CommRingCat.Hom.hom f).FaithfullyFlat → CategoryTheory.IsRegularMono f
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- A preconnected set `s` has the property that every map to a
discrete space that is continuous on `s` is constant on `s`  -/
IsPreconnected.constant : ∀ {α : Type u} [inst : TopologicalSpace α] {Y : Type u_3} [inst_1 : TopologicalSpace Y] [DiscreteTopology Y]
  {s : Set α}, IsPreconnected s → ∀ {f : α → Y}, ContinuousOn f s → ∀ {x y : α}, x ∈ s → y ∈ s → f x = f y
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.toContinuousMapAddMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : AddMonoid Y]
  [inst_3 : ContinuousAdd Y] (f : LocallyConstant X Y), LocallyConstant.toContinuousMapAddMonoidHom f = ↑f
-- Mathlib.CategoryTheory.IsoCat
/-- The composition `functor ⋙ inverse` is equal to the identity.  -/
CategoryTheory.IsoCat.unit_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (self : CategoryTheory.IsoCat C D),
  CategoryTheory.Functor.id C = self.functor.comp self.inverse
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.self_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k}, (cmp k (t.insertIfNew k v).maxKey!).isLE = true
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_eq_tmod_of_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → a.fmod b = a.tmod b
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.limsup_measure_compl_le_of_le_liminf_measure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω}
  {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω},
  MeasurableSet E → μ E ≤ Filter.liminf (fun i => (μs i) E) L → Filter.limsup (fun i => (μs i) Eᶜ) L ≤ μ Eᶜ
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.below.of_presieve : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → CategoryTheory.MorphismProperty.sourceLocalClosure K P x → Prop} {X Y : C}
  (f : X ⟶ Y) (R : CategoryTheory.Presieve X) (hR : R ∈ K.coverings X)
  (h :
    ∀ (U : C) (g : U ⟶ X),
      R g → CategoryTheory.MorphismProperty.sourceLocalClosure K P (CategoryTheory.CategoryStruct.comp g f)),
  (∀ (U : C) (g : U ⟶ X) (a : R g), CategoryTheory.MorphismProperty.sourceLocalClosure.below ⋯) →
    (∀ (U : C) (g : U ⟶ X) (a : R g), motive (CategoryTheory.CategoryStruct.comp g f) ⋯) →
      CategoryTheory.MorphismProperty.sourceLocalClosure.below ⋯
-- Mathlib.Data.Set.Order
AntitoneOn.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β) (s : Set α),
  AntitoneOn f s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f b ≤ f a
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The oriented angle between three points is `π` if and only if the unoriented angle is `π`.  -/
EuclideanGeometry.oangle_eq_pi_iff_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_congr : ∀ {R : Type u_1} [inst : CommSemiring R] {a a' c : R} {b b' : ℕ}, a = a' → b = b' → a' ^ b' = c → a ^ b = c
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given two lines sharing a common point lying strictly outside the segments determined by the
defining points. Fixing one point from each line as the endpoints, choosing either remaining point
as the vertex yields oriented angles with the same sign.  -/
Sbtw.oangle_sign_eq_of_sbtw_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ p₄ : P},
  Sbtw ℝ p p₁ p₃ → Sbtw ℝ p p₂ p₄ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₃ p₂).sign
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- Every ordinal has a fundamental sequence.  -/
Ordinal.exists_isFundamentalSeq : ∀ {a o : Ordinal.{u_1}}, o.cof.ord = a → ∃ f, Ordinal.IsFundamentalSeq f
-- Mathlib.Data.Set.Defs
/-- Membership in a set  -/
Set.Mem : {α : Type u} → Set α → α → Prop
-- Mathlib.Data.Multiset.ZeroCons
Multiset.empty_eq_zero : ∀ {α : Type u_1}, ∅ = 0
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- In a Turán-maximal graph, non-adjacency is an equivalence relation.  -/
SimpleGraph.IsTuranMaximal.equivalence_not_adj : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ},
  G.IsTuranMaximal r → Equivalence fun x1 x2 => ¬G.Adj x1 x2
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wDest'.eq_1 : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n}, P.wDest' = P.wRec fun a f' f x => ⟨a, TypeVec.splitFun f' f⟩
-- Mathlib.Order.CompleteLattice.Basic
Prod.supSet : (α : Type u_1) → (β : Type u_2) → [SupSet α] → [SupSet β] → SupSet (α × β)
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instNeg.eq_1 : ∀ {α : Type u} [inst : Neg α], WithZero.instNeg = { neg := fun a => Option.map Neg.neg a }
-- Mathlib.GroupTheory.OrderOfElement
zpow_eq_one_iff_modEq : ∀ {G : Type u_1} [inst : Group G] {x : G} {n : ℤ}, x ^ n = 1 ↔ n ≡ 0 [ZMOD ↑(orderOf x)]
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_star_eq_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] {M : Matrix m n α},
  M.map star = 0 ↔ M = 0
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_neg : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : AddGroup G] [MeasurableNeg G] [μ.IsNegInvariant] {f : G → F},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun t => f (-t)) μ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a b : α} {fallback : β}, (a == b) = true → m.getD a fallback = m.getD b fallback
-- Mathlib.Util.Notation3
/-- This stores the assignments of variables to subexpressions (and their contexts)
that have been found so far during the course of the matching algorithm.
We store the contexts since we need to delaborate expressions after we leave
scoping constructs.  -/
Mathlib.Notation3.MatchState.vars : Mathlib.Notation3.MatchState → Std.HashMap Lean.Name (Lean.SubExpr × Lean.LocalContext × Lean.LocalInstances)
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_succAbove_predAbove : ∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), (i.succAbove j).succAbove (j.predAbove i) = i
-- Init.Data.Int.Order
Int.natAbs_eq_iff_mul_eq_zero : ∀ {a : ℤ} {n : ℕ}, a.natAbs = n ↔ (a - ↑n) * (a + ↑n) = 0
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.nonempty_iso_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X Y : C), Nonempty (X ≅ Y) ↔ Nonempty (Y ≅ X)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- An `r + 1`-cliquefree graph is `r`-Turán-maximal if any other `r + 1`-cliquefree graph on
the same vertex set has the same or fewer number of edges.  -/
SimpleGraph.IsTuranMaximal : {V : Type u_1} → [Fintype V] → (G : SimpleGraph V) → [DecidableRel G.Adj] → ℕ → Prop
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_pow_count_prod : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : DecidableEq α] {x : α},
  x ≠ 0 →
    Associated
      (∏ p ∈ (UniqueFactorizationMonoid.factors x).toFinset, p ^ Multiset.count p (UniqueFactorizationMonoid.factors x))
      x
-- Mathlib.RingTheory.PowerBasis
PowerBasis.liftEquiv_symm_apply : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S)
  (y : { y // (Polynomial.aeval y) (minpoly A pb.gen) = 0 }), pb.liftEquiv.symm y = pb.lift ↑y ⋯
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to a `UInt32`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toUInt32 : Float.Model → UInt32
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.instIsSeparatedOfIsSeparated : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [X.IsSeparated], AlgebraicGeometry.IsSeparated f
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomRight : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : Cᵒᵖ) (x x_1 : Dᵒᵖ) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight (Opposite.unop c) f.unop).op
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.flag.injEq : ∀ (name : Lean.Name) (default : Bool) (name_1 : Lean.Name) (default_1 : Bool),
  (Lean.Doc.ArgSpec.flag✝ name default = Lean.Doc.ArgSpec.flag✝ name_1 default_1) =
    (name = name_1 ∧ default = default_1)