mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.div_def : ∀ {R : Type u} [inst : Field R] {p q : Polynomial R},
  p / q = Polynomial.C q.leadingCoeff⁻¹ * (p /ₘ (q * Polynomial.C q.leadingCoeff⁻¹))
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.addConst_empty_right : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A : Finset G), A.addConst ∅ = 0
-- Init.Data.Order.Classes
Std.LawfulOrderLeftLeaningMin.min_eq_left : ∀ {α : Type u} {inst : Min α} {inst_1 : LE α} [self : Std.LawfulOrderLeftLeaningMin α] (a b : α), a ≤ b → a ⊓ b = a
-- Mathlib.Data.Finite.Prod
Finite.Set.finite_prod : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) [Finite ↑s] [Finite ↑t], Finite ↑(s ×ˢ t)
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtr.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {a : α}, IsLocalExtr f a → ∀ {g : β → γ}, Antitone g → IsLocalExtr (g ∘ f) a
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkPushforward.comp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y Z : TopCat}
  (ℱ : TopCat.Presheaf C X) (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  TopCat.Presheaf.stalkPushforward C (CategoryTheory.CategoryStruct.comp f g) ℱ x =
    CategoryTheory.CategoryStruct.comp
      (TopCat.Presheaf.stalkPushforward C g ((TopCat.Presheaf.pushforward C f).obj ℱ)
        ((CategoryTheory.ConcreteCategory.hom f) x))
      (TopCat.Presheaf.stalkPushforward C f ℱ x)
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.mk : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → CategoryTheory.MonoidalCoherence X Y
-- Mathlib.Probability.Decision.Risk.Defs
/-- The average risk of an estimator `κ` on an estimation task with loss `ℓ` and
data generating kernel `P` with respect to a prior `π`.  -/
ProbabilityTheory.avgRisk : {Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΘ : MeasurableSpace Θ} →
        {m𝓧 : MeasurableSpace 𝓧} →
          {m𝓨 : MeasurableSpace 𝓨} →
            (Θ → 𝓨 → ENNReal) →
              ProbabilityTheory.Kernel Θ 𝓧 → ProbabilityTheory.Kernel 𝓧 𝓨 → MeasureTheory.Measure Θ → ENNReal
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_le_of_ae_bound : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F} {C : ℝ},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMRight.eq_1 : ∀ (a b : ℕ),
  a.factorizationLCMRight b =
    (a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then 1 else p ^ n
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.prev_nat_succ : ∀ (i : ℕ), (ComplexShape.up ℕ).prev (i + 1) = i
-- Lean.Compiler.IR.Basic
Lean.IR.instHashableJoinPointId.hash : Lean.IR.JoinPointId → UInt64
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.replicate.match_1.splitter : {α : Type u_2} →
  (motive : ℕ → α → Sort u_1) →
    (x : ℕ) → (x_1 : α) → ((x : α) → motive 0 x) → ((n : ℕ) → (a : α) → motive n.succ a) → motive x x_1
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.sSameSide_affineSpan_pair_incenter_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → line[ℝ, t.points i₂, t.points i₃].SSameSide (Affine.Simplex.incenter t) (t.points i₁)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Right.pos_add_of_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [IsBotZeroClass α] [AddRightMono α] {b : α},
  0 < b → ∀ (a : α), 0 < a + b
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.smulOfNeZero_apply : ∀ (K : Type u_3) (M : Type u_5) [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M] (a : K) (ha : a ≠ 0)
  (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha) a_1 = a • a_1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.mk_one : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], { toLinearMap := 1, cont := ⋯ } = 1
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  {x Y : Finset (CategoryTheory.Discrete α)} (h : x ⟶ Y),
  ((CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).obj F).map h =
    CategoryTheory.Limits.Sigma.desc fun y => CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩
-- Mathlib.Order.Concept
Concept.instInhabited : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → Inhabited (Concept α β r)
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_mul' : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a b : ℚ},
  ↑a.den ≠ 0 →
    ↑b.den ≠ 0 →
      Lean.Grind.Field.NormNum.ofRat (a * b) = Lean.Grind.Field.NormNum.ofRat a * Lean.Grind.Field.NormNum.ofRat b
