mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.inv_δᵣ : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.RightLinear C] (c : C) (d : D),
  CategoryTheory.inv (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c) = CategoryTheory.Functor.LaxRightLinear.μᵣ F d c
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.adj_snd : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, ¬p.Nil → G.Adj v p.snd
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_add_one_of_ne_neg_one : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R} (n : ℤ), n ≠ -1 → A ^ (n + 1) = A ^ n * A
-- Mathlib.Data.List.Permutation
List.length_foldr_permutationsAux2' : ∀ {α : Type u_1} (t : α) (ts : List α) (r L : List (List α)) (n : ℕ),
  (∀ l ∈ L, l.length = n) →
    (List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) r L).length = n * L.length + r.length
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesLimit_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [inst_3 : sInfHomClass F α β] {J : Type w} [inst_4 : CategoryTheory.Category.{w', w} J]
  (K : CategoryTheory.Functor J α), CategoryTheory.Limits.PreservesLimit K (↑f).toFunctor
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- A *(regular) continued fraction* ((r)cf) is a simple continued fraction (scf) whose partial
denominators are all positive. It is the subtype of scfs that satisfy `SimpContFract.IsContFract`.
 -/
ContFract : (α : Type u_1) → [One α] → [Zero α] → [LT α] → Type (max 0 u_1)
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.repeatEq.match_1.eq_1 : ∀ (motive : (x : ℕ) → TypeVec.{u_1} x → Sort u_2) (x : TypeVec.{u_1} 0) (h_1 : (x : TypeVec.{u_1} 0) → motive 0 x)
  (h_2 : (n : ℕ) → (α : TypeVec.{u_1} n.succ) → motive n.succ α),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, α => h_2 n α) =
    h_1 x
-- Mathlib.Algebra.RingQuot
RingQuot.instNatPow : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → NatPow (RingQuot r)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- An equivalence `E` is left adjoint to its inverse.  -/
CategoryTheory.Functor.adjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : CategoryTheory.Functor C D) → [inst_2 : E.IsEquivalence] → E ⊣ E.inv
-- Mathlib.Algebra.Group.Action.Defs
smul_smul : ∀ {M : Type u_1} {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α] (a₁ a₂ : M) (b : α),
  a₁ • a₂ • b = (a₁ * a₂) • b
-- Mathlib.Topology.Algebra.Ring.Basic
IsSemitopologicalRing.mk : ∀ {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocRing R]
  [toIsSemitopologicalSemiring : IsSemitopologicalSemiring R] [toContinuousNeg : ContinuousNeg R],
  IsSemitopologicalRing R
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.hasColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (J : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat],
  CategoryTheory.Limits.HasColimitsOfShape J (PresheafOfModules R)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
/-- This is an auxiliary correction term for proving how E2 transforms. It allows us to work with
nicer indexing sets for our infinite sums. The key is the `aux_identity` below.  -/
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.δ : (Fin 2 → ℤ) → ℂ
-- Mathlib.Algebra.Group.Action.End
/-- The tautological action by `AddAut M` on `M`.  -/
AddAut.applyAddDistribAddAction : {M : Type u_2} → [inst : AddMonoid M] → AddDistribAddAction (AddAut M) M
-- Mathlib.Data.List.Cycle
Cycle.next.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] (s s_1 : Cycle α) (e_s : s = s_1) (_hs : s.Nodup) (x x_1 : α) (e_x : x = x_1)
  (_hx : x ∈ s), s.next _hs x _hx = s_1.next ⋯ x_1 ⋯
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {α β : X ≅ Y}, α = β ↔ α.hom = β.hom
-- Mathlib.MeasureTheory.Integral.IntegrableOn
stronglyMeasurableAt_bot : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β}, StronglyMeasurableAtFilter f ⊥ μ
-- Std.Http.Data.URI.Encoding
Std.Http.URI.instDecidableIsAllowedEncodedChars : {r : UInt8 → Bool} → {s : ByteArray} → Decidable (Std.Http.URI.IsAllowedEncodedChars r s)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.card_pow_eq_one_le : ∀ {α : Type u_1} [inst : Group α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] [IsCyclic α] {n : ℕ},
  0 < n → {a | a ^ n = 1}.card ≤ n
