mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.equivOfTensorIsoUnit_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M)
  (h₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  (h₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj n m ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  (H :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h₁.hom m)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor m).hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator m n m).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m h₂.hom)
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor m).hom))
  [inst_3 : F.Monoidal],
  (CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).unitIso = (CategoryTheory.unitOfTensorIsoUnit F m n h₁).symm
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X)
  (hx : IsClosed {x}),
  AlgebraicGeometry.Spec.map (AlgebraicGeometry.residueFieldIsoBase f x hx).inv =
    CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_zero_right : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.monomial n) 0 = 0
-- Mathlib.Condensed.TopCatAdjunction
/-- The counit of the adjunction `condensedSetToTopCat ⊣ topCatToCondensedSet` is always bijective,
but not an isomorphism in general (the inverse isn't continuous unless `X` is compactly generated).
 -/
CondensedSet.topCatAdjunctionCounitEquiv : (X : TopCat) → ↑X.toCondensedSet.toTopCat ≃ ↑X
-- Mathlib.MeasureTheory.Group.Arithmetic
List.aemeasurable_prod : ∀ {M : Type u_2} {α : Type u_3} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (l : List (α → M)),
  (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
/-- Combine two `OpenPartialHomeomorph`s with disjoint sources and disjoint targets. We reuse
`OpenPartialHomeomorph.piecewise` then override `toPartialEquiv` to `PartialEquiv.disjointUnion`.
This way we have better definitional equalities for `source` and `target`.  -/
OpenPartialHomeomorph.disjointUnion : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e e' : OpenPartialHomeomorph X Y) →
          [(x : X) → Decidable (x ∈ e.source)] →
            [(y : Y) → Decidable (y ∈ e.target)] →
              Disjoint e.source e'.source → Disjoint e.target e'.target → OpenPartialHomeomorph X Y
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.seq.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (x_3 : Fin 0 → α → β) (x_4 : Fin 0 → α), FinVec.seq x_3 x_4 = ![]
-- Lean.Environment
_private.Lean.Environment.0.Lean.setImportedEntries.unsafe_impl_5 : Array (Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState) →
  ℕ → Array Lean.EnvExtensionState → Array Lean.EnvExtensionEntry → ℕ → Array Lean.EnvExtensionState
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- If `s ⊆ f.source` and `g x ∈ f'.source` whenever `x ∈ s`, then `g` is continuous on `s` if and
only if `g` written in charts `f.extend I` and `f'.extend I'` is continuous on `f.extend I '' s`.  -/
OpenPartialHomeomorph.continuousOn_writtenInExtend_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] (f : OpenPartialHomeomorph M H)
  {I : ModelWithCorners 𝕜 E H} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  [inst_7 : TopologicalSpace H'] [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} {s : Set M}
  {f' : OpenPartialHomeomorph M' H'} {g : M → M'},
  s ⊆ f.source →
    Set.MapsTo g s f'.source →
      (ContinuousOn (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I) '' s) ↔ ContinuousOn g s)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Given any distinguished triangle `T`, then we know `T.inv_rotate` is also distinguished.
 -/
CategoryTheory.Pretriangulated.inv_rot_of_distTriang : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    T.invRotate ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_le_of_ball : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F}
  {ε C : ℝ}, 0 < ε → 0 ≤ C → (∀ x ∈ Metric.ball 0 ε, ‖f x‖ ≤ C * ‖x‖) → ‖f‖ ≤ C
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.EStateM.run_bind.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((x : α) → (s : σ) → motive (EStateM.Result.ok x s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instMulOneClass.eq_1 : ∀ {α : Type u} [inst : Mul α],
  WithOne.instMulOneClass = { toOne := WithOne.instOne, toMul := WithOne.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.algEquiv_symm_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [inst_1 : CommSemiring R]
  [inst_2 : Ring S] [inst_3 : Algebra R S] (v : Valuation S Γ₀) (x : S),
  (WithVal.algEquiv R v).symm x = WithVal.toVal v x
-- Mathlib.Order.Bounds.Lattice
isGLB_iUnion_iff_of_isGLB : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_2} {s : ι → Set α} {u : ι → α},
  (∀ (i : ι), IsGLB (s i) (u i)) → ∀ (c : α), IsGLB (Set.range u) c ↔ IsGLB (⋃ i, s i) c
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.finite_torsion_of_isSMulRegular : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) (n : ℕ), IsSMulRegular 𝕜 n → {x | n • x = 0}.Finite
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instLawfulSingleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α],
  LawfulSingleton α (Subtype MeasurableSet)
