mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_prodMap : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁]
  [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [inst_7 : Fintype m]
  [inst_8 : DecidableEq m] [inst_9 : DecidableEq (n ⊕ m)] (φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂),
  (LinearMap.toMatrix (v₁.prod v₂) (v₁.prod v₂)) (LinearMap.prodMap φ₁ φ₂) =
    Matrix.fromBlocks ((LinearMap.toMatrix v₁ v₁) φ₁) 0 0 ((LinearMap.toMatrix v₂ v₂) φ₂)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.eq_zero_of_squarefree_of_dvd_eq_zero : ∀ {R : Type u_1} [inst : MonoidWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {m n : ℕ}, Squarefree n → m ∣ n → f m = 0 → f n = 0
-- Mathlib.Algebra.Order.Field.Power
zpow_eq_neg_one_iff₀ : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  a ^ n = -1 ↔ a = -1 ∧ Odd n
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.mk : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → ℕ → Std.IterM m β → Std.Iterators.Types.Drop α m β
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.map_one₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P}
  (f : M →+ N →+ P) (n : N), (f 0) n = 0
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.RingObjCat.X : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.RingObjCat C → C
-- Mathlib.MeasureTheory.Constructions.Pi
/-- A measure on a finite product space equals the product measure if they are equal on
rectangles.  -/
MeasureTheory.Measure.pi_eq : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  {μ' : MeasureTheory.Measure ((i : ι) → α i)},
  (∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (s i)) → μ' (Set.univ.pi s) = ∏ i, (μ i) (s i)) →
    MeasureTheory.Measure.pi μ = μ'
-- Mathlib.Algebra.Algebra.Subalgebra.Rank
Subalgebra.finrank_sup_eq_finrank_right_mul_finrank_of_free : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  [Module.Free R ↥B] [Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)],
  Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥B * Module.finrank ↥B ↥(Algebra.adjoin ↥B ↑A)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
/-- (An auxiliary definition for `functorCategoryMonoidal`.)
Tensor product of functors `C ⥤ D`, when `D` is monoidal.
 -/
CategoryTheory.Monoidal.FunctorCategory.tensorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor C D → CategoryTheory.Functor C D → CategoryTheory.Functor C D
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.instPreservesFiniteLimitsObjFunctorLeftExactFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ⥤ₗ D), CategoryTheory.Limits.PreservesFiniteLimits F.obj
-- Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
CategoryTheory.ObjectProperty.instIsStableUnderTransfiniteCompositionIsLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.isLocal.IsStableUnderTransfiniteComposition
-- Mathlib.AlgebraicGeometry.Gluing
/-- (Implementation detail)
The intersection `V` in the glue data associated to a locally directed diagram.  -/
AlgebraicGeometry.Scheme.IsLocallyDirected.V : {J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] → (i : J) → J → (F.obj i).Opens
-- Mathlib.RingTheory.Ideal.Defs
Ideal.unit_mul_mem_iff_mem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) {x y : α}, IsUnit y → (y * x ∈ I ↔ x ∈ I)
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.toPreimages_obj : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J}
  (s : Set (F.obj i)) (j : J), (F.toPreimages s).obj j = ↑(⋂ f, ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⁻¹' s)
-- Mathlib.Order.Interval.Set.Monotone
Monotone.Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  Monotone f → Antitone g → Antitone fun x => Set.Icc (f x) (g x)
-- Mathlib.Control.Monad.Cont
StateT.mkLabel : {m : Type u → Type v} → {α β σ : Type u} → MonadCont.Label (α × σ) m (β × σ) → MonadCont.Label α (StateT σ m) β
-- Mathlib.Algebra.Lie.Abelian
LieAlgebra.isFaithful_self_iff : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieModule.IsFaithful R L L ↔ LieAlgebra.center R L = ⊥
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.log_le_iff_le_exp : ∀ {G : Type u_3} [inst : Preorder G] {a : G} [inst_1 : AddGroup G] {x : WithZero (Multiplicative G)},
  x ≠ 0 → (x.log ≤ a ↔ x ≤ WithZero.exp a)
-- Mathlib.Order.Filter.Partial
Filter.mem_rcomap' : ∀ {α : Type u} {β : Type v} (r : SetRel α β) (l : Filter β) (s : Set α),
  s ∈ Filter.rcomap' r l ↔ ∃ t ∈ l, r.preimage t ⊆ s
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.resolutionMap_id : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (i : ℕ),
  ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) (CategoryTheory.CategoryStruct.id X) i =
    CategoryTheory.CategoryStruct.id (X.resolutionX i)
-- Mathlib.Order.Hom.Lattice
OrderHomClass.to_lattice_hom_apply : ∀ {F : Type u_1} (α : Type u_2) (β : Type u_3) [inst : FunLike F α β] [inst_1 : LinearOrder α] [inst_2 : Lattice β]
  [inst_3 : OrderHomClass F α β] (f : F) (a : α), (OrderHomClass.toLatticeHom α β f) a = f a
-- Batteries.Tactic.PrintPrefix
/-- Function elaborating `Config`.  -/
Batteries.Tactic.elabPrintPrefixConfig : Lean.Syntax →
  optParam Batteries.Tactic.PrintPrefixConfig { } →
    optParam Bool true → Lean.Elab.Command.CommandElabM Batteries.Tactic.PrintPrefixConfig
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.postcomp_injective : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M},
  solution.IsPresentation →
    ∀ {N : Type v'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] {f f' : M →ₗ[A] N},
      solution.postcomp f = solution.postcomp f' → f = f'
-- Mathlib.Order.Basic
le_of_forall_gt_imp_ne : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ (c : α), a < c → c ≠ b) → b ≤ a
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_le_of_mem : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n i : ι} {ω : Ω} {m : ι}, n ≤ i → i ≤ m → u i ω ∈ s → MeasureTheory.hittingBtwn u s n m ω ≤ i
-- Mathlib.GroupTheory.Congruence.Opposite
/-- The additive congruences on `M` bijects to the additive
congruences on `Mᵃᵒᵖ`  -/
AddCon.orderIsoOp : {M : Type u_1} → [inst : Add M] → AddCon M ≃o AddCon Mᵃᵒᵖ
-- Mathlib.FieldTheory.PrimitiveElement
Field.FiniteDimensional.of_finite_intermediateField : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [Finite (IntermediateField F E)], FiniteDimensional F E
-- Init.Data.SInt.Lemmas
ISize.toInt8_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt8 = OfNat.ofNat n
-- Mathlib.Algebra.Homology.Embedding.Extend
_private.Mathlib.Algebra.Homology.Embedding.Extend.0.HomologicalComplex.extend.d.match_1.eq_3 : ∀ {ι : Type u_1} (motive : Option ι → Option ι → Sort u_2) (val : ι) (h_1 : (x : Option ι) → motive none x)
  (h_2 : (i j : ι) → motive (some i) (some j)) (h_3 : (val : ι) → motive (some val) none),
  (match some val, none with
    | none, x => h_1 x
    | some i, some j => h_2 i j
    | some val, none => h_3 val) =
    h_3 val
