mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Protocol.H1.Writer
/-- When the user specifies the exact body size upfront, `Content-Length` framing is
used instead of chunked transfer encoding.
 -/
Std.Http.Protocol.H1.Writer.knownSize : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Option Std.Http.Body.Length
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} [inst_3 : Inhabited β],
  (List.map Prod.fst l).contains k = false → Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.ofList l cmp) k = default
-- Mathlib.Data.Finset.Basic
Finset.sdiff_erase_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∈ s → s \ s.erase a = {a}
-- Batteries.Data.UnionFind.Basic
/-- Validity for rank  -/
Batteries.UnionFind.rankD_lt : ∀ (self : Batteries.UnionFind) {i : ℕ},
  Batteries.UnionFind.parentD self.arr i ≠ i →
    Batteries.UnionFind.rankD self.arr i < Batteries.UnionFind.rankD self.arr (Batteries.UnionFind.parentD self.arr i)
-- Init.Data.Array.Lemmas
/-- We can prove that two folds over the same array are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the array,
preserves the relation.
 -/
Array.foldl_rel : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ}
  {r : β → γ → Prop},
  r a b →
    (∀ a ∈ xs, ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) →
      r (Array.foldl (fun acc a => f acc a) a xs) (Array.foldl (fun acc a => g acc a) b xs)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (self : CategoryTheory.CommComon C), CategoryTheory.IsCommComonObj self.X
-- Mathlib.Data.Fintype.EquivFin
/-- Construct an equivalence from functions that are inverse to each other.  -/
Equiv.ofLeftInverseOfCardLE : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Fintype α] →
      [inst_1 : Fintype β] →
        Fintype.card β ≤ Fintype.card α → (f : α → β) → (g : β → α) → Function.LeftInverse g f → α ≃ β
-- Std.Data.String.ToNat
String.Slice.isNat_copy : ∀ {s : String.Slice}, s.copy.isNat = s.isNat
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.append : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instPartialOrder_1 : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → PartialOrder (LieSubalgebra R L)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D),
  i.isoInverseOfIsoFunctor.inv.app X =
    CategoryTheory.CategoryStruct.comp (G'.inverse.map (G.counitIso.inv.app X))
      (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.hom.app (G.inverse.obj X)))
        (G'.unitIso.inv.app (G.inverse.obj X)))
-- Init.Grind.ToInt
Lean.Grind.IntInterval.instMembershipInt : Membership ℤ Lean.Grind.IntInterval
-- Init.Data.Array.Erase
Array.mem_of_mem_eraseIdx : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {h : i < xs.size} {a : α}, a ∈ xs.eraseIdx i h → a ∈ xs
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.smul_def : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (g : SpecialLinearGroup R V) (v : V), g • v = SpecialLinearGroup.toLinearEquiv g • v
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze : Lean.Option Bool
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_union_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α}
  (contains_eq_false : m₂.contains k = false) {h' : (m₁.union m₂).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (m₁.union m₂) k h' = Std.DHashMap.Internal.Raw₀.Const.get m₁ k ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k a : α} [inst_1 : Inhabited (β a)] {v : β k},
      (t.insert k v).get! a = if h : cmp k a = Ordering.eq then cast ⋯ v else t.get! a
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.D2_inv : ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), SlashAction.map 2 A⁻¹ (EisensteinSeries.D2 A) = -EisensteinSeries.D2 A⁻¹
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.LocallyOfFinitePresentation.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FinitePresentation) →
    AlgebraicGeometry.LocallyOfFinitePresentation f
