mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.IsLimit.hom_ext : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.WeightedCone W F}
  (hc : c.IsLimit) {Z : C} {f g : Z ⟶ c.pt},
  (∀ {j : J} (x : W.obj j),
      CategoryTheory.CategoryStruct.comp f (c.π x) = CategoryTheory.CategoryStruct.comp g (c.π x)) →
    f = g
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f, g) = (-1)ᵐⁿ Res(g, f)`  -/
Polynomial.resultant_comm : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ),
  f.resultant g m n = (-1) ^ (m * n) * g.resultant f n m
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionBase.solution_spec' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : IsAlgClosed k] {a₁ : WittVector p k},
  a₁.coeff 0 ≠ 0 →
    ∀ (a₂ : WittVector p k),
      WittVector.RecursionBase.solution p a₁ a₂ ^ p * a₁.coeff 0 =
        WittVector.RecursionBase.solution p a₁ a₂ * a₂.coeff 0
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfLEArgs.toPreorderOfLEArgs : {α : Type u} → Std.Packages.LinearPreorderOfLEArgs α → Std.Packages.PreorderOfLEArgs α
-- Lean.Server.References
/-- Reduces `identicalImports` with the same module name by merging their flags.
Yields `none` if `identicalImports` is empty or `identicalImports` contains an import that
has a name or uri that is not identical to the others.
 -/
Lean.Server.ModuleImport.collapseIdenticalImports? : Array Lean.Server.ModuleImport → Option Lean.Server.ModuleImport
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_eq_singleton : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X} {x : X}, (Convexity.convexHull R) s = {x} ↔ s = {x}
-- Mathlib.Analysis.Meromorphic.Order
/-- Adding a locally vanishing function does not change the order.
 -/
meromorphicOrderAt_add_of_top_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜},
  meromorphicOrderAt f₂ x = ⊤ → meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.InjectiveInfo.us : Lean.Meta.Grind.InjectiveInfo → List Lean.Level
-- Init.Data.Array.Lex.Lemmas
/-- `l₁` is lexicographically less than `l₂` if either
- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.size`,
  and `l₁` is shorter than `l₂` or
- there exists an index `i` such that
  - for all `j < i`, `l₁[j] == l₂[j]` and
  - `l₁[i] < l₂[i]`
 -/
Array.lex_eq_true_iff_exists : ∀ {α : Type u_1} {l₁ l₂ : Array α} [inst : BEq α] (lt : α → α → Bool),
  l₁.lex l₂ lt = true ↔
    (l₁.isEqv (l₂.take l₁.size) fun x1 x2 => x1 == x2) = true ∧ l₁.size < l₂.size ∨
      ∃ i,
        ∃ (h₁ : i < l₁.size) (h₂ : i < l₂.size),
          (∀ (j : ℕ) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.comap_comp : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (g : C(Y, Z)) (f : C(X, Y)) (S : DiscreteQuotient Z),
  DiscreteQuotient.comap (g.comp f) S = DiscreteQuotient.comap f (DiscreteQuotient.comap g S)
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem : ∀ {R : Type u} [inst : CommRing R] {𝓟 : Ideal R} {f : Polynomial R},
  f.IsWeaklyEisensteinAt 𝓟 → ∀ {x : R}, f.IsRoot x → f.Monic → ∀ (i : ℕ), f.natDegree ≤ i → x ^ i ∈ 𝓟
-- Mathlib.CategoryTheory.Yoneda
/-- Two morphisms of presheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `yoneda.obj X ⟶ P` agree.  -/
CategoryTheory.hom_ext_yoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : P ⟶ Q},
  (∀ (X : C) (p : CategoryTheory.yoneda.obj X ⟶ P),
      CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) →
    f = g
