mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Bases
TopologicalSpace.instSecondCountableTopologyForallOfCountable : ∀ {ι : Type u_1} {X : ι → Type u_2} [Countable ι] [inst : (a : ι) → TopologicalSpace (X a)]
  [∀ (a : ι), SecondCountableTopology (X a)], SecondCountableTopology ((a : ι) → X a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The proposition that a projective point class on a Weierstrass curve `W` is nonsingular.

If `P` is a projective point representative on `W`, then `W.NonsingularLift ⟦P⟧` is definitionally
equivalent to `W.Nonsingular P`.

Note that this definition is only mathematically accurate for fields.  -/
WeierstrassCurve.Projective.NonsingularLift : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Projective R → WeierstrassCurve.Projective.PointClass R → Prop
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- If `s` is not in `-ℕ`, and either `a ≠ 0` or `s ≠ 1`, then
`hurwitzZetaEven a (1 - s)` is an explicit multiple of `cosZeta s`.  -/
HurwitzZeta.hurwitzZetaEven_one_sub : ∀ (a : UnitAddCircle) {s : ℂ},
  (∀ (n : ℕ), s ≠ -↑n) →
    a ≠ 0 ∨ s ≠ 1 →
      HurwitzZeta.hurwitzZetaEven a (1 - s) =
        2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.cos (↑Real.pi * s / 2) * HurwitzZeta.cosZeta a s
-- Lean.Elab.Do.Legacy
/-- If the given syntax is a `doIf`, return an equivalent `doIf` that has an `else` but no `else if`s or `if let`s.   -/
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.expandDoIf? : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)
-- Init.Data.List.BasicAux
List.instAntisymmLeOfTrichotomousLt : ∀ {α : Type u_1} [inst : LT α] [s : Std.Trichotomous fun x1 x2 => x1 < x2], Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.π₀.mk_eq_mk_iff : ∀ {X : SSet} (x₀ x₁ : X.obj (Opposite.op { len := 0 })),
  SSet.π₀.mk x₀ = SSet.π₀.mk x₁ ↔ Relation.EqvGen SSet.π₀Rel x₀ x₁
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_succ_right_eq_cons_map : ∀ {m n : ℕ}, m ≤ n → (m...n + 1).toList = m :: List.map (fun x => x + 1) (m...n).toList
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_transpose_add_self : ∀ {α : Type u_1} {n : Type u_4} [inst : AddCommMonoid α] [inst_1 : StarAddMonoid α] (A : Matrix n n α),
  (A.conjTranspose + A).IsHermitian
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkAndCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.mkAndCached input = aig.mkGateCached input
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Pos.find?_char_eq_some_iff_splits : ∀ {c : Char} {s : String} {pos : s.Pos} {t u : String},
  pos.Splits t u →
    ∀ {pos' : s.Pos}, pos.find? c = some pos' ↔ ∃ v w, pos'.Splits (t ++ v) (String.singleton c ++ w) ∧ c ∉ v.toList
-- Mathlib.Computability.Language
Language.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
  Language.map f = { toFun := Set.image (List.map f), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.traj_apply : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) (x : (i : ↥(Finset.Iic a)) → X ↑i),
  (ProbabilityTheory.Kernel.traj κ a) x = ProbabilityTheory.Kernel.trajFun κ a x
-- Init.Data.Nat.Basic
Nat.pow_lt_pow_left : ∀ {a b n : ℕ}, a < b → n ≠ 0 → a ^ n < b ^ n
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.iSup_mul : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {ι : Sort u_4} (S : ι → AddSubmonoid R) (T : AddSubmonoid R),
  (⨆ i, S i) * T = ⨆ i, S i * T
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey? k = m₁.getKey? k
-- Std.Time.Date.Unit.Month
/-- Converts a `Ordinal` into a `Offset`.
 -/
Std.Time.Month.Ordinal.toOffset : Std.Time.Month.Ordinal → Std.Time.Month.Offset
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.one_eq_zero_unsat_cert.eq_1 : ∀ (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.one_eq_zero_unsat_cert p =
    (p.beq' (Lean.Grind.CommRing.Poly.num 1) || p.beq' (Lean.Grind.CommRing.Poly.num (-1)))
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.refineOneHypercover_I₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  [inst_1 : E.HasPullbacks]
  (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀),
  (E.refineOneHypercover F).I₁ i j = (F i j).I₀
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.instInhabitedHomLaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → {F G : CategoryTheory.LaxFunctor B C} → {η : F ⟶ G} → Inhabited (η ⟶ η)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addSemigroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddSemigroup (f i)],
  Pi.addSemigroup = { toAdd := Pi.instAdd, add_assoc := ⋯ }
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpack_packedZero : ∀ {spec : Float.Model.Format} {sign : Float.Model.UnpackedFloat.Sign},
  Float.Model.UnpackedFloat.unpack spec (Float.Model.UnpackedFloat.packedZero spec sign) =
    Float.Model.UnpackedFloat.zero sign
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.sum_equivFun : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] (b : Module.Basis ι R M) (u : M), ∑ i, b.equivFun u i • b i = u
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [EquivBEq α] [LawfulHashable α] {a : α},
  ∅.contains a = false
