mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The class `DayConvolutionMonoidalCategory C V D` bundles the necessary data to
turn a monoidal category `D` into a monoidal full subcategory of a category of
functors `C ⥤ V` endowed with a Day convolution monoidal structure.
The design of this class is to bundle a fully faithful functor into `C ⥤ V` with
left extensions on its values representing the fact that it maps tensors products
in `D` to Day convolutions, and furthermore ask that this data is "lawful", i.e that
once realized in the functor category, the objects behave like the corresponding ones
in the category `C ⥤ V`.  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory V] →
            (D : Type u₃) →
              [inst : CategoryTheory.Category.{v₃, u₃} D] →
                [CategoryTheory.MonoidalCategoryStruct D] → Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (D : F.DescentData f) (Y : C) (q : Y ⟶ S') (j₁ j₂ : ι') (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂)
  (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q),
  (CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj w D).hom q f₁ f₂ hf₁ hf₂ =
    CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D (CategoryTheory.CategoryStruct.comp f₁ (f' j₁)) f₁ f₂
      ⋯ ⋯
-- Mathlib.Order.CountableSupClosed
iSup_mem_countableSupClosure : ∀ {ι : Sort u_1} {α : Type u_2} {s : Set α} [inst : CompleteLattice α] [Countable ι] [Nonempty ι] {A : ι → α},
  (∀ (n : ι), A n ∈ s) → ⨆ n, A n ∈ countableSupClosure s
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isReduced_of_isAffine_isReduced : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] [IsReduced ↑(X.presheaf.obj (Opposite.op ⊤))],
  AlgebraicGeometry.IsReduced X
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntryD.eq_3 : ∀ {α : Type u} {β : α → Type v} (x : (a : α) × β a) (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β)
  (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l_1 r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxEntryD x =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntryD x
-- Lean.Parser.Term
Lean.Parser.Term.leftact.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Sync.SharedMutex
Std.instNonemptySharedMutex : ∀ {α : Type} [Nonempty α], Nonempty (Std.SharedMutex α)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_iInf : ∀ {ι : Sort u_1} {α : Type u_2} [inst : BooleanAlgebra α] {a : α} {f : ι → BooleanSubalgebra α},
  a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.mem_support_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {f : SkewMonoidAlgebra k G} {a : G}, a ∈ f.support ↔ f.coeff a ≠ 0
-- Lean.Meta.HasNotBit
Lean.mkHasNotBitProof : Lean.Expr → Array ℕ → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_smul_vsub_vadd_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p₁ p₂ : P},
  x ∉ s → p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, t < 0 → s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.rightUnitorEquivalence_counitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.prod.rightUnitorEquivalence C).counitIso =
    CategoryTheory.Iso.refl ((CategoryTheory.prod.rightInverseUnitor C).comp (CategoryTheory.prod.rightUnitor C))
-- Mathlib.Order.Bounds.Basic
IsCoinitialFor.rfl : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsCoinitialFor s s
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limMap_mono' : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] (α : F ⟶ G)
  [CategoryTheory.Mono α], CategoryTheory.Mono (CategoryTheory.Limits.limMap α)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_add : ∀ {R : Type u_1} [inst : CommSemiring R] {a c₁ c₂ : R} {b₁ b₂ : ℕ} {d : R},
  a ^ b₁ = c₁ → a ^ b₂ = c₂ → c₁ * c₂ = d → a ^ (b₁ + b₂) = d
-- Mathlib.NumberTheory.SelbergSieve
/-- A sequence of coefficients $\mu^{+}$ is upper Moebius if $\mu * \zeta ≤ \mu^{+} * \zeta$. These
coefficients then yield an upper bound on the sifted sum.  -/
BoundingSieve.IsUpperMoebius : (ℕ → ℝ) → Prop
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsHaarMeasure.mk : ∀ {G : Type u_3} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [toIsFiniteMeasureOnCompacts : MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [toIsMulLeftInvariant : μ.IsMulLeftInvariant] [toIsOpenPosMeasure : μ.IsOpenPosMeasure], μ.IsHaarMeasure
-- Mathlib.Data.Finsupp.Lex
Pi.lex_eq_finsupp_lex : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] {r : α → α → Prop} {s : N → N → Prop} (a b : α →₀ N),
  Pi.Lex r (fun {i} => s) ⇑a ⇑b = Finsupp.Lex r s a b