-- Lean.Parser.Syntax
Lean.Parser.Command.mixfixKind.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The orbit corresponding to an element of the quotient by `MulAction.orbitRel`  -/
MulAction.orbitRel.Quotient.orbit : {G : Type u_1} → {α : Type u_2} → [inst : Group G] → [inst_1 : MulAction G α] → MulAction.orbitRel.Quotient G α → Set α
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr_mapAccumr₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {s₁ : σ₁}
  {s₂ : σ₂} (xs : List.Vector α n) (ys : List.Vector β n) (f₁ : γ → σ₁ → σ₁ × ζ) (f₂ : α → β → σ₂ → σ₂ × γ),
  List.Vector.mapAccumr f₁ (List.Vector.mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    have m :=
      List.Vector.mapAccumr₂
        (fun x y s =>
          have r₂ := f₂ x y s.2;
          have r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_smul : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : Monoid A] [inst_2 : MulAction R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : StarMul R] [inst_6 : StarMul A]
  [inst_7 : StarModule R A] (r : ↥(unitary R)) (a : ↥(unitary A)), ↑(r • a) = r • ↑a
-- Init.Grind.AC
Lean.Grind.AC.diseq_norm_aci : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} {x : Std.Commutative ctx.op}
  {x : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)} (lhs rhs : Lean.Grind.AC.Expr)
  (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_aci_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Expr.denote ctx lhs ≠ Lean.Grind.AC.Expr.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' ≠ Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_surjective : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F],
  Function.Surjective ContinuousLinearMapWOT.toCLM
-- Mathlib.Tactic.Translate.Core
/-- A list of positions of type variables that should not be translated.  -/
Mathlib.Tactic.Translate.Config.dontTranslate : Mathlib.Tactic.Translate.Config → List ℕ
-- Mathlib.Data.Nat.Factorization.Basic
Nat.Prime.pow_dvd_iff_le_factorization : ∀ {p k n : ℕ}, Nat.Prime p → n ≠ 0 → (p ^ k ∣ n ↔ k ≤ n.factorization p)
-- Mathlib.RingTheory.Ideal.Operations
Submodule.mem_smul_top_iff : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (I : Ideal R)
  (N : Submodule R M) (x : ↥N), x ∈ I • ⊤ ↔ ↑x ∈ I • N
-- Mathlib.Algebra.Star.Module
IsSelfAdjoint.algebraMap : ∀ {R : Type u_1} (A : Type u_2) [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A] [inst_3 : StarMul A]
  [inst_4 : Algebra R A] [StarModule R A] {r : R}, IsSelfAdjoint r → IsSelfAdjoint ((algebraMap R A) r)
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.isEulerian_iff : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} (p : G.Walk u v),
  p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Parameter used by the Besicovitch greedy algorithm  -/
