mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] [inst_2 : CategoryTheory.LocallySmall.{max w' w, v₁, u₁} C],
  CategoryTheory.CategoryStruct.comp S.shrinkFunctorUliftFunctorIso.inv
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι
        CategoryTheory.uliftFunctor.{w', w}) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{max w' w, v₁, u₁} S).ι
      (CategoryTheory.shrinkYonedaUliftFunctorIso.inv.app X)
-- Mathlib.Order.Interval.Basic
Interval.map_pure : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (a : α),
  Interval.map f (Interval.pure a) = Interval.pure (f a)
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- The underlying quiver of a reflexive quiver  -/
CategoryTheory.ReflQuiv.toQuiv : CategoryTheory.ReflQuiv → CategoryTheory.Quiv
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.mem_dynEntourage : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} {x y : X},
  (x, y) ∈ Dynamics.dynEntourage T U n ↔ ∀ k < n, (T^[k] x, T^[k] y) ∈ U
-- Mathlib.Order.LiminfLimsup
Filter.liminf_top_eq_iInf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (u : β → α), Filter.liminf u ⊤ = ⨅ i, u i
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coeSubgraph_le : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (H' : H.coe.Subgraph), SimpleGraph.Subgraph.coeSubgraph H' ≤ H
-- Mathlib.Analysis.ODE.ExistUnique
/-- There exists only one global solution to an ODE $\dot x=v(t, x)$ with a given initial value
provided that the RHS is Lipschitz continuous.  -/
ODE_solution_unique_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {t₀ : ℝ},
  (∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) →
    (∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) →
      (∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) → f t₀ = g t₀ → f = g
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.then.eq_1 : ∀ (a : List ℕ), (Turing.ToPartrec.Cfg.halt a).then = fun k' => Turing.ToPartrec.stepRet k' a
-- Mathlib.Tactic.CategoryTheory.CancelIso
/-- Given expressions `C x y z f g` assumed to represent
composable morphisms `f : x ⟶ y` and `g : y ⟶ z` in a category `C`,
check if `g` is equal to the inverse of `f` by
1. first checking the objects match (i.e x = z).
2. Checking that `f` is an isomorphism by looking for an `IsIso` instance,
  allowing us to write `inv f`.
3. running `push inv` on both `inv f` and `g`, and checking that the results are equal.

If they are inverse, return a proof of `inv f = g`.
If any of the tests above fail, return none.  -/
Mathlib.Tactic.CategoryTheory.CancelIso.tryCancelPair : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Init.Data.List.Lex
List.not_le_iff_gt : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, ¬l₁ ≤ l₂ ↔ l₂ < l₁
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.div : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {u v : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} [inst_1 : Group β]
  [MeasurableDiv₂ β],
  MeasureTheory.IsProgressive f u →
    MeasureTheory.IsProgressive f v → MeasureTheory.IsProgressive f fun i ω => u i ω / v i ω
-- Mathlib.FieldTheory.Finite.GaloisField
GaloisField.finrank : ∀ (p : ℕ) [h_prime : Fact (Nat.Prime p)] {n : ℕ}, n ≠ 0 → Module.finrank (ZMod p) (GaloisField p n) = n
-- Init.Data.UInt.Basic
instMaxUInt16 : Max UInt16
-- Std.Data.ByteSlice
/-- Extracts a byte from the byte slice, or returns a default value `v₀` when the index is out of
bounds.

The index is relative to the start and end of the byte slice, rather than the underlying byte array.
 -/
ByteSlice.getD : ByteSlice → ℕ → UInt8 → UInt8
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousWithinAt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {x : α},
  LowerSemicontinuousWithinAt f s x ↔ ∀ y < f x, ∀ᶠ (x' : α) in nhdsWithin x s, y < f x'
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.unitizationAlgEquiv_symm_apply_ofLp : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A]
  [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A] (R : Type u_3) [inst_5 : CommSemiring R]
  [inst_6 : Algebra R 𝕜] [inst_7 : DistribMulAction R A] [inst_8 : IsScalarTower R 𝕜 A] (a : Unitization 𝕜 A),
  ((WithLp.unitizationAlgEquiv R).symm a).ofLp = a
-- Init.Data.SInt.Lemmas
Int16.neg_add : ∀ {a b : Int16}, -(a + b) = -a - b
-- Mathlib.Topology.Connected.Basic
/-- If any two points of a set are contained in a preconnected subset,
then the original set is preconnected as well.  -/
isPreconnected_of_forall_pair : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  (∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t) → IsPreconnected s
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- The implementation of `UpwardEnumerable.succ?` for `α` is injective.  -/
Std.PRange.LinearlyUpwardEnumerable.eq_of_succ?_eq : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} [self : Std.PRange.LinearlyUpwardEnumerable α] (a b : α),
  Std.PRange.succ? a = Std.PRange.succ? b → a = b