-- Mathlib.Topology.Algebra.Constructions
AddUnits.continuous_embedProduct : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M], Continuous ⇑(AddUnits.embedProduct M)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- If a category has kernels, then it has weak kernels.  -/
CategoryTheory.Limits.HasWeakKernelsOfHasKernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasKernels C], CategoryTheory.Limits.HasWeakKernels C
-- Init.Omega.Int
Lean.Omega.Int.ofNat_fst_mk : ∀ {β : Type u_1} {x : ℕ} {y : β}, ↑(x, y).1 = ↑x
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Uniform equicontinuity on a subset implies equicontinuity on that subset.  -/
UniformEquicontinuousOn.equicontinuousOn : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α} {S : Set β},
  UniformEquicontinuousOn F S → EquicontinuousOn F S
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `a` and `b`, the derivative `f'` is nonnegative on
`Ioo a b` and nonpositive on `Ioi b`. Then `f` attains its maximum on `Ici a` at `b`.  -/
isMaxOn_Ici_of_deriv : ∀ {f : ℝ → ℝ} {a b : ℝ},
  ContinuousAt f a →
    ContinuousAt f b →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        DifferentiableOn ℝ f (Set.Ioi b) →
          (∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioi b, deriv f x ≤ 0) → IsMaxOn f (Set.Ici a) b
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_left_surjective : ∀ {x : ℝ}, x ≠ 0 → Function.Surjective fun y => y ^ x
-- Mathlib.Data.Finmap
Finmap.Disjoint.eq_1 : ∀ {α : Type u} {β : α → Type v} (s₁ s₂ : Finmap β), s₁.Disjoint s₂ = ∀ x ∈ s₁, x ∉ s₂
-- Mathlib.Util.AtLocation
/-- Log a warning if this action has no effect.  -/
Mathlib.Tactic.BehaviorIfUnchanged.warning : Mathlib.Tactic.BehaviorIfUnchanged
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.antilipschitz : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), AntilipschitzWith 1 ⇑e
-- Init.Data.List.Range
List.range_subset : ∀ {m n : ℕ}, List.range m ⊆ List.range n ↔ m ≤ n
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.id : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → ℕ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} {he : t.alter k f ≠ ∅},
  (t.alter k f).minKey he = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Init.Data.String.PosRaw
String.instHAddRaw_1 : HAdd String.Pos.Raw String String.Pos.Raw
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.symm_trans_self : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N), e.symm.trans e = ContinuousAddEquiv.refl N
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.eq_of_empty : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [h : IsEmpty α]
  (f g : BoundedContinuousFunction α β), f = g
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The top subgroup is isomorphic to the group.

