mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
/-- Two bilinear forms over a ring `R` are equivalent
if there exists an isometric equivalence between them:
a linear equivalence that transforms one bilinear form into the other.  -/
LinearMap.BilinForm.Equivalent : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] → [inst_4 : Module R M₂] → LinearMap.BilinForm R M₁ → LinearMap.BilinForm R M₂ → Prop
-- Plausible.Arbitrary
Plausible.String.Arbitrary : Plausible.Arbitrary String
-- Mathlib.Tactic.Push.Attr
/-- The `push` attribute is used to tag lemmas that "push" a constant into an expression.

For example:
```lean
@[push] theorem log_mul (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y
@[push] theorem log_abs : log |x| = log x

@[push] theorem not_imp (p q : Prop) : ¬(p → q) ↔ p ∧ ¬q
@[push] theorem not_iff (p q : Prop) : ¬(p ↔ q) ↔ (p ∧ ¬q) ∨ (¬p ∧ q)
@[push] theorem not_not (p : Prop) : ¬ ¬p ↔ p
@[push] theorem not_le : ¬a ≤ b ↔ b < a
```

Note that some `push` lemmas don't push the constant away from the head (`log_abs`) and
some `push` lemmas cancel the constant out (`not_not` and `not_le`).
For the other lemmas that are "genuine" `push` lemmas, a `pull` attribute is automatically added
in the reverse direction. To not add a `pull` tag, use `@[push only]`.

To tag the reverse direction of the lemma, use `@[push ←]`.
 -/
Mathlib.Tactic.Push.pushAttr : Lean.ParserDescr
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.bell_eq_sum_erase : ∀ {n : ℕ} (p : (n + 1).Partition), p.parts.bell = ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.lmfdbIdParser.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullbackCongr_eq_eqToIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : C} {f g : X ⟶ Y} (h : f = g),
  J.overMapPullbackCongr A h = CategoryTheory.eqToIso ⋯
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.congr_right : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g₁ g₂ : α → F} {l : Filter α},
  f =o[𝕜; l] g₁ → (∀ (x : α), g₁ x = g₂ x) → f =o[𝕜; l] g₂
-- Init.Data.String.TakeDrop
/-- Creates a string slice that contains the longest suffix of `s` in which `pat` matched
\(potentially repeatedly\).

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".takeEndWhile Char.isLower == "blue".toSlice`

* `"red green blue".takeEndWhile 'e' == "e".toSlice`

* `"red green blue".takeEndWhile (fun (_ : Char) => true) == "red green blue".toSlice`
 -/
String.takeEndWhile : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → String.Slice
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- The monoid `E →L[𝕜] E` of continuous linear endomorphisms of `E` acts smoothly on `E`.  -/
instContMDiffSMulContinuousLinearMapIdModelWithCornersSelf : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞},
  ContMDiffSMul (modelWithCornersSelf 𝕜 (E →L[𝕜] E)) (modelWithCornersSelf 𝕜 E) n (E →L[𝕜] E) E
-- Mathlib.Analysis.Convex.Function
concaveOn_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [inst_6 : SMul 𝕜 E]
  [inst_7 : SMul 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄,
            y ∈ s →
              ∀ ⦃a b : 𝕜⦄,
                0 ≤ a →
                  0 ≤ b →
                    0 < a + b → (a / (a + b)) • f x + (b / (a + b)) • f y ≤ f ((a / (a + b)) • x + (b / (a + b)) • y)
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- In a monoid with a single unit, irreducible elements lie in all generating sets.  -/
irreducible_subset_of_submonoidClosure_eq_top : ∀ {M : Type u_1} [inst : CommMonoid M] [Subsingleton Mˣ] {S : Set M}, Submonoid.closure S = ⊤ → {p | Irreducible p} ⊆ S
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.trivialization_baseSet : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
  (Bundle.Trivial.trivialization B F).baseSet = Set.univ
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.quotEquivOfEq_symm : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided] [inst_2 : J.IsTwoSided] (h : I = J),
  (Ideal.quotEquivOfEq h).symm = Ideal.quotEquivOfEq ⋯