-- Mathlib.RingTheory.AdicCompletion.RingHom
/-- Uniqueness of the lift.
Given a compatible family of linear maps `f n : R →ₗ[R] S ⧸ (I ^ n)`.
If `F : R →+* S` makes the following diagram commute
```
  R
  | \
 F|  \ f n
  |   \
  v    v
  S --> S ⧸ (I ^ n)
```
Then it is the map `IsAdicComplete.lift`.
 -/
IsAdicComplete.eq_liftRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  [inst_2 : IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (F : R →+* S),
  (∀ (n : ℕ), (Ideal.Quotient.mk (I ^ n)).comp F = f n) → F = IsAdicComplete.liftRingHom I f ⋯
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.equivQuotMaximalIdeal.congr_simp : ∀ {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] (Rₚ : Type u_8) [inst_2 : CommRing Rₚ]
  [inst_3 : Algebra R Rₚ] [inst_4 : IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ],
  IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ = IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ
-- Std.Data.ExtHashMap.Basic
/-- Inserts multiple mappings into the hash map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.ExtHashMap.insertMany : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] →
          [LawfulHashable α] → {ρ : Type w} → [ForIn Id ρ (α × β)] → Std.ExtHashMap α β → ρ → Std.ExtHashMap α β
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.instIsContDiffCompatible : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] [inst_1 : NormedSpace ℝ X] [inst_2 : FiniteDimensional ℝ X],
  Diffeology.IsContDiffCompatible X
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
/-- The property that any morphism in a concrete category can be functorially
factored as a surjective map followed by an injective map.  -/
CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type u_2} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] → [CategoryTheory.ConcreteCategory C FC] → Prop
-- Mathlib.Analysis.RCLike.Basic
RCLike.natCast_re : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ), RCLike.re ↑n = ↑n
-- Mathlib.Data.Int.DivMod
Int.emod_eq_sub_self_emod : ∀ {a b : ℤ}, a % b = (a - b) % b
-- Mathlib.Data.Multiset.Fintype
Multiset.coe_consEquiv_of_eq_of_lt : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {v : α} (x : (v ::ₘ m).ToType) (hx : x.fst = v)
  (hx2 : ↑x.snd < Multiset.count v m), Multiset.consEquiv x = some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- The yoneda embedding for `Grp C` is fully faithful.  -/
CategoryTheory.yonedaGrpFullyFaithful : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.yonedaGrp.FullyFaithful
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.of_dvd_omega0_opow : ∀ {b : Ordinal.{0}} {e : ONote} {n : ℕ+} {a : ONote},
  (e.oadd n a).NF → Ordinal.omega0 ^ b ∣ (e.oadd n a).repr → b ≤ e.repr ∧ Ordinal.omega0 ^ b ∣ a.repr
