mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft_assoc : ∀ {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 C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft (CategoryTheory.CategoryStruct.id c) d)
      h =
    h
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem.below.base : ∀ {α : Type u_1} {S : Set (Set α)} {motive : (a : Set α) → generatePiSystem S a → Prop} {s : Set α} (h_s : s ∈ S),
  generatePiSystem.below ⋯
-- Mathlib.Algebra.Group.Basic
add_sub_right_comm : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a + b - c = a - c + b
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.buildAdditionalLocalRules : Lean.MVarId → Aesop.Frontend.RuleExpr → Lean.Elab.TermElabM (Array Aesop.LocalRuleSetMember)
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv_nhdsGE : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, Filter.Tendsto Inv.inv (nhdsWithin a (Set.Ici a)) (nhdsWithin a⁻¹ (Set.Iic a⁻¹))
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
/-- Corollary of `integrableOn_cartanKernel`: If `f : ℂ → ℂ` is meromorphic, then the function
`α ↦ ∫ β in 0..2 * π, Cartan.cartanKernel f R α β` is integrable.
 -/
ValueDistribution.Cartan.integrableOn_intervalIntegral_cartanKernel_right : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    MeasureTheory.IntegrableOn (fun x => ∫ (β : ℝ) in 0..2 * Real.pi, ValueDistribution.Cartan.cartanKernel f R x β)
      (Set.Ioc 0 (2 * Real.pi)) MeasureTheory.volume
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
IsIntegralClosure.lift.eq_1 : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] {S : Type u_4} [inst_6 : CommRing S]
  [inst_7 : Algebra R S] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R S B] [inst_10 : Algebra R A]
  [inst_11 : IsScalarTower R A B] [isIntegral : Algebra.IsIntegral R S],
  IsIntegralClosure.lift R A B =
    { toFun := fun x => IsIntegralClosure.mk' A ((algebraMap S B) x) ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
      map_add' := ⋯, commutes' := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- An `AffineTargetMorphismProperty` can be extended to a `MorphismProperty` such that it
*never* holds when the target is not affine  -/
AlgebraicGeometry.AffineTargetMorphismProperty.toProperty : AlgebraicGeometry.AffineTargetMorphismProperty → CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Mathlib.Data.Quot
Quot.Subsingleton : ∀ {α : Sort u_1} {ra : α → α → Prop} [Subsingleton α], Subsingleton (Quot ra)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_le_iff_le_comap : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {s : AffineSubspace k P₁}
  {t : AffineSubspace k P₂}, AffineSubspace.map f s ≤ t ↔ s ≤ AffineSubspace.comap f t
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `infPrime_toDual`. -/
SupPrime.dual : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, SupPrime a → InfPrime (OrderDual.toDual a)
-- Mathlib.AlgebraicGeometry.Restrict
/-- Restricting a morphism twice is isomorphic to one restriction.  -/
AlgebraicGeometry.morphismRestrictRestrict : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (U : Y.Opens) →
      (V : (↑U).Opens) →
        CategoryTheory.Arrow.mk (f ∣_ U ∣_ V) ≅
          CategoryTheory.Arrow.mk (f ∣_ (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.instDiffeologicalSpaceReal : DiffeologicalSpace ℝ
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D]
  [inst_3 : CategoryTheory.Abelian D] [P.IsSerreClass] (F : CategoryTheory.Functor D C)
  [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F],
  (P.inverseImage F).IsSerreClass
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- Notation for `Sum.elim`, scoped within the `Matrix` namespace.  -/
Matrix.«term_⊕ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.forget_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Mon.forget C).Faithful
-- Init.Omega.LinearCombo
/-- Evaluate a linear combination `⟨r, [c_1, …, c_k]⟩` at values `[v_1, …, v_k]` to obtain
`r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0))))`.
 -/
Lean.Omega.LinearCombo.eval : Lean.Omega.LinearCombo → Lean.Omega.Coeffs → ℤ
-- Mathlib.Data.Finset.Preimage
Finset.sigma_preimage_mk_of_subset : ∀ {α : Type u} {β : α → Type u_1} [inst : DecidableEq α] (s : Finset ((a : α) × β a)) {t : Finset α},
  Finset.image Sigma.fst s ⊆ t → (t.sigma fun a => s.preimage (Sigma.mk a) ⋯) = s
-- Mathlib.Data.Int.Init
/-- Immediate predecessor of an integer: `pred n = n - 1`  -/
Int.pred : ℤ → ℤ
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.powerlt_zero : ∀ {a : Cardinal.{u_1}}, a ^< 0 = 0
-- Mathlib.Order.Monotone.Monovary
Antivary.comp_right : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
  {g : ι → β}, Antivary f g → ∀ (k : ι' → ι), Antivary (f ∘ k) (g ∘ k)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.getElem?_toArray_eq : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ},
  r.toArray[i]? = Option.filter (fun x => decide (x ≤ r.upper)) (Std.PRange.succMany? i r.lower)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The additive equivalence between morphisms in `CochainComplex C ℤ` and `0`-cocycles.  -/
CochainComplex.HomComplex.Cocycle.equivHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (F G : CochainComplex C ℤ) → (F ⟶ G) ≃+ CochainComplex.HomComplex.Cocycle F G 0
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.isoClosure_eq_essImage : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, (CategoryTheory.ObjectProperty.isoClosure fun x => x ∈ Set.range F.obj) = F.essImage
-- Mathlib.Order.Filter.TendstoCofinite
/-- The class of functions `f` such that `Tendsto f cofinite cofinite`, it is equivalent to
`f` having finite fibers, see `Filter.tendstoCofinite_iff_finite_preimage_singleton`.  -/
Filter.TendstoCofinite : {α : Type u_1} → {β : Type u_2} → (α → β) → Prop
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.Functor.commShiftIso_eq_ofInduced : ∀ {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] (F : CategoryTheory.Functor C D) (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a : A),
  CategoryTheory.Functor.commShiftIso F a = (i a).symm
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.pair.injEq : ∀ (a a_1 a_2 a_3 : Nat.Partrec.Code), (a.pair a_1 = a_2.pair a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_three_mul : ∀ (x : ℝ), Real.sinh (3 * x) = 4 * Real.sinh x ^ 3 + 3 * Real.sinh x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtTreeMap.ofList l cmp).getKeyD k fallback = fallback
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.foldM_filterMapWithPostcondition.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (some c))
  (h_2 : (x : Option γ) → motive x),
  (match some c with
    | some c => h_1 c
    | x => h_2 x) =
    h_1 c
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Ioo : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a b : α i),
  Pi.single i '' Set.Ioo a b = Set.Ioo (Pi.single i a) (Pi.single i b)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.coconeOfCoconeForget_ι_app : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))) (j : J),
  (TopCat.coconeOfCoconeForget c).ι.app j =
    TopCat.ofHom { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)), continuous_toFun := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.hasPushoutVertPaste : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)],
  CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp f f') g