-- Mathlib.Order.Filter.Prod
Filter.Frequently.uncurry : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α → β → Prop},
  (∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p x y) → ∃ᶠ (xy : α × β) in la ×ˢ lb, p xy.1 xy.2
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.instFunLike : {α : Type u_1} → FunLike (PMF α) α ENNReal
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- **Alias** of `PrimeSpectrum.zeroLocus_sdiff_singleton_zero`. -/
PrimeSpectrum.zeroLocus_diff_singleton_zero : ∀ {R : Type u} [inst : CommSemiring R] (s : Set R), PrimeSpectrum.zeroLocus (s \ {0}) = PrimeSpectrum.zeroLocus s
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.continuousWithinAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {s : Set E}
  {x : E}, ContinuousWithinAt (↑I.symm) s x
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_abs : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (q : ℚ), ↑|q| = |↑q|
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- For each `i : Fin n`, this structure is a candidate for the relation saying
that `fg` is the product of `f` and `g` in the homotopy group (of a Kan complex).
It is so if `g`, `fg` and `f` are respectively the `i.castSucc.castSucc`,
`i.castSucc.succ` and `i.succ.succ` faces of a `n + 1`-simplex such that
all the other faces are constant. (The multiplication on homotopy groups will be
defined using `i := Fin.last _`, but in general, this structure is useful in
order to obtain properties of `RelStruct`.)  -/
SSet.PtSimplex.MulStruct : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} → X.PtSimplex n x → X.PtSimplex n x → X.PtSimplex n x → Fin n → Type u
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2_zero : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_1, u, u} k H}
  {B : Rep.{u_1, u, u} k G} (f : G →* H), groupCohomology.mapShortComplexH2 f 0 = 0
-- Mathlib.AlgebraicGeometry.ResidueField
/-- A helper lemma to work with `AlgebraicGeometry.Scheme.SpecToEquivOfField`.  -/
AlgebraicGeometry.Scheme.SpecToEquivOfField_eq_iff : ∀ {K : Type u_1} [inst : Field K] {X : AlgebraicGeometry.Scheme}
  {f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)},
  f₁ = f₂ ↔
    ∃ (e : f₁.fst = f₂.fst),
      f₁.snd = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e).hom f₂.snd
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prodComparison_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{w', u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) {A B : C} [inst_3 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))]
  [inst_6 : CategoryTheory.Limits.HasBinaryProduct ((F.comp G).obj A) ((F.comp G).obj B)],
  CategoryTheory.Limits.prodComparison (F.comp G) A B =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.prodComparison F A B))
      (CategoryTheory.Limits.prodComparison G (F.obj A) (F.obj B))
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.prodCategoryInstance2 : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Category.{max u₁ v₁, max (max (max (v₁ + 1) u₁) v₁) u₁} (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁))
-- Batteries.Data.Array.Match
Array.Matcher.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (table : Array.PrefixTable α) (state : Fin (table.size + 1)),
  sizeOf { table := table, state := state } = 1 + sizeOf table + sizeOf state
-- Lean.Elab.Tactic.RCases
/-- Generalize all the arguments as specified in `args` to fvars if they aren't already  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.generalizeExceptFVar : Lean.MVarId → Array Lean.Meta.GeneralizeArg → Lean.MetaM (Array Lean.Expr × Array Lean.FVarId × Lean.MVarId)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.derivFamily_lt_ord : ∀ {ι : Type u} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}},
  c.IsRegular →
    Cardinal.mk ι < c →
      c ≠ Cardinal.aleph0 →
        (∀ (i : ι), ∀ b < c.ord, f i b < c.ord) → ∀ {a : Ordinal.{u}}, a < c.ord → Ordinal.derivFamily f a < c.ord
-- Mathlib.Geometry.Manifold.Immersion
/-- Prefer using `IsImmersionAt.continuousAt` instead  -/
Manifold.IsImmersionAt.continuousOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x), ContinuousOn f h.domChart.source
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple
of a rotation of another by `π / 2`, version subtracting vectors.  -/
Orientation.oangle_sub_right_smul_rotation_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V},
  x ≠ 0 →
    ∀ (r : ℝ), o.oangle (r • (o.rotation ↑(Real.pi / 2)) x) (r • (o.rotation ↑(Real.pi / 2)) x - x) = ↑(Real.arctan r⁻¹)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.tendsto_logb_nhdsNE_zero_of_base_lt_one : ∀ {b : ℝ}, 0 < b → b < 1 → Filter.Tendsto (Real.logb b) (nhdsWithin 0 {0}ᶜ) Filter.atTop