-- Mathlib.Algebra.Group.Defs
/-- An `AddRightCancelSemigroup` is an additive semigroup such that
`a + b = c + b` implies `a = c`.  -/
AddRightCancelSemigroup : Type u → Type u
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.lintegral_preimage : ∀ {d : Type u_1} [inst : Fintype d] (f : UnitAddTorus d → ENNReal) (a : d → ℝ),
  ∫⁻ (x : UnitAddTorus d), f x = ∫⁻ (x : d → ℝ) in {x | ∀ (i : d), x i ∈ Set.Ioc (a i) (a i + 1)}, f fun i => ↑(x i)
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
/-- Auxiliary definition for `monoidalClosed`.  -/
CategoryTheory.Monoidal.Reflective.closed : {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.MonoidalCategory D] →
          [CategoryTheory.SymmetricCategory D] →
            [CategoryTheory.MonoidalClosed D] →
              [inst_5 : CategoryTheory.MonoidalCategory C] →
                {L : CategoryTheory.Functor D C} →
                  [L.Monoidal] →
                    {R : CategoryTheory.Functor C D} →
                      [R.Faithful] → [R.Full] → (L ⊣ R) → (c : C) → CategoryTheory.Closed c
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Equations to process.  -/
Lean.Meta.Grind.AC.Struct.queue : Lean.Meta.Grind.AC.Struct → Lean.Meta.Grind.AC.Queue
-- Mathlib.Data.Nat.Nth
Nat.nth_false : ∀ (n : ℕ), Nat.nth (fun x => False) n = 0
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype V] [inst_2 : DecidableRel G.Adj]
  {G' : SimpleGraph V},
  G ≤ G' →
    ∀ (c' : G'.ConnectedComponent) [inst_3 : Fintype ↑c'.supp] [inst_4 : DecidablePred fun c => c.supp ⊆ c'.supp],
      {c | c.supp ⊆ c'.supp}.disjiUnion (fun c => c.supp.toFinset) ⋯ = c'.supp.toFinset
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- A version of `Matrix.toLin' A` that produces linear equivalences.  -/
SpecialLinearGroup.toLinearEquiv : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → SpecialLinearGroup R V →* V ≃ₗ[R] V
-- Init.Data.String.Basic
String.Pos.ofSliceFrom_lt_ofSliceFrom_iff : ∀ {s : String} {p : s.Pos} {q r : (s.sliceFrom p).Pos}, String.Pos.ofSliceFrom q < String.Pos.ofSliceFrom r ↔ q < r
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ),
  p ≠ 0 → (p * Polynomial.X ^ n).natDegree = p.natDegree + n
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
Polynomial.annIdealGenerator_eq_zero_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] {a : A},
  Polynomial.annIdealGenerator 𝕜 a = 0 ↔ Polynomial.annIdeal 𝕜 a = ⊥
-- Mathlib.Algebra.Order.Monoid.Units
/-- `val : add_units α → α` as an order embedding.  -/
AddUnits.orderEmbeddingVal : {α : Type u_1} → [inst : AddMonoid α] → [inst_1 : LinearOrder α] → AddUnits α ↪o α
-- Init.Data.UInt.Lemmas
UInt32.ofNat_div : ∀ {a b : ℕ}, a < 2 ^ 32 → b < 2 ^ 32 → UInt32.ofNat (a / b) = UInt32.ofNat a / UInt32.ofNat b
-- Mathlib.Order.Compare
Ordering.Compares.eq_lt : ∀ {α : Type u_1} [inst : Preorder α] {o : Ordering} {a b : α}, o.Compares a b → (o = Ordering.lt ↔ a < b)
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan.eq_1 : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J),
  CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j =
    CategoryTheory.GradedObject.CofanMapObjFun.mk
      (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj Y) p j
      (Y j) fun a ha =>
      if ha_1 : a.1 = 0 then
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha_1).hom
          (CategoryTheory.eqToHom ⋯)
      else (CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIsInitial F X Y a ha_1).to (Y j)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AccLevelState : Type
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The kernel of `g.unop` is the opposite of `cokernel g`.  -/
CategoryTheory.kernelUnopUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B : Cᵒᵖ} → (g : A ⟶ B) → CategoryTheory.Limits.kernel g.unop ≅ Opposite.unop (CategoryTheory.Limits.cokernel g)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_le_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  BddAbove t → s.Nonempty → s ⊆ t → sSup s ≤ sSup t
-- Mathlib.Order.Filter.Defs
/-- `f.Frequently p` or `∃ᶠ x in f, p x` mean that `{x | ¬p x} ∉ f`. E.g., `∃ᶠ x in atTop, p x`
means that there exist arbitrarily large `x` for which `p` holds true.  -/
Filter.«term∃ᶠ_In_,_» : Lean.ParserDescr
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.size.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (sz : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α)
  (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (sz : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node sz l x r)),
  (match Ordnode.node sz l x r with
    | Ordnode.nil => h_1 ()
    | Ordnode.node sz l x r => h_2 sz l x r) =
    h_2 sz l x r
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.containsThenInsertIfNew₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {b : β a}, m.WF → (↑(Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨m, h⟩ a b).2).WF
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDerivWithin_succ_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} (n : ℕ) (c : F),
  iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s = 0