-- Init.Data.Vector.MapIdx
Vector.toArray_mapIdxM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  {f : ℕ → α → m β}, Vector.toArray <$> Vector.mapIdxM f xs = Array.mapIdxM f xs.toArray
-- Mathlib.Algebra.Category.Grp.Ulift
CommGrpCat.uliftFunctor_preservesLimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J CommGrpCat),
  CategoryTheory.Limits.PreservesLimit K CommGrpCat.uliftFunctor
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_erase_le : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, (↑(m.erase k)).size ≤ (↑m).size
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- The composition of `C^n` functions at points is `C^n`.  -/
ContMDiffAt.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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {n : WithTop ℕ∞} {g : M' → M''} (x : M),
  ContMDiffAt I' I'' n g (f x) → ContMDiffAt I I' n f x → ContMDiffAt I I'' n (g ∘ f) x
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.SMulAntidiagonal.eq_1 : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s : Set G} {t : Set P} (a : P) (h : (s.smulAntidiagonal t a).Finite),
  Finset.SMulAntidiagonal a h = h.toFinset
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.tsum_geometric_two : ∑' (n : ℕ), 2⁻¹ ^ n = 2
-- Mathlib.Computability.TuringMachine.Computable
/-- a time function  -/
Turing.TM2ComputableInTime.time : {α β αΓ βΓ : Type} → {ea : α → List αΓ} → {eb : β → List βΓ} → {f : α → β} → Turing.TM2ComputableInTime ea eb f → ℕ → ℕ
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instIntCast : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [IntCast β] → IntCast (MeasureTheory.SimpleFunc α β)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.Context.mk : Option Lean.Name →
  Lean.Elab.MacroStack →
    Bool →
      Bool →
        Option Lean.Elab.AutoBoundImplicitContext →
          (Lean.Name → Bool) →
            Lean.NameMap Lean.Name →
              Lean.NameMap Lean.Expr →
                Bool →
                  Bool →
                    Bool →
                      Bool →
                        Bool →
                          Bool →
                            Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot) →
                              Bool → Bool → Bool → Array Lean.Elab.Term.FixedTermElabRef → Lean.Elab.Term.Context
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.size.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.PairingHeapImp.Heap α → Sort u_2) →
    (x : Batteries.PairingHeapImp.Heap α) →
      (Unit → motive Batteries.PairingHeapImp.Heap.nil) →
        ((a : α) → (c s : Batteries.PairingHeapImp.Heap α) → motive (Batteries.PairingHeapImp.Heap.node a c s)) →
          motive x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k a : α},
  (m.erase k)[a]! = if (k == a) = true then default else m[a]!
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- If `f : G → H` is a multiplicative homomorphism between two additive monoids, then
`AddMonoidAlgebra.mapDomain f` is a ring homomorphism between their additive monoid algebras.  -/
AddMonoidAlgebra.mapDomainNonUnitalRingHom : (R : Type u_3) →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : Add M] → [inst_2 : Add N] → (M →ₙ+ N) → AddMonoidAlgebra R M →ₙ+* AddMonoidAlgebra R N
-- Init.Core
Union.mk : {α : Type u} → (α → α → α) → Union α
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isZero₂₃ : ∀ {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,
    CategoryTheory.Limits.IsZero T.obj₂ → CategoryTheory.Limits.IsZero T.obj₃ → CategoryTheory.Limits.IsZero T.obj₁
-- Aesop.EMap
Aesop.EMap.insertWith : {α : Type} → Lean.Expr → (Option α → α) → Aesop.EMap α → Lean.MetaM (Aesop.EMap α × Option α × α)
-- Mathlib.CategoryTheory.Sites.Pullback
/-- The pullback functor is left adjoint to the pushforward functor.  -/
CategoryTheory.Functor.sheafAdjunctionContinuous : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        (G : CategoryTheory.Functor C D) →
          (A : Type u₁) →
            [inst_2 : CategoryTheory.Category.{v₁, u₁} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [inst_3 : G.IsContinuous J K] →
                    [inst_4 : (G.sheafPushforwardContinuous A J K).IsRightAdjoint] →
                      G.sheafPullback A J K ⊣ G.sheafPushforwardContinuous A J K
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = true → t.getKey? a = some (t.getKey! a)
-- Lean.MetavarContext
Lean.MetavarContext.setFVarType : Lean.MetavarContext → Lean.MVarId → Lean.FVarId → Lean.Expr → Lean.MetavarContext
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The predicate for a simple graph to be bipartite.  -/
SimpleGraph.IsBipartite : {V : Type u_1} → SimpleGraph V → Prop
-- Mathlib.Computability.NFA
NFA.cons_mem_acceptsFrom : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} {a : α} {x : List α},
  a :: x ∈ M.acceptsFrom S ↔ x ∈ M.acceptsFrom (M.stepSet S a)
-- Mathlib.Algebra.Homology.HomotopyCofiber
Homotopy.equivSubZero.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D},
  Homotopy.equivSubZero =
    { toFun := fun h => { hom := fun i j => h.hom i j, zero := ⋯, comm := ⋯ },
      invFun := fun h => { hom := fun i j => h.hom i j, zero := ⋯, comm := ⋯ }, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- An isomorphism between the essential parts of `decDom` and `decCodom`.  -/
ContinuousLinearMap.FredholmPackage.equiv : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] →
                    {u : E →L[𝕜] F} → (self : u.FredholmPackage) → ↥self.decDom.X₁ ≃L[𝕜] ↥self.decCodom.X₁
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.Pushforward.id_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X)
  (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (TopCat.Presheaf.Pushforward.id ℱ).hom.app U =
    CategoryTheory.CategoryStruct.id
      (((TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.id X)).obj ℱ).obj U)