-- Std.Http.Protocol.H1.Parser
/-- Parses trailer headers after a chunked body and returns them as an array of name-value pairs.

This is exposed for callers that need the trailer values directly (e.g. clients). The
internal protocol machine uses `parseLastChunkBody` instead, which discards trailer values.
 -/
Std.Http.Protocol.H1.parseTrailers : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser (Array (String × String))
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_hom_inv_isIso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) [inst_2 : CategoryTheory.IsIso η],
  CategoryTheory.CategoryStruct.comp (F.map₂ η) (F.map₂ (CategoryTheory.inv η)) =
    CategoryTheory.CategoryStruct.id (F.map f)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)), (h.isoMap φ hφ).hom = F.map φ
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.get_seqRight : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (mx : m α), get *> mx = mx
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.prod_withDensity_left₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {mβ : MeasurableSpace β}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : α → ENNReal},
  AEMeasurable f μ → (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun z => f z.1
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- **Alias** of `RingHom.domRestrict_apply`. -/
RingHom.restrict_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σR : Type u_1}
  [inst_2 : SetLike σR R] [inst_3 : SubsemiringClass σR R] (f : R →+* S) {s : σR} (x : ↥s), (f.domRestrict s) x = f ↑x
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.braiding_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (X.braiding Y).hom.f = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.instInhabited.eq_1 : ∀ {M : Type u_4} [inst : Mul M], MulEquiv.instInhabited = { default := MulEquiv.refl M }
-- Mathlib.Algebra.CharP.Defs
CharP.neg_one_ne_one : ∀ (R : Type u_1) [inst : AddGroupWithOne R] (p : ℕ) [CharP R p] [Fact (2 < p)], -1 ≠ 1
-- Mathlib.Data.NNRat.Floor
NNRat.floor_def : ∀ (q : ℚ≥0), ⌊q⌋₊ = q.num / q.den
-- Mathlib.Analysis.Convex.Deriv
/-- Reformulation of `ConvexOn.slope_le_of_hasDerivWithinAt` using `derivWithin`.  -/
ConvexOn.slope_le_derivWithin : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f S y → slope f x y ≤ derivWithin f S y
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.isSome_succMany?_of_lt_size_toArray : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ}, i < r.toArray.size → (Std.PRange.succMany? (i + 1) r.lower).isSome = true
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The family of canonical injection maps, with `i` left implicit  -/
LinearAlgebra.FreeProduct.of : {I : Type u_1} →
  [inst : DecidableEq I] →
    (R : Type u_2) →
      [inst_1 : CommSemiring R] →
        (A : I → Type u_3) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] → {i : I} → A i →ₐ[R] LinearAlgebra.FreeProduct R A
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_single_of_not_mem_range : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] {f : α → β} {b : β},
  b ∉ Set.range f →
    ∀ (m : M) (hf : Set.InjOn f (f ⁻¹' ↑(fun₀ | b => m).support)), Finsupp.comapDomain f (fun₀ | b => m) hf = 0
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.primeIdealOf.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x x_1 : ↥U),
  x = x_1 → hU.primeIdealOf x = hU.primeIdealOf x_1
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.of_subsingleton : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} [IsDomain R] [Module.IsTorsionFree R M] [Subsingleton ι] (i : ι), v i ≠ 0 → LinearIndependent R v
-- Mathlib.Order.SetAccumulate
Set.partialSups_eq_accumulate : ∀ {α : Type u_1} (f : ℕ → Set α), ⇑(partialSups f) = Set.accumulate f
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.length_toList : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxo.HasSize α] [inst_5 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α],
  r.toList.length = r.size
