mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRight_id : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv)
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of the `n`th power of a field element `x` (with `n : ℤ`)
is the `|n|`th power of the multiplicative height of `x`.  -/
Height.mulHeight₁_zpow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K) (n : ℤ),
  Height.mulHeight₁ (x ^ n) = Height.mulHeight₁ x ^ n.natAbs
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.hasFiniteProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.Limits.HasFiniteProducts D
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_inv_smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {f : α → ε} {c : ENNReal},
  c ≠ 0 → c ≠ ⊤ → (MeasureTheory.Integrable f (c⁻¹ • μ) ↔ MeasureTheory.Integrable f μ)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintTooltip.markdown : Lean.Lsp.MarkupContent → Lean.Lsp.InlayHintTooltip
-- Mathlib.Data.Holor
Holor.CPRankMax1.below.nil : ∀ {α : Type} [inst : Mul α] {motive : {ds : List ℕ} → (a : Holor α ds) → a.CPRankMax1 → Prop} (x : Holor α []),
  Holor.CPRankMax1.below ⋯
-- Mathlib.Algebra.Group.Center
/-- Conditions for an element to be additively central  -/
IsAddCentral : {M : Type u_1} → [Add M] → M → Prop
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instBraidedMonMapMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [inst_4 : CategoryTheory.SymmetricCategory C] →
                [inst_5 : CategoryTheory.SymmetricCategory D] → [inst_6 : F.Braided] → F.mapMon.Braided
-- Mathlib.Order.Max
OrderDual.noMaxOrder : ∀ {α : Type u_1} [inst : LT α] [NoMinOrder α], NoMaxOrder αᵒᵈ
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Structure.ext : ∀ {L : FirstOrder.Language} {M : Type w} {x y : L.Structure M},
  @FirstOrder.Language.Structure.funMap L M x = @FirstOrder.Language.Structure.funMap L M y →
    @FirstOrder.Language.Structure.RelMap L M x = @FirstOrder.Language.Structure.RelMap L M y → x = y
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.snd_inr : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] (x : H₀), (MonoidWithZeroHom.snd G₀ H₀) ((MonoidWithZeroHom.inr G₀ H₀) x) = x
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- `Function.extend s f 1` as a bundled hom.  -/
Function.ExtendByOne.hom : {ι : Type u_1} → {η : Type v} → (R : Type w) → (ι → η) → [inst : MulOneClass R] → (ι → R) →* η → R
-- Mathlib.Topology.UnitInterval
/-- The image of `[0,1]` under the homeomorphism `fun x ↦ a * x + b` is `[b, a+b]`.
 -/
affineHomeomorph_image_I : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [inst_4 : IsTopologicalRing 𝕜] (a b : 𝕜) (h : 0 < a), ⇑(affineHomeomorph a b ⋯) '' Set.Icc 0 1 = Set.Icc b (a + b)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernelBorel.congr_simp : ∀ {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] {mΩ : MeasurableSpace Ω} [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] (κ κ_1 : ProbabilityTheory.Kernel α (γ × Ω)) (e_κ : κ = κ_1)
  [inst_3 : ProbabilityTheory.IsFiniteKernel κ], κ.condKernelBorel = κ_1.condKernelBorel
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.ext : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {x y : DirectSum ι β},
  (∀ (i : ι), x i = y i) → x = y
-- Mathlib.Algebra.Ring.Commute
sub_sq' : ∀ {R : Type u} [inst : CommRing R] (a b : R), (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.ofBijective_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {f : A →ₗc[R] B} (hf : Function.Bijective ⇑f) (a : A),
  (CoalgEquiv.ofBijective hf) a = f a
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.push : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {len : ℕ} → aig.RefVec len → aig.Ref → aig.RefVec (len + 1)
-- Mathlib.Topology.Bornology.Absorbs
absorbs_iInter : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α] {t : Set α}
  {ι : Sort u_3} [Finite ι] {s : ι → Set α}, Absorbs G₀ (⋂ i, s i) t ↔ ∀ (i : ι), Absorbs G₀ (s i) t
-- Lean.Elab.Level
Lean.Elab.Level.Context.options : Lean.Elab.Level.Context → Lean.Options
-- Init.Data.List.Basic
/-- Replaces the first element of the list `l` that is equal to `a` with `b`. If no element is equal to
`a`, then the list is returned unchanged.

`O(|l|)`.

Examples:
* `[1, 4, 2, 3, 3, 7].replace 3 6 = [1, 4, 2, 6, 3, 7]`
* `[1, 4, 2, 3, 3, 7].replace 5 6 = [1, 4, 2, 3, 3, 7]`
 -/