-- Mathlib.Topology.Compactness.Paracompact
Homeomorph.paracompactSpace_iff : ∀ {X : Type v} {Y : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  ParacompactSpace X ↔ ParacompactSpace Y
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.brecOn : ∀ {α : Type u_3} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.DynkinSystem.GenerateHas s a → Prop}
  {a : Set α} (t : MeasurableSpace.DynkinSystem.GenerateHas s a),
  (∀ (a : Set α) (t : MeasurableSpace.DynkinSystem.GenerateHas s a),
      MeasurableSpace.DynkinSystem.GenerateHas.below t → motive a t) →
    motive a t
-- Mathlib.Data.Fintype.WithTopBot
instFiniteWithTop : ∀ {α : Type u_1} [Finite α], Finite (WithTop α)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- `sumFrom n lo f` is the sum of `f` over the half-open interval `[lo, n)`.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.sumFrom_eq_sum_Ico : ∀ {R : Type u_1} [inst : CommRing R] {n lo : ℕ} (f : ℕ → R), BirdDet.sumFrom n lo f = ∑ k ∈ Finset.Ico lo n, f k
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.instUnique : (V : Type u_2) → [inst : CategoryTheory.ReflQuiver V] → [Unique V] → Unique (CategoryTheory.Cat.FreeRefl V)
-- Aesop.Forward.State
Aesop.ClusterState.AddM.Context.mk : Array Lean.MVarId → Array Lean.LMVarId → Aesop.ClusterState.AddM.Context
-- Mathlib.LinearAlgebra.Matrix.StdBasis
/-- The standard basis of `Matrix m n M` given a basis on `M`.  -/
Module.Basis.matrix : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      (m : Type u_4) →
        (n : Type u_5) →
          [Fintype m] →
            [Fintype n] →
              [inst : Semiring R] →
                [inst_1 : AddCommMonoid M] →
                  [inst_2 : Module R M] → Module.Basis ι R M → Module.Basis (m × n × ι) R (Matrix m n M)
-- Mathlib.Data.TypeVec
TypeVec.prod.fst.eq_def : ∀ (x : ℕ) (x_1 x_2 : TypeVec.{u} x) (x_3 : Fin2 x),
  TypeVec.prod.fst x_3 =
    match (motive := (x : ℕ) → (x_4 x_5 : TypeVec.{u} x) → (x_6 : Fin2 x) → x_4.prod x_5 x_6 → x_4 x_6) x, x_1, x_2,
      x_3 with
    | n.succ, α, β, i.fs => TypeVec.prod.fst i
    | n.succ, x, x_4, Fin2.fz => Prod.fst
-- Mathlib.Data.Tree.Get
/-- Finds the index of an element in the tree assuming the tree has been
constructed according to the provided decidable order on its elements.
If it hasn't, the result will be incorrect. If it has, but the element
is not in the tree, returns none.  -/
BinaryTree.indexOf : {α : Type u_1} → (lt : α → α → Prop) → [DecidableRel lt] → α → BinaryTree α → Option PosNum
-- Mathlib.Data.List.Cycle
List.nextOr_eq_getElem_idxOf_succ_of_mem_dropLast : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α} (ha : a ∈ l.dropLast) (d : α),
  l.nextOr a d = l[List.idxOf a l + 1]
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.eq_of_toPoly_eq : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (a b : Lean.Grind.CommRing.Expr),
  (a.toPoly == b.toPoly) = true → Lean.Grind.CommRing.Expr.denote ctx a = Lean.Grind.CommRing.Expr.denote ctx b
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_center_homothety : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  nndist p₁ ((AffineMap.homothety p₁ c) p₂) = ‖c‖₊ * nndist p₁ p₂
-- Mathlib.RingTheory.PowerBasis
PowerBasis.mk.inj : ∀ {R : Type u_7} {S : Type u_8} {inst : CommRing R} {inst_1 : Ring S} {inst_2 : Algebra R S} {gen : S} {dim : ℕ}
  {basis : Module.Basis (Fin dim) R S} {basis_eq_pow : ∀ (i : Fin dim), basis i = gen ^ ↑i} {gen_1 : S} {dim_1 : ℕ}
  {basis_1 : Module.Basis (Fin dim_1) R S} {basis_eq_pow_1 : ∀ (i : Fin dim_1), basis_1 i = gen_1 ^ ↑i},
  { gen := gen, dim := dim, basis := basis, basis_eq_pow := basis_eq_pow } =
      { gen := gen_1, dim := dim_1, basis := basis_1, basis_eq_pow := basis_eq_pow_1 } →
    gen = gen_1 ∧ dim = dim_1 ∧ basis ≍ basis_1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.le_rpow_inv_iff : ∀ {x y : NNReal} {z : ℝ}, 0 < z → (x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y)