-- Init.Data.List.Nat.Pairwise
/-- The list `List.finRange n` has no duplicate entries.  -/
List.nodup_finRange : ∀ (n : ℕ), (List.finRange n).Nodup
-- Mathlib.Analysis.InnerProductSpace.CanonicalTensor
/-- The canonical contravariant tensor corresponding to the inner product  -/
InnerProductSpace.canonicalContravariantTensor : (E : Type u_1) → [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℝ E] → TensorProduct ℝ E E →ₗ[ℝ] ℝ
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHAddOffset : HAdd Std.Time.WallTime Std.Time.Day.Offset Std.Time.WallTime
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.rmatch.match_1.eq_2 : ∀ {α : Type u_1} (motive : RegularExpression α → List α → Sort u_2) (P : RegularExpression α) (a : α) (as : List α)
  (h_1 : (P : RegularExpression α) → motive P [])
  (h_2 : (P : RegularExpression α) → (a : α) → (as : List α) → motive P (a :: as)),
  (match P, a :: as with
    | P, [] => h_1 P
    | P, a :: as => h_2 P a as) =
    h_2 P a as
-- Mathlib.Analysis.Normed.Group.Basic
dist_zero_left : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), dist 0 a = ‖a‖
-- Mathlib.Analysis.SpecificLimits.Normed
/-- For a real `r > 1` we have `n = o(r ^ n)` as `n → ∞`.  -/
isLittleO_coe_const_pow_of_one_lt : ∀ {R : Type u_2} [inst : NormedRing R] {r : ℝ}, 1 < r → Nat.cast =o[Filter.atTop] fun n => r ^ n
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- In a matroid known to have finite rank, `Matroid.indep_iff_eRk_eq_encard_of_finite`
is true without the finiteness assumption.  -/
Matroid.indep_iff_eRk_eq_encard : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} [M.RankFinite], M.Indep I ↔ M.eRk I = I.encard
-- Mathlib.Algebra.Field.Rat
NNRat.divNat_eq_div : ∀ (a b : ℕ), NNRat.divNat a b = ↑a / ↑b
-- Mathlib.Topology.VectorBundle.Basic
/-- A mixin class for `Pretrivialization`, stating that a pretrivialization is fiberwise linear with
respect to given module structures on its fibers and the model fiber.  -/
Bundle.Pretrivialization.IsLinear : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : AddCommMonoid F] →
                [Module R F] →
                  [inst_5 : (x : B) → AddCommMonoid (E x)] →
                    [(x : B) → Module R (E x)] → Bundle.Pretrivialization F Bundle.TotalSpace.proj → Prop
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure.  -/
AddSubmonoidClass.toAddMonoid : {M : Type u_4} →
  [inst : AddMonoid M] → {A : Type u_5} → [inst_1 : SetLike A M] → [AddSubmonoidClass A M] → (S : A) → AddMonoid ↥S
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)} {h : k' ∈ m.alter k f},
  (m.alter k f).get k' h = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯
-- Init.Data.ByteArray.Basic
/-- Creates an iterator at the beginning of an array.  -/
ByteArray.iter : ByteArray → ByteArray.Iterator
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pullbackObjIso_hom_comp_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D)
  {Z : C} (h : F.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackObjIso f g d).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f.app d) (g.app d)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback.fst f g).app d) h
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- The evaluation at a point, as a continuous linear map from `C(X, R)₀` to `R`.  -/
ContinuousMapZero.evalCLM : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : CommSemiring R] →
            [inst_4 : IsTopologicalSemiring R] →
              (𝕜 : Type u_3) →
                [inst_5 : Semiring 𝕜] →
                  [inst_6 : Module 𝕜 R] → [inst_7 : ContinuousConstSMul 𝕜 R] → X → ContinuousMapZero X R →L[𝕜] R
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.dense_image : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  IsDenseInducing i → ∀ {s : Set α}, Dense (i '' s) ↔ Dense s
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.ModelsBoundedFormula.realize_formula : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α},
  T ⊨ᵇ φ → ∀ (M : Type u_1) [inst : L.Structure M] [M ⊨ T] [Nonempty M] {v : α → M}, φ.Realize v
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The condition that the portion of the simple graph `G` _between_ `s` and `t` is complete, that
is, every vertex in `s` is adjacent to every vertex in `t`, and vice versa.  -/
SimpleGraph.IsCompleteBetween : {V : Type u} → SimpleGraph V → Set V → Set V → Prop