mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Basic
/-- Each element of the monoid defines a monoid homomorphism.  -/
MulDistribMulAction.toMonoidEnd : (M : Type u_2) →
  (A : Type u_3) → [inst : Monoid M] → [inst_1 : Monoid A] → [MulDistribMulAction M A] → M →* Monoid.End A
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.copyIndep_IsBase : ∀ {α : Type u_1} (M : Matroid α) (E : Set α) (Indep : Set α → Prop) (hE : E = M.E)
  (h : ∀ (I : Set α), Indep I ↔ M.Indep I) (a : Set α), (M.copyIndep E Indep hE h).IsBase a = M.IsBase a
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the first quadrant. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open first quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open first quadrant
  for some `A`, `B`, and `c < 2`;
* `f` is equal to zero on the boundary of the first quadrant.

Then `f` is equal to zero on the closed first quadrant.  -/
PhragmenLindelof.eq_zero_on_quadrant_I : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
  DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (∀ (x : ℝ), 0 ≤ x → f ↑x = 0) →
        (∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = 0) → Set.EqOn f 0 {z | 0 ≤ z.re ∧ 0 ≤ z.im}
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symmL_continuousLinearMapAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet →
    ∀ (y : E b), (Bundle.Trivialization.symmL R e b) ((Bundle.Trivialization.continuousLinearMapAt R e b) y) = y
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.isPrime_map_quotientMk_of_isPrime : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] {p : Ideal R} [p.IsPrime],
  I ≤ p → (Ideal.map (Ideal.Quotient.mk I) p).IsPrime
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.insertManyIfNew_list_eq_foldl : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β}
  {l : List ((a : α) × β a)}, ↑(m.insertManyIfNew l) = List.foldl (fun a b => a.insertIfNew b.fst b.snd) m l
-- Mathlib.Algebra.Algebra.Bilinear
NonUnitalAlgHom.comp_mul' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : Module R B] [inst_7 : SMulCommClass R B B]
  [inst_8 : IsScalarTower R B B] (f : A →ₙₐ[R] B),
  ↑f ∘ₗ LinearMap.mul' R A = LinearMap.mul' R B ∘ₗ TensorProduct.map ↑f ↑f