-- Mathlib.Data.EReal.Operations
EReal.add_le_of_forall_lt : ∀ {a b c : EReal}, (∀ a' < a, ∀ b' < b, a' + b' ≤ c) → a + b ≤ c
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.uproj.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {i : ℕ} {var : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_9} {i_1 : ℕ}
  {var_1 : Lean.FVarId} {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_9},
  Lean.Compiler.LCNF.LetValue.uproj i var h = Lean.Compiler.LCNF.LetValue.uproj i_1 var_1 h_1 → i = i_1 ∧ var = var_1
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_univ_le_add_compl : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  (s : Set α), μ Set.univ ≤ μ s + μ sᶜ
-- Mathlib.CategoryTheory.Elements
/-- If `F` is corepresented by `X`, `X` with its universal element is the initial object of
`F.Elements.`  -/
CategoryTheory.Functor.Elements.isInitialOfCorepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type u_1)} →
      {X : C} →
        (h : F.CorepresentableBy X) →
          CategoryTheory.Limits.IsInitial (CategoryTheory.Functor.Elements.initialOfCorepresentableBy h)
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.boundedBy_zero : ∀ {α : Type u_1}, MeasureTheory.OuterMeasure.boundedBy 0 = 0
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
uniformContinuous_nndist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α], UniformContinuous fun p => nndist p.1 p.2
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.eqToHom_toOrderHom : ∀ {x y : SimplexCategory} (h : CategoryTheory.WithInitial.of x = CategoryTheory.WithInitial.of y),
  SimplexCategory.Hom.toOrderHom (CategoryTheory.WithInitial.down (CategoryTheory.eqToHom h)) =
    (Fin.castOrderIso ⋯).toOrderEmbedding.toOrderHom
-- Mathlib.SetTheory.Lists
Lists'.toList.eq_1 : ∀ {α : Type u_1} (a : α), (Lists'.atom a).toList = []
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- Constructor for morphisms into the chosen end of a functor.  -/
CategoryTheory.Limits.chosenEnd.lift : {J : Type u_3} →
  {C : Type u_4} →
    [inst : CategoryTheory.Category.{v_3, u_4} C] →
      [inst_1 : CategoryTheory.Category.{v_4, u_3} J] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] →
            {X : C} →
              (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) →
                (∀ ⦃i j : J⦄ (g : i ⟶ j),
                    CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
                      CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) →
                  (X ⟶ CategoryTheory.Limits.chosenEnd F)
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixedPoints_addSubgroup_antitone : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α],
  Antitone fun P => AddAction.fixedPoints (↥P) α
-- Mathlib.Util.Notation3
/-- Returns a `Term` that represents a `Matcher` for the given pattern `stx`.
The `boundNames` set determines which identifiers are variables in the pattern.
Fails in the `OptionT` sense if it comes across something it's unable to handle.

Also returns constant names that could serve as a key for a delaborator.
For example, if it's for a function `f`, then `app.f`.  -/
Mathlib.Notation3.mkExprMatcher : Lean.Term → Array Lean.Name → OptionT Lean.Elab.TermElabM (List Mathlib.Notation3.DelabKey × Lean.Term)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.mk.injEq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴}
  (toNatTrans : CategoryTheory.NatTrans F.toFunctor G.toFunctor)
  (isHomLift' :
    autoParam (∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (toNatTrans.app a))
      CategoryTheory.BasedNatTrans.isHomLift'._autoParam)
  (toNatTrans_1 : CategoryTheory.NatTrans F.toFunctor G.toFunctor)
  (isHomLift'_1 :
    autoParam (∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (toNatTrans_1.app a))
      CategoryTheory.BasedNatTrans.isHomLift'._autoParam),
  ({ toNatTrans := toNatTrans, isHomLift' := isHomLift' } =
      { toNatTrans := toNatTrans_1, isHomLift' := isHomLift'_1 }) =
    (toNatTrans = toNatTrans_1)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.reverse_bijective : ∀ {T : Type u_1}, Function.Bijective ContextFreeGrammar.reverse
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instRepr : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Repr α] → [Repr β] → Repr (Std.TreeMap.Raw α β cmp)
-- Mathlib.Order.Concept
Concept.swap_swap : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r), c.swap.swap = c
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.zero : (R : Type u_1) → [inst : Zero R] → Zero (ArithmeticFunction R)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prodAssoc_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {τ : MeasureTheory.Measure γ}
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite τ],
  MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Clean.State.mk.sizeOf_spec : ∀ (used : Lean.PHashSet Lean.Name) (next : Lean.PHashMap Lean.Name ℕ),
  sizeOf { used := used, next := next } = 1 + sizeOf used + sizeOf next