List.replace : {α : Type u} → [BEq α] → List α → α → α → List α
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The bundled derivative of a `C^{n+1}` function is `C^n`.  -/
ContDiff.contDiff_fderiv_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : E → F},
  ContDiff 𝕜 n f → m + 1 ≤ n → ContDiff 𝕜 m fun p => (fderiv 𝕜 f p.1) p.2
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode.eq_def : ∀ (x : Nat.Partrec.Code),
  x.encodeCode =
    match x with
    | Nat.Partrec.Code.zero => 0
    | Nat.Partrec.Code.succ => 1
    | Nat.Partrec.Code.left => 2
    | Nat.Partrec.Code.right => 3
    | cf.pair cg => 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
    | cf.comp cg => 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode + 1) + 4
    | cf.prec cg => 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 1 + 4
    | cf.rfind' => 2 * (2 * cf.encodeCode + 1) + 1 + 4
-- Init.Grind.ToInt
/-- The half-infinite interval `(-∞, hi)`.  -/
Lean.Grind.IntInterval.io : ℤ → Lean.Grind.IntInterval
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_iff_nat_mul_le : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =o[l] g' ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g' x‖
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Kernels
/-- The cokernel projection is itself a cokernel in the functor category.  -/
CategoryTheory.Limits.cokerIsCokernel : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasCokernels C] →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.coker.π C) ⋯)
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- A preadditive category that already has finite biproducts is equivalent to its additive envelope.

Note that we only prove this for a large category;
otherwise there are universe issues that I haven't attempted to sort out.
 -/
CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts : (C : Type (u₁ + 1)) →
  [inst : CategoryTheory.LargeCategory C] →
    [inst_1 : CategoryTheory.Preadditive C] → [CategoryTheory.Limits.HasFiniteBiproducts C] → CategoryTheory.Mat_ C ≌ C
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_subset : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E},
  s ⊆ t →
    UniqueDiffWithinAt 𝕜 s x →
      DifferentiableWithinAt 𝕜 V t x →
        DifferentiableWithinAt 𝕜 W t x → VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracketWithin 𝕜 V W t x
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.Model.union : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T T' : L.Theory}, M ⊨ T → M ⊨ T' → M ⊨ T ∪ T'
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioc_castSucc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioc a.castSucc b.castSucc, f i = ∑ i ∈ Finset.Ioc a b, f i.castSucc
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonMarkupContent.fromJson : Lean.Json → Except String Lean.Lsp.MarkupContent
-- Mathlib.Data.Finset.SDiff
Finset.union_sdiff_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t) \ t = s \ t
-- Batteries.Data.Fin.Coding
Fin.encodeSubtype.eq_def : ∀ {n : ℕ} (P : Fin n → Prop) [inst : DecidablePred P] (i : { i // P i }),
  Fin.encodeSubtype P i =
    match n, P, inst, i with
    | n.succ, P, inst, ⟨⟨0, ⋯⟩, hp⟩ =>
      have this := ⋯;
      ⟨0, this⟩
    | n.succ, P, inst, ⟨⟨i.succ, hi⟩, hp⟩ =>
      match Fin.encodeSubtype (fun i => P i.succ) ⟨⟨i, ⋯⟩, hp⟩ with
      | ⟨k, hk⟩ =>
        if h0 : P 0 then
          have this := ⋯;
          Fin.cast this ⟨k + 1, ⋯⟩
        else
          have this := ⋯;
          Fin.cast this ⟨k, hk⟩
-- Init.Data.String.Basic
String.Slice.Pos.toReplaceStart : {s : String.Slice} → (p₀ pos : s.Pos) → p₀ ≤ pos → (s.sliceFrom p₀).Pos
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- A variant of `topologically_isZariskiLocalAtSource`
that takes one iff statement instead of two implications.  -/
AlgebraicGeometry.topologically_isZariskiLocalAtSource' : ∀ (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop)
  [(AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso],
  (∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) {ι : Type u}
      (U : ι → TopologicalSpace.Opens X),
      TopologicalSpace.IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P (f ∘ Subtype.val))) →
    AlgebraicGeometry.IsZariskiLocalAtSource
      (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P)
-- Mathlib.Tactic.Widget.SelectPanelUtils
instSelectInsertParamsClassSelectInsertParams : SelectInsertParamsClass SelectInsertParams
-- Mathlib.Topology.Sets.Compacts
/-- The type of compact sets with nonempty interior of a topological space.
See also `TopologicalSpace.Compacts` and `TopologicalSpace.NonemptyCompacts`.  -/
TopologicalSpace.PositiveCompacts : (α : Type u_4) → [TopologicalSpace α] → Type u_4
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_vaddConst_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (p : P),
  ⇑(AffineIsometryEquiv.vaddConst 𝕜 p).symm = fun p' => p' -ᵥ p
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_alter_le_size : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, (m.alter k f).size ≤ m.size + 1
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticWith : {a : Type} → [Inhabited a] → Inhabited (Lean.Lsp.DiagnosticWith a)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.descColimitType_surjective_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes),
  Function.Surjective (F.descColimitType c) ↔ ∀ (z : c.pt), ∃ i x, c.ι i x = z