-- Init.Data.UInt.Lemmas
USize.ofNatLT_div : ∀ {a b : ℕ} (ha : a < 2 ^ System.Platform.numBits) (hb : b < 2 ^ System.Platform.numBits),
  USize.ofNatLT (a / b) ⋯ = USize.ofNatLT a ha / USize.ofNatLT b hb
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- If a monotone function `u : ι → α` tends to `atBot` along *some* non-trivial filter `l`, then
it tends to `atBot` along `atBot`.  -/
Filter.tendsto_atBot_of_monotone_of_filter : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : Preorder α] {l : Filter ι} {u : ι → α},
  Monotone u → ∀ [l.NeBot], Filter.Tendsto u l Filter.atBot → Filter.Tendsto u Filter.atBot Filter.atBot
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod.eq_1 : ∀ {M : Type u_3} [inst : CommMonoid M], Multiset.prod = Multiset.foldr (fun x1 x2 => x1 * x2) 1
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.mem_comap : ∀ {α : Type u} {β : Type v} {m : α → β} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m ∈ u)
  {s : Set α}, s ∈ u.comap inj large ↔ m '' s ∈ u
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ` tends to zero exponentially:
for some `0 < a < 1`, `‖p n‖ rⁿ = o(aⁿ)`.  -/
FormalMultilinearSeries.isLittleO_of_lt_radius : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
  ↑r < p.radius → ∃ a ∈ Set.Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[Filter.atTop] fun x => a ^ x
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns a list of all values present in the tree map in ascending  order.  -/
Std.DTreeMap.Raw.values : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → List β
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.modify.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp]
  (t t_1 : Std.ExtDTreeMap α (fun x => β) cmp),
  t = t_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (f f_1 : β → β), f = f_1 → Std.ExtDTreeMap.Const.modify t a f = Std.ExtDTreeMap.Const.modify t_1 a_1 f_1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- `Multifork.ofPiFork` as a functor.  -/
CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        {c : CategoryTheory.Limits.Fan I.left} →
          {d : CategoryTheory.Limits.Fan I.right} →
            (hd : CategoryTheory.Limits.IsLimit d) →
              CategoryTheory.Functor (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd))
                (CategoryTheory.Limits.Multifork I)
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.instPreservesColimitsOfShapeFunctorLim : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] {D : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} D] [CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_5 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.Limits.lim],
  CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.Limits.lim
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- Open immersions are stable under base-change.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (CategoryTheory.Limits.pullback.fst g f)
-- Init.Data.List.Find
List.IsPrefix.findIdx_le : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁ <+: l₂ → List.findIdx p l₁ ≤ List.findIdx p l₂
-- Init.Prelude
/-- Some value of type `α`.  -/
Option.some : {α : Type u} → α → Option α
-- Mathlib.Order.Ideal
/-- **Alias** of the reverse direction of `Order.Ideal.biSup_mem_iff`. -/
Order.Ideal.biSup_mem : ∀ {P : Type u_1} [inst : CompleteLattice P] {I : Order.Ideal P} {α : Type u_2} {f : α → P} {s : Set α},
  s.Finite → (∀ i ∈ s, f i ∈ I) → ⨆ i ∈ s, f i ∈ I
-- Lean.Parser.Types
Lean.Parser.Parser.mk.inj : ∀ {info : Lean.Parser.ParserInfo} {fn : Lean.Parser.ParserFn} {info_1 : Lean.Parser.ParserInfo}
  {fn_1 : Lean.Parser.ParserFn}, { info := info, fn := fn } = { info := info_1, fn := fn_1 } → info = info_1 ∧ fn = fn_1
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Partial order on Dyck words: `p ≤ q` if a (possibly empty) sequence of
`insidePart` and `outsidePart` operations can turn `q` into `p`.  -/
DyckWord.instPartialOrder : PartialOrder DyckWord
-- Mathlib.Analysis.Convex.Segment
Ioo_subset_openSegment : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜},
  Set.Ioo x y ⊆ openSegment 𝕜 x y
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.foldr.match_1.splitter : {α : Type u_1} →
  {σ : Sort u_3} →
    (motive : RBTree.RBNode α → σ → Sort u_2) →
      (x : RBTree.RBNode α) →
        (x_1 : σ) →
          ((b : σ) → motive RBTree.RBNode.nil b) →
            ((c : RBTree.RBColor) →
                (l : RBTree.RBNode α) →
                  (v : α) → (r : RBTree.RBNode α) → (b : σ) → motive (RBTree.RBNode.node c l v r) b) →
              motive x x_1
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.get! : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → [Inhabited β] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → β
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.norm_natCast_zmodRepr_eq_one_iff : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {x : ℤ_[p]}, ‖↑x.zmodRepr‖ = 1 ↔ ‖x‖ = 1
-- Init.Data.List.Impl
List.insertIdx.eq_1 : ∀ {α : Type u} (xs : List α) (i : ℕ) (a : α), xs.insertIdx i a = xs.modifyTailIdx i (List.cons a)
-- Init.Data.UInt.Bitwise
UInt32.ofBitVec_or : ∀ (a b : BitVec 32), { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from groups to monoids preserves all limits.

This means the underlying monoid of a limit can be computed as a limit in the category of monoids.
 -/
GrpCat.forget₂Mon_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ GrpCat MonCat)
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.absNorm_pow_inertiaDeg : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [Module.Finite R S] [q.IsPrime] [q.LiesOver p] [inst_6 : IsDedekindDomain R]
  [inst_7 : IsDedekindDomain S] [inst_8 : Module.Free ℤ R] [inst_9 : Module.Free ℤ S],
  Ideal.absNorm p ^ q.inertiaDeg R = Ideal.absNorm q
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.TryTacticM : Type → Type
-- Mathlib.Algebra.WithConv
WithConv.toConv_bijective : ∀ {A : Type u_2}, Function.Bijective WithConv.toConv
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.unop_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} {Z' : C}
  {h : Opposite.unop X ⟶ Z'},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).unop h =
    CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.CategoryStruct.comp f.unop h)
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂RightOrthogonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty 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]
  [inst_5 : CategoryTheory.Pretriangulated C], P.rightOrthogonal.IsTriangulatedClosed₂
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.iUnion_filter_not : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop),
  (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion
-- Mathlib.Algebra.Module.ZLattice.Covolume
/-- A more general version of `covolume_div_covolume_eq_relIndex`;
see the `Naming conventions` section in the introduction.
 -/
ZLattice.covolume_div_covolume_eq_relIndex' : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (L₁ L₂ : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L₁]
  [IsZLattice ℝ L₁] [inst_7 : DiscreteTopology ↥L₂] [IsZLattice ℝ L₂],
  L₁ ≤ L₂ →
    ZLattice.covolume L₁ MeasureTheory.volume / ZLattice.covolume L₂ MeasureTheory.volume =
      ↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.sub_fst : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x y : WithCStarModule A (E × F)) [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F], (x - y).1 = x.1 - y.1
-- Lean.MetavarContext
Lean.MetavarContext.mk.inj : ∀ {depth levelAssignDepth lmvarCounter mvarCounter : ℕ}
  {lDecls : Lean.PersistentHashMap Lean.LMVarId Lean.LevelMetavarDecl}
  {decls : Lean.PersistentHashMap Lean.MVarId Lean.MetavarDecl}
  {userNames : Lean.PersistentHashMap Lean.Name Lean.MVarId}
  {lAssignment : Lean.PersistentHashMap Lean.LMVarId Lean.Level}
  {eAssignment : Lean.PersistentHashMap Lean.MVarId Lean.Expr}
  {dAssignment : Lean.PersistentHashMap Lean.MVarId Lean.DelayedMetavarAssignment}
  {depth_1 levelAssignDepth_1 lmvarCounter_1 mvarCounter_1 : ℕ}
  {lDecls_1 : Lean.PersistentHashMap Lean.LMVarId Lean.LevelMetavarDecl}
  {decls_1 : Lean.PersistentHashMap Lean.MVarId Lean.MetavarDecl}
  {userNames_1 : Lean.PersistentHashMap Lean.Name Lean.MVarId}
  {lAssignment_1 : Lean.PersistentHashMap Lean.LMVarId Lean.Level}
  {eAssignment_1 : Lean.PersistentHashMap Lean.MVarId Lean.Expr}
  {dAssignment_1 : Lean.PersistentHashMap Lean.MVarId Lean.DelayedMetavarAssignment},
  { depth := depth, levelAssignDepth := levelAssignDepth, lmvarCounter := lmvarCounter, mvarCounter := mvarCounter,
        lDecls := lDecls, decls := decls, userNames := userNames, lAssignment := lAssignment,
        eAssignment := eAssignment, dAssignment := dAssignment } =
      { depth := depth_1, levelAssignDepth := levelAssignDepth_1, lmvarCounter := lmvarCounter_1,
        mvarCounter := mvarCounter_1, lDecls := lDecls_1, decls := decls_1, userNames := userNames_1,
        lAssignment := lAssignment_1, eAssignment := eAssignment_1, dAssignment := dAssignment_1 } →
    depth = depth_1 ∧
      levelAssignDepth = levelAssignDepth_1 ∧
        lmvarCounter = lmvarCounter_1 ∧
          mvarCounter = mvarCounter_1 ∧
            lDecls = lDecls_1 ∧
              decls = decls_1 ∧
                userNames = userNames_1 ∧
                  lAssignment = lAssignment_1 ∧ eAssignment = eAssignment_1 ∧ dAssignment = dAssignment_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.contains'_compare : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {l : Std.DTreeMap.Internal.Impl α β},
  Std.DTreeMap.Internal.Impl.contains' (compare k) l = Std.DTreeMap.Internal.Impl.contains k l
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Differentiable.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → (∀ (x : E), f x ≠ 0) → Differentiable ℝ fun x => Real.log (f x)
-- Mathlib.Topology.Connected.PathConnected
/-- A path-connected space must be nonempty.  -/
PathConnectedSpace.nonempty : ∀ {X : Type u_4} {inst : TopologicalSpace X} [self : PathConnectedSpace X], Nonempty X
-- Mathlib.Order.Fin.Finset
Fin.orderIsoTriple_two : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableEq α] (a b c : α) (hab : a < b) (hbc : b < c),
  ↑((Fin.orderIsoTriple a b c hab hbc) 2) = c
-- Mathlib.Order.Sublattice
Sublattice.mk.inj : ∀ {α : Type u_2} {inst : Lattice α} {carrier : Set α} {supClosed' : SupClosed carrier} {infClosed' : InfClosed carrier}
  {carrier_1 : Set α} {supClosed'_1 : SupClosed carrier_1} {infClosed'_1 : InfClosed carrier_1},
  { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' } =
      { carrier := carrier_1, supClosed' := supClosed'_1, infClosed' := infClosed'_1 } →
    carrier = carrier_1
-- Mathlib.Order.Directed
DirectedOn.proj : ∀ {ι : Type u_5} {α : ι → Type u_6} {r : (i : ι) → α i → α i → Prop} {d : Set ((i : ι) → α i)},
  DirectedOn (fun x y => ∀ (i : ι), r i (x i) (y i)) d → ∀ (i : ι), DirectedOn (r i) ((fun a => a i) '' d)
-- Mathlib.Algebra.Star.Basic
star_injective : ∀ {R : Type u} [inst : InvolutiveStar R], Function.Injective star
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.coeff_inv : ∀ {k : Type u_2} [inst : Field k] (n : ℕ) (φ : PowerSeries k),
  (PowerSeries.coeff n) φ⁻¹ =
    if n = 0 then (PowerSeries.constantCoeff φ)⁻¹
    else
      -(PowerSeries.constantCoeff φ)⁻¹ *
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          if x.2 < n then (PowerSeries.coeff x.1) φ * (PowerSeries.coeff x.2) φ⁻¹ else 0
-- Init.Data.Array.MinMax
Array.max?_singleton_append : ∀ {α : Type u_1} {x : α} [inst : Max α] [Std.Associative max] {xs : Array α},
  (#[x] ++ xs).max? = some (xs.max?.elim x (max x))
-- Mathlib.Algebra.Quandle
/-- Given a homomorphism from a rack to a group, it factors through the enveloping group.
 -/
Rack.toEnvelGroup.univ : ∀ (R : Type u_1) [inst : Rack R] (G : Type u_2) [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G)),
  (Quandle.Conj.map (Rack.toEnvelGroup.map f)).comp (Rack.toEnvelGroup R) = f
-- Batteries.Data.Fin.Lemmas
Fin.find?_eq_find?_finRange : ∀ {n : ℕ} {p : Fin n → Bool}, Fin.find? p = List.find? p (List.finRange n)
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.sigmaFunctor_map : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] [inst_1 : UnivLE.{v, u}]
  {X Y : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Cover.sigmaFunctor.map f = AlgebraicGeometry.Scheme.Cover.Hom.sigma f
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.of_one_hadamard : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} [inst : MulOneClass α] (A : Matrix m n α), (Matrix.of 1).hadamard A = A
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_subtype_iff_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α} {s : Set β},
  HasSum (f ∘ Subtype.val) a ↔ HasSum (s.indicator f) a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ : Std.TreeMap α β cmp} {l : List (α × β)},
  (t₁.insertMany l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) t₁ l)
-- Init.Data.String.Basic
String.Slice.startPos_copy : ∀ {s : String.Slice}, s.copy.startPos = s.startPos.copy
-- Mathlib.Topology.KrullDimension
/-- The topological Krull dimension of any subspace is at most the dimension of the
ambient space.  -/
topologicalKrullDim_subspace_le : ∀ (X : Type u_3) [inst : TopologicalSpace X] (Y : Set X), topologicalKrullDim ↑Y ≤ topologicalKrullDim X
-- Mathlib.Data.Finset.Option
Finset.card_eraseNone_eq_card_erase : ∀ {α : Type u_1} [inst : DecidableEq (Option α)] (s : Finset (Option α)),
  (Finset.eraseNone s).card = (s.erase none).card
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.specTargetImageFactorization_app_injective : ∀ {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.Spec A),
  Function.Injective
    ⇑(CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.specTargetImageFactorization f)))
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.brecOn.go : {n : ℕ} →
  {P : MvPFunctor.{u} (n + 1)} →
    {motive : (a : P.last.W) → (a_1 : Fin2 n) → P.WPath a a_1 → Sort u_1} →
      {a : P.last.W} →
        {a_1 : Fin2 n} →
          (t : P.WPath a a_1) →
            ((a : P.last.W) → (a_2 : Fin2 n) → (t : P.WPath a a_2) → MvPFunctor.WPath.below t → motive a a_2 t) →
              motive a a_1 t ×' MvPFunctor.WPath.below t
-- Lean.Elab.PreDefinition.Basic
_private.Lean.Elab.PreDefinition.Basic.0.Lean.Elab.compileDecl : Lean.Declaration → Lean.Elab.TermElabM Unit
-- Mathlib.Data.Fintype.Sets
Subtype.fintype : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → [Fintype α] → Fintype { x // p x }
-- Mathlib.Computability.TuringMachine.Tape
/-- Apply a function to a value stored at the nth position of the list.  -/
Turing.ListBlank.modifyNth : {Γ : Type u_1} → [inst : Inhabited Γ] → (Γ → Γ) → ℕ → Turing.ListBlank Γ → Turing.ListBlank Γ
-- Mathlib.Data.NNReal.Defs
NNReal.instIsOrderedRing_1 : IsOrderedRing NNReal
-- Lean.ProjFns
Lean.instReprProjectionFunctionInfo : Repr Lean.ProjectionFunctionInfo
-- Init.SimpLemmas
/-- `Arrow α β` is definitionally equal to `α → β`, but represented as a function
application rather than `Expr.forallE`.

This representation is useful for proof automation that builds nested implications
like `pₙ → ... → p₂ → p₁`. With `Expr.forallE`, each nesting level introduces a
binder that bumps de Bruijn indices in subterms, destroying sharing even with
hash-consing. For example, if `p₁` contains `#20`, then at depth 2 it becomes `#21`,
at depth 3 it becomes `#22`, etc., causing quadratic proof growth.

