mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.FunctorToTypes.shrink_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w'))
  [inst_1 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} F).map f =
    TypeCat.ofHom
      (⇑(equivShrink (F.obj Y)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(equivShrink (F.obj X)).symm)
-- Mathlib.Analysis.Analytic.Constructions
analyticWithinAt_pi_iff : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E}, AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) s e ↔ ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.monoid : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Monoid (Matrix.SpecialLinearGroup n R)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.ofNat_nonneg : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (x : ℕ), OfNat.ofNat x ≥ 0
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.isNormal_opow : ∀ {a : Ordinal.{u_1}}, 1 < a → Order.IsNormal fun x => a ^ x
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_finCongr_Ioi : ∀ {n m : ℕ} (h : n = m) (i : Fin n), Finset.map (finCongr h).toEmbedding (Finset.Ioi i) = Finset.Ioi (Fin.cast h i)
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.TrySuggestionEntry.prio : Lean.Elab.Tactic.Try.TrySuggestionEntry → ℕ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.ndrec_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Sort u}
  (f : (a : M) → (b : ↥S) → p (Localization.mk a b))
  (H : ∀ {a c : M} {b d : ↥S} (h : (Localization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (a : M) (b : ↥S),
  Localization.rec f H (Localization.mk a b) = f a b
-- Lean.LocalContext
Lean.LocalContext.foldlM : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → [Monad m] → Lean.LocalContext → (β → Lean.LocalDecl → m β) → β → optParam ℕ 0 → m β
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.isoOfEquiv_inv : ∀ {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X)
  (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y)
  (h₃ : autoParam (∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯) CategoryTheory.Cat.isoOfEquiv._auto_1)
  (h₄ : autoParam (∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯) CategoryTheory.Cat.isoOfEquiv._auto_3),
  (CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄).inv = e.inverse.toCatHom
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.eraseManyEntries!_eq_foldl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β},
  ↑(t.eraseManyEntries! l) =
    List.foldl
      (fun acc x_1 =>
        match x_1 with
        | ⟨k, snd⟩ => Std.DTreeMap.Internal.Impl.erase! k acc)
      t l
-- Mathlib.RingTheory.Perfection
Perfection.coe_pthRoot_eq_symm_frobeniusEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p],
  ⇑(Perfection.pthRoot R p) = ⇑(frobeniusEquiv (Perfection R p) p).symm
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.eq_of_comp_arrow_eq_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {P : CategoryTheory.Subobject Y}
  {f g : X ⟶ CategoryTheory.Subobject.underlying.obj P},
  f = g ↔ CategoryTheory.CategoryStruct.comp f P.arrow = CategoryTheory.CategoryStruct.comp g P.arrow
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.MemLp.mono_exponent : ∀ {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ε}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {p q : ENNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp f q μ → p ≤ q → MeasureTheory.MemLp f p μ
-- Std.Net.Addr
Std.Net.MACAddr.mk : Vector UInt8 6 → Std.Net.MACAddr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  t.WF → ∀ {a b : α}, cmp a b = Ordering.eq → Std.DTreeMap.Raw.Const.get! t a = Std.DTreeMap.Raw.Const.get! t b
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.structuredArrowMapCone_π_app : ∀ {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) (G : CategoryTheory.Functor D H) (α : L.comp G ⟶ F)
  (Y : D) (f : CategoryTheory.StructuredArrow Y L),
  (L.structuredArrowMapCone F G α Y).π.app f = CategoryTheory.CategoryStruct.comp (G.map f.hom) (α.app f.right)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The category of Eilenberg-Moore algebras for a monad.
cf Definition 5.2.4 in [Riehl][riehl2017].  -/
CategoryTheory.Monad.Algebra.eilenbergMoore : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → CategoryTheory.Category.{v₁, max u₁ v₁} T.Algebra
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrLeftEquiv_refl : ∀ {M : Type u_4} {N : Type u_8} [inst : MulOneClass M] [inst_1 : Monoid N],
  (MulEquiv.refl M).monoidHomCongrLeftEquiv = Equiv.refl (M →* N)
-- Lean.Elab.DeclModifiers
Lean.Elab.instInhabitedModifiers.default : Lean.Elab.Modifiers
-- Mathlib.RingTheory.ClassGroup.Basic
FractionalIdeal.canonicalEquiv_mk0 : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] [inst_5 : IsDedekindDomain R] (K' : Type u_3) [inst_6 : Field K']
  [inst_7 : Algebra R K'] [inst_8 : IsFractionRing R K'] (I : ↥(nonZeroDivisors (Ideal R))),
  (FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K') ↑((FractionalIdeal.mk0 K) I) = ↑((FractionalIdeal.mk0 K') I)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instIntCast : {Γ : Type u_1} →
  {R : Type u_3} → [Zero Γ] → [inst : PartialOrder Γ] → [inst_1 : Zero R] → [IntCast R] → IntCast (HahnSeries Γ R)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.reindex_refl_refl : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), (Matrix.reindex (Equiv.refl m) (Equiv.refl n)) A = A
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_biUnion_null_iff : ∀ {α : Type u_1} {ι : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α]
  {μ : F} {I : Set ι}, I.Countable → ∀ {s : ι → Set α}, μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s \ t ⊆ s
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.load.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → σ) (a_1 : Turing.TM2.Stmt Γ Λ σ)
  (a_2 : σ → σ) (a_3 : Turing.TM2.Stmt Γ Λ σ),
  (Turing.TM2.Stmt.load a a_1 = Turing.TM2.Stmt.load a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.hasSheafComposeEssentiallySmallSite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₃)
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (B : Type u₄) [inst_2 : CategoryTheory.Category.{v₄, u₄} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.EssentiallySmall.{w, v₁, u₁} C]
  [((CategoryTheory.equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F], J.HasSheafCompose F
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.extractSafePrefixGoal : Lean.Environment → Aesop.Goal → Aesop.SafePrefixM✝ Unit
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has bounded variation, then the variation on
small closed intervals to the right of this point tends to the contribution of the point, i.e.,
the distance between the right limit and the value at the point  -/
BoundedVariationOn.tendsto_eVariationOn_Icc_right : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {l : E},
  BoundedVariationOn f s →
    ∀ {x : α},
      Filter.Tendsto f (nhdsWithin x (s ∩ Set.Ioi x)) (nhds l) →
        x ∈ s →
          Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Icc x y)) (nhdsWithin x (s ∩ Set.Ioi x))
            (nhds (edist (f x) l))
-- Lean.Parser.Term
Lean.Parser.Command.commentBody : Lean.Parser.Parser
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.mem_of_mem_closure : ∀ {α : Type u_1} {M : Matroid α} {e : α} {X : Set α}, M.IsColoop e → e ∈ M.closure X → e ∈ X
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.mkBaseProjections : Lean.Name → Lean.Name → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Language.constantMap.eq_1 : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (c : L.Constants),
  ↑c = FirstOrder.Language.Structure.funMap c default
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.bound : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), ∃ C, 0 < C ∧ ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
-- Mathlib.AlgebraicGeometry.Morphisms.Descent
/-- If `X` admits a morphism `p : T ⟶ X` from an affine scheme satisfying `P'`, to
show a property descends along a morphism `f : X ⟶ Z` satisfying `P'`, `X` may assumed to
be affine.  -/
AlgebraicGeometry.IsStableUnderBaseChange.of_pullback_fst_of_isAffine : ∀ (P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P'.RespectsIso] [P'.IsStableUnderComposition]
  [P.IsStableUnderBaseChange],
  (∀ {R : CommRingCat} {S X : AlgebraicGeometry.Scheme} (f : AlgebraicGeometry.Spec R ⟶ S) (g : X ⟶ S),
      P' f → P (CategoryTheory.Limits.pullback.fst f g) → P g) →
    ∀ {X Y Z T : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine T] (p : T ⟶ X),
      P' p → ∀ (f : X ⟶ Z) (g : Y ⟶ Z), P' f → P (CategoryTheory.Limits.pullback.fst f g) → P g
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprodXIso.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  K.biprodXIso L i = (HomologicalComplex.eval C c i).mapBiprod K L
-- Mathlib.Data.List.Basic
List.length_eraseP_add_one : ∀ {α : Type u} {p : α → Bool} {l : List α} {a : α}, a ∈ l → p a = true → (List.eraseP p l).length + 1 = l.length
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Alias** of `intervalIntegral.integral_deriv_smul_deriv_comp`. -/
intervalIntegral.integral_deriv_comp_smul_deriv : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g g' : ℝ → E}
  [CompleteSpace E],
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivAt g (g' (f x)) (f x)) →
      ContinuousOn f' (Set.uIcc a b) → Continuous g' → ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
-- Lean.Server.References
Lean.Server.ModuleImport.mk.injEq : ∀ (module : Lean.Name) (uri : Lean.Lsp.DocumentUri) (isAll isPrivate : Bool) (metaKind : Lean.Lsp.LeanImportMetaKind)
  (module_1 : Lean.Name) (uri_1 : Lean.Lsp.DocumentUri) (isAll_1 isPrivate_1 : Bool)
  (metaKind_1 : Lean.Lsp.LeanImportMetaKind),
  ({ module := module, uri := uri, isAll := isAll, isPrivate := isPrivate, metaKind := metaKind } =
      { module := module_1, uri := uri_1, isAll := isAll_1, isPrivate := isPrivate_1, metaKind := metaKind_1 }) =
    (module = module_1 ∧ uri = uri_1 ∧ isAll = isAll_1 ∧ isPrivate = isPrivate_1 ∧ metaKind = metaKind_1)
-- Init.Sym.Lemmas
Lean.Sym.UInt8.lt_eq_true : ∀ (a b : UInt8), decide (a < b) = true → (a < b) = True
-- Mathlib.Algebra.Order.Group.Finset
/-- Also see `Finset.add_sup'` that works for ordered groups.  -/
Finset.add_sup'' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [CanonicallyOrderedAdd M]
  [inst_3 : Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} (hs : s.Nonempty) (f : ι → M) (a : M),
  a + s.sup' hs f = s.sup' hs fun i => a + f i
-- Mathlib.Order.Category.LinOrd
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
LinOrd.Hom.Simps.hom : (X Y : LinOrd) → X.Hom Y → ↑X →o ↑Y
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.diam_image_le : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (s : Set α), Bornology.IsBounded s → Metric.diam (f '' s) ≤ ↑K * Metric.diam s
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.inv_rev : ∀ {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜'] {c : ℝ}
  {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'},
  Asymptotics.IsBigOWith c l f g →
    (∀ᶠ (x : α) in l, f x = 0 → g x = 0) → Asymptotics.IsBigOWith c l (fun x => (g x)⁻¹) fun x => (f x)⁻¹
-- Init.Data.Dyadic.Basic
Dyadic.instHShiftLeftInt : HShiftLeft Dyadic ℤ Dyadic
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects limits of `K.op : Jᵒᵖ ⥤ C`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects
colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.reflectsColimit_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimit K.leftOp F.unop],
  CategoryTheory.Limits.ReflectsColimit K F
-- Init.Meta.Defs
/-- Whenever `min a b` or `max a b` is found, rewrite in terms of the definition
`if a ≤ b ...`, for later case splitting.
 -/
Lean.Meta.Omega.OmegaConfig.splitMinMax : Lean.Meta.Omega.OmegaConfig → Bool
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.below.sUnion : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → TopologicalSpace.GenerateOpen g a → Prop} (S : Set (Set α))
  (a : ∀ s ∈ S, TopologicalSpace.GenerateOpen g s),
  (∀ (s : Set α) (a_1 : s ∈ S), TopologicalSpace.GenerateOpen.below ⋯) →
    (∀ (s : Set α) (a_1 : s ∈ S), motive s ⋯) → TopologicalSpace.GenerateOpen.below ⋯
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorIsoMk_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  (A B : CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C))
  (iso₁ : A.comp CategoryTheory.Pretriangulated.Triangle.π₁ ≅ B.comp CategoryTheory.Pretriangulated.Triangle.π₁)
  (iso₂ : A.comp CategoryTheory.Pretriangulated.Triangle.π₂ ≅ B.comp CategoryTheory.Pretriangulated.Triangle.π₂)
  (iso₃ : A.comp CategoryTheory.Pretriangulated.Triangle.π₃ ≅ B.comp CategoryTheory.Pretriangulated.Triangle.π₃)
  (comm₁ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂) iso₂.hom =
      CategoryTheory.CategoryStruct.comp iso₁.hom (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂))
  (comm₂ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃) iso₃.hom =
      CategoryTheory.CategoryStruct.comp iso₂.hom (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃))
  (comm₃ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)
        (CategoryTheory.Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp iso₃.hom (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)),
  (CategoryTheory.Pretriangulated.Triangle.functorIsoMk A B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv =
    CategoryTheory.Pretriangulated.Triangle.functorHomMk B A iso₁.inv iso₂.inv iso₃.inv ⋯ ⋯ ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b_relation : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2
-- Init.Data.Range.Polymorphic.IntLemmas
Std.PRange.Int.succ_eq : ∀ {n : ℤ}, Std.PRange.succ n = n + 1
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_eq`. -/
Set.restrict_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), s.domRestrict f = f ∘ Subtype.val
-- Mathlib.Topology.MetricSpace.Polish
/-- Pulling back a Polish topology under an equiv gives again a Polish topology.  -/
Equiv.polishSpace_induced : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] [PolishSpace β] (f : α ≃ β), PolishSpace α
-- Mathlib.Analysis.Normed.Group.Ultra
/-- **Alias** of `IsUltrametricDist.exists_norm_finsetProd_le`.

---

Given a function `f : ι → M` and a finite set `t ⊆ ι`, we can always find `i : ι`, belonging to `t`
if `t` is nonempty, such that `‖∏ j ∈ t, f j‖ ≤ ‖f i‖`.
 -/
IsUltrametricDist.exists_norm_finset_prod_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] (t : Finset ι) [Nonempty ι]
  (f : ι → M), ∃ i, (t.Nonempty → i ∈ t) ∧ ‖∏ j ∈ t, f j‖ ≤ ‖f i‖
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.sum_apply : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] {ι : Type u_3} (s : Finset ι)
  [inst_2 : AddCommMonoid R] [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R] (f : ι → BoundedContinuousFunction α R)
  (a : α), (∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a
-- Mathlib.Data.Finset.Insert
Finset.insert_subset_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) {s t : Finset α}, s ⊆ t → insert a s ⊆ insert a t
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegularWRT_isCompact_closure_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [R1Space α],
  μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.combine'.match_1.eq_3 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (a : ℤ) (x : Int.Internal.Linear.Var)
  (p : Int.Internal.Linear.Poly) (k₂ : ℤ)
  (h_1 : (k₁ k₂ : ℤ) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.num k₂))
  (h_2 :
    (k₁ a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.add a x p))
  (h_3 :
    (a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k₂ : ℤ) → motive (Int.Internal.Linear.Poly.add a x p) (Int.Internal.Linear.Poly.num k₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)),
  (match Int.Internal.Linear.Poly.add a x p, Int.Internal.Linear.Poly.num k₂ with
    | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.num k₂ => h_1 k₁ k₂
    | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.add a x p => h_2 k₁ a x p
    | Int.Internal.Linear.Poly.add a x p, Int.Internal.Linear.Poly.num k₂ => h_3 a x p k₂
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_3 a x p k₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.instNonnegSpectrumClassComplexNonUnital : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A], NonnegSpectrumClass ℂ A
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.depthUB_le : ∀ (c : RBTree.RBColor) (n : ℕ), RBTree.RBNode.depthUB c n ≤ 2 * n + 1
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.getProofForDecl : Lean.Name → Lean.MetaM Lean.Expr
-- Mathlib.Data.Set.Lattice.Image
Set.surjOn_iInter_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α} {t : ι → Set β} {f : α → β},
  (∀ (i : ι), Set.SurjOn f (s i) (t i)) → Set.InjOn f (⋃ i, s i) → Set.SurjOn f (⋂ i, s i) (⋂ i, t i)
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly_add_left : ∀ {F : Type u_1} [inst : Field F] (p q : Polynomial F) (d : ℕ),
  (p + q).hilbertPoly d = p.hilbertPoly d + q.hilbertPoly d
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.notMem_empty : ∀ (x : ZFSet.{u}), x ∉ ∅
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.DihedralGroup.mul.eq_4 : ∀ {n : ℕ} (a b : ZMod n), DihedralGroup.mul✝ (DihedralGroup.sr a) (DihedralGroup.sr b) = DihedralGroup.r (b - a)
-- Mathlib.FieldTheory.LinearDisjoint
/-- Linear disjointness is symmetric.  -/
IntermediateField.linearDisjoint_comm : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.LinearDisjoint ↥B ↔ B.LinearDisjoint ↥A
-- Mathlib.RingTheory.Localization.Basic
/-- `AlgHom` version of `IsLocalization.lift`.  -/
IsLocalization.liftAlgHom : {A : Type u_4} →
  [inst : CommSemiring A] →
    {R : Type u_5} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Algebra A R] →
          {M : Submonoid R} →
            {S : Type u_6} →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra A S] →
                  [inst_5 : Algebra R S] →
                    [IsScalarTower A R S] →
                      {P : Type u_7} →
                        [inst_7 : CommSemiring P] →
                          [inst_8 : Algebra A P] →
                            [IsLocalization M S] → {f : R →ₐ[A] P} → (∀ (y : ↥M), IsUnit (f ↑y)) → S →ₐ[A] P
-- Mathlib.Condensed.TopComparison
/-- The sheaf on `CompHausLike P` of continuous maps to a topological space.
 -/
TopCat.toSheafCompHausLike : (P : TopCat → Prop) →
  TopCat →
    [inst : CompHausLike.HasExplicitFiniteCoproducts P] →
      [inst_1 : CompHausLike.HasExplicitPullbacks P] →
        (hs :
            ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
              CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
          have this := ⋯;
          CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.isIso_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), S.f = 0 → CategoryTheory.IsIso h.π
-- Mathlib.Order.Interval.Set.Monotone
strictAntiOn_Ici_of_lt_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {ψ : α → β} [inst_2 : PredOrder α]
  [IsPredArchimedean α] {n : α}, (∀ (m : α), n < m → ψ m < ψ (Order.pred m)) → StrictAntiOn ψ (Set.Ici n)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∈ t₂ → (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_rupUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : ℕ), (f.deleteOne id).rupUnits = f.rupUnits