-- Mathlib.Topology.IsClosedRestrict
Topology.restrict_compl_reorderRestrictProd : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι}
  (p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)), Sᶜ.domRestrict (Topology.reorderRestrictProd S s p) = ↑p.1
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
/-- If `K` generates `J`, then any presheaf `Cᵒᵖ ⥤ Type w` that satisfies the sheaf
condition for all `K`-coverings, is a `J`-sheaf.  -/
CategoryTheory.Precoverage.Generates.isSheaf_of_forall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {J : CategoryTheory.GrothendieckTopology C},
  K.Generates J →
    ∀ (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
      (∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) → CategoryTheory.Presieve.IsSheaf J F
-- Init.GrindInstances.Ring.UInt
UInt8.intCast : IntCast UInt8
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt_of_mem_nhds : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P → ChartedSpace.LiftPropAt P g x → s ∈ nhds x → ChartedSpace.LiftPropWithinAt P g s x
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0) → 0 = f
-- Aesop.EMap
Aesop.EMap.foldlM : {m : Type → Type u_1} → [Monad m] → {σ : Type} → {α : Type u_2} → σ → (σ → Lean.Expr → α → m σ) → Aesop.EMap α → m σ
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- **Alias** of `IsGaloisGroup.smul_mem_of_normal`. -/
smul_mem_of_normal : ∀ (G : Type u_1) (B : Type u_3) [inst : Group G] [inst_1 : Semiring B] [inst_2 : MulSemiringAction G B] {C : Type u_4}
  [inst_3 : CommSemiring C] [inst_4 : Algebra C B] (N : Subgroup G) [hN : N.Normal] [hC : IsGaloisGroup (↥N) C B]
  (g : G) (x : C), g • (algebraMap C B) x ∈ Set.range ⇑(algebraMap C B)
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- Pull back the normed ring structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
algebra homomorphism `Unitization.splitMul 𝕜 A`.  -/
Unitization.instNormedRing : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] →
            [inst_4 : SMulCommClass 𝕜 A A] → [RegularNormedAlgebra 𝕜 A] → NormedRing (Unitization 𝕜 A)
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The structure for rewrite lemmas stored in the `RefinedDiscrTree`.  -/
Mathlib.Tactic.ClickSuggestions.RwLemma : Type
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- A variant of `app_inv_app` that gives an `eqToHom` instead of `homOfLe`.  -/
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)
  (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base)) {Z : C}
  (h :
    Y.presheaf.obj
        (Opposite.op
          ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj
            ((TopologicalSpace.Opens.map f.hom.base).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.hom.base).obj U)) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h