-- Mathlib.Order.Cofinal
isCofinal_empty_iff : ∀ {α : Type u_1} [inst : LE α], IsCofinal ∅ ↔ IsEmpty α
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.AdicCauchySequence.map_comp_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u_4} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (a : AdicCompletion.AdicCauchySequence I M),
  (AdicCompletion.AdicCauchySequence.map I g) ((AdicCompletion.AdicCauchySequence.map I f) a) =
    (AdicCompletion.AdicCauchySequence.map I (g ∘ₗ f)) a
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.enorm : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l : Filter α},
  MeasureTheory.IntegrableAtFilter f l μ → MeasureTheory.IntegrableAtFilter (fun x => ‖f x‖ₑ) l μ
-- Init.Prelude
instHPow : {α : Type u_1} → {β : Type u_2} → [Pow α β] → HPow α β α
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_self_sub_of_bmod_eq : ∀ {a : ℤ} {b : ℕ} {c : ℤ}, a.bmod b = c → ↑b ∣ a - c
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.biproductIsoPi_inv_comp_π : ∀ {J : Type} [inst : Finite J] (f : J → AddCommGrpCat) (j : J),
  CategoryTheory.CategoryStruct.comp (AddCommGrpCat.biproductIsoPi f).inv (CategoryTheory.Limits.biproduct.π f j) =
    AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j => ↑(f j)) j)
-- Mathlib.Order.Lattice.Nat
Nat.sInf_mem : ∀ {s : Set ℕ}, s.Nonempty → sInf s ∈ s
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The identity modification.  -/
CategoryTheory.Oplax.StrongTrans.Modification.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (η : F ⟶ G) → CategoryTheory.Oplax.StrongTrans.Modification η η
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.friendlyOperation_iff_dist_le_dist : ∀ {α : Type u_1} (op : Stream'.Seq α → Stream'.Seq α),
  Tactic.ComputeAsymptotics.Seq.FriendlyOperation op ↔ ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
-- Mathlib.Order.Nucleus
Nucleus.instCompleteSemilatticeInf : {X : Type u_1} → [inst : CompleteLattice X] → CompleteSemilatticeInf (Nucleus X)
-- Mathlib.Data.Nat.Log
Nat.clog.go.eq_1 : ∀ (n a : ℕ), Nat.clog.go n a 0 = (a / n, 0)
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- `iSup U` as a cocone over the opens sets contained in some element of the cover.

(In fact this is a colimit cocone.)
 -/