-- Init.Data.BitVec.Basic
/-- Unexpander for bitvector literals.  -/
BitVec.unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_neg_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : InvolutiveNeg α] {A : Matrix n n α}, (-A).IsSymm ↔ A.IsSymm
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- A pushout cocone in `C` is colimit iff it becomes limit
after the application of `yoneda.obj X` for all `X : C`.  -/
CategoryTheory.Limits.PushoutCocone.isColimitYonedaEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          (c : CategoryTheory.Limits.PushoutCocone f g) →
            CategoryTheory.Limits.IsColimit c ≃
              ((X_1 : C) → CategoryTheory.Limits.IsLimit (c.op.map (CategoryTheory.yoneda.obj X_1)))
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.comp.sizeOf_spec : ∀ (a a_1 : Turing.ToPartrec.Code), sizeOf (a.comp a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.stream.eq_def : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) (x : ℕ),
  GenContFract.IntFractPair.stream v x =
    match x with
    | 0 => some (GenContFract.IntFractPair.of v)
    | n.succ =>
      (GenContFract.IntFractPair.stream v n).bind fun ap_n =>
        if ap_n.fr = 0 then none else some (GenContFract.IntFractPair.of ap_n.fr⁻¹)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.startsWith_bool_iff_get : ∀ {p : Char → Bool} {s : String.Slice},
  s.startsWith p = true ↔ ∃ (h : s.startPos ≠ s.endPos), p (s.startPos.get h) = true
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.deriv2_negMulLog : ∀ (x : ℝ), deriv^[2] Real.negMulLog x = -x⁻¹
-- Batteries.Tactic.Lint.Misc
/-- A linter for checking definition doc strings.  -/
Batteries.Tactic.Lint.docBlame : Batteries.Tactic.Lint.Linter
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.fst_map : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {X Y : B × C}
  (a : X ⟶ Y), (CategoryTheory.Bicategory.Prod.fst B C).map a = a.1
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The composition `t.truncGE b ⋙ t.truncLT a`.  -/
CategoryTheory.Triangulated.TStructure.truncLTGE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → ℤ → ℤ → CategoryTheory.Functor C C
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_alter_of_not_compare_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)}, ¬cmp k k' = Ordering.eq → (t.alter k f).contains k' = t.contains k'
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.instStrict : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C} [CategoryTheory.Bicategory.Strict C],
  CategoryTheory.Bicategory.Strict (CategoryTheory.Bicategory.InducedBicategory C F)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
ModuleCat.shortComplex_shortExact : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom S.f) ⇑(CategoryTheory.ConcreteCategory.hom S.g) →
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom S.f) →
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom S.g) → S.ShortExact
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapDomainNonUnitalAlgHom.eq_1 : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Mul M] [inst_4 : Mul N] (f : M →ₙ* N),
  MonoidAlgebra.mapDomainNonUnitalAlgHom R A f =
    { toFun := (MonoidAlgebra.mapDomainNonUnitalRingHom A f).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
      map_mul' := ⋯ }
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.var.sizeOf_spec : ∀ (v : Nat.Internal.Linear.Var), sizeOf (Nat.Internal.SOM.Expr.var v) = 1 + sizeOf v
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.reverse_involutive : ∀ {T : Type u_1} {N : Type u_2}, Function.Involutive ContextFreeRule.reverse
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instBotElemOpensOpenNhdsBot : {α : Type u_1} → [inst : TopologicalSpace α] → Bot ↑⊥.openNhds
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- For any positive `ε`, there exists a positive natural number `m` such that
`μ (x ^ (m : ℕ)) ^ (1 / m : ℝ) < iInf (fun (n : PNat), (μ(x ^(n : ℕ)))^(1/(n : ℝ))) + ε/2`.  -/
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.smoothingSeminormSeq_exists_pnat : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) (x : R) {ε : ℝ},
  0 < ε → ∃ m, μ (x ^ ↑m) ^ (1 / ↑↑m) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- **Alias** of `Filter.Tendsto.congr_dist`. -/
tendsto_of_tendsto_of_dist : ∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α},
  Filter.Tendsto f₁ p (nhds a) → Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0) → Filter.Tendsto f₂ p (nhds a)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- A morphism satisfying `P.relative` is representable.  -/
CategoryTheory.MorphismProperty.relative.rep : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} {f : X ⟶ Y},
  CategoryTheory.MorphismProperty.relative F P f → F.relativelyRepresentable f
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.instAlgebraQuotientComapRingHomAlgebraMap : (R : Type u_5) →
  {A : Type u_6} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        (I : Ideal A) → [inst_2 : Algebra R A] → Algebra (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.takeWhile : ∀ (p : Char → Bool) {s : Substring.Raw}, s.Valid → (s.takeWhile p).Valid
-- Init.Data.String.Defs
String.instHAddSliceRaw : HAdd String.Slice String.Pos.Raw String.Pos.Raw
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yn_ge_n : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), n ≤ Pell.yn a1 n
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.instIsMulCommutative_closure : ∀ (M : Type u_1) [inst : Monoid M] {S : Type u_2} [inst_1 : SetLike S M] [inst_2 : MulMemClass S M] (s : S)
  [IsMulCommutative ↥s], IsMulCommutative ↥(Submonoid.closure ↑s)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- **Alias** of the forward direction of `isComplete_image_iff`.

---