-- Mathlib.Data.List.Destutter
List.destutter_of_isChain : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), List.IsChain R l → List.destutter R l = l
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldlM.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    {δ : Type u_4} →
      (motive : δ → Std.DHashMap.Internal.AssocList α β → Sort u_3) →
        (x : δ) →
          (x_1 : Std.DHashMap.Internal.AssocList α β) →
            ((d : δ) → motive d Std.DHashMap.Internal.AssocList.nil) →
              ((d : δ) →
                  (a : α) →
                    (b : β a) →
                      (es : Std.DHashMap.Internal.AssocList α β) →
                        motive d (Std.DHashMap.Internal.AssocList.cons a b es)) →
                motive x x_1
-- Mathlib.CategoryTheory.Sites.Canonical
/-- Check that if `P ∈ Ps`, then `P` is indeed a sheaf for the finest topology on `Ps`.  -/
CategoryTheory.Sheaf.sheaf_for_finestTopology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type w))),
  P ∈ Ps → CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.finestTopology Ps) P
-- Mathlib.RingTheory.Localization.FractionRing
/-- This says that `fieldEquivOfAlgEquiv f` is an extension of `f` (i.e., it agrees with `f` on
`B`). Whereas `(fieldEquivOfAlgEquiv f).commutes` says that `fieldEquivOfAlgEquiv f` fixes `K`.  -/
IsFractionRing.fieldEquivOfAlgEquiv_algebraMap : ∀ {A : Type u_8} {B : Type u_9} {C : Type u_10} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] (FA : Type u_12) (FB : Type u_13) (FC : Type u_14) [inst_5 : Field FA]
  [inst_6 : Field FB] [inst_7 : Field FC] [inst_8 : Algebra A FA] [inst_9 : Algebra B FB] [inst_10 : Algebra C FC]
  [inst_11 : IsFractionRing A FA] [inst_12 : IsFractionRing B FB] [inst_13 : IsFractionRing C FC]
  [inst_14 : Algebra A FB] [inst_15 : IsScalarTower A B FB] [inst_16 : Algebra A FC] [inst_17 : IsScalarTower A C FC]
  [inst_18 : Algebra FA FB] [inst_19 : IsScalarTower A FA FB] [inst_20 : Algebra FA FC]
  [inst_21 : IsScalarTower A FA FC] (f : B ≃ₐ[A] C) (b : B),
  (IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f) ((algebraMap B FB) b) = (algebraMap C FC) (f b)
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- A multiplicative `R`-algebra norm extends the norm on `R`.  -/
MulAlgebraNorm.extends_norm : ∀ {R : outParam (Type u_1)} {S : outParam (Type u_2)} [inst : SeminormedCommRing R] [inst_1 : Ring S]
  [inst_2 : Algebra R S] (f : MulAlgebraNorm R S) (a : R), f ((algebraMap R S) a) = ‖a‖
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp]
  (t t_1 : Std.DTreeMap.Raw α β cmp),
  t = t_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → t.getThenInsertIfNew? a b = t_1.getThenInsertIfNew? a b_1
-- Mathlib.CategoryTheory.Subobject.Presheaf
/-- This is the presheaf that sends every object `X : C` to its type of subobjects `Subobject X`,
and every morphism `f : X ⟶ Y` to the function `Subobject Y → Subobject X` that maps every
subobject of `Y` to its pullback along `f`.  -/
Subobject.presheaf : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Functor Cᵒᵖ (Type (max u v))
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.finiteCoproduct.ι_desc_assoc : ∀ {P : TopCat → Prop} {α : Type w} [inst : Finite α] (X : α → CompHausLike P)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] {B : CompHausLike P} (e : (a : α) → X a ⟶ B) (a : α)
  {Z : CompHausLike P} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a)
      (CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.desc X e) h) =
    CategoryTheory.CategoryStruct.comp (e a) h
-- Init.Notation
/-- `command` is the syntax category for things that appear at the top level
of a lean file. For example, `def foo := 1` is a `command`, as is
`namespace Foo` and `end Foo`. Commands generally have an effect on the state of
adding something to the environment (like a new definition), as well as
commands like `variable` which modify future commands within a scope.  -/
Lean.Parser.Category.command : Lean.Parser.Category
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.subset_extendLe : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V}
  (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t),
  s ⊆ Set.range ⇑(Module.Basis.extendLe hs hst ht)
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.neg : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  Memℓp f p → Memℓp (-f) p
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeAction.mk : Lean.Lsp.WorkDoneProgressParams →
  Lean.Lsp.PartialResultParams →
    String →
      Option Lean.Lsp.CodeActionKind →
        Option (Array Lean.Lsp.Diagnostic) →
          Option Bool →
            Option Lean.Lsp.CodeActionDisabled →
              Option Lean.Lsp.WorkspaceEdit → Option Lean.Lsp.Command → Option Lean.Json → Lean.Lsp.CodeAction
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- **Alias** of the reverse direction of `Matrix.isDetpBalanced_transpose_iff`. -/
Matrix.IsDetpBalanced.transpose : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b : R}, A.IsDetpBalanced a b → A.transpose.IsDetpBalanced a b
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.isDiameter_ofDiameter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ : P), (EuclideanGeometry.Sphere.ofDiameter p₁ p₂).IsDiameter p₁ p₂
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.kernelSequence_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.kernelSequence f).X₂ = X
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.apply_of_revSkipWhile_le_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos pos' : s.Pos} (h₁ : pos' < pos),
  pos.revSkipWhile P ≤ pos' → P (pos'.get ⋯)