With `arrow`, both arguments are explicit (not under binders), so subterms remain
identical across nesting levels and can be shared, yielding linear-sized proofs.
 -/
Lean.Arrow : Sort u → Sort v → Sort (imax u v)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_nonempty : ∀ {V : Type u} {G : SimpleGraph V}, G.edgeSet.Nonempty ↔ G ≠ ⊥
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.isLocalDiffeomorphAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] (I : ModelWithCorners 𝕜 E H₁)
  (J : ModelWithCorners 𝕜 F H₂) {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] (n : WithTop ℕ∞) (φ : PartialDiffeomorph I J M N n)
  {x : M}, x ∈ φ.source → IsLocalDiffeomorphAt I J n (↑φ.toPartialEquiv) x
-- Mathlib.Data.PNat.Basic
instAddLeftCancelSemigroupPNat : AddLeftCancelSemigroup ℕ+
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Group the balls into disjoint families, by assigning to a ball the smallest color for which
it does not intersect any already chosen ball of this color.  -/
Besicovitch.TauPackage.color : {α : Type u_1} → [MetricSpace α] → {β : Type u} → [Nonempty β] → Besicovitch.TauPackage β α → Ordinal.{u} → ℕ
-- Lean.Message
/-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag`
is true.

This does not descend into lazily generated subtrees (`.ofLazy`); message tags
of interest (like those added by `logLinter`) are expected to be near the root
of the `MessageData`, and not hidden inside `.ofLazy`.
 -/
Lean.MessageData.hasTag : (Lean.Name → Bool) → Lean.MessageData → Bool
-- Init.Data.BitVec.Lemmas
BitVec.getElem_rotateRight : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ} (h : i < w),
  (x.rotateRight r)[i] = if h' : i < w - r % w then x[r % w + i] else x[i - (w - r % w)]
-- Mathlib.Algebra.Lie.Basic
/-- The identity map is a Lie algebra morphism.  -/
LieHom.instOne : {R : Type u} →
  {L₁ : Type v} → [inst : CommRing R] → [inst_1 : LieRing L₁] → [inst_2 : LieAlgebra R L₁] → One (L₁ →ₗ⁅R⁆ L₁)
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- An equivalence of bialgebras is an invertible bialgebra homomorphism.  -/
«term_≃ₐc[_]_» : Lean.TrailingParserDescr
-- Mathlib.ModelTheory.Substructures
/-- The range of a first-order hom `f : M → N` is a submodule of `N`.
See Note [range copy pattern].  -/
FirstOrder.Language.Hom.range : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type u_1} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Hom M N → L.Substructure N
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.map_zero_mem_openCell`. -/
Topology.CWComplex.map_zero_mem_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), ↑(Topology.RelCWComplex.map n i) 0 ∈ Topology.RelCWComplex.openCell n i