A set is complete iff its image under a uniform inducing map is complete.  -/
isComplete_of_complete_image : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {m : α → β} {s : Set α},
  IsUniformInducing m → IsComplete (m '' s) → IsComplete s
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.cellFrontier_subset_of_mem : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n},
  i ∈ E.I n → Topology.RelCWComplex.cellFrontier n i ⊆ ↑E
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Pi.convexCombPair_apply : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {ι : Type u_3}
  {X : ι → Type u_4} [inst_3 : (i : ι) → Convexity.ConvexSpace R (X i)] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b)
  (hab : a + b = 1) (f g : (i : ι) → X i) (i : ι),
  Convexity.convexCombPair a b ha hb hab f g i = Convexity.convexCombPair a b ha hb hab (f i) (g i)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
ModuleCat.instMonoidalClosed : {R : Type u} → [inst : CommRing R] → CategoryTheory.MonoidalClosed (ModuleCat R)
-- Mathlib.Data.FinEnum
FinEnum.instUInt8 : FinEnum UInt8
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Star ↥(pinGroup Q)
-- Mathlib.ModelTheory.Skolem
FirstOrder.Language.Substructure.skolem₁_reduct_isElementary : ∀ {L : FirstOrder.Language} {M : Type w} [inst : Nonempty M] [inst_1 : L.Structure M]
  (S : (L.sum L.skolem₁).Substructure M), (FirstOrder.Language.LHom.sumInl.substructureReduct S).IsElementary
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_subtype : ∀ {α : Type u_1} [inst : CompleteLattice α] (L : CompleteSublattice α), ⇑L.subtype = Subtype.val
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The composition of homotopy equivalences.  -/
CategoryTheory.ShortComplex.HomotopyEquiv.trans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} → S₁.HomotopyEquiv S₂ → S₂.HomotopyEquiv S₃ → S₁.HomotopyEquiv S₃
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiconeMorphism.mk.inj : ∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} {hom : A.pt ⟶ B.pt}
  {wfst :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.fst = A.fst)
      CategoryTheory.Limits.BinaryBiconeMorphism.wfst._autoParam}
  {wsnd :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.snd = A.snd)
      CategoryTheory.Limits.BinaryBiconeMorphism.wsnd._autoParam}
  {winl :
    autoParam (CategoryTheory.CategoryStruct.comp A.inl hom = B.inl)
      CategoryTheory.Limits.BinaryBiconeMorphism.winl._autoParam}
  {winr :
    autoParam (CategoryTheory.CategoryStruct.comp A.inr hom = B.inr)
      CategoryTheory.Limits.BinaryBiconeMorphism.winr._autoParam}
  {hom_1 : A.pt ⟶ B.pt}
  {wfst_1 :
    autoParam (CategoryTheory.CategoryStruct.comp hom_1 B.fst = A.fst)
      CategoryTheory.Limits.BinaryBiconeMorphism.wfst._autoParam}
  {wsnd_1 :
    autoParam (CategoryTheory.CategoryStruct.comp hom_1 B.snd = A.snd)
      CategoryTheory.Limits.BinaryBiconeMorphism.wsnd._autoParam}
  {winl_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.inl hom_1 = B.inl)
      CategoryTheory.Limits.BinaryBiconeMorphism.winl._autoParam}
  {winr_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.inr hom_1 = B.inr)
      CategoryTheory.Limits.BinaryBiconeMorphism.winr._autoParam},
  { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr } =
      { hom := hom_1, wfst := wfst_1, wsnd := wsnd_1, winl := winl_1, winr := winr_1 } →
    hom = hom_1
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso X i).inv.left = ⋯.isoPushout.hom
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_map_smul : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (p : Polynomial R)
  (M : Matrix n n (Polynomial R)),
  matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.φ_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → (RatFunc.Luroth.φ✝ E).natDegree = Module.finrank (↥E) (RatFunc K)
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- Abbreviation of `PowerSeries.derivative`, the formal derivative on `R⟦X⟧`  -/
PowerSeries.«termD⁄dX» : Lean.ParserDescr
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.smul_coeffs : ∀ {lc : Lean.Omega.LinearCombo} {i : ℤ}, (i * lc).coeffs = i * lc.coeffs
-- Mathlib.Data.Quot
Quotient.hrecOn₂'_mk'' : ∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {φ : Quotient s₁ → Quotient s₂ → Sort u_5}
  (f : (a : α) → (b : β) → φ (Quotient.mk'' a) (Quotient.mk'' b))
  (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ ≍ f a₂ b₂) (x : α) (qb : Quotient s₂),
  (Quotient.mk'' x).hrecOn₂' qb f c = qb.hrecOn' (f x) ⋯