-- Mathlib.Algebra.Group.Defs
isMulCommutative_iff : ∀ {M : Type u_2} [inst : Mul M], IsMulCommutative M ↔ ∀ (a b : M), a * b = b * a
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.shearMulRight_coe : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G],
  ⇑(Homeomorph.shearMulRight G) = fun z => (z.1, z.1 * z.2)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α}, k ∉ t₁ → Std.ExtDTreeMap.Const.get? (t₁ \ t₂) k = none
-- Init.Data.Int.Order
Int.le_neg_of_le_neg : ∀ {a b : ℤ}, a ≤ -b → b ≤ -a
-- Mathlib.Data.Rat.Cast.Defs
Rat.commute_cast : ∀ {α : Type u_3} [inst : DivisionRing α] (a : α) (r : ℚ), Commute a ↑r
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_lt_one_of_lt' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, a < 1 → b < c → a * b < c
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_apply_of_not_continuousOn : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f : R → R} (a : A),
  ¬ContinuousOn f (spectrum R a) → cfc f a = 0
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.deterministic_deterministic : ∀ (X Y : SFinKer) (κ : ProbabilityTheory.Kernel X.carrier Y.carrier) [ProbabilityTheory.IsDeterministic κ]
  [inst : ProbabilityTheory.IsMarkovKernel κ], CategoryTheory.Deterministic { hom := κ, property := ⋯ }
-- Mathlib.Algebra.Order.Ring.StandardPart
/-- The constructor for `FiniteElement`.  -/
ArchimedeanClass.FiniteElement.mk : {K : Type u_1} →
  [inst : LinearOrder K] →
    [inst_1 : Field K] →
      [inst_2 : IsOrderedRing K] → (x : K) → 0 ≤ ArchimedeanClass.mk x → ArchimedeanClass.FiniteElement K