-- Mathlib.Topology.Maps.Basic
Topology.IsCoinducing.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsCoinducing g → Topology.IsCoinducing f → Topology.IsCoinducing (g ∘ f)
-- Mathlib.Data.PNat.Notation
/-- `ℕ+` is the type of positive natural numbers. It is defined as a subtype,
and the VM representation of `ℕ+` is the same as `ℕ` because the proof
is not stored.  -/
PNat : Type
-- Init.Data.String.Decode
Char.utf8Size_le_four : ∀ (c : Char), c.utf8Size ≤ 4
-- Mathlib.Algebra.Group.Conj
isAddConj_iff : ∀ {α : Type u} [inst : AddGroup α] {a b : α}, IsAddConj a b ↔ ∃ c, c + a + -c = b
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.cyclesFunctor_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C],
  (CategoryTheory.ShortComplex.cyclesFunctor C).Additive
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D)
  [inst_2 : CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
  (a : CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A ⟶ B),
  ((CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B) a).f =
    ↑(((CategoryTheory.Limits.Cofork.IsColimit.homIso
              (CategoryTheory.Limits.colimit.isColimit
                (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))))
              B).trans
          ((adj.homEquiv A.A B).subtypeEquiv ⋯))
        a)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.coe_nonempty_iff : ∀ {α : Type u_1} {n : ℕ} {s : ↑(Set.powersetCard α n)}, (↑s).Nonempty ↔ 1 ≤ n
-- Lean.Util.NumApps
_private.Lean.Util.NumApps.0.Lean.Expr.numApps.unsafe_impl_2 : Lean.Expr → Lean.NameMap ℕ
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_pow : ∀ (a : UInt8) (n : ℕ), (a ^ n).toBitVec = a.toBitVec ^ n
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- A metric space which realizes the optimal coupling between `X` and `Y`  -/
GromovHausdorff.OptimalGHCoupling : (X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [CompactSpace X] → [Nonempty X] → [inst : MetricSpace Y] → [CompactSpace Y] → [Nonempty Y] → Type (max v u)
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The least common multiple between two elements.  -/
GCDMonoid.lcm : {α : Type u_2} → {inst : CommMonoidWithZero α} → [self : GCDMonoid α] → α → α → α
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertListIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertListIfNew l toInsert) =
    (Std.Internal.List.containsKey k l || (List.map Sigma.fst toInsert).contains k)
-- Init.Data.List.Lex
List.not_lt_nil : ∀ {α : Type u_1} [inst : LT α] (l : List α), ¬l < []
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt : ∀ {F : Type u_1} [inst : Field F] [CharZero F] {p : Polynomial F} {d : ℕ},
  p ≠ 0 → Polynomial.rootMultiplicity 1 p < d → (p.hilbertPoly d).natDegree = d - Polynomial.rootMultiplicity 1 p - 1
-- Mathlib.Combinatorics.Colex
Finset.Colex.isInitSeg_initSeg : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} [inst_1 : Fintype α],
  Finset.Colex.IsInitSeg (Finset.Colex.initSeg s) s.card
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_filter_key_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {f : α → Bool} {k : α},
  (↑m).WF →
    ((Std.DHashMap.Internal.Raw₀.filter (fun a x => f a) m).contains k = true ↔
      ∃ (h : m.contains k = true), f (m.getKey k h) = true)
-- Lean.CoreM
/-- Incremental reuse primitive: if `reusableResult?` is `none`, runs `act` and returns its result
together with the saved monadic state after `act` including the heartbeats used by it. If
`reusableResult?` on the other hand is `some (a, state)`, restores full `state` including heartbeats
used and returns `(a, state)`.

The intention is for steps that support incremental reuse to initially pass `none` as
`reusableResult?` and store the result and state in a snapshot. In a further run, if reuse is
possible, `reusableResult?` should be set to the previous result and state, ensuring that the state
after running `withRestoreOrSaveFull` is identical in both runs. Note however that necessarily this
is only an approximation in the case of heartbeats as heartbeats used by `withRestoreOrSaveFull`
itself after calling `act` as well as by reuse-handling code such as the one supplying
`reusableResult?` are not accounted for.
 -/
Lean.Core.withRestoreOrSaveFull : {α : Type} → Option (α × Lean.Core.SavedState) → Lean.CoreM α → Lean.CoreM (α × Lean.Core.SavedState)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_mono : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {φ₁ φ₂ : Prop},
  (φ₁ → φ₂) → Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂)
-- Mathlib.Control.Traversable.Instances
List.comp_traverse : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G] {α : Type u_1}
  {β γ : Type u} (f : β → F γ) (g : α → G β) (x : List α),
  List.traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) x = Functor.Comp.mk (List.traverse f <$> List.traverse g x)
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuous_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactlyCoherentSpace X], Continuous ⇑(CompactCoherentification.mk X)
-- Mathlib.Order.SuccPred.Basic
Order.Ico_succ_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ico (Order.succ a) b = Set.Ioo a b
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- **Alias** of `IsEllipticSequence.smul`. -/
IsEllSequence.smul : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R}, IsEllipticSequence W → ∀ (x : R), IsEllipticSequence (x • W)
-- Mathlib.Algebra.Category.CommHopfAlgCat
instHopfAlgebraCarrierUnopCommAlgCatOfGrpObjOpposite : {R : Type u} →
  [inst : CommRing R] → (A : (CommAlgCat R)ᵒᵖ) → [CategoryTheory.GrpObj A] → HopfAlgebra R ↑(Opposite.unop A)
