mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.toRightDerivedZero.app X)
      (CategoryTheory.CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) h) =
    h
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.subtype_symm_apply_coe : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] {p : α → Prop} {q : β → Prop}
  (e : α ≃ᵤ β) (h : ∀ (a : α), p a ↔ q (e a)) (b : { b // q b }), ↑((e.subtype h).symm b) = e.symm ↑b
-- Mathlib.Algebra.Homology.Augment
ChainComplex.truncateAugment_hom_f : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ℕ),
  (C.truncateAugment f w).hom.f i = CategoryTheory.CategoryStruct.id (C.X i)
-- Batteries.Data.Vector.Basic
_private.Batteries.Data.Vector.Basic.0.Vector.USize.succ_toNat_of_lt : ∀ {start stop : USize} {n : ℕ}, start < stop → stop.toNat ≤ n → n < USize.size → (start + 1).toNat = start.toNat + 1
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.postcomp_map_heq' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D} {X Y : C} {f : X ⟶ Y}
  (H : CategoryTheory.Functor D E),
  (∀ (X : C), F.obj X = G.obj X) → (∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f) → (F.comp H).map f ≍ (G.comp H).map f
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Result.rfl.injEq : ∀ (done done_1 : Bool), (Lean.Meta.Sym.DSimp.Result.rfl done = Lean.Meta.Sym.DSimp.Result.rfl done_1) = (done = done_1)
-- Mathlib.Order.CompleteLattice.Basic
sSup_image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ},
  sSup (Set.image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_add_const_right : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f : α → G} (C : G), Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x + C) l Filter.atBot
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.inseparable_iff : ∀ {α : Type u} [inst : UniformSpace α] {f g : CauchyFilter α}, Inseparable f g ↔ ↑f ×ˢ ↑g ≤ uniformity α
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- If `ringChar F = 2`, then `quadraticCharFun F` takes the value `1` on nonzero elements.  -/
quadraticCharFun_eq_one_of_char_two : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F = 2 → ∀ {a : F}, a ≠ 0 → quadraticCharFun F a = 1
-- Lean.Elab.Util
Lean.Elab.mkUnusedBaseName : Lean.Name → Lean.MacroM Lean.Name
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Whiskering a right exact functor by a right exact functor yields a right exact functor.  -/
CategoryTheory.RightExactFunctor.whiskeringLeft : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            CategoryTheory.Functor (C ⥤ᵣ D) (CategoryTheory.Functor (D ⥤ᵣ E) (C ⥤ᵣ E))
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.prop₁_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (e : X ≅ Y), W₁ e.hom
-- Std.Data.DTreeMap.Basic
/-- Returns the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.DTreeMap.keyAtIdxD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → ℕ → α → α
-- Mathlib.Data.W.Basic
WType.brecOn.go : {α : Type u_1} →
  {β : α → Type u_2} →
    {motive : WType β → Sort u} → (t : WType β) → ((t : WType β) → WType.below t → motive t) → motive t ×' WType.below t
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isClub_empty_iff : ∀ {α : Type v} [inst : LinearOrder α], IsClub ∅ ↔ IsEmpty α
-- Init.Internal.Order.Lemmas
_private.Init.Data.Array.Basic.0.Array.mapM.map.induct : ∀ {α : Type u} {β : Type v} (as : Array α) (motive : ℕ → Array β → Prop),
  (∀ (i : ℕ) (bs : Array β), i < as.size → (∀ (__do_lift : β), motive (i + 1) (bs.push __do_lift)) → motive i bs) →
    (∀ (i : ℕ) (bs : Array β), ¬i < as.size → motive i bs) → ∀ (i : ℕ) (bs : Array β), motive i bs
-- Mathlib.MeasureTheory.Group.Measure
/-- Continuity of the measure of translates of a compact set:
Given a closed compact set `k` in a topological group,
the measure of `g • k \ k` tends to zero as `g` tends to `1`.  -/
MeasureTheory.tendsto_measure_smul_sdiff_isCompact_isClosed : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [μ.InnerRegularCompactLTTop] {k : Set G},
  IsCompact k → IsClosed k → Filter.Tendsto (fun g => μ (g • k \ k)) (nhds 1) (nhds 0)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant monoid homomorphisms.  -/
MulDistribMulActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        (M →* N) →
          (A : Type u_4) →
            [inst_2 : Monoid A] →
              [MulDistribMulAction M A] →
                (B : Type u_5) → [inst : Monoid B] → [MulDistribMulAction N B] → Type (max u_4 u_5)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.toFun_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N), (↑f).toFun = ⇑f
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.adjp.eq_1 : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix n n R),
  Matrix.adjp s A = Matrix.of fun i j => ∑ σ ∈ Equiv.Perm.ofSign s with σ j = i, ∏ k ∈ {j}ᶜ, A k (σ k)
-- Mathlib.Data.List.Forall2
List.forall₂_map_right_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : α → β → Prop} {f : γ → β} {l : List α} {u : List γ},
  List.Forall₂ R l (List.map f u) ↔ List.Forall₂ (fun a c => R a (f c)) l u
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.πObj_ιIteration_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πObj I κ f)
      (CategoryTheory.Arrow.Hom.right ((CategoryTheory.SmallObject.ιIteration I κ).app (CategoryTheory.Arrow.mk f))) =
    ((CategoryTheory.SmallObject.iteration I κ).obj (CategoryTheory.Arrow.mk f)).hom
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.liftKaehlerDifferential.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (D D_1 : Derivation R S M), D = D_1 → D.liftKaehlerDifferential = D_1.liftKaehlerDifferential
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.instIsIsoδFunctorOppositePresheafFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
  [∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  (P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ Φ.presheafFiber P₁ P₂)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {sq₁ sq₂ : CategoryTheory.Square C} {τ₁ : sq₁.X₁ ⟶ sq₂.X₁}
  {τ₂ : sq₁.X₂ ⟶ sq₂.X₂} {τ₃ : sq₁.X₃ ⟶ sq₂.X₃} {τ₄ : sq₁.X₄ ⟶ sq₂.X₄}
  {comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₂)
      CategoryTheory.Square.Hom.comm₁₂._autoParam}
  {comm₁₃ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₃)
      CategoryTheory.Square.Hom.comm₁₃._autoParam}
  {comm₂₄ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₂ sq₂.f₂₄)
      CategoryTheory.Square.Hom.comm₂₄._autoParam}
  {comm₃₄ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₃ sq₂.f₃₄)
      CategoryTheory.Square.Hom.comm₃₄._autoParam}
  {τ₁_1 : sq₁.X₁ ⟶ sq₂.X₁} {τ₂_1 : sq₁.X₂ ⟶ sq₂.X₂} {τ₃_1 : sq₁.X₃ ⟶ sq₂.X₃} {τ₄_1 : sq₁.X₄ ⟶ sq₂.X₄}
  {comm₁₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂_1 = CategoryTheory.CategoryStruct.comp τ₁_1 sq₂.f₁₂)
      CategoryTheory.Square.Hom.comm₁₂._autoParam}
  {comm₁₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃_1 = CategoryTheory.CategoryStruct.comp τ₁_1 sq₂.f₁₃)
      CategoryTheory.Square.Hom.comm₁₃._autoParam}
  {comm₂₄_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄_1 = CategoryTheory.CategoryStruct.comp τ₂_1 sq₂.f₂₄)
      CategoryTheory.Square.Hom.comm₂₄._autoParam}
  {comm₃₄_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄_1 = CategoryTheory.CategoryStruct.comp τ₃_1 sq₂.f₃₄)
      CategoryTheory.Square.Hom.comm₃₄._autoParam},
  { τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, τ₄ := τ₄, comm₁₂ := comm₁₂, comm₁₃ := comm₁₃, comm₂₄ := comm₂₄, comm₃₄ := comm₃₄ } =
      { τ₁ := τ₁_1, τ₂ := τ₂_1, τ₃ := τ₃_1, τ₄ := τ₄_1, comm₁₂ := comm₁₂_1, comm₁₃ := comm₁₃_1, comm₂₄ := comm₂₄_1,
        comm₃₄ := comm₃₄_1 } →
    τ₁ = τ₁_1 ∧ τ₂ = τ₂_1 ∧ τ₃ = τ₃_1 ∧ τ₄ = τ₄_1
-- Mathlib.Algebra.IsPrimePow
not_isPrimePow_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsReduced R], ¬IsPrimePow 0
-- Mathlib.Algebra.Group.Defs
AddRightCancelSemigroup.mk : {G : Type u} → [toAddSemigroup : AddSemigroup G] → [toIsRightCancelAdd : IsRightCancelAdd G] → AddRightCancelSemigroup G
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mrange_eq_top : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F}, AddMonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.FieldTheory.Finite.Basic
Int.ModEq.pow_prime_eq_self : ∀ {p : ℕ}, Nat.Prime p → ∀ (n : ℤ), n ^ p ≡ n [ZMOD ↑p]
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.frontier_ball_eq_empty : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x : X) (r : ℝ), frontier (Metric.ball x r) = ∅
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.map_injective_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f), Function.Injective (TopologicalSpace.NonemptyCompacts.map f hf) ↔ Function.Injective f
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.of_transcendental : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {K : Type u_4}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : Algebra S K] [IsScalarTower R S K] [FaithfulSMul R S]
  [FaithfulSMul S K] {x : S}, Transcendental R ((algebraMap S K) x) → IsStronglyTranscendental R x
-- Std.Http.Data.Body.Stream
/-- Creates an empty `Stream` body channel (already closed, no data).

Prefer `Body.Empty` when you need a concrete zero-cost type. Use this when the calling
context requires a `Stream` specifically.
 -/
Std.Http.Body.empty : Std.Async.Async Std.Http.Body.Stream
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.realizeConst.realizeAndReport : Lean.Name → Lean.MetaM Unit → Lean.Core.Context → Lean.Environment → Lean.Options → BaseIO (Lean.Environment × Dynamic)
-- Mathlib.GroupTheory.Coset.Basic
rightAddCoset_zero : ∀ {α : Type u_1} [inst : AddMonoid α] (s : Set α), AddOpposite.op 0 +ᵥ s = s
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.hasLeftDerivedFunctor_iff_of_iso : ∀ {C : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_2} H] {F F' : CategoryTheory.Functor C H} (e : F ≅ F')
  (W : CategoryTheory.MorphismProperty C), F.HasLeftDerivedFunctor W ↔ F'.HasLeftDerivedFunctor W
-- Mathlib.Order.Hom.WithTopBot
OrderHom.withTopMap_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), ⇑f.withTopMap = WithTop.map ⇑f
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressProcessingInfo.kind : Lean.Lsp.LeanFileProgressProcessingInfo → Lean.Lsp.LeanFileProgressKind
-- Std.Internal.Do.WP.Basic
/-- Soundness for `StateM` (discarding final state).  -/
Std.Internal.Do.StateM.of_wp_run'_eq : ∀ {α σ : Type} {x : α} {prog : StateM σ α} {s : σ},
  StateT.run' prog s = x → ∀ (P : α → Prop), Std.Internal.Do.wp prog (fun a x => P a) epost⟨⟩ s → P x
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.refl : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} (x : R), RingConGen.Rel r x x
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.isIdCont : String → Lean.ParseImports.State → Bool
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.id_μ_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.Monad.id C).μ.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.isProjectiveLimit_trajFun : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) (x₀ : (i : ↥(Finset.Iic a)) → X ↑i),
  MeasureTheory.IsProjectiveLimit (ProbabilityTheory.Kernel.trajFun κ a x₀)
    (MeasureTheory.inducedFamily fun n => (ProbabilityTheory.Kernel.partialTraj κ a n) x₀)
-- Batteries.Data.MLList.Basic
/-- Take the first `n` elements, as an array inside the monad.  -/
MLList.takeAsArray : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → ℕ → m (Array α)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
/-- Auxiliary definition for `FreeMonoidalCategory.project`.  -/
CategoryTheory.FreeMonoidalCategory.projectMap : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v', u'} D] →
      [inst_1 : CategoryTheory.MonoidalCategory D] →
        (f : C → D) →
          (X Y : CategoryTheory.FreeMonoidalCategory C) →
            (X ⟶ Y) →
              (CategoryTheory.FreeMonoidalCategory.projectObj f X ⟶ CategoryTheory.FreeMonoidalCategory.projectObj f Y)
-- Init.Data.Dyadic.Basic
Dyadic.mul.eq_1 : ∀ (y : Dyadic), Dyadic.zero.mul y = Dyadic.zero
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The fundamental property of the adjoint.  -/
ContinuousLinearMap.adjoint_inner_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) (x : E) (y : F),
  inner 𝕜 ((ContinuousLinearMap.adjoint A) y) x = inner 𝕜 y (A x)
-- Mathlib.Data.Set.Function
/-- Variant of `EqOn.image_eq`, for one function being the identity.  -/
Set.EqOn.image_eq_self : ∀ {α : Type u_1} {s : Set α} {f : α → α}, Set.EqOn f id s → f '' s = s
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (a_1 : a ⟶ b) (x : Bᵒᵖ) (x_1 : Opposite.unop x ⟶ a),
  ((CategoryTheory.Bicategory.yoneda.map a_1).app x).toFunctor.obj x_1 = CategoryTheory.CategoryStruct.comp x_1 a_1
-- Mathlib.RingTheory.Idempotents
/-- Idempotents lift along nil ideals.  -/
exists_isIdempotentElem_eq_of_ker_isNilpotent : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (∀ x ∈ RingHom.ker f, IsNilpotent x) → ∀ e ∈ f.range, IsIdempotentElem e → ∃ e', IsIdempotentElem e' ∧ f e' = e
-- Mathlib.Geometry.Euclidean.Incenter
/-- The normalized weights of the vertices in an affine combination that gives an excenter with
signs determined by the given set of indices.  An excenter with those signs exists if and only if
the sum of these weights is 1.  -/
Affine.Simplex.excenterWeights : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Finset (Fin (n + 1)) → Fin (n + 1) → ℝ
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.minKey!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] (x : Std.DTreeMap.Internal.Impl α β),
  x.minKey! =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.minKey!" 413 13
        "Map is empty"
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => k
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      l.minKey!
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.instInhabitedMorApplication : Inhabited Mathlib.Meta.FunProp.MorApplication
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
AlternatingMap.alternatizeUncurryFinLM_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N),
  AlternatingMap.alternatizeUncurryFinLM f = AlternatingMap.alternatizeUncurryFin f
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- If E/L/K is a tower of field extensions with E/L algebraic, and if M is an algebraically
closed extension of K, then any embedding of L/K into M/K extends to an embedding of E/K.
Known as the extension lemma in https://math.stackexchange.com/a/687914.  -/
IsAlgClosed.surjective_domRestrict_of_isAlgebraic : ∀ {K : Type u} [inst : Field K] {L : Type v} {M : Type w} [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : Field M]
  [inst_4 : Algebra K M] [IsAlgClosed M] {E : Type u_1} [inst_6 : Field E] [inst_7 : Algebra K E] [inst_8 : Algebra L E]
  [inst_9 : IsScalarTower K L E] [Algebra.IsAlgebraic L E], Function.Surjective fun φ => AlgHom.domRestrict L φ
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.lift_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C}
  (k : CategoryTheory.IsKernelPair f a b) (p q : S ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (k.lift p q w) (CategoryTheory.CategoryStruct.comp a h) =
    CategoryTheory.CategoryStruct.comp p h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k k' : α} {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).getKey! k' =
    if cmp k k' = Ordering.eq then if (f (Std.DTreeMap.Const.get? t k)).isSome = true then k else default
    else t.getKey! k'
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a nonzero vector and itself.  -/
InnerProductGeometry.angle_self : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x : V},
  x ≠ 0 → InnerProductGeometry.angle x x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks.0.CategoryTheory.Limits.cospanOp.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingCospan → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : Unit → motive (some CategoryTheory.Limits.WalkingPair.left))
  (h_3 : Unit → motive (some CategoryTheory.Limits.WalkingPair.right)),
  (match some CategoryTheory.Limits.WalkingPair.left with
    | none => h_1 ()
    | some CategoryTheory.Limits.WalkingPair.left => h_2 ()
    | some CategoryTheory.Limits.WalkingPair.right => h_3 ()) =
    h_2 ()
-- Mathlib.Topology.Closure
dense_iff_closure_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Dense s ↔ closure s = Set.univ
-- Std.Internal.Do.Triple.Basic
Std.Internal.Do.Triple.entails_wp_of_pre : ∀ {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {x : Prog}
  {pre pre' : Pred} {post : Value → Pred} {epost : EPred},
  ⦃ pre' ⦄ x ⦃ post; epost ⦄ →
    Lean.Order.PartialOrder.rel pre pre' → Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost)
-- Lean.Meta.LazyDiscrTree
/-- Return root key for an entry.  -/
Lean.Meta.LazyDiscrTree.InitEntry.key : {α : Type} → Lean.Meta.LazyDiscrTree.InitEntry α → Lean.Meta.LazyDiscrTree.Key
-- Mathlib.Analysis.Normed.Order.UpperLower
dist_anti_right_pi : ∀ {ι : Type u_2} [inst : Fintype ι] {x : ι → ℝ}, AntitoneOn (dist x) (Set.Iic x)
-- Std.Sat.AIG.Basic
/-- A pair of `Ref`s, useful for `LawfulOperator`s that act on two `Ref`s at a time.
 -/
Std.Sat.AIG.BinaryInput : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → Type
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.monotone_extensionProductIter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P Q : CategoryTheory.ObjectProperty C}, P ≤ Q → ∀ (n : ℕ), P.extensionProductIter n ≤ Q.extensionProductIter n
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.one_apply_eq_one_iff : ∀ {M₀ : Type u_7} {N₀ : Type u_8} [inst : MulZeroOneClass M₀] [inst_1 : MulZeroOneClass N₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : Nontrivial M₀] [inst_4 : NoZeroDivisors M₀] [Nontrivial N₀]
  {x : M₀}, 1 x = 1 ↔ x ≠ 0
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom.category_id_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (X Y : CategoryTheory.Bicategory.InducedBicategory C F) (f : X ⟶ Y),
  (CategoryTheory.CategoryStruct.id f).hom = CategoryTheory.CategoryStruct.id f.hom