Besicovitch.TauPackage.τ : {β : Type u_1} → {α : Type u_2} → Besicovitch.TauPackage β α → ℝ
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mk_lt_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Preorder β] {f g : α → β}
  {hf : ∀ (x : β), MeasurableSet (f ⁻¹' {x})} {hg : ∀ (x : β), MeasurableSet (g ⁻¹' {x})} {hf' : (Set.range f).Finite}
  {hg' : (Set.range g).Finite},
  { toFun := f, measurableSet_fiber' := hf, finite_range' := hf' } <
      { toFun := g, measurableSet_fiber' := hg, finite_range' := hg' } ↔
    f < g
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symmEquiv_apply_apply : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (a : M₂),
  (LinearEquiv.symmEquiv e) a = ((↑e).inverse ⇑e.symm ⋯ ⋯) a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcₙ_le : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : NNReal},
  (∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ ≤ c) → ‖cfcₙ f a‖₊ ≤ c
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.toRingHom_apply : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) {f : hI.DPMorphism hJ} {a : A}, f.toRingHom a = f a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α], t.WF → ∀ {k fallback : α}, k ∈ t → t.getKeyD k fallback = k
-- Init.Internal.Order.Lemmas
Lean.Order.Option.monotone_elimM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (a : γ → m (Option α)) (n : γ → m β)
  (s : γ → α → m β),
  Lean.Order.monotone a →
    Lean.Order.monotone n → Lean.Order.monotone s → Lean.Order.monotone fun x => Option.elimM (a x) (n x) (s x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.modify.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  (t t_1 : Std.ExtDTreeMap α β cmp), t = t_1 → ∀ (a : α) (f f_1 : β a → β a), f = f_1 → t.modify a f = t_1.modify a f_1
-- Mathlib.Topology.Order.OrderClosed
iInf_eq_of_forall_le_of_tendsto : ∀ {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [inst : ConditionallyCompleteLattice α]
  [inst_1 : TopologicalSpace α] [ClosedIciTopology α] {a : α} {f : ι → α},
  (∀ (i : ι), a ≤ f i) → Filter.Tendsto f F (nhds a) → ⨅ i, f i = a
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_eq_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] {φ : Polynomial R}, ↑φ = 0 ↔ φ = 0
-- Init.Prelude
/-- Typeclass used for adapting monads. This is similar to `MonadLift`, but instances are allowed to
make use of default state for the purpose of synthesizing such an instance, if necessary.
Every `MonadLift` instance gives a `MonadEval` instance.

The purpose of this class is for the `#eval` command,
which looks for a `MonadEval m CommandElabM` or `MonadEval m IO` instance.
 -/
MonadEval : semiOutParam (Type u → Type v) → (Type u → Type w) → Type (max (max (u + 1) v) w)
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.setTag : Lean.IR.VarId → ℕ → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.Order.Antichain
IsAntichain.top_mem_iff : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [inst_1 : OrderTop α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → (⊤ ∈ s ↔ s = {⊤})
-- Mathlib.Data.Seq.Computation
/-- `Terminates s` asserts that the computation `s` eventually terminates with some value.  -/
Computation.Terminates : {α : Type u} → Computation α → Prop
-- Init.Internal.Order.Basic
Lean.Order.le_inf : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] {x : α} {c : α → Prop},
  (∀ (y : α), c y → Lean.Order.PartialOrder.rel x y) → Lean.Order.PartialOrder.rel x (Lean.Order.inf c)
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallyEtale R A ↔ Algebra.FormallyUnramified R A ∧ Algebra.FormallySmooth R A
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.congr : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u v : Set α},
  MeasureTheory.AEDisjoint μ s t → u =ᵐ[μ] s → v =ᵐ[μ] t → MeasureTheory.AEDisjoint μ u v
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressParams.mk.inj : ∀ {textDocument : Lean.Lsp.VersionedTextDocumentIdentifier} {processing : Array Lean.Lsp.LeanFileProgressProcessingInfo}
  {textDocument_1 : Lean.Lsp.VersionedTextDocumentIdentifier}
  {processing_1 : Array Lean.Lsp.LeanFileProgressProcessingInfo},
  { textDocument := textDocument, processing := processing } =
      { textDocument := textDocument_1, processing := processing_1 } →
    textDocument = textDocument_1 ∧ processing = processing_1
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Given a set of `LeanSemanticToken`, computes the `AbsoluteLspSemanticToken` with absolute
LSP position information for each token.
 -/
Lean.Server.FileWorker.computeAbsoluteLspSemanticTokens : Lean.FileMap →
  String.Pos.Raw →
    Option String.Pos.Raw →
      Array Lean.Server.FileWorker.LeanSemanticToken → Array Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Lean.Structure
_private.Lean.Structure.0.Lean.getFnForFieldUsing? : (Lean.Name → Lean.Name) → Lean.Environment → Lean.Name → Lean.Name → Option Lean.Name
-- Init.Data.Dyadic.Basic
Int.trailingZeros.aux.induct_unfolding : ∀ (motive : (k : ℕ) → (i : ℤ) → i ≠ 0 → i.natAbs ≤ k → ℕ → ℕ → Prop),
  (∀ (i : ℤ) (hi : i ≠ 0) (acc k : ℕ) (x : k + 1 ≠ 0) (hk : i.natAbs ≤ k + 1) (h : i % 2 = 0),
      motive k (i / 2) ⋯ ⋯ (acc + 1) (Int.trailingZeros.aux k (i / 2) ⋯ ⋯ (acc + 1)) →
        motive k.succ i hi hk acc (Int.trailingZeros.aux k (i / 2) ⋯ ⋯ (acc + 1))) →
    (∀ (i : ℤ) (hi : i ≠ 0) (acc k : ℕ),
        k + 1 ≠ 0 → ∀ (hk : i.natAbs ≤ k + 1), ¬i % 2 = 0 → motive k.succ i hi hk acc acc) →
      ∀ (k : ℕ) (i : ℤ) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : ℕ),
        motive k i hi hk acc (Int.trailingZeros.aux k i hi hk acc)