-- Mathlib.Lean.ContextInfo
/-- Run a tactic computation in the context of an infotree node.  -/
Lean.Elab.ContextInfo.runTactic : {α : Type} →
  Lean.Elab.ContextInfo →
    Lean.Elab.TacticInfo → Lean.MVarId → (Lean.MVarId → Lean.MetaM α) → Lean.Elab.Command.CommandElabM α
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Subshift.ofForbidden.eq_1 : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Inhabited A] {G : Type u_2} [inst_2 : AddMonoid G]
  [inst_3 : IsLeftCancelAdd G] [inst_4 : DiscreteTopology A] (F : Set (SymbolicDynamics.FullShift.Pattern A G)),
  SymbolicDynamics.FullShift.Subshift.ofForbidden F =
    { carrier := SymbolicDynamics.FullShift.forbidden F, isClosed := ⋯, mapsTo := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → Inhabited (CategoryTheory.AddGrp C)
-- Mathlib.Order.Antichain
IsAntichain.least_iff : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Preorder α], IsAntichain (fun x1 x2 => x1 ≤ x2) s → (IsLeast s a ↔ s = {a})
-- Mathlib.Analysis.Normed.Module.Bases
/-- The dimension of the range of the projection `P n` is `n`.  -/
SchauderBasis.finrank_range_proj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n : ℕ), Module.finrank 𝕜 ↥(↑(b.proj n)).range = n
-- Mathlib.Probability.Kernel.MeasurableIntegral
MeasureTheory.StronglyMeasurable.integral_kernel_prod_left' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_4} [inst : NormedAddCommGroup E] [ProbabilityTheory.IsSFiniteKernel κ] [inst_2 : NormedSpace ℝ E]
  ⦃f : β × α → E⦄,
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun y => ∫ (x : β), f (x, y) ∂κ y
-- Mathlib.Algebra.Order.Ring.Pow
/-- Bernoulli's inequality for linear ordered semirings.  -/
one_add_le_pow_of_two_add_nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] {a : R},
  0 ≤ 2 + a → ∀ (n : ℕ), 1 + ↑n * a ≤ (1 + a) ^ n
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n₁ : ℤ) {Z : CochainComplex C ℤ}
  (h : L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι✝ f n₁)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.π✝ K L n₁) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Data.Set.Monotone
/-- **Alias** of the reverse direction of `strictMono_domRestrict`. -/
StrictMonoOn.domRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → StrictMono (s.domRestrict f)
-- Mathlib.CategoryTheory.Limits.Final.Type
CategoryTheory.Functor.colimitTypePrecomp_ιColimitType : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {P : CategoryTheory.Functor D (Type w)} (i : C) (x : P.obj (F.obj i)),
  F.colimitTypePrecomp P ((F.comp P).ιColimitType i x) = P.ιColimitType (F.obj i) x