-- Mathlib.Data.Set.Countable
Set.countable_insert : ∀ {α : Type u} {s : Set α} {a : α}, (insert a s).Countable ↔ s.Countable
-- Init.Data.Vector.Algebra
/-- Componentwise scalar multiplication of vectors.  -/
Vector.smul : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → [SMul α β] → α → Vector β n → Vector β n
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_apply₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → (μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ
-- Lean.Meta.SynthInstance
/-- `typeHasMVars := true` if type of `mvar` contains metavariables.
We store this information to implement an optimization that relies on the fact
that instances are "morally canonical."
That is, we need to find at most one answer for this generator node if the type
does not have metavariables.
 -/
Lean.Meta.SynthInstance.GeneratorNode.typeHasMVars : Lean.Meta.SynthInstance.GeneratorNode → Bool
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.imp.injEq : ∀ (e : Lean.Expr) (h : e.isForall = true) (source : Lean.Meta.Grind.SplitSource) (e_1 : Lean.Expr)
  (h_1 : e_1.isForall = true) (source_1 : Lean.Meta.Grind.SplitSource),
  (Lean.Meta.Grind.SplitInfo.imp e h source = Lean.Meta.Grind.SplitInfo.imp e_1 h_1 source_1) =
    (e = e_1 ∧ source = source_1)
-- Mathlib.Order.SuccPred.Basic
Order.pred_ne_pred_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  Order.pred a ≠ Order.pred b ↔ a ≠ b
-- Mathlib.Data.Num.ZNum
Num.mod_to_nat : ∀ (n d : Num), ↑(n % d) = ↑n % ↑d
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.connected_of_ediam_ne_top : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], G.ediam ≠ ⊤ → G.Connected
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.map_id : ∀ {α : Type u_1}, FreeAddMonoid.map id = AddMonoidHom.id (FreeAddMonoid α)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {k fallback : α}, (cmp k (t.minD fallback)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `HasSumLocallyUniformlyOn f g s` means that the (potentially infinite) sum
`∑' i, f i b` for `b : β` converges locally uniformly on `s` to `g b` (in the sense of
`TendstoLocallyUniformlyOn`).  -/
HasSumLocallyUniformlyOn : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} → [AddCommMonoid α] → (ι → β → α) → (β → α) → Set β → [UniformSpace α] → [TopologicalSpace β] → Prop
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_subtype_le_of_subset : ∀ {α : Type u} {p q : α → Prop}, (∀ ⦃x : α⦄, p x → q x) → Cardinal.mk (Subtype p) ≤ Cardinal.mk (Subtype q)
-- Mathlib.Data.Multiset.Bind
Multiset.bind.eq_1 : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β), s.bind f = (Multiset.map f s).join
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.comp_map_eq_const : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (s : X.PtSimplex n x) {Y : SSet}
  (φ : Y ⟶ SSet.stdSimplex.obj { len := n }) [Y.HasDimensionLT n],
  CategoryTheory.CategoryStruct.comp φ s.map = SSet.const x
-- Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
/-- An additive functor which preserves homology preserves finite limits.  -/
CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] [F.PreservesHomology]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasFiniteProducts C]
  [CategoryTheory.Limits.HasKernels C], CategoryTheory.Limits.PreservesFiniteLimits F
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₁.getKey k ⋯
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
/-- Local extension for the `positivity` tactic: A few facts that are needed many times for the
proof of Szemerédi's regularity lemma.  -/
SzemerediRegularity.Positivity.tacticSz_positivity : Lean.ParserDescr
-- Lean.Util.Trace
Lean.TraceState.mk : UInt64 → Lean.PersistentArray Lean.TraceElem → Lean.TraceState
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
SSet.Subcomplex.unionProd.pushoutObjObj_pt : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  (SSet.Subcomplex.unionProd.pushoutObjObj S T).pt = (S.unionProd T).toSSet
-- Mathlib.Order.Atoms
isAtom_iff_eq_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α] {a : α}, IsAtom a ↔ a = ⊤
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_codRestrict : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (p : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : ∀ (c : M), f c ∈ p), (LinearMap.codRestrict p f hf).ker = f.ker
-- Lean.Declaration
Lean.Declaration.inductDecl : List Lean.Name → ℕ → List Lean.InductiveType → Bool → Lean.Declaration
-- Mathlib.Algebra.Ring.BooleanRing
/-- Turn a ring homomorphism from Boolean rings `α` to `β` into a bounded lattice homomorphism
from `α` to `β` considered as Boolean algebras.  -/
RingHom.asBoolAlg : {α : Type u_1} →
  {β : Type u_2} →
    [inst : BooleanRing α] → [inst_1 : BooleanRing β] → (α →+* β) → BoundedLatticeHom (AsBoolAlg α) (AsBoolAlg β)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.isBasis_self : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → M.IsBasis I I
-- Mathlib.GroupTheory.OrderOfElement
Pi.addOrderOf : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → AddMonoid (α i)] [inst_1 : Fintype ι] (x : (i : ι) → α i),
  addOrderOf x = Finset.univ.lcm fun i => addOrderOf (x i)
-- Init.Core
PNonScalar.mk.injEq : ∀ (v v_1 : ℕ), (PNonScalar.mk v = PNonScalar.mk v_1) = (v = v_1)
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Variant of `ENNReal.rpow_add_le_mul_rpow_add_rpow'` with `p : ℝ≥0∞`.  -/
ENNReal.rpow_add_le_mul_rpow_add_rpow'' : ∀ (z₁ z₂ : ENNReal) {p : ENNReal}, (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j),
  CategoryTheory.SmallObject.SuccStruct.extendToSucc.map hj F τ i₁ i₂ hi ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi))
        (CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso F X ⟨i₂, hi₂⟩).inv)