-- Init.Core
Relation.TransGen.below.tail : ∀ {α : Sort u} {r : α → α → Prop} {a : α} {motive : (a_1 : α) → Relation.TransGen r a a_1 → Prop} {b c : α}
  (a_1 : Relation.TransGen r a b) (a_2 : r b c), Relation.TransGen.below a_1 → motive b a_1 → Relation.TransGen.below ⋯
-- Init.Grind.Order
Lean.Grind.Order.lt_eq_false_of_le_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] (a b : α) (k₁ k₂ : ℤ),
  (k₂ + k₁).ble' 0 = true → a ≤ b + ↑k₁ → (b < a + ↑k₂) = False
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
/-- The local inverse of an analytic function (at a point where its derivative does not vanish)
is itself analytic.  -/
AnalyticAt.analyticAt_localInverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} [inst_1 : CompleteSpace 𝕜] [CharZero 𝕜]
  (hf : AnalyticAt 𝕜 f x) (hf' : deriv f x ≠ 0),
  AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)
-- Mathlib.RingTheory.Smooth.NoetherianDescent
Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u) (B : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (n : ℕ) [Algebra.IsStandardSmoothOfRelativeDimension n A B],
  ∃ A₀ B₀ x x_1,
    A₀.FG ∧ Algebra.IsStandardSmoothOfRelativeDimension n (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct (↥A₀) A B₀)
-- Mathlib.FieldTheory.KummerExtension
isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top : ∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L],
  (primitiveRoots (Module.finrank K L) K).Nonempty →
    ∀ {a : K} {α : L},
      α ^ Module.finrank K L = (algebraMap K L) a →
        K⟮α⟯ = ⊤ → Polynomial.IsSplittingField K L (Polynomial.X ^ Module.finrank K L - Polynomial.C a)
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
subset_balancedCore : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s t : Set E}, 0 ∈ t → (∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t) → s ⊆ balancedCore 𝕜 t
-- Mathlib.Algebra.Star.StarProjection
/-- `q - p` is a star projection when `q * p = p`.  -/
IsStarProjection.sub_of_mul_eq_right : ∀ {R : Type u_1} {p q : R} [inst : NonUnitalNonAssocRing R] [inst_1 : StarRing R],
  IsStarProjection p → IsStarProjection q → q * p = p → IsStarProjection (q - p)
-- Lean.Elab.PreDefinition.WF.Fix
Lean.Elab.WF.mkFix : Lean.Elab.PreDefinition →
  Array Lean.Expr →
    Lean.Meta.ArgsPacker →
      Lean.Expr → Array Lean.Name → Array (Option Lean.Elab.DecreasingBy) → Lean.Elab.TermElabM Lean.Expr
-- Lean.Meta.Tactic.Grind.Core
/-- Ensures collection of equations to be processed is empty.  -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.resetNewFacts : Lean.Meta.Grind.GoalM Unit
-- Init.Data.Range.Polymorphic.RangeIterator
/-- The pure function mapping a range iterator of type `Iter` to the next step of the iterator.
 -/
Std.Rxc.Iterator.step : {α : Type u} →
  [Std.PRange.UpwardEnumerable α] → [inst : LE α] → [DecidableLE α] → Std.Iter α → Std.IterStep (Std.Iter α) α
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biUnion_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] (a : α) (s : Finset α) (t : α → Set β),
  ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x
-- Init.Data.List.MapIdx
List.mapIdx.go.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : ℕ → α → β) (a : Array β), List.mapIdx.go f [] a = a.toList
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.add_mk'_zero_eq_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f x + f.mk' 0 y = f.mk' x y
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_smul : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V) (c : 𝕜), (c • f).normDet = ‖c‖ ^ Module.finrank 𝕜 U * f.normDet
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.inv_mul : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n]
  (t : Matrix.TransvectionStruct n R), t.inv.toMatrix * t.toMatrix = 1
-- Mathlib.RingTheory.Kaehler.Basic
/-- The quotient ring of `S ⊗ S ⧸ J ^ 2` by `Ω[S⁄R]` is isomorphic to `S`.  -/
KaehlerDifferential.quotientCotangentIdealRingEquiv : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ (KaehlerDifferential.ideal R S).cotangentIdeal ≃+*
            S
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.eval_polynomialY : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R),
  (MvPolynomial.eval P) W'.polynomialY = 2 * P 1 * P 2 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 2