-- Init.Prelude
/-- Get the ending position of the syntax, if possible.
If `canonicalOnly` is true, non-canonical `synthetic` nodes are treated as not carrying
position information.
 -/
Lean.Syntax.getTailPos? : Lean.Syntax → optParam Bool false → Option String.Pos.Raw
-- Mathlib.Order.CompleteBooleanAlgebra
symmDiff_iSup_le : ∀ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ι → α} [Nonempty ι] {a : α},
  symmDiff a (⨆ i, f i) ≤ ⨆ i, symmDiff a (f i)
-- Mathlib.Data.Set.Function
Set.EqOn.trans : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ f₃ : α → β}, Set.EqOn f₁ f₂ s → Set.EqOn f₂ f₃ s → Set.EqOn f₁ f₃ s
-- Lean.Data.Lsp.Extra
/-- Array of RPC references to release.  -/
Lean.Lsp.RpcReleaseParams.refs : Lean.Lsp.RpcReleaseParams → Array Lean.Json
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_eq_left : ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, IsAddUnit a → (a + b = a ↔ b = 0)
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_pow_left_iff : ∀ {n : ℕ}, 0 < n → ∀ (a b : ℕ), (a ^ n).Coprime b ↔ a.Coprime b
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {s : σ →₀ ℕ}, (MvPolynomial.monomial s) 0 = 0
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.mul_one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.mul RingCat.Colimits.Prequotient.one) x
-- Init.Data.String.Lemmas.Pattern.Find.String
_private.Init.Data.String.Lemmas.Pattern.Find.String.0.String.Slice.contains_eq_true_of_isEmpty : ∀ {pat : String.Slice}, pat.isEmpty = true → ∀ (s : String.Slice), s.contains pat = true
-- Init.Data.UInt.Lemmas
USize.toUInt16_ofNat' : ∀ (n : ℕ), (USize.ofNat n).toUInt16 = UInt16.ofNat n
-- Mathlib.Topology.Category.Profinite.Extend
/-- A cone over `S.diagram'` whose cone point is `S`.  -/
Profinite.asLimitCone' : (S : Profinite) → CategoryTheory.Limits.Cone S.diagram'
-- Mathlib.Combinatorics.Matroid.Map
Matroid.IsBase.map : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {B : Set α},
  M.IsBase B → ∀ {f : α → β} (hf : Set.InjOn f M.E), (M.map f hf).IsBase (f '' B)