-- Lean.Elab.Tactic.Basic
/-- Return expected type for the main goal.  -/
Lean.Elab.Tactic.getMainTarget : Lean.Elab.Tactic.TacticM Lean.Expr
-- Lean.Meta.Tactic.Grind.Anchor
_private.Lean.Meta.Tactic.Grind.Anchor.0.Lean.Meta.Grind.getAnchor.match_1.eq_1 : ∀ (motive : Option UInt64 → Sort u_1) (a : UInt64) (h_1 : (a : UInt64) → motive (some a))
  (h_2 : (x : Option UInt64) → motive x),
  (match some a with
    | some a => h_1 a
    | x => h_2 x) =
    h_1 a
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- This is a common reasoning sequence in C⋆-algebra theory. If `0 ≤ x ≤ y ≤ 1`, then the norm of
`z - y * z` is controlled by the norm of `star z * (1 - x) * z`, which is advantageous because the
latter is nonnegative. This is a key step in establishing the existence of an increasing approximate
unit in general C⋆-algebras.  -/
CStarAlgebra.nnnorm_sub_mul_self_le : ∀ {A : Type u_2} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x y : A} (z : A),
  0 ≤ x → y ∈ Set.Icc x 1 → ∀ {c : NNReal}, ‖star z * (1 - x) * z‖₊ ≤ c ^ 2 → ‖z - y * z‖₊ ≤ c
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
/-- The identity natural transformation exhibits a simplicial set as a right extension of its
restriction along `(Truncated.inclusion n).op`.  -/
CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      (n : ℕ) →
        (SimplexCategory.Truncated.inclusion n).op.RightExtension ((SimplexCategory.Truncated.inclusion n).op.comp X)
-- Mathlib.MeasureTheory.Measure.Real
/-- Extension for the `positivity` tactic: applications of `μ.real` are nonnegative.  -/
Mathlib.Meta.Positivity.evalMeasureReal : Mathlib.Meta.Positivity.PositivityExt
-- Init.Data.UInt.Lemmas
UInt64.toUSize_mul : ∀ (a b : UInt64), (a * b).toUSize = a.toUSize * b.toUSize
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.measurable_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {f : α → β},
  MeasurableEmbedding f → ∀ {g : α → γ} {g' : β → γ}, Measurable g → Measurable g' → Measurable (Function.extend f g g')
-- Init.Data.Nat.ToString
Nat.repr_ne_empty : ∀ {n : ℕ}, n.repr ≠ ""
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The (unique) morphism from a pointwise left Kan extension.  -/
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.homFrom : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E : L.LeftExtension F} → E.IsPointwiseLeftKanExtension → (G : L.LeftExtension F) → E ⟶ G
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instInhabitedCfg' : Inhabited Turing.PartrecToTM2.Cfg'
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.baseChange_comp_cancelBaseChange_symm_self : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module A N]
  (f : TensorProduct R A M →ₗ[A] N),
  LinearMap.baseChange A f ∘ₗ ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A A A M).symm =
    ↑(TensorProduct.lid A N).symm ∘ₗ f
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.mem_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : Mul M]
  [inst_3 : IsScalarTower R M M] {p q : SubMulAction R M} {x : M}, x ∈ p * q ↔ ∃ y ∈ p, ∃ z ∈ q, y * z = x
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.ofSubtype_support_disjoint : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α}
  (x : Equiv.Perm ↑(Function.fixedPoints ⇑σ)), Disjoint (Equiv.Perm.ofSubtype x).support σ.support
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedCtorInfo : Inhabited Lean.Compiler.LCNF.CtorInfo
-- Mathlib.Analysis.ConstantSpeed
/-- If both `f` and `f ∘ φ` have unit speed (on `t` and `s` respectively) and `φ`
monotonically maps `s` onto `t`, then `φ` is just a translation (on `s`).
 -/
unique_unit_speed : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {φ : ℝ → ℝ},
  MonotoneOn φ s →
    HasUnitSpeedOn (f ∘ φ) s → HasUnitSpeedOn f (φ '' s) → ∀ ⦃x : ℝ⦄, x ∈ s → Set.EqOn φ (fun y => y - x + φ x) s
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.mem_orbit_conjAct : ∀ {G : Type u_3} [inst : Group G] {g h : G}, g ∈ MulAction.orbit (ConjAct G) h ↔ IsConj g h
-- Lean.Server.Completion
Lean.Server.Completion.find? : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position →
    Lean.FileMap →
      String.Pos.Raw →
        Lean.Syntax →
          Lean.Elab.InfoTree → Lean.Lsp.ClientCapabilities → Lean.Server.CancellableM Lean.Lsp.ResolvableCompletionList
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.filterMap : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} → ((a : α) → β a → Option (γ a)) → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α γ
-- Mathlib.Algebra.Group.Prod
AddHom.coe_fst : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N], ⇑(AddHom.fst M N) = Prod.fst
-- Mathlib.Topology.Inseparable
/-- The map `(x, y) ↦ (mk x, mk y)` is a quotient map.  -/
SeparationQuotient.isQuotientMap_prodMap_mk : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsQuotientMap (Prod.map SeparationQuotient.mk SeparationQuotient.mk)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.map_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [BorelSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β),
  (MeasureTheory.Measure.map (⇑f) μ).InnerRegular ↔ μ.InnerRegular
-- Mathlib.Algebra.Ring.Equiv
/-- The equivalence of additive monoids underlying an equivalence of (semi)rings.  -/
RingEquiv.toAddEquiv : {R : Type u_7} →
  {S : Type u_8} → [inst : Mul R] → [inst_1 : Mul S] → [inst_2 : Add R] → [inst_3 : Add S] → R ≃+* S → R ≃+ S
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey!_alter!_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.Const.alter! k f t).minKey! = k ↔
          (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.toSubmodule_inj : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (L₁' L₂' : LieSubalgebra R L), L₁'.toSubmodule = L₂'.toSubmodule ↔ L₁' = L₂'
-- Mathlib.ModelTheory.DirectLimit
/-- **Alias** of `DirectedSystem.map_map'`. -/
FirstOrder.Language.DirectedSystem.map_map : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] ⦃i j k : ι⦄ (hij : i ≤ j) (hjk : j ≤ k) (x : F i),
  (f j k hjk) ((f i j hij) x) = (f i k ⋯) x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_le_max!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (cmp t.max! (t.insert k).max!).isLE = true
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.nodup_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.keys.Nodup
-- Mathlib.Order.WithBot
WithBot.map_eq_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : WithBot α}, WithBot.map f a = ⊥ ↔ a = ⊥
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
ProbabilityTheory.HasIndepIncrements.map : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : Preorder T] [inst_1 : MeasurableSpace E] {R : Type u_4} {F : Type u_5} [inst_2 : Semiring R]
  [inst_3 : SeminormedAddCommGroup E] [inst_4 : Module R E] [OpensMeasurableSpace E] [inst_6 : SeminormedAddCommGroup F]
  [inst_7 : Module R F] [inst_8 : MeasurableSpace F] [BorelSpace F] (L : E →L[R] F),
  ProbabilityTheory.HasIndepIncrements X P → ProbabilityTheory.HasIndepIncrements (fun t ω => L (X t ω)) P
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] {i j : E.toPreOneHypercover.I₀} (k : E.toPreOneHypercover.I₁ i j),
  E.toSaturateOfHasPullbacks.h₁ k = CategoryTheory.CategoryStruct.id (E.toPreOneHypercover.Y k)
-- Mathlib.Data.Int.Lemmas
Int.natAbs_inj_of_nonpos_of_nonpos : ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → (a.natAbs = b.natAbs ↔ a = b)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.eq_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [PreconnectedSpace X] {f : X → Y},
  IsLocallyConstant f → ∀ (x : X), f = Function.const X (f x)
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.top_mem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : OrderTop α], IsUpperSet s → (⊤ ∈ s ↔ s.Nonempty)