-- Init.Data.Array.Monadic
Array.toList_filterMapM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  {f : α → m (Option β)}, Array.toList <$> Array.filterMapM f xs = List.filterMapM f xs.toList
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.coe_restrict_scalarsL' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type u_3}
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : Module 𝕜 F]
  {𝕜' : Type u_4} [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F] {𝕜'' : Type u_5}
  [inst_15 : Ring 𝕜''] [inst_16 : Module 𝕜'' F] [inst_17 : ContinuousConstSMul 𝕜'' F] [inst_18 : SMulCommClass 𝕜 𝕜'' F]
  [inst_19 : SMulCommClass 𝕜' 𝕜'' F],
  ⇑(ContinuousLinearMap.restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalars 𝕜'
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.orderMonoidIso_spec₀ : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀}
  (h : v.IsEquiv w) (a : R),
  h.orderMonoidIso ((MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) a) =
    (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass w)) a
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.universal_property : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ⟶ b) [p.IsHomLift f φ'],
  ∃! χ, p.IsHomLift (CategoryTheory.CategoryStruct.id R) χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'
-- Mathlib.Topology.MetricSpace.Isometry
/-- The injection from a subtype is an isometry  -/
isometry_subtype_coe : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Isometry Subtype.val
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_snd_le : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (j : ℕ) {a b : α},
  (∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b) → (F.intervalGapsWithin h a b ↑j).2 ≤ b
-- Mathlib.Data.Num.Lemmas
Num.pred.eq_2 : ∀ (p : PosNum), (Num.pos p).pred = p.pred'
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postEquiv_inverse : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : T ≌ D),
  (CategoryTheory.Under.postEquiv X F).inverse =
    (CategoryTheory.Under.post F.inverse).comp (CategoryTheory.Under.map (F.unitIso.hom.app X))
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_le : ∀ {n : ℕ}, 0 < n → n.minFac ≤ n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.constant.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.constant = 1
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L] [Module.Finite K L]
  (Φ : LinearMap.BilinForm K L),
  Φ.Nondegenerate →
    ∀ (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ),
      Φ.IsRefl →
        (∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) →
          ∀ (I : LieIdeal K L), IsAtom I → IsCompl ↑I ↑(LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.minEntryD : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → (a : α) × β a → (a : α) × β a
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_add_of_disjoint : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} [inst_1 : DecidableEq σ],
  Disjoint p.degrees q.degrees → (p + q).degrees = p.degrees ∪ q.degrees
-- Aesop.RuleSet
Aesop.LocalRuleSet.onBaseM : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    [Monad m] → (Aesop.BaseRuleSet → m (Aesop.BaseRuleSet × α)) → Aesop.LocalRuleSet → m (Aesop.LocalRuleSet × α)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.instHasColimitOfHasColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasColimit F
-- Mathlib.Algebra.Lie.Basic
LieEquiv.symm_trans_self : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), e.symm.trans e = LieEquiv.refl
-- Mathlib.NumberTheory.Dioph
Poly.coe_add : ∀ {α : Type u_1} (f g : Poly α), ⇑(f + g) = ⇑f + ⇑g
-- Lean.Parser.Term
/-- A named subsection of `where ... finally`. In the future, sections such as `decreasing_by` might become
syntactic sugar for an `where ... finally` subsection `| decreasing => ...`.
 -/
Lean.Parser.Term.whereFinallySubsection : Lean.Parser.Parser
-- Mathlib.Algebra.Category.Grp.Colimits
/-- (implementation detail) Part of the universal property of the colimit cocone, but without
assuming that `Quot F` lives in the correct universe.  -/
AddCommGrpCat.Colimits.Quot.desc : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      (c : CategoryTheory.Limits.Cocone F) → [inst_1 : DecidableEq J] → AddCommGrpCat.Colimits.Quot F →+ ↑c.pt
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.Over.toOverSectionsAdj_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (I : C) [inst_2 : CategoryTheory.Closed I]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)]
  [inst_4 : CategoryTheory.BraidedCategory C] (Y : CategoryTheory.Over I),
  (CategoryTheory.Over.toOverSectionsAdj I).counit.app Y =
    CategoryTheory.Over.sectionsUncurry
      (CategoryTheory.CategoryStruct.id
        (CategoryTheory.ChosenPullbacksAlong.pullbackObj ((CategoryTheory.ihom I).map Y.hom)
          (CategoryTheory.curryRightUnitorHom I)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {k : α} {f : β k → β k},
  t.WF → (Std.DTreeMap.Internal.Impl.modify k f t).maxKey? = t.maxKey?
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂},
  Std.DTreeMap.Raw.Const.get (m₁ ∪ m₂) k h' = Std.DTreeMap.Raw.Const.get m₂ k ⋯
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_inv_left₀`. -/
AntivaryOn.of_inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → AntivaryOn f⁻¹ g s → MonovaryOn f g s
-- Mathlib.Data.List.Cycle
Cycle.Nodup.nontrivial_iff : ∀ {α : Type u_1} {s : Cycle α}, s.Nodup → (s.Nontrivial ↔ ¬s.Subsingleton)
-- Mathlib.Analysis.Convex.Basic
AntitoneOn.convex_ge : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, AntitoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ r ≤ f x}
-- Lean.Syntax
Lean.Syntax.getQuotContent : Lean.Syntax → Lean.Syntax