-- Init.Data.Iterators.Consumers.Loop
/-- Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldlM`.
 -/
Std.Iter.foldM : {m : Type x → Type x'} →
  [Monad m] →
    {α β : Type w} →
      {γ : Type x} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → (γ → β → m γ) → γ → Std.Iter β → m γ
-- Mathlib.Analysis.Calculus.Deriv.Abs
hasDerivAt_abs : ∀ {x : ℝ}, x ≠ 0 → HasDerivAt (fun x => |x|) (↑(SignType.sign x)) x
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- Constructor for homotopies between morphisms to a mapping cone.  -/
CochainComplex.mappingCone.liftHomotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {K : CochainComplex C ℤ} →
              (f₁ f₂ : K ⟶ CochainComplex.mappingCone φ) →
                (α : CochainComplex.HomComplex.Cochain K F 0) →
                  (β : CochainComplex.HomComplex.Cochain K G (-1)) →
                    (CochainComplex.HomComplex.Cochain.ofHom f₁).comp ↑(CochainComplex.mappingCone.fst φ) ⋯ =
                        -CochainComplex.HomComplex.δ 0 1 α +
                          (CochainComplex.HomComplex.Cochain.ofHom f₂).comp ↑(CochainComplex.mappingCone.fst φ) ⋯ →
                      (CochainComplex.HomComplex.Cochain.ofHom f₁).comp (CochainComplex.mappingCone.snd φ) ⋯ =
                          CochainComplex.HomComplex.δ (-1) 0 β + α.comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ +
                            (CochainComplex.HomComplex.Cochain.ofHom f₂).comp (CochainComplex.mappingCone.snd φ) ⋯ →
                        Homotopy f₁ f₂
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.cons.congr_simp : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g g_1 : G i) (e_g : g = g_1)
  (w w_1 : Monoid.PushoutI.NormalWord d) (e_w : w = w_1) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range),
  Monoid.PushoutI.NormalWord.cons g w hmw hgr = Monoid.PushoutI.NormalWord.cons g_1 w_1 ⋯ ⋯
-- Mathlib.Data.Nat.PrimeFin
Nat.primeFactors_eq_empty : ∀ {n : ℕ}, n.primeFactors = ∅ ↔ n = 0 ∨ n = 1
-- Init.Data.Option.Lemmas
Option.join_eq_some_iff : ∀ {α : Type u_1} {a : α} {x : Option (Option α)}, x.join = some a ↔ x = some (some a)
-- Qq.MetaM
Qq.MaybeDefEq.notDefEq : {u : Lean.Level} →
  {α :
      let u := u;
      Q(Sort u)} →
    {a b : Q(«$α»)} → Qq.MaybeDefEq a b
-- Mathlib.CategoryTheory.EssentialImage
/-- A functor `F : C ⥤ D` is essentially surjective if every object of `D` is in the essential
image of `F`. In other words, for every `Y : D`, there is some `X : C` with `F.obj X ≅ Y`.  -/
CategoryTheory.Functor.EssSurj : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Ring.Action.Group
instMulSemiringActionRingEquiv : (R : Type u_2) → [inst : Semiring R] → MulSemiringAction (R ≃+* R) R
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.map_inv_hom_id_eval_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {X Y : CategoryTheory.GradedObject J C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  (j : J) (Y_1 : D),
  CategoryTheory.CategoryStruct.comp ((F.map (e.inv j)).app Y_1) ((F.map (e.hom j)).app Y_1) =
    CategoryTheory.CategoryStruct.id ((F.obj (Y j)).obj Y_1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.coreflective : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [L.Full] [L.Faithful]
  [inst_5 : ∀ (F : CategoryTheory.Functor C H), L.HasPointwiseLeftKanExtension F], CategoryTheory.IsIso L.lanUnit
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_map_objs_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {D : Type u_1}
  [inst_1 : CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (d : D),
  d ∈ (CategoryTheory.Subgroupoid.map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = d
-- Mathlib.Combinatorics.Enumerative.DyckWord
instInhabitedDyckStep : Inhabited DyckStep
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.ext_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f g : M →ₙ* N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.LinearAlgebra.Dimension.Finite
rank_pos_iff_nontrivial : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M], 0 < Module.rank R M ↔ Nontrivial M
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.equiv'_symm_toAlgHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (g : Polynomial R)
  (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0)
  (h₂ : (Polynomial.aeval pb.gen) g = 0), ↑(AdjoinRoot.equiv' g pb h₁ h₂).symm = pb.lift (AdjoinRoot.root g) h₁
-- Mathlib.Data.Set.Sups
Set.infs_nonempty : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α}, (s ⊼ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Init.Data.UInt.Lemmas
UInt32.neg_eq_neg_one_mul : ∀ (a : UInt32), -a = -1 * a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.  -/
BitVec.reduceHShiftLeft' : Lean.Meta.Simp.DSimproc
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Composing two open partial homeomorphisms, by restricting to the maximal domain where their
composition is well defined.
Within the `Manifold` namespace, there is the notation `e ≫ₕ f` for this.  -/
Manifold.«term_≫ₕ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Distribution.Distribution
Distribution.delta_eq_zero_of_notMem : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞},
  ∀ x ∉ Ω, Distribution.delta x = 0
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
ExteriorAlgebra.GradedAlgebra.ι_sq_zero : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (m : M),
  (ExteriorAlgebra.GradedAlgebra.ι R M) m * (ExteriorAlgebra.GradedAlgebra.ι R M) m = 0