-- Mathlib.Algebra.Group.Submonoid.Units
/-- Given some `x : M` which is a member of the submonoid of unit elements corresponding to a
subgroup of units, produce a unit of `M` whose coercion is equal to `x`.  -/
Subgroup.unit_of_mem_ofUnits : {M : Type u_1} → [inst : Monoid M] → (S : Subgroup Mˣ) → {x : M} → x ∈ S.ofUnits → Mˣ
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubMulAction.subset_closure : ∀ {R : Type u_1} {M : Type u_2} [inst : SMul R M] {s : Set M}, s ⊆ ↑(SubMulAction.closure R s)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.ite.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a a_1 a_2 : Std.Tactic.BVDecide.BoolExpr α),
  sizeOf (a.ite a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulCommClass_sphere_sphere_ball : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [SMulCommClass 𝕜 𝕜' E], SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)
-- Mathlib.RingTheory.Finiteness.Basic
/-- Pushforwards of finite submodules are finite.  -/
Module.Finite.map : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (p : Submodule R M) [Module.Finite R ↥p] (f : M →ₗ[R] N),
  Module.Finite R ↥(Submodule.map f p)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.support_C_mul_T : ∀ {R : Type u_1} [inst : Semiring R] (a : R) (n : ℤ),
  (LaurentPolynomial.C a * LaurentPolynomial.T n).coeff.support ⊆ {n}
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- `F.RightLinear C` asserts that `F` is both lax and oplax left-linear,
in a compatible way, i.e that `μᵣ` is inverse to `δᵣ`.  -/
CategoryTheory.Functor.RightLinear : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        CategoryTheory.Functor D D' →
          (C : Type u_3) →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
                  [CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] → Type (max (max u_1 u_3) v_2)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  {inst_1 : LinearOrder J} {inst_2 : SuccOrder J} {inst_3 : OrderBot J}
  {inst_4 : CategoryTheory.Limits.HasIterationOfShape J C} {inst_5 : WellFoundedLT J} {j : J} {x y : Φ.Iteration j},
  x.F = y.F → x = y
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.functorialityCompFunctoriality`.

---

Functoriality is functorial.  -/
CategoryTheory.Limits.Cocones.functorialityCompFunctoriality : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {E : Type u₅} →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} E] →
                (F : CategoryTheory.Functor J C) →
                  (G : CategoryTheory.Functor C D) →
                    (H : CategoryTheory.Functor D E) →
                      (CategoryTheory.Limits.Cocone.functoriality F G).comp
                          (CategoryTheory.Limits.Cocone.functoriality (F.comp G) H) ≅
                        CategoryTheory.Limits.Cocone.functoriality F (G.comp H)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- A numeric identifier for the BitVec variable.
 -/
Std.Tactic.BVDecide.BVBit.var : Std.Tactic.BVDecide.BVBit → ℕ
-- Mathlib.Tactic.FunProp.Theorems
/-- array of argument indices about which this theorem is about  -/
Mathlib.Meta.FunProp.FunctionTheorem.mainArgs : Mathlib.Meta.FunProp.FunctionTheorem → Array ℕ
-- Init.Prelude
/-- Creates a `UInt32` from a `BitVec 32`. This function is overridden with a native implementation.
 -/
UInt32.ofBitVec : BitVec 32 → UInt32
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stWrite.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (v : σ) (l : List (Γ k)) (f : σ → Γ k),
  Turing.TM2to1.stWrite v l (Turing.TM2to1.StAct.push f) = f v :: l
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.forget_map : ∀ {X Y : MonCat} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget MonCat).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
continuousAt_const_cpow' : ∀ {a b : ℂ}, b ≠ 0 → ContinuousAt (fun x => a ^ x) b
-- Mathlib.Order.Monotone.Defs
/-- A function `f` is strictly antitone if `a < b` implies `f b < f a`.  -/
StrictAnti : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Prop
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.sub_zsmul : ∀ {M : Type u} [inst : Lean.Grind.IntModule M] (k₁ k₂ : ℤ) (a : M), (k₁ - k₂) • a = k₁ • a - k₂ • a
-- Mathlib.Topology.Order
instTopologicalSpaceInt : TopologicalSpace ℤ
-- Mathlib.Order.Filter.Pointwise
Filter.zero_smul_filter_nonpos : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] {g : Filter β}, 0 • g ≤ 0