-- Init.Data.UInt.Lemmas
UInt32.toFin_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatClamp n).toFin = ⟨n, hn⟩
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_pow : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (f : F →L[𝕜₂] F) (n : ℕ),
  ContinuousLinearMapWOT.ofCLM (f ^ n) = ContinuousLinearMapWOT.ofCLM f ^ n
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.op_smul_set_stabilizer_subset : ∀ {G : Type u_1} [inst : Group G] {a : G} {s : Set G}, a ∈ s → MulOpposite.op a • ↑(MulAction.stabilizer G s) ⊆ s
-- Mathlib.Algebra.Homology.Homotopy
/-- homotopy is closed under composition  -/
Homotopy.comp : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C₁ C₂ C₃ : HomologicalComplex V c} →
            {f₁ g₁ : C₁ ⟶ C₂} →
              {f₂ g₂ : C₂ ⟶ C₃} →
                Homotopy f₁ g₁ →
                  Homotopy f₂ g₂ →
                    Homotopy (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp g₁ g₂)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trNormal.eq_5 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal (Turing.TM2.Stmt.branch a q₁ q₂) =
    Turing.TM1.Stmt.branch (fun x => a) (Turing.TM2to1.trNormal q₁) (Turing.TM2to1.trNormal q₂)
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` is a commutative semigroup.  -/
Subsemigroup.closureCommSemigroupOfComm : (M : Type u_1) →
  [inst : Semigroup M] → {s : Set M} → (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) → CommSemigroup ↥(Subsemigroup.closure s)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.flatMap_eq_flatMapTR.go : ∀ (α : Type u_2) (β : Type u_1) (f : α → List β) (as : List α) (acc : Array β),
  List.flatMapTR.go✝ f as acc = acc.toList ++ List.flatMap f as
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.entryAtIdx_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : t₁.WF)
  (h₂ : t₂.WF) (h : t₁.Equiv t₂) {i : ℕ} {h' : i < t₁.size}, t₁.entryAtIdx ⋯ i h' = t₂.entryAtIdx ⋯ i ⋯
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonServerInfo : Lean.ToJson Lean.Lsp.ServerInfo
-- Mathlib.Data.Nat.BinaryRec
/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases  -/
Nat.binaryRecFromOne : {motive : ℕ → Sort u} →
  motive 0 → motive 1 → ((b : Bool) → (n : ℕ) → n ≠ 0 → motive n → motive (Nat.bit b n)) → (n : ℕ) → motive n
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.hasImage_comp_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g],
  CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.toOpen_eq : ∀ (R : CommRingCat) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R)),
  CommRingCat.ofHom (algebraMap ↑R ↑((AlgebraicGeometry.Spec.structureSheaf ↑R).presheaf.obj (Opposite.op U))) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
      ((AlgebraicGeometry.Spec R).presheaf.map (CategoryTheory.homOfLE ⋯).op)
-- Mathlib.Algebra.Lie.Weights.Linear
_private.Mathlib.Algebra.Lie.Weights.Linear.0.LieModule.shiftedGenWeightSpace.aux : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R) [h : Nontrivial ↥(LieModule.shiftedGenWeightSpace R L M χ)],
  LieModule.genWeightSpace M χ ≠ ⊥
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.Eval.Result.mk.injEq : ∀ (expr : Mathlib.Tactic.BicategoryLike.NormalExpr) (proof : Lean.Expr)
  (expr_1 : Mathlib.Tactic.BicategoryLike.NormalExpr) (proof_1 : Lean.Expr),
  ({ expr := expr, proof := proof } = { expr := expr_1, proof := proof_1 }) = (expr = expr_1 ∧ proof = proof_1)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Vertical composition of modifications.  -/
CategoryTheory.Oplax.StrongTrans.Modification.vcomp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ ι : F ⟶ G} →
            CategoryTheory.Oplax.StrongTrans.Modification η θ →
              CategoryTheory.Oplax.StrongTrans.Modification θ ι → CategoryTheory.Oplax.StrongTrans.Modification η ι
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_X_pow_add_C : ∀ {R : Type u} [Nontrivial R] [inst : Semiring R] {n : ℕ} {r : R}, (Polynomial.X ^ n + Polynomial.C r).natDegree = n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
SpectrumRestricts.isClosedEmbedding_starAlgHom : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S] [inst_6 : StarRing S]
  [inst_7 : MetricSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S] [inst_10 : Ring A]
  [inst_11 : StarRing A] [inst_12 : Algebra S A] [inst_13 : Algebra R S] [inst_14 : Algebra R A]
  [inst_15 : IsScalarTower R S A] [inst_16 : StarModule R S] [inst_17 : ContinuousSMul R S]
  [inst_18 : TopologicalSpace A] [CompleteSpace R] {a : A} {φ : C(↑(spectrum S a), S) →⋆ₐ[S] A},
  Topology.IsClosedEmbedding ⇑φ →
    ∀ {f : C(S, R)} (h : SpectrumRestricts a ⇑f),
      IsUniformEmbedding ⇑(algebraMap R S) → Topology.IsClosedEmbedding ⇑(SpectrumRestricts.starAlgHom φ h)
-- Mathlib.Order.SuccPred.Archimedean
/-- **Alias** of `Order.pred_min`. -/
pred_min : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] (a b : α),
  Order.pred (min a b) = min (Order.pred a) (Order.pred b)
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- `Finsupp.mapRange` as a `LinearEquiv`.  -/
Finsupp.mapRange.linearEquiv : {α : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {R : Type u_5} →
        {R₂ : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : Semiring R₂] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : Module R M] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R₂ N] →
                      {σ₁₂ : R →+* R₂} →
                        {σ₂₁ : R₂ →+* R} →
                          [inst_6 : RingHomInvPair σ₁₂ σ₂₁] →
                            [inst_7 : RingHomInvPair σ₂₁ σ₁₂] → (M ≃ₛₗ[σ₁₂] N) → (α →₀ M) ≃ₛₗ[σ₁₂] α →₀ N
-- Mathlib.Logic.Basic
forall₃_true_iff : ∀ {α : Sort u_1} {β : α → Sort u_3} {γ : (a : α) → β a → Sort u_4}, (∀ (a : α) (b : β a) (a : γ a b), True) ↔ True
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- If `x : R` is multiplicative for `f`, then `seminormFromConst' c f x = f x`.  -/
seminormFromConst_apply_of_isMul : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → ∀ {x : R}, (∀ (y : R), f (x * y) = f x * f y) → seminormFromConst' c f x = f x
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essImage_ext : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : F.EssImageSubcategory} (f g : X ⟶ Y),
  F.essImage.ι.map f = F.essImage.ι.map g → f = g
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.signExtend_elim' : ∀ {v : ℕ} {x : BitVec v} {w : ℕ}, w ≤ v → BitVec.signExtend w x = BitVec.extractLsb' 0 w x
-- Init.Data.Int.DivMod.Lemmas
Int.add_neg_mul_emod_self_left : ∀ (a b c : ℤ), (a + -(b * c)) % b = a % b
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsTransitive.inter : ∀ {x y : ZFSet.{u}}, x.IsTransitive → y.IsTransitive → (x ∩ y).IsTransitive
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.supNorm_le_choose_natDegree_div_two_mul_mahlerMeasure : ∀ (p : Polynomial ℂ), p.supNorm ≤ ↑(p.natDegree.choose (p.natDegree / 2)) * p.mahlerMeasure
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair_obj : ∀ (x : CategoryTheory.Limits.WalkingParallelPair),
  CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.obj x =
    match x with
    | CategoryTheory.Limits.WalkingParallelPair.one => CategoryTheory.Limits.WalkingReflexivePair.zero
    | CategoryTheory.Limits.WalkingParallelPair.zero => CategoryTheory.Limits.WalkingReflexivePair.one
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.separableSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  TopologicalSpace.SeparableSpace (TopologicalSpace.Compacts α) ↔ TopologicalSpace.SeparableSpace α
-- Init.Data.String.Defs
String.exists_eq_asString : ∀ (s : String), ∃ l, s = String.ofList l
-- Mathlib.RingTheory.Ideal.Over
/-- An `A ⧸ p`-algebra isomorphism between `B ⧸ P` and `C ⧸ Q` induced by an `A`-algebra
isomorphism between `B` and `C`, where `P = σ⁻¹ Q`.  -/
Ideal.Quotient.algEquivOfEqComap : {A : Type u_3} →
  {B : Type u_4} →
    {C : Type u_5} →
      [inst : CommRing A] →
        [inst_1 : CommRing B] →
          [inst_2 : CommRing C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra A C] →
                {P : Ideal B} →
                  {Q : Ideal C} →
                    (p : Ideal A) →
                      [inst_5 : Q.LiesOver p] →
                        [inst_6 : P.LiesOver p] →
                          {E : Type u_7} →
                            [inst_7 : EquivLike E B C] →
                              [inst_8 : AlgEquivClass E A B C] → (σ : E) → P = Ideal.comap σ Q → (B ⧸ P) ≃ₐ[A ⧸ p] C ⧸ Q
-- Mathlib.Algebra.Category.Grp.Yoneda
/-- The `AddCommGrpCat`-valued coyoneda embedding composed with the forgetful functor is the usual
coyoneda embedding.  -/
AddCommGrpCat.coyonedaForget : AddCommGrpCat.coyoneda.comp
    ((CategoryTheory.Functor.whiskeringRight AddCommGrpCat AddCommGrpCat (Type u_1)).obj
      (CategoryTheory.forget AddCommGrpCat)) ≅
  CategoryTheory.coyoneda
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.map_iInf_of_ker_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  Function.Surjective ⇑f →
    ∀ {ι : Sort u_8} {p : ι → Submodule R M}, f.ker ≤ ⨅ i, p i → Submodule.map f (⨅ i, p i) = ⨅ i, Submodule.map f (p i)