-- Mathlib.Algebra.Polynomial.Laurent
/-- The `R`-algebra map, taking a polynomial with coefficients in `R` to a Laurent polynomial
with coefficients in `R`.  -/
Polynomial.toLaurentAlg : {R : Type u_1} → [inst : CommSemiring R] → Polynomial R →ₐ[R] LaurentPolynomial R
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (↑(m.alter k f)).size =
        if m.contains k = true ∧ (f (m.get? k)).isNone = true then (↑m).size - 1
        else if ¬m.contains k = true ∧ (f (m.get? k)).isSome = true then (↑m).size + 1 else (↑m).size
-- Mathlib.Algebra.Group.Ext
AddCancelCommMonoid.ext_iff : ∀ {M : Type u_1} {m₁ m₂ : AddCancelCommMonoid M}, m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} [inst_2 : SizeOf α]
  (lhs rhs cin : aig.Ref), sizeOf { lhs := lhs, rhs := rhs, cin := cin } = 1 + sizeOf lhs + sizeOf rhs + sizeOf cin
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorMap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S : C}
  (X : C) {πX : X ⟶ S}
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  CategoryTheory.SmallObject.functorMap f (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk πX)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.SmallObject.functorObj f πX)
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.finsum : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_5} {F : ι → 𝕜 → 𝕜'},
  (∀ (σ : ι), Meromorphic (F σ)) → Meromorphic (∑ᶠ (σ : ι), F σ)
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.groupObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J GrpCat) → (j : J) → Group ((F.comp (CategoryTheory.forget GrpCat)).obj j)
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instSubgroupClass : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G], SubgroupClass (ClosedSubgroup G) G
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instDecidableMem : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [inst : Std.TransCmp cmp] → {m : Std.ExtTreeMap α β cmp} → {a : α} → Decidable (a ∈ m)
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.instIsDenseFunctorOppositeTypeUliftYoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.uliftYoneda.{w, v₁, u₁}.IsDense
-- Init.SimpLemmas
ite_cond_eq_true : ∀ {α : Sort u} {c : Prop} {x : Decidable c} (a b : α), c = True → (if c then a else b) = a
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isValidSearchFrom_iff_isValidSearchFrom_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos} {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidSearchFrom pat pos l ↔
    String.Slice.Pattern.Model.IsValidSearchFrom pat.toSlice pos l
-- Mathlib.Order.Closure
GaloisConnection.lowerAdjoint_toFun : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (gc : GaloisConnection l u) (a : α), gc.lowerAdjoint.toFun a = l a
-- Mathlib.NumberTheory.Cyclotomic.Basic
IntermediateField.isCyclotomicExtension_singleton_iff_eq_adjoin : ∀ (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (F : IntermediateField K L) {ζ : L}, IsPrimitiveRoot ζ n → (IsCyclotomicExtension {n} K ↥F ↔ F = K⟮ζ⟯)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.mul : ℤ → Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] {P : Ideal R} [inst_5 : P.IsPrime] [inst_6 : FaithfulSMul R S],
  IsFractionRing (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (FractionRing S)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.mul_toMatrix_mul : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} {o : Type u_6} [inst_3 : Fintype n] [inst_4 : Fintype o] [inst_5 : DecidableEq n]
  (b : Module.Basis n R₁ M₁) {M₂' : Type u_7} [inst_6 : AddCommMonoid M₂'] [inst_7 : Module R₁ M₂']
  (c : Module.Basis o R₁ M₂') [inst_8 : DecidableEq o] (B : LinearMap.BilinForm R₁ M₁) (M : Matrix o n R₁)
  (N : Matrix n o R₁),
  M * (LinearMap.BilinForm.toMatrix b) B * N =
    (LinearMap.BilinForm.toMatrix c) (B.comp ((Matrix.toLin c b) M.transpose) ((Matrix.toLin c b) N))
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
/-- The "snake input" which gives the exact sequence
`0 ⟶ ker f ⟶ ker (f ≫ g) ⟶ ker g ⟶ coker f ⟶ coker (f ≫ g) ⟶ coker g ⟶ 0`,
see `kernelCokernelCompSequence_exact`.  -/
CategoryTheory.kernelCokernelCompSequence.snakeInput : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → {X Y Z : C} → (X ⟶ Y) → (Y ⟶ Z) → CategoryTheory.ShortComplex.SnakeInput C
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pos.skip?_string_eq_skip?_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos}, pos.skip? pat = pos.skip? pat.toSlice
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedLeapSecond : Inhabited Std.Time.TimeZone.TZif.LeapSecond
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.empty : ∀ {α : Type u_2} {𝒜 : Set (Set α)}, MeasureTheory.generateSetAlgebra 𝒜 ∅
-- Init.Data.Iterators.Consumers.Partial
Std.Iter.Partial.mk.inj : ∀ {α β : Type w} {it it_1 : Std.Iter β}, { it := it } = { it := it_1 } → it = it_1
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial_constantCoeff : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Finite ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂),
  MvPolynomial.constantCoeff (LinearMap.toMvPolynomial b₁ b₂ f i) = 0
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of a product is the product of the trailing coefficients.
 -/
meromorphicTrailingCoeffAt_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜},
  (∀ σ ∈ s, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x = ∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.mem_chart_source_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (p q : TangentBundle I M),
  p ∈ (chartAt (ModelProd H E) q).source ↔ p.proj ∈ (chartAt H q.proj).source
-- Lean.Message
/-- The traced action failed (❌️, `crossEmoji`).  -/
Lean.TraceResult.failure : Lean.TraceResult
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_le_size_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, m.size - 1 ≤ (m.alter k f).size
-- Mathlib.Analysis.Convex.Join
convexJoin_union_left : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s₁ s₂ t : Set E), convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_inv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (x : F.obj a),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a)) (Sum.inl x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.coprod.inl.app a)) x
-- Batteries.Data.String.Lemmas
String.modify_of_valid : ∀ {f : Char → Char} (cs cs' : List Char),
  String.Pos.Raw.modify (String.ofList (cs ++ cs')) { byteIdx := String.utf8Len cs } f =
    String.ofList (cs ++ List.modifyHead f cs')
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.sigmaCofan_ι_app : ∀ {ι : Type v} (α : ι → TopCat) (X : CategoryTheory.Discrete ι), (TopCat.sigmaCofan α).ι.app X = TopCat.sigmaι α X.as
-- Init.Data.Int.Order
Int.neg_neg_of_pos : ∀ {a : ℤ}, 0 < a → -a < 0
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- The map into the completion has dense range.  -/
AbstractCompletion.dense : ∀ {α : Type u} [inst : UniformSpace α] (self : AbstractCompletion.{v, u} α), DenseRange self.coe
-- Init.Control.State
/-- Creates a suitable implementation of `ForIn.forIn` from a `ForM` instance.
 -/
ForM.forIn : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {ρ : Type u_3} →
      {α : Type u_4} → [Monad m] → [ForM (StateT β (ExceptT β m)) ρ α] → ρ → β → (α → β → m (ForInStep β)) → m β
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_basis_dist_le_pow : ∀ {α : Type u} [inst : PseudoMetricSpace α] {r : ℝ},
  0 < r → r < 1 → (uniformity α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 ≤ r ^ n}
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mapId_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.mapId C).inv.app X =
    (match X with
      | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of a)
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv