mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.exactAt_map_chainComplex_succ : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X : A) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A] (n : ℕ),
  ((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).ExactAt (n + 1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getToIntTermType? : Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.LinearAlgebra.RootSystem.Reduced
/-- See also `RootPairing.pairingIn_neg_one_neg_four_iff`.  -/
RootPairing.pairing_neg_one_neg_four_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι) [Finite ι]
  [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [Module.IsTorsionFree R N],
  P.pairing i j = -1 ∧ P.pairing j i = -4 ↔ P.root j = -2 • P.root i
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : SizeOf M] [inst_3 : SizeOf N] (toFun : M → N)
  (map_fun' :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (toFun ∘ x))
      FirstOrder.Language.Hom.map_fun'._autoParam)
  (map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (toFun ∘ x))
      FirstOrder.Language.Hom.map_rel'._autoParam),
  sizeOf { toFun := toFun, map_fun' := map_fun', map_rel' := map_rel' } = 1
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findClosestInfoWithLocalContextAt?.isBetter : Lean.Elab.ContextInfo × Lean.Elab.Info → Lean.Elab.ContextInfo × Lean.Elab.Info → Bool
-- Lean.SubExpr
Lean.SubExpr.Pos.pushLetVarType : Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Mathlib.Logic.Equiv.Basic
Function.Injective.map_swap : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → β},
  Function.Injective f → ∀ (x y z : α), f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- In a star magma (i.e., a multiplication with an antimultiplicative involutive star
operation), any star-closed subset which is also closed under multiplication is itself a star
magma.  -/
StarMemClass.instStarMul : {S : Type u_1} →
  {R : Type u_2} →
    [inst : Mul R] →
      [inst_1 : StarMul R] →
        [inst_2 : SetLike S R] → [inst_3 : MulMemClass S R] → [StarMemClass S R] → (s : S) → StarMul ↥s
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.hasZeroMorphismsPUnit : CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.Discrete PUnit.{u_1 + 1})
-- Mathlib.Algebra.Order.ToIntervalMod
_private.Mathlib.Algebra.Order.ToIntervalMod.0.toIxxMod_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (x₁ x₂ x₃ : α),
  toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx.eq_def : ∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.Balanced) (x_2 : ℕ)
  (x_3 : x_2 < x.size),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx x x_1 x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | Std.DTreeMap.Internal.Impl.inner size k v l' r', hl, n, h =>
      match h_1 : compare n l'.size with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx l' ⋯ n ⋯
      | Ordering.eq => (k, v)
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx r' ⋯ (n - l'.size - 1) ⋯
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.mk : ∀ {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  (∃ r, IsLocalization.Away r S) → Algebra.IsStandardOpenImmersion R S
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.apply_eq_iff_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) {x : α} {y : β}, e x = y ↔ x = e.symm y
-- Mathlib.Algebra.Group.TypeTags.Basic
toMul_sub : ∀ {α : Type u} [inst : Div α] (x y : Additive α), Additive.toMul (x - y) = Additive.toMul x / Additive.toMul y
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
MonoidHom.coe_finsuppProd : ∀ {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [inst : Zero β] [inst_1 : MulOneClass N]
  [inst_2 : CommMonoid P] (f : α →₀ β) (g : α → β → N →* P), ⇑(f.prod g) = f.prod fun i fi => ⇑(g i fi)
-- Mathlib.Topology.Algebra.ConstMulAction
Topology.IsInducing.continuousConstSMul : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α] {N : Type u_4}
  {β : Type u_5} [inst_3 : SMul N β] [inst_4 : TopologicalSpace β] {g : β → α},
  Topology.IsInducing g → ∀ (f : N → M), (∀ {c : N} {x : β}, g (c • x) = f c • g x) → ContinuousConstSMul N β
-- Mathlib.Topology.NhdsWithin
eventually_mem_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, ∀ᶠ (x : α) in nhdsWithin a s, x ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
_private.Mathlib.CategoryTheory.Limits.Shapes.Kernels.0.CategoryTheory.Limits.compNatIso.match_1.splitter : (motive : CategoryTheory.Limits.WalkingParallelPair → Sort u_1) →
  (j : CategoryTheory.Limits.WalkingParallelPair) →
    (Unit → motive CategoryTheory.Limits.WalkingParallelPair.zero) →
      (Unit → motive CategoryTheory.Limits.WalkingParallelPair.one) → motive j
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.degree.eq_def : ∀ (x : Lean.Grind.CommRing.Mon),
  x.degree =
    match x with
    | Lean.Grind.CommRing.Mon.unit => 0
    | Lean.Grind.CommRing.Mon.mult pw m => pw.k + m.degree
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {fallback : α}, t.get! (t.maxD fallback) = t.maxD fallback
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.H.map_id_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {F : CategoryTheory.Sheaf J AddCommGrpCat}
  {n : ℕ} (x : F.H n), (CategoryTheory.Sheaf.H.map (CategoryTheory.CategoryStruct.id F) n) x = x
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GSemiring.toGMonoid : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddMonoid ι] →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] → [self : DirectSum.GSemiring A] → GradedMonoid.GMonoid A
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {he : t.isEmpty = false} {km : α}, t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Data.PNat.Defs
Nat.toPNat'_coe : ∀ (n : ℕ), ↑n.toPNat' = if 0 < n then n else 1
-- Mathlib.Analysis.Complex.TaylorSeries
/-- A function that is complex differentiable on the open ball of radius `r ≤ ∞` around `c`
is given by evaluating its Taylor series at `c` on this open ball.  -/
Complex.taylorSeries_eq_on_eball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄
  ⦃r : ENNReal⦄,
  DifferentiableOn ℂ f (Metric.eball c r) →
    ∀ ⦃z : ℂ⦄, z ∈ Metric.eball c r → ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.monotoneOn : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  s.Subsingleton → MonotoneOn f s
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse.  -/
InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 ∨ y = 0 → ‖x‖ / Real.cos (InnerProductGeometry.angle x (x + y)) = ‖x + y‖
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
CategoryTheory.Limits.instHasFiniteCoproductsFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] [CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Limits.HasFiniteCoproducts (CategoryTheory.Functor K C)
-- Mathlib.Data.Multiset.MapFold
Multiset.foldl_swap : ∀ {α : Type u_1} {β : Type v} (f : β → α → β) [inst : RightCommutative f] (b : β) (s : Multiset α),
  Multiset.foldl f b s = Multiset.foldr (fun x y => f y x) b s
-- Mathlib.GroupTheory.GroupAction.Hom
SMulCommClass.toDistribMulActionHom_toFun : ∀ {M : Type u_13} (N : Type u_11) (A : Type u_12) [inst : Monoid N] [inst_1 : AddMonoid A] [inst_2 : DistribSMul M A]
  [inst_3 : DistribMulAction N A] [inst_4 : SMulCommClass M N A] (c : M) (x : A),
  (SMulCommClass.toDistribMulActionHom N A c) x = c • x
-- Mathlib.Lean.GoalsLocation
/-- The root expression of the position specified by the `GoalsLocation`.  -/
Lean.SubExpr.GoalsLocation.rootExpr : Lean.SubExpr.GoalsLocation → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsOpenImmersionSigmaSpec : ∀ {ι : Type u} (R : ι → CommRingCat), AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.sigmaSpec R)
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_empty : ∀ {α : Type u_1} {β : Type u_2} {f : (i : ℕ) → α → i < 0 → β}, #v[].mapFinIdx f = #v[]
-- Mathlib.Algebra.Lie.Nilpotent
LieIdeal.lcs_zero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M], I.lcs M 0 = ⊤
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_stalkSpecializes : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y),
  CategoryTheory.CategoryStruct.comp (F.germ U y hy) (F.stalkSpecializes h) = F.germ U x ⋯
-- Init.Data.SInt.Basic
/-- Obtains the `Int64` whose 2's complement representation is the given `BitVec 64`.  -/
Int64.ofBitVec : BitVec 64 → Int64
-- Lean.Data.Lsp.Internal
/-- All references for the file.  -/
Lean.Lsp.LeanIleanInfoParams.references : Lean.Lsp.LeanIleanInfoParams → Lean.Lsp.ModuleRefs
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.constOfIsEmpty_toAlternatingMap : ∀ (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : IsEmpty ι] (m : N),
  (ContinuousAlternatingMap.constOfIsEmpty R M ι m).toAlternatingMap = AlternatingMap.constOfIsEmpty R M ι m
-- Init.Data.String.Basic
String.Slice.Pos.prevAux.go : {s : String.Slice} → (off : ℕ) → off < s.utf8ByteSize → String.Pos.Raw
-- Mathlib.Data.List.Cycle
Cycle.coe_eq_coe : ∀ {α : Type u_1} {l₁ l₂ : List α}, ↑l₁ = ↑l₂ ↔ l₁ ~r l₂
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instLTSpan : LT Std.Time.Nanosecond.Span
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.homologyData₀_left_liftK : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) {T : C} (f : T ⟶ (X.chainComplex R).X 0),
  (X.homologyData₀ R).left.liftK f ⋯ = f
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.HeightOneSpectrum.instRankOneWithZeroMultiplicativeIntValuation : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsDedekindDomain R] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                [Module.Finite ℤ R] → [Module.Free ℤ R] → (IsDedekindDomain.HeightOneSpectrum.valuation K v).RankOne
-- Init.Data.Nat.Lemmas
Nat.decidableExistsLT'_eq_decidableExistsLT'TR : @Nat.decidableExistsLT' = @Nat.decidableExistsLT'TR
-- Mathlib.Order.GameAdd
Sym2.GameAdd.eq_1 : ∀ {α : Type u_1} (rα : α → α → Prop),
  Sym2.GameAdd rα =
    Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ => Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- The base change of `B[M]` to an `R`-algebra `A` is isomorphic to `(A ⊗[R] B)[M]`
as an `A`-algebra.  -/
MonoidAlgebra.rTensorEquivAlgEquiv : (R : Type u_1) →
  {M : Type u_2} →
    (S : Type u_4) →
      (A : Type u_5) →
        (B : Type u_6) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : CommSemiring A] →
                [inst_3 : CommSemiring B] →
                  [inst_4 : Algebra R S] →
                    [inst_5 : Algebra R A] →
                      [inst_6 : Algebra R B] →
                        [inst_7 : Algebra S A] →
                          [inst_8 : IsScalarTower R S A] →
                            [inst_9 : CommMonoid M] →
                              TensorProduct R A (MonoidAlgebra B M) ≃ₐ[S] MonoidAlgebra (TensorProduct R A B) M
-- Mathlib.MeasureTheory.Integral.IntegrableOn
StronglyMeasurableAtFilter.eventually : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {l : Filter α} {f : α → β}
  {μ : MeasureTheory.Measure α},
  StronglyMeasurableAtFilter f l μ → ∀ᶠ (s : Set α) in l.smallSets, MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv_def : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : RCLike 𝕜] {E : Type u_9} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) [inst_5 : DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V)
  (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ),
  DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV' =
    have b := DirectSum.IsInternal.collectedOrthonormalBasis hV' hV fun i => stdOrthonormalBasis 𝕜 ↥(V i);
    Fintype.equivFinOfCardEq ⋯
-- Mathlib.Topology.UniformSpace.Compact
Disjoint.exists_uniform_thickening : ∀ {α : Type ua} [inst : UniformSpace α] {A B : Set α},
  IsCompact A →
    IsClosed B →
      Disjoint A B → ∃ V ∈ uniformity α, Disjoint (⋃ x ∈ A, UniformSpace.ball x V) (⋃ x ∈ B, UniformSpace.ball x V)
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} (Z : C) [inst_3 : CategoryTheory.Preadditive C]
  [∀ (a : M), (CategoryTheory.shiftFunctor C a).PreservesZeroMorphisms] {a : M} (β : CategoryTheory.ShiftedHom X Y a)
  {b c : M} (h : b + a = c), β.comp 0 h = 0
-- Mathlib.Order.BooleanAlgebra.Basic
compl_sup_eq_top : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], xᶜ ⊔ x = ⊤
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- For a multiply pretransitive action, computes the index
of the `fixingSubgroup` of a subset of adequate cardinality  -/
MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mul : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α] {k : ℕ},
  MulAction.IsMultiplyPretransitive G α k →
    ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k).factorial = (Nat.card α).factorial
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax : ∀ (R : Type w) [inst : Ring R]
  [CategoryTheory.Limits.HasColimitsOfSize.{u, v, max w w', max (w + 1) (w' + 1)} AddCommGrpMax],
  CategoryTheory.Limits.PreservesColimitsOfSize.{u, v, max w w', max w w', max (w + 1) (w' + 1), max (w + 1) (w' + 1)}
    (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Init.Data.List.Impl
List.find?.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α),
  List.find? p (a :: as) =
    match p a with
    | true => some a
    | false => List.find? p as
-- Lean.Exception
Lean.instInhabitedException : Inhabited Lean.Exception
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.mkNatIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (e₀ : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ≅ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
  (e₁ : F.obj CategoryTheory.Limits.WalkingReflexivePair.one ≅ G.obj CategoryTheory.Limits.WalkingReflexivePair.one)
  (h₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀.hom =
        CategoryTheory.CategoryStruct.comp e₁.hom (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left))
      CategoryTheory.Limits.reflexivePair.mkNatIso._auto_1)
  (h₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀.hom =
        CategoryTheory.CategoryStruct.comp e₁.hom (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
      CategoryTheory.Limits.reflexivePair.mkNatIso._auto_3)
  (h₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁.hom =
        CategoryTheory.CategoryStruct.comp e₀.hom (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion))
      CategoryTheory.Limits.reflexivePair.mkNatIso._auto_5)
  (x : CategoryTheory.Limits.WalkingReflexivePair),
  (CategoryTheory.Limits.reflexivePair.mkNatIso e₀ e₁ h₁ h₂ h₃).hom.app x =
    match x with
    | CategoryTheory.Limits.WalkingReflexivePair.zero => e₀.hom
    | CategoryTheory.Limits.WalkingReflexivePair.one => e₁.hom
-- Mathlib.Control.Functor
Functor.Comp.run_seq : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Applicative F] [inst_1 : Applicative G] {α β : Type v}
  (f : Functor.Comp F G (α → β)) (x : Functor.Comp F G α), (f <*> x).run = (fun x1 x2 => x1 <*> x2) <$> f.run <*> x.run
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.right.inj : ∀ {J : CategoryTheory.Limits.MulticospanShape} {a a_1 : J.R},
  CategoryTheory.Limits.WalkingMulticospan.right a = CategoryTheory.Limits.WalkingMulticospan.right a_1 → a = a_1
-- Mathlib.Data.Analysis.Topology
instInhabitedCtopSet : {α : Type u_1} → Inhabited (Ctop α (Set α))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mk_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T),
  (CategoryTheory.CostructuredArrow.mk f).right = { as := PUnit.unit }
-- Lean.Parser.Extension
Lean.Parser.ParserResolution.alias.sizeOf_spec : ∀ (p : Lean.Parser.ParserAliasValue), sizeOf (Lean.Parser.ParserResolution.alias p) = 1 + sizeOf p
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.boxed : Lean.IR.IRType → Lean.IR.IRType
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- The (additive) monoid equivalence between `ZMod k`
and the powers of a primitive root of unity `ζ`.  -/
IsPrimitiveRoot.zmodEquivZPowers : {R : Type u_4} →
  {k : ℕ} → [inst : CommRing R] → {ζ : Rˣ} → IsPrimitiveRoot ζ k → ZMod k ≃+ Additive ↥(Subgroup.zpowers ζ)
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.representableBy.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x x_1 : F.obj (Opposite.op X)} (e_x : x = x_1) (h : F.IsRepresentedBy x), h.representableBy = ⋯.representableBy
-- Init.Data.SInt.Bitwise
Int32.toInt8_xor : ∀ (a b : Int32), (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
-- Init.Sym.Lemmas
Lean.Sym.UInt8.le_eq_false : ∀ (a b : UInt8), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap_injective : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W), Function.Injective fun f => f.toLinearMap
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.brecOn.go : {motive : Mathlib.Tactic.ITauto.IProp → Sort u} →
  (t : Mathlib.Tactic.ITauto.IProp) →
    ((t : Mathlib.Tactic.ITauto.IProp) → Mathlib.Tactic.ITauto.IProp.below t → motive t) →
      motive t ×' Mathlib.Tactic.ITauto.IProp.below t
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- The residue of the Hurwitz zeta function at `s = 1` is `1`.  -/
HurwitzZeta.hurwitzZeta_residue_one : ∀ (a : UnitAddCircle), Filter.Tendsto (fun s => (s - 1) * HurwitzZeta.hurwitzZeta a s) (nhdsWithin 1 {1}ᶜ) (nhds 1)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatch_iff_isLongestRevMatch_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch p pos ↔
    String.Slice.Pattern.Model.IsLongestRevMatch (fun x => decide (p x)) pos
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.mkTupleHint.prodArity : Lean.Expr → ℕ
-- Init.Core
String.ofByteArray.inj : ∀ {toByteArray : ByteArray} {isValidUTF8 : toByteArray.IsValidUTF8} {toByteArray_1 : ByteArray}
  {isValidUTF8_1 : toByteArray_1.IsValidUTF8},
  { toByteArray := toByteArray, isValidUTF8 := isValidUTF8 } =
      { toByteArray := toByteArray_1, isValidUTF8 := isValidUTF8_1 } →
    toByteArray = toByteArray_1
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.toOpenPartialHomeomorph_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) (x : E),
  ↑φ.toOpenPartialHomeomorph x = (φ.leftFun x, φ.rightFun x)
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.monotone_cod : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Monotone fun f => f.cod
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.exists_mem_sup : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p p' : Submodule R M) {P : M → Prop}, (∃ x ∈ p ⊔ p', P x) ↔ ∃ x₁ ∈ p, ∃ x₂ ∈ p', P (x₁ + x₂)