-- Mathlib.Data.Finset.Image
Finset.attach_cons : ∀ {α : Type u_1} (a : α) (s : Finset α) (ha : a ∉ s),
  (Finset.cons a s ha).attach = Finset.cons ⟨a, ⋯⟩ (Finset.map { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ } s.attach) ⋯
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.ToType.mk_symm_apply_coe : ∀ {o : Ordinal.{u_1}} (x : o.ToType),
  ↑((RelIso.symm Ordinal.ToType.mk) x) = (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding x
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ},
  CategoryTheory.Limits.coneLeftOpOfCoconeEquiv =
    CategoryTheory.Equivalence.mk''
      { obj := fun c => CategoryTheory.Limits.coneLeftOpOfCocone (Opposite.unop c),
        map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
      { obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeLeftOp c),
        map := fun {Y X} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
      (CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ))
      (CategoryTheory.Iso.refl
        ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeLeftOp c),
              map := fun {Y X} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
          { obj := fun c => CategoryTheory.Limits.coneLeftOpOfCocone (Opposite.unop c),
            map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }))
      ⋯
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.toAddZeroClass.eq_1 : ∀ {M : Type u_5} [inst : AddZeroClass M] (S : AddSubmonoid M), S.toAddZeroClass = AddSubmonoidClass.toAddZeroClass S
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [hF : F.Final] [hG : G.Final], (F.comp G).Final
-- Mathlib.Analysis.Analytic.Composition
/-- The auxiliary set corresponding to the composition of partial sums asymptotically contains
all possible compositions.  -/
FormalMultilinearSeries.compPartialSumTarget_tendsto_atTop : Filter.Tendsto (fun N => FormalMultilinearSeries.compPartialSumTarget 0 N N) Filter.atTop Filter.atTop
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.setIntegral_prod_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {L : Type u_5} [inst_4 : RCLike L]
  (f : α → L) (g : β → L) (s : Set α) (t : Set β),
  ∫ (z : α × β) in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν
-- Mathlib.Topology.Algebra.UniformField
UniformSpace.Completion.hatInv_extends : ∀ {K : Type u_1} [inst : Field K] [inst_1 : UniformSpace K] [IsTopologicalDivisionRing K] {x : K},
  x ≠ 0 → (↑x).hatInv = ↑x⁻¹
-- Mathlib.Data.List.Basic
List.getElem?_idxOf : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∈ l → l[List.idxOf a l]? = some a
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Precompiled version of `evalTermOrExprWithElab (α := Bool)` that
also makes use of the cached `item.bool?` value.
 -/
Lean.Elab.ConfigEval.evalBoolItem : Lean.Elab.ConfigEval.ConfigItem → Lean.Elab.TermElabM Bool
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_iff' : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i j k : ι),
  c.prev j = i →
    c.next j = k →
      ∀ [inst_2 : K.HasHomology j] [inst_3 : L.HasHomology j] [inst_4 : (K.sc' i j k).HasHomology]
        [inst_5 : (L.sc' i j k).HasHomology],
        QuasiIsoAt f j ↔
          CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C c i j k).map f)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωSup_le_iff : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {c : OmegaCompletePartialOrder.Chain α} {x : α},
  OmegaCompletePartialOrder.ωSup c ≤ x ↔ ∀ (i : ℕ), c i ≤ x
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The property that a morphism property `W` is stable under products indexed by a type `J`.  -/
CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Type u_1 → Prop
-- Mathlib.Order.Filter.Bases.Basic
/-- Sets of a filter basis.  -/
FilterBasis.sets : {α : Type u_6} → FilterBasis α → Set (Set α)
-- Lean.Util.Path
Lean.searchModuleNameOfFileName : System.FilePath → Lean.SearchPath → IO (Option Lean.Name)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code : Lean.Compiler.LCNF.Purity → Type
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.not_mem_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α}, a ∉ ∅
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)]
  [h₁ : HomotopicalAlgebra.Fibration f₁] [h₂ : HomotopicalAlgebra.Fibration f₂]
  [inst_5 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂] [inst_6 : CategoryTheory.Limits.HasBinaryProduct Y₁ Y₂],
  HomotopicalAlgebra.Fibration (CategoryTheory.Limits.prod.map f₁ f₂)
-- Init.Data.SInt.Lemmas
Int16.toInt8_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt8 = OfNat.ofNat n
-- Mathlib.RingTheory.Morita.Matrix
ModuleCat.toMatrixModCat_obj_carrier : ∀ (R : Type u) (ι : Type v) [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (M : ModuleCat R),
  ↑((ModuleCat.toMatrixModCat R ι).obj M) = (ι → ↑M)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_le_comap_smul : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (c : R₂), Submodule.comap f q ≤ Submodule.comap (c • f) q
-- Mathlib.Analysis.Normed.Module.Completion
UniformSpace.Completion.norm_toComplL : ∀ {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [Nontrivial E], ‖UniformSpace.Completion.toComplL‖ = 1