This is the group version of `Submonoid.topEquiv`.  -/
Subgroup.topEquiv : {G : Type u_1} → [inst : Group G] → ↥⊤ ≃* G
-- Mathlib.Data.Nat.Bitwise
Nat.bit_mod_two_eq_one_iff : ∀ (a : Bool) (x : ℕ), Nat.bit a x % 2 = 1 ↔ a = true
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Zero β] → FunLike (CompactlySupportedContinuousMap α β) α β
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_id : ∀ {α : Type u_1} {M : Matroid α}, M.map id ⋯ = M
-- Init.Data.Array.Count
Array.countP_eq_zero : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.countP p xs = 0 ↔ ∀ a ∈ xs, ¬p a = true
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_natCast : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {n : ℕ}, (↑n).IsPositive
-- Mathlib.Data.Num.Lemmas
PosNum.sub'_one : ∀ (a : PosNum), a.sub' 1 = a.pred'.toZNum
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.erase k).getD k fallback = fallback
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.containsThenInsert_fst : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β}, (m.containsThenInsert k v).1 = m.contains k
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_of_le_mul : ∀ {a b c : ℤ}, 0 < c → a ≤ b * c → a / c ≤ b
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.Hom.ext : ∀ {R S : CommRingCat} {x y : R.Hom S}, x.hom' = y.hom' → x = y
-- Mathlib.Topology.Algebra.Module.Star
/-- Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications `M` and `M₂` will be topological modules over the topological
ring `R`.  -/
«term_→L⋆[_]_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_sup_right : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) [K.Normal], K.relIndex (H ⊔ K) = K.relIndex H
-- Aesop.Stats.Basic
Aesop.MonadStats.modifyStats : {m : Type → Type} → [self : Aesop.MonadStats m] → (Aesop.Stats → Aesop.Stats) → m Unit
-- Mathlib.GroupTheory.GroupAction.Basic
/-- If `α` is non-empty, an additive action is pretransitive if and only if the
quotient has exactly one element.  -/
AddAction.pretransitive_iff_unique_quotient_of_nonempty : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α] [Nonempty α],
  AddAction.IsPretransitive G α ↔ Nonempty (Unique (AddAction.orbitRel.Quotient G α))
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.ExceptT.bindCont.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.Tactic.Translate.GuessName
_private.Mathlib.Tactic.Translate.GuessName.0.Mathlib.Tactic.GuessName.fixAbbreviationAux.eq_def : ∀ (g : Mathlib.Tactic.GuessName.GuessNameData) (x x_1 : List String),
  Mathlib.Tactic.GuessName.fixAbbreviationAux g x x_1 =
    match x, x_1 with
    | [], [] => ""
    | [], x :: s => x ++ Mathlib.Tactic.GuessName.fixAbbreviationAux g s []
    | pre :: l, s' =>
      have s := s' ++ [pre];
      have t := String.join s;
      if (pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true then
        s[0]! ++ Mathlib.Tactic.GuessName.fixAbbreviationAux g (List.drop 1 s ++ l) []
      else
        match g.abbreviationDict.get? (Mathlib.Tactic.GuessName.String.decapitalizeSeq t) with
        | some post =>
          Mathlib.Tactic.GuessName.decapitalizeLike t post ++ Mathlib.Tactic.GuessName.fixAbbreviationAux g l []
        | none => Mathlib.Tactic.GuessName.fixAbbreviationAux g l s
-- Batteries.Data.List.Perm
List.Perm.union_left : ∀ {α : Type u_1} {t₁ t₂ : List α} [inst : BEq α] [LawfulBEq α] (l : List α), t₁.Perm t₂ → (l ∪ t₁).Perm (l ∪ t₂)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_closure : ∀ {G : Type u_2} [inst : AddGroup G] (s : Set G),
  (AddSubgroup.closure s).op = AddSubgroup.closure (AddOpposite.unop ⁻¹' s)
-- Std.Data.HashMap.Raw
/-- Checks if any element satisfies the predicate, short-circuiting if a predicate succeeds.  -/
Std.HashMap.Raw.any : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → (α → β → Bool) → Bool
-- Mathlib.Data.Finset.Filter
Finset.filter_empty : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], Finset.filter p ∅ = ∅
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
Polynomial.exists_image_comap_of_monic : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R),
  g.Monic →
    ∃ t,
      PrimeSpectrum.comap Polynomial.C '' (PrimeSpectrum.zeroLocus {g} \ PrimeSpectrum.zeroLocus {f}) =
        (PrimeSpectrum.zeroLocus ↑t)ᶜ
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.center_mem_iff : ∀ {P : Type u_2} [inst : MetricSpace P] {s : EuclideanGeometry.Sphere P}, s.center ∈ s ↔ s.radius = 0
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_X : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S],
  Polynomial.X.aroots S = {0}
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- Calculate the integral of `g ∘ f : α →ₛ F`, where `f` is an integrable function from `α` to `E`
and `g` is a function from `E` to `F`. We require `g 0 = 0` so that `g ∘ f` is integrable.  -/
MeasureTheory.SimpleFunc.map_integral : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E)
  (g : E → F),
  MeasureTheory.Integrable (⇑f) μ →
    g 0 = 0 →
      MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map g f) = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • g x
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instSubOffset : Sub Std.Time.Millisecond.Offset
-- Mathlib.Order.Nucleus
/-- Every nucleus is a `ClosureOperator`.  -/
Nucleus.toClosureOperator : {X : Type u_1} → [inst : SemilatticeInf X] → Nucleus X → ClosureOperator X
-- Mathlib.Algebra.WithConv
/-- Lift an equivalence between `A` and `B` to `WithConv A` and `WithConv B`.  -/
WithConv.congr : {A : Type u_2} → {B : Type u_3} → A ≃ B → WithConv A ≃ WithConv B
-- Mathlib.LinearAlgebra.Matrix.WithConv
instCommMagmaWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [CommMagma α] → CommMagma (WithConv (Matrix m n α))
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (I : ModelWithCorners 𝕜 E H) [inst_5 : ChartedSpace H M] (x : M), extChartAt I x = (chartAt H x).extend I
-- Mathlib.Algebra.Lie.Solvable
_private.Mathlib.Algebra.Lie.Solvable.0.LieAlgebra.derivedAbelianOfIdeal.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey? k = none
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.isStableUnderRetracts_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.IsStableUnderRetracts ↔ ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : CategoryTheory.RetractArrow f g), P g → P f
-- Lean.DocString.Types
Lean.Doc.Block.other.injEq : ∀ {i : Type u} {b : Type v} (container : b) (content : Array (Lean.Doc.Block i b)) (container_1 : b)
  (content_1 : Array (Lean.Doc.Block i b)),
  (Lean.Doc.Block.other container content = Lean.Doc.Block.other container_1 content_1) =
    (container = container_1 ∧ content = content_1)
-- Mathlib.Topology.EMetricSpace.Defs
/-- `Metric.closedEBall x ε` is the set of all points `y` with `edist y x ≤ ε`  -/
Metric.closedEBall : {α : Type u} → [PseudoEMetricSpace α] → α → ENNReal → Set α
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.trivialCofibrations_rlp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)],
  (HomotopicalAlgebra.trivialCofibrations C).rlp = HomotopicalAlgebra.fibrations C