-- Init.Data.Int.Linear
Int.Internal.Linear.pow_eq : ∀ (a : ℤ) (b : ℕ) (a' b' k : ℤ), a = a' → ↑b = b' → (k == a' ^ b'.toNat) = true → a ^ b = k
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_homOfCocone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cocones.CorepresentableBy X) (s : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h (CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h s) = s
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_comap_comap_eq_relfinrank_inf : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A B : Subfield E) (f : L →+* E),
  (Subfield.comap f A).relfinrank (Subfield.comap f B) = A.relfinrank (B ⊓ f.fieldRange)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.isoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (h h_1 : A₀.a ≅ A₁.a) (e_h : h = h_1)
  (w : CategoryTheory.CategoryStruct.comp (F.map h.hom) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str h.hom),
  CategoryTheory.Endofunctor.Algebra.isoMk h w = CategoryTheory.Endofunctor.Algebra.isoMk h_1 ⋯
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.instNormedAddCommGroupComplement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              (h : Manifold.IsImmersionAt I J n f x) → NormedAddCommGroup h.complement
-- Lean.Meta.RecExt
/-- Returns `true` if `declName` was defined using well-founded recursion, or structural recursion.
 -/
Lean.Meta.isRecursiveDefinition : Lean.Name → Lean.CoreM Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_preservesLimitsOfShape : ∀ {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] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J F]
  [CategoryTheory.Limits.PreservesLimitsOfShape J G], CategoryTheory.Limits.PreservesLimitsOfShape J (F.comp G)
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- If `G` is a group acting additively on a set, then the action is transitive if
there is a single element whose orbit is everything.  -/
AddAction.IsPretransitive.of_orbit : ∀ {G : Type u_2} {X : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G X] {x₀ : X},
  (∀ (x : X), ∃ g, g +ᵥ x₀ = x) → AddAction.IsPretransitive G X
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.inj_jointly_surjective_of_isColimit : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.CofanTypes F},
  CategoryTheory.Functor.CoconeTypes.IsColimit c → ∀ (x : c.pt), ∃ i y, c.inj i y = x
-- Mathlib.Algebra.Lie.Submodule
/-- `lieSpan` forms a Galois insertion with the coercion from `LieSubmodule` to `Set`.  -/
LieSubmodule.gi : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] → GaloisInsertion (LieSubmodule.lieSpan R L) SetLike.coe
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_factors_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (h : W ⟶ X),
  (CategoryTheory.Limits.kernelSubobject f).Factors h ↔ CategoryTheory.CategoryStruct.comp h f = 0
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.action : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.Action
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S],
  AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).hom =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤))))).hom
      (CommRingCat.ofHom
        (MvPolynomial.eval₂Hom
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace n S ↘ S)))
          (AlgebraicGeometry.AffineSpace.coord S)))
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint_preserves_invariant_helper : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n)
  (acc :
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
      Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool)
  (hsize : acc.1.size = n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  f.DerivedLitsInvariant f_assignments_size acc.1 hsize acc.2.1 →
    ¬Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment l.2 acc.1[↑l.1]! = true →
      have hsize' := ⋯;
      f.DerivedLitsInvariant f_assignments_size
        (acc.1.modify (↑l.1) (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment l.2)) hsize' (l :: acc.2.1)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.tsumCLM_apply : ∀ (𝕜 : Type u_1) (α : Type u_3) (E : Type u_5) [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜]
  [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] [inst_4 : CompleteSpace E] (f : ↥(lp (fun x => E) 1)),
  (lp.tsumCLM 𝕜 α E) f = ∑' (i : α), ↑f i
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.monotone_mapOfLE : ∀ {K : Type u} [inst : Field K] (R S : ValuationSubring K) (h : R ≤ S), Monotone ⇑(R.mapOfLE S h)
-- Aesop.Tree.State
Aesop.MVarCluster.isProvenNoCache : Aesop.MVarCluster → BaseIO Bool
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.restrict_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (a : α),
  μ.restrict {a} = μ {a} • MeasureTheory.Measure.dirac a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.fromOpcycles_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) S₂.fromOpcycles =
    CategoryTheory.CategoryStruct.comp S₁.fromOpcycles φ.τ₃
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get!_eq_get!ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] (k : α)
  [inst_3 : Inhabited (β k)] (l : Std.DTreeMap.Internal.Impl α β), l.get! k = l.get!ₘ k
-- Mathlib.LinearAlgebra.Dimension.Finite
iSupIndep.subtype_ne_bot_le_rank : ∀ {ι : Type w} {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] {V : ι → Submodule R M},
  iSupIndep V → Cardinal.lift.{v, w} (Cardinal.mk { i // V i ≠ ⊥ }) ≤ Cardinal.lift.{w, v} (Module.rank R M)
-- Init.Data.UInt.Bitwise
UInt8.and_zero : ∀ {a : UInt8}, a &&& 0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.ne_of_adj : ∀ {V : Type u} (G : SimpleGraph V) {a b : V}, G.Adj a b → a ≠ b
-- Init.Data.Nat.Compare
Nat.compare_ne_lt : ∀ {a b : ℕ}, compare a b ≠ Ordering.lt ↔ b ≤ a
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.AlgHom.termσ_1 : Lean.ParserDescr
-- Mathlib.NumberTheory.Divisors
Nat.divisorsAntidiagonal.eq_1 : ∀ (n : ℕ),
  n.divisorsAntidiagonal =
    Finset.filterMap
      (fun x =>
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Finset.Icc 1 n) ⋯
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIci.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (a x : α), Set.projIci a x = ⟨max a x, ⋯⟩
-- Lean.Meta.Basic
Lean.Meta.instReprProjReductionKind.repr : Lean.Meta.ProjReductionKind → ℕ → Std.Format
-- Mathlib.Algebra.Lie.Prod
LieHom.inl_apply : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (x : L₁), (LieHom.inl R L₁ L₂) x = (x, 0)
-- Lean.Expr
Lean.Literal.strVal.injEq : ∀ (val val_1 : String), (Lean.Literal.strVal val = Lean.Literal.strVal val_1) = (val = val_1)
-- Mathlib.Probability.Independence.Integrable
/-- If a nonzero function belongs to `ℒ^p` and is independent of another function, then
the space is a probability space.  -/
MeasureTheory.MemLp.isProbabilityMeasure_of_indepFun : ∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : NormedAddCommGroup E] [inst_2 : MeasurableSpace E] [OpensMeasurableSpace E] [inst_4 : MeasurableSpace F]
  (f : Ω → E) (g : Ω → F) {p : ENNReal},
  p ≠ 0 →
    p ≠ ⊤ →
      MeasureTheory.MemLp f p μ →
        (¬∀ᵐ (ω : Ω) ∂μ, f ω = 0) → ProbabilityTheory.IndepFun f g μ → MeasureTheory.IsProbabilityMeasure μ
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.Suggestion.mk.injEq : ∀ (suggestion : Lean.Meta.Tactic.TryThis.SuggestionText) (preInfo? postInfo? : Option String)
  (style? : Option Lean.Meta.Tactic.TryThis.SuggestionStyle) (messageData? : Option Lean.MessageData)
  (toCodeActionTitle? : Option (String → String)) (suggestion_1 : Lean.Meta.Tactic.TryThis.SuggestionText)
  (preInfo?_1 postInfo?_1 : Option String) (style?_1 : Option Lean.Meta.Tactic.TryThis.SuggestionStyle)
  (messageData?_1 : Option Lean.MessageData) (toCodeActionTitle?_1 : Option (String → String)),
  ({ suggestion := suggestion, preInfo? := preInfo?, postInfo? := postInfo?, style? := style?,
        messageData? := messageData?, toCodeActionTitle? := toCodeActionTitle? } =
      { suggestion := suggestion_1, preInfo? := preInfo?_1, postInfo? := postInfo?_1, style? := style?_1,
        messageData? := messageData?_1, toCodeActionTitle? := toCodeActionTitle?_1 }) =
    (suggestion = suggestion_1 ∧
      preInfo? = preInfo?_1 ∧
        postInfo? = postInfo?_1 ∧
          style? = style?_1 ∧ messageData? = messageData?_1 ∧ toCodeActionTitle? = toCodeActionTitle?_1)