TopCat.Presheaf.SheafCondition.opensLeCoverCocone : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      CategoryTheory.Limits.Cocone (CategoryTheory.ObjectProperty.ι fun V => ∃ i, V ≤ U i)
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.Progress.matchedOutOfScope.sizeOf_spec : ∀ (lctx : Lean.LocalContext), sizeOf (Mathlib.Tactic.GRewrite.Progress.matchedOutOfScope✝ lctx) = 1 + sizeOf lctx
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- Elements of `t` which are "above" `a` according to relation `r`.  -/
Finset.bipartiteAbove : {α : Type u_2} → {β : Type u_3} → (r : α → β → Prop) → Finset β → (a : α) → [DecidablePred (r a)] → Finset β
-- Mathlib.RingTheory.WittVector.Basic
/-- Evaluates the `n`th Witt polynomial on the first `n` coefficients of `x`,
producing a value in `R`.
This function will be bundled as the ring homomorphism `WittVector.ghostMap`
once the ring structure is available,
but we rely on it to set up the ring structure in the first place.  -/
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun : {p : ℕ} → {R : Type u_1} → [CommRing R] → WittVector p R → ℕ → R
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.instInhabited : (α : Type u_2) → [inst : TopologicalSpace α] → [inst_1 : Preorder α] → Inhabited (α →Co α)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rio_eq_some : ∀ {n i : ℕ}, i < n → (*...n).toList[i]? = some i
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- In an (extended) metric space with second countable topology, the Hausdorff dimension
of a set `s` is the supremum over all `x` of the limit superiors of `dimH t` along
`(𝓝[s] x).smallSets`.  -/
iSup_limsup_dimH : ∀ {X : Type u_2} [inst : EMetricSpace X] [SecondCountableTopology X] (s : Set X),
  ⨆ x, Filter.limsup dimH (nhdsWithin x s).smallSets = dimH s
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.acc_dvdNotUnit_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q : M}, Associated p q → (Acc DvdNotUnit p ↔ Acc DvdNotUnit q)
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec.map` as a `MulEquiv` on hom-sets.  -/
AlgebraicGeometry.Spec.mapMulEquiv : {R S T : Type u} →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      [inst_2 : CommRing T] →
        [inst_3 : Bialgebra R S] →
          [inst_4 : Algebra R T] →
            WithConv (S →ₐ[R] T) ≃*
              ((AlgebraicGeometry.Spec (CommRingCat.of T)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶
                (AlgebraicGeometry.Spec (CommRingCat.of S)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)))
-- Init.Data.List.Sublist
List.prefix_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : List α} {l₂ : List β},
  l₂ <+: List.map f l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = List.map f l
-- Mathlib.Analysis.Complex.Trigonometric
/-- The complex hyperbolic cosine function, defined via `exp`  -/
Complex.cosh : ℂ → ℂ
-- Mathlib.Topology.Order.Basic
tendstoIocClassNhds : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a : α),
  Filter.TendstoIxxClass Set.Ioc (nhds a) (nhds a)
-- Mathlib.Algebra.Algebra.Bilinear
/-- The multiplication map on a non-unital algebra, as an `R`-linear map from `A ⊗[R] A` to `A`.  -/
LinearMap.mul' : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [SMulCommClass R A A] → [IsScalarTower R A A] → TensorProduct R A A →ₗ[R] A
-- Mathlib.Logic.IsEmpty.Basic
Function.extend_of_isEmpty : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [IsEmpty α] (f : α → β) (g : α → γ) (h : β → γ),
  Function.extend f g h = h
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.add_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  MonovaryOn f₁ g s → MonovaryOn f₂ g s → MonovaryOn (f₁ + f₂) g s
-- Mathlib.Order.LiminfLimsup
Filter.liminf_le_limsup : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} [f.NeBot] {u : β → α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.liminf_le_limsup._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_limsup._auto_3 →
      Filter.liminf u f ≤ Filter.limsup u f
-- Mathlib.Topology.Algebra.MulAction
/-- If a scalar action is central, then its right action is continuous when its left action is.  -/
ContinuousSMul.op : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X] [inst_4 : SMul Mᵐᵒᵖ X] [IsCentralScalar M X], ContinuousSMul Mᵐᵒᵖ X
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.decomposeAux_single : ∀ {M : Type u_1} {ι : Type u_2} {R : Type u_3} [inst : AddMonoid M] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : CommSemiring R] (f : M →+ ι) (m : M) (r : R),
  (AddMonoidAlgebra.decomposeAux f) (AddMonoidAlgebra.single m r) =
    (DirectSum.of (fun i => ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)) (f m)) ⟨AddMonoidAlgebra.single m r, ⋯⟩
-- Mathlib.Analysis.Analytic.Constructions
/-- Analytic functions on products are analytic in the first coordinate  -/
AnalyticAt.curry_left : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {p : E × F},
  AnalyticAt 𝕜 f p → AnalyticAt 𝕜 (fun x => f (x, p.2)) p.1
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c_nonneg : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)], 0 ≤ NumberField.house.c✝ K
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.contains_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : β → β}, (Std.DHashMap.Const.modify m k f).contains k' = m.contains k'
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instCanLiftSubmoduleToSubmoduleIsClosedCoe : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M], CanLift (Submodule R M) (ClosedSubmodule R M) ClosedSubmodule.toSubmodule fun x => IsClosed ↑x
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHomClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : TopologicalSpace α] [inst_3 : TopologicalSpace β] [inst_4 : FunLike F α β]
  [toContinuousMapClass : ContinuousMapClass F α β], (∀ (f : F), Monotone ⇑f) → ContinuousOrderHomClass F α β
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift_surjective_iff_closure_range_eq_top : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f : α → β},
  Function.Surjective ⇑(FreeAddGroup.lift f) ↔ AddSubgroup.closure (Set.range f) = ⊤
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- `IsFreeGroupoid.Generators G` is a type synonym for `G`. We think of this as
the vertices of the generating quiver of `G` when `G` is free. We can't use `G` directly,
since `G` already has a quiver instance from being a groupoid.  -/
IsFreeGroupoid.Generators : (G : Type u_1) → [CategoryTheory.Groupoid G] → Type u_1
-- Mathlib.Topology.Order
TopologicalSpace.leftInverse_generateFrom : ∀ {α : Type u}, Function.LeftInverse TopologicalSpace.generateFrom fun t => {s | IsOpen s}
-- Lean.Compiler.LCNF.Types
Lean.Compiler.LCNF.anyExpr : Lean.Expr
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_le_sqrt_iff : ∀ {x y : ℝ}, 0 ≤ y → (√x ≤ √y ↔ x ≤ y)
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.isNoetherianRing_fin_0 : ∀ {R : Type u} [inst : CommRing R] [IsNoetherianRing R], IsNoetherianRing (MvPolynomial (Fin 0) R)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_one : ∀ {R : Type u} [inst : Semiring R] {x : R}, Polynomial.eval x 1 = 1
-- Init.Core
/-- `pure (a : α) s` means that the block exited normally with return value `a`  -/
DoResultPR.pure : {α β σ : Type u} → α → σ → DoResultPR α β σ
-- Init.Data.SInt.Basic
/-- Multiplies two 64-bit signed integers, wrapping around on over- or underflow.  Usually accessed via
the `*` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.mul : Int64 → Int64 → Int64
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.instBEqError : BEq Std.Http.Protocol.H1.Error
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.hom_base_inv_base_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) {Z : TopCat} (h : ↑X.toPresheafedSpace ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.hom.base (CategoryTheory.CategoryStruct.comp e.inv.base h) = h
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.submatrix_updateCol_equiv : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq o]
  [inst_1 : DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α) (e : l ≃ m) (f : o ≃ n),
  (A.updateCol j c).submatrix ⇑e ⇑f = (A.submatrix ⇑e ⇑f).updateCol (f.symm j) fun i => c (e i)
-- Init.Prelude
/-- Make name `s₁.s₂.s₃.s₄`  -/
Lean.Name.mkStr4 : String → String → String → String → Lean.Name
-- Std.Data.TreeMap.Basic
Std.TreeMap.instRepr : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Repr α] → [Repr β] → Repr (Std.TreeMap α β cmp)