-- Mathlib.Topology.Compactness.Compact
IsCompact.elim_nhds_subcover_nhdsSet : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ {U : X → Set X}, (∀ x ∈ s, U x ∈ nhds x) → ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ nhdsSet s
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAtChain.eq_of_isLongestRevMatchAt_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat startPos endPos →
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat endPos endPos → startPos = endPos
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.Tendsto.mul : ∀ {α : Type u_1} {f : Filter α} {ma mb : α → ENNReal} {a b : ENNReal},
  Filter.Tendsto ma f (nhds a) →
    a ≠ 0 ∨ b ≠ ⊤ →
      Filter.Tendsto mb f (nhds b) → b ≠ 0 ∨ a ≠ ⊤ → Filter.Tendsto (fun a => ma a * mb a) f (nhds (a * b))
-- Init.Data.SInt.Basic
/-- Constructs an `Int64` from an `Int`, clamping if the value is too small or too large.  -/
Int64.ofIntClamp : ℤ → Int64
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J)
  (x y : ↑(F.obj j)),
  RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j (x + y))
    ((RingCat.Colimits.Prequotient.of j x).add (RingCat.Colimits.Prequotient.of j y))
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesColimitπ₂ : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)]
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)]
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)],
  CategoryTheory.Limits.PreservesColimit F CategoryTheory.ShortComplex.π₂
-- Mathlib.Data.Analysis.Topology
/-- A `Compact.Realizer s` is a realization that `s` is compact, namely it is a
choice of finite open covers for each set family covering `s`.  -/
Compact.Realizer : {α : Type u_1} → [TopologicalSpace α] → Set α → Type (max (max (max u_1 (u_5 + 1)) u_5) u_1)
-- Mathlib.Algebra.Group.Action.Units
AddUnits.instAddAction : {M : Type u_3} → {α : Type u_5} → [inst : AddMonoid M] → [AddAction M α] → AddAction (AddUnits M) α
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instFstScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsFinite g],
  AlgebraicGeometry.IsFinite (CategoryTheory.Limits.pullback.fst f g)
-- Batteries.Data.List.Basic
/-- `findIdxNth p xs n` returns the index of the `n`th element for which `p` returns `true`.
For example:
```
findIdxNth (· < 3) [5, 1, 3, 2, 4, 0, 1, 4] 2 = 5
```
 -/
List.findIdxNth : {α : Type u_1} → (α → Bool) → List α → ℕ → ℕ
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.ClosureState : Type
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.BifibrantObject.HoCat C),
  CategoryTheory.IsIso (HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'.app X)
-- Mathlib.Order.Defs.Unbundled
InvImage.irrefl : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [Std.Irrefl r], Std.Irrefl (InvImage r f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {he : t.isEmpty = false}, t.getKey! (t.minKey he) = t.minKey he
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.sSupClosed' : ∀ {α : Type u_1} [inst : CompleteLattice α] (self : CompleteSublattice α) ⦃s : Set α⦄,
  s ⊆ self.carrier → sSup s ∈ self.carrier
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- For each q, `Hσ q` is a natural transformation.  -/
AlgebraicTopology.DoldKan.natTransHσ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      ℕ → (AlgebraicTopology.alternatingFaceMapComplex C ⟶ AlgebraicTopology.alternatingFaceMapComplex C)
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- `arcosh` is the left inverse of `cosh` over $[0, ∞)$.  -/
Real.arcosh_cosh : ∀ {x : ℝ}, 0 ≤ x → Real.arcosh (Real.cosh x) = x
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- The identity profunctor from `C` to `C`. This is defined as the Yoneda bifunctor.  -/
CategoryTheory.Profunctor.id : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Profunctor.{v₁, v₁, v₁, u₁, u₁} C C
-- Lean.Elab.ConfigEval.Commands
/-- `declare_core_config_elab f struct binders* [where ...]` defines a configuration elaborator
```lean
f binders* (cfg : Syntax) (init : struct := {}) (logExceptions : Bool := false) : CoreM struct
```
that evaluates the `cfg` configuration items to update `init`.
Acceptable configuration syntax is documented in `Lean.Elab.ConfigEval.foldConfigM`,
which includes anything that looks like `Lean.Parser.Term.optConfig`, possibly wrapped
in null nodes.

The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr`
instances to support evaluation of configuration options for structure fields.
These instances will be `private local`.

See `ConfigEval.defEvalConfigItemCmd` for further documentation.

See also `declare_term_config_elab`, `declare_config_elab`, and `declare_command_config_elab`.
 -/
Lean.Elab.ConfigEval.declareCoreConfigElab : Lean.ParserDescr
-- Mathlib.Data.Finmap
Finmap.keys_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ : Finmap β}, (s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys