mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictAntiOn_comp_ofDual_iff`. -/
StrictMonoOn.dual_left : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → StrictAntiOn (f ∘ ⇑OrderDual.ofDual) s
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
BinaryTree.treesOfNumNodesEq.eq_def : ∀ (x : ℕ),
  BinaryTree.treesOfNumNodesEq x =
    match x with
    | 0 => {BinaryTree.nil}
    | n.succ =>
      (Finset.HasAntidiagonal.antidiagonal n).attach.biUnion fun ijh =>
        BinaryTree.pairwiseNode (BinaryTree.treesOfNumNodesEq (↑ijh).1) (BinaryTree.treesOfNumNodesEq (↑ijh).2)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValueCast.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (l : List ((a : α) × β a))
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getValueCast a l h = (Std.Internal.List.getValueCast? a l).get ⋯
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
borel_eq_generateFrom_Iic : ∀ (α : Type u_1) [inst : TopologicalSpace α] [SecondCountableTopology α] [inst_2 : LinearOrder α] [OrderTopology α],
  borel α = MeasurableSpace.generateFrom (Set.range Set.Iic)
-- Mathlib.Topology.Connected.TotallyDisconnected
IsTotallySeparated.eq_1 : ∀ {α : Type u} [inst : TopologicalSpace α] (s : Set α),
  IsTotallySeparated s = s.Pairwise fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ s ⊆ u ∪ v ∧ Disjoint u v
-- Mathlib.Control.Applicative
Functor.Comp.seq_assoc : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
  [LawfulApplicative G] {α β γ : Type v} (x : Functor.Comp F G α) (f : Functor.Comp F G (α → β))
  (g : Functor.Comp F G (β → γ)), g <*> (f <*> x) = Function.comp <$> g <*> f <*> x
-- Mathlib.Logic.Basic
/-- **Alias** of `Decidable.em`. -/
dec_em : ∀ (p : Prop) [Decidable p], p ∨ ¬p
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjOpcyclesSelfIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B) {Z : C} (h : ((HomologicalComplex.single C c j).obj B).opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((HomologicalComplex.single C c j).map f) j)
        h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j B).hom h)
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- A local algebra isomorphism induces an algebra isomorphism on the residue fields.

See `mapAlgEquiv'` for a variant where the base ring `R` is also quotiented.  -/
IsLocalRing.ResidueField.mapAlgEquiv : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : IsLocalRing S] →
            [inst_3 : CommRing T] →
              [inst_4 : IsLocalRing T] →
                [inst_5 : Algebra R S] →
                  [inst_6 : Algebra R T] → (S ≃ₐ[R] T) → IsLocalRing.ResidueField S ≃ₐ[R] IsLocalRing.ResidueField T
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_mod : ∀ (a b : Ordinal.{u_4}), a % b % b = a % b
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instIsOrderedRing : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommSemiring α] [inst_2 : PartialOrder α]
  [inst_3 : CanonicallyOrderedAdd α] [inst_4 : NoZeroDivisors α] [inst_5 : Nontrivial α], IsOrderedRing (WithTop α)
-- Mathlib.CategoryTheory.Yoneda
/-- A chosen term in `F.CorepresentableBy (coreprX F)` when `F.IsCorepresentable` holds.  -/
CategoryTheory.Functor.corepresentableBy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor C (Type v)) → [hF : F.IsCorepresentable] → F.CorepresentableBy F.coreprX
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addHaarContent_outerMeasure_closure_pos : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G),
  0 < (MeasureTheory.Measure.haar.addHaarContent K₀).outerMeasure (closure ↑K₀)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.toUniformSpace_eq : ∀ {α : Type u} [inst : PseudoMetricSpace α], PseudoMetricSpace.toUniformSpace = UniformSpace.ofDist dist ⋯ ⋯ ⋯
-- Mathlib.Util.Export
Lean.Export.OfState : (α : Type) → [BEq α] → [Hashable α] → Type
-- Mathlib.GroupTheory.Order.Min
Monoid.minOrder.eq_1 : ∀ (α : Type u_2) [inst : Monoid α], Monoid.minOrder α = ⨅ a, ⨅ (_ : a ≠ 1), ⨅ (_ : IsOfFinOrder a), ↑(orderOf a)
-- Mathlib.Order.CompleteLattice.Basic
sInf_univ : ∀ {α : Type u_1} [inst : CompleteLattice α], sInf Set.univ = ⊥
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst.eq_1 : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] (a : σ → MvPowerSeries τ S) (f : MvPowerSeries σ R),
  MvPowerSeries.subst a f = MvPowerSeries.eval₂ (algebraMap R (MvPowerSeries τ S)) a f
-- Std.Time.Format.Basic
Std.Time.Awareness.instCoeTimeZone : Coe Std.Time.TimeZone Std.Time.Awareness
-- Std.Do.SPred.Laws
_private.Std.Do.SPred.Laws.0.Std.Do.SPred.entails.match_1.eq_2 : ∀ (motive : (σs : List (Type u_1)) → Std.Do.SPred σs → Std.Do.SPred σs → Sort u_2) (σ : Type u_1)
  (tail : List (Type u_1)) (P Q : Std.Do.SPred (σ :: tail)) (h_1 : (P Q : Std.Do.SPred []) → motive [] P Q)
  (h_2 : (σ : Type u_1) → (tail : List (Type u_1)) → (P Q : Std.Do.SPred (σ :: tail)) → motive (σ :: tail) P Q),
  (match σ :: tail, P, Q with
    | [], P, Q => h_1 P Q
    | σ :: tail, P, Q => h_2 σ tail P Q) =
    h_2 σ tail P Q
-- Mathlib.Analysis.ODE.PicardLindelof
/-- If the time-dependent vector field `f` is $C^n$ and the curve `α` is continuous, then
`picard f t₀ x₀ α` is also $C^n$. This version works for `n : ℕ∞`.

TODO: Extend to the analytic `n = ⊤` case.  -/
ODE.contDiffOn_enat_picard_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {α : ℝ → E}
  {u : Set E} {t₀ tmin tmax : ℝ},
  t₀ ∈ Set.Icc tmin tmax →
    ∀ {n : ℕ∞},
      ContDiffOn ℝ (↑n) (Function.uncurry f) (Set.Icc tmin tmax ×ˢ u) →
        ContinuousOn α (Set.Icc tmin tmax) →
          (∀ t ∈ Set.Icc tmin tmax, α t ∈ u) →
            ∀ (x₀ : E),
              (∀ t ∈ Set.Icc tmin tmax, α t = ODE.picard f t₀ x₀ α t) →
                ContDiffOn ℝ (↑n) (ODE.picard f t₀ x₀ α) (Set.Icc tmin tmax)
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [inst_5 : G.IsContinuous J K]
  (F : CategoryTheory.Sheaf J A),
  ((G.sheafAdjunctionCocontinuous A J K).counit.app F).hom = (G.op.ranAdjunction A).counit.app F.obj
-- Mathlib.Data.QPF.Multivariate.Constructions.Quot
/-- Functorial quotient type  -/
MvQPF.Quot1 : {n : ℕ} → {F : TypeVec.{u} n → Type u} → (⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) → TypeVec.{u} n → Type u
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.instBraidedCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.BraidedCategory (CommAlgCat R)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace E]
  {f : Ω → F} {g : Ω → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.Integrable (fun ω => (B (f ω)) (g ω)) μ →
      MeasureTheory.Integrable g μ → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (f ω)) (μ[g | m] ω)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Product of a multiset of elements in an intermediate field is in the intermediate field.  -/
IntermediateField.multiset_prod_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (m : Multiset L), (∀ a ∈ m, a ∈ S) → m.prod ∈ S
-- Mathlib.Topology.Sober
IsGenericPoint.def : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S : Set α}, IsGenericPoint x S → closure {x} = S
-- Mathlib.Algebra.Field.Basic
add_div_eq_mul_add_div : ∀ {K : Type u_1} [inst : DivisionSemiring K] {c : K} (a b : K), c ≠ 0 → a + b / c = (a * c + b) / c
-- Aesop.Forward.SlotIndex
Aesop.instOrdSlotIndex.ord : Aesop.SlotIndex → Aesop.SlotIndex → Ordering
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given closed range as a list in ascending order.
 -/
Std.Ric.toList : {α : Type u} →
  [Std.PRange.Least? α] →
    [inst : LE α] →
      [DecidableLE α] →
        [inst_2 : Std.PRange.UpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxc.IsAlwaysFinite α] → Std.Ric α → List α
-- Init.Data.List.OfFn
Fin.foldr_cons_eq_append : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α} {xs : List α}, Fin.foldr n (fun i xs => f i :: xs) xs = List.ofFn f ++ xs
-- Init.Data.String.Basic
String.Pos.Raw.isValid_append : ∀ {s t : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid (s ++ t) p ↔ String.Pos.Raw.IsValid s p ∨ s.rawEndPos ≤ p ∧ String.Pos.Raw.IsValid t (p - s)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_refl : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (ω : E → E →L[𝕜] F) (a : E),
  curveIntegralFun ω (Path.refl a) = 0
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- The Frobenius automorphism of `k` induces an automorphism of `K`.  -/
WittVector.FractionRing.frobenius : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst_1 : CommRing k] →
        [CharP k p] → [PerfectRing k p] → FractionRing (WittVector p k) ≃+* FractionRing (WittVector p k)
-- Mathlib.Order.PiLex
Pi.instOrderTopColexForallOfWellFoundedGT : {ι : Type u_1} →
  {β : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [WellFoundedGT ι] →
        [inst_2 : (a : ι) → PartialOrder (β a)] → [(a : ι) → OrderTop (β a)] → OrderTop (Colex ((a : ι) → β a))
-- Mathlib.Logic.Basic
/-- **Alias** of `Classical.propComplete`. -/
Classical.prop_complete : ∀ (a : Prop), a = True ∨ a = False
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
/-- The identity, as a `X`-continous map.  -/
Topology.ContinuousMapGeneratedBy.id : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} → [inst_1 : TopologicalSpace Y] → Topology.ContinuousMapGeneratedBy X Y Y
-- Mathlib.Algebra.Torsor.Defs
/-- Multiplying by a group element then dividing by the original point
produces that group element.  -/
smul_sdiv : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (g : G) (p : P), g • p /ₛ p = g
-- Std.Time.Format.DateFormat
/-- Full weekday names (7 elements, index 0 = Monday).
 -/
Std.Time.DateFormatSymbols.weekdayLong : Std.Time.DateFormatSymbols → Vector String 7
-- Mathlib.Data.Set.Basic
Set.eq_empty_iff_forall_notMem : ∀ {α : Type u} {s : Set α}, s = ∅ ↔ ∀ (x : α), x ∉ s
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.Context.uri : Lean.Server.Completion.Context✝ → Lean.Lsp.DocumentUri
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- **Alias** of `Polynomial.div_prod_eq_quo_add_sum_rem_div`.

---

Let `R` be an integral domain and `f : R[X]`. Let `s` be a finite index set.
Then a fraction of the form `f / ∏ i ∈ s, g i` evaluated in a field `K` containing `R[X]`
can be rewritten as `q + ∑ i ∈ s, r i / g i`, where
`degree (r i) < degree (g i)`, provided that the `g i` are monic and pairwise coprime.
See `quo_add_sum_rem_div_unique` for the uniqueness of this representation.  -/
div_eq_quo_add_sum_rem_div : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra (Polynomial R) K]
  [FaithfulSMul (Polynomial R) K] (f : Polynomial R) {ι : Type u_3} {g : ι → Polynomial R} {s : Finset ι},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)
-- Init.Data.Int.Linear
Int.Internal.Linear.mod_eq' : ∀ (a b b' k : ℤ), b = b' → (k == a % b') = true → a % b = k
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.symm_monoidHomCongrRightEquiv : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : MulOneClass M] [inst_1 : Monoid N₁] [inst_2 : Monoid N₂]
  (e : N₁ ≃* N₂), e.monoidHomCongrRightEquiv.symm = e.symm.monoidHomCongrRightEquiv
-- Mathlib.Analysis.Matrix.Spectrum
/-- The spectrum of a matrix `A` coincides with the spectrum of `toEuclideanLin A`.  -/
Matrix.spectrum_toEuclideanLin : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n],
  spectrum 𝕜 (Matrix.toEuclideanLin A) = spectrum 𝕜 A
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- `n₀` is always positive  -/
AkraBazziRecurrence.n₀_gt_zero : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r), 0 < self.n₀
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.State.mk.sizeOf_spec : ∀ (numSteps : ℕ) (cache : Lean.Meta.Sym.DSimp.Cache),
  sizeOf { numSteps := numSteps, cache := cache } = 1 + sizeOf numSteps + sizeOf cache
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Integrable.comp_mul_left' : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] {g : ℝ → F},
  MeasureTheory.Integrable g MeasureTheory.volume →
    ∀ {R : ℝ}, R ≠ 0 → MeasureTheory.Integrable (fun x => g (R * x)) MeasureTheory.volume
-- Mathlib.RingTheory.RingHomProperties
RingHom.HasEqualizers.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.instSeminormedAddCommGroup : {ι : Type u_1} →
  [Fintype ι] →
    {𝕜 : Type u_2} →
      {E : ι → Type u_3} →
        [inst : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_1 : NormedField 𝕜] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] → SeminormedAddCommGroup (PiTensorProduct 𝕜 fun i => E i)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.boundedBy_measure : ∀ {α : Type u_1} [ms : MeasurableSpace α] (μ : MeasureTheory.Measure α),
  MeasureTheory.OuterMeasure.boundedBy ⇑μ = μ.toOuterMeasure
-- Mathlib.CategoryTheory.Limits.Skeleton
CategoryTheory.Limits.hasLimitsOfSize_thinSkeleton : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [Quiver.IsThin C]
  [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} C],
  CategoryTheory.Limits.HasLimitsOfSize.{w, w', u₂, u₂} (CategoryTheory.ThinSkeleton C)
-- Mathlib.CategoryTheory.Products.Basic
/-- `snd` is the functor `(X, Y) ↦ Y`.  -/
CategoryTheory.Prod.snd : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C × D) D
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.I₀) {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X j ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd s.fst (𝒰.f j)) h)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsInitial Y)
  (c : CategoryTheory.Limits.BinaryCofan X Y), Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inl
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Algebra.TensorProduct.linearEquivIncludeRange_tmul : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] (x : S) (y : T),
  (Algebra.TensorProduct.linearEquivIncludeRange R S T) (x ⊗ₜ[R] y) =
    Algebra.TensorProduct.includeLeft.rangeRestrict x ⊗ₜ[R] Algebra.TensorProduct.includeRight.rangeRestrict y
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a p : α}, a ≠ 0 → Irreducible p → p ∣ a → ∃ q ∈ UniqueFactorizationMonoid.normalizedFactors a, Associated p q
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- `filtered` will be shown in the filtered view.  -/
Mathlib.Tactic.ClickSuggestions.Result.filtered : {α : Type} → Mathlib.Tactic.ClickSuggestions.Result α → Option ProofWidgets.Html
-- Mathlib.Algebra.Ring.Equiv
/-- A ring iso `α ≃+* β` can equivalently be viewed as a ring iso `αᵐᵒᵖ ≃+* βᵐᵒᵖ`.  -/
RingEquiv.op : {α : Type u_7} →
  {β : Type u_8} → [inst : Add α] → [inst_1 : Mul α] → [inst_2 : Add β] → [inst_3 : Mul β] → α ≃+* β ≃ (αᵐᵒᵖ ≃+* βᵐᵒᵖ)
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  {k k' : ℕ} {hk : k < n} {hk' : k' < n} {a : (X k hk).fst} {a_1 : (X k' hk').fst} {k_1 k'_1 : ℕ} {hk_1 : k_1 < n}
  {hk'_1 : k'_1 < n} {a_2 : (X k_1 hk_1).fst} {a_3 : (X k'_1 hk'_1).fst},
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min✝ hk hk' a a_1 =
      CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min✝ hk_1 hk'_1 a_2 a_3 →
    k = k_1 ∧ k' = k'_1 ∧ a ≍ a_2 ∧ a_1 ≍ a_3
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_self : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Ioo a a = ∅
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The backward direction of `Comon (Mon C) ≌ Mon (Comon C)`  -/
CategoryTheory.Bimon.ofMonComon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.Mon (CategoryTheory.Comon C)) (CategoryTheory.Bimon C)
-- Mathlib.RingTheory.PrincipalIdealDomain
PrincipalIdealRing.isNoetherianRing : ∀ {R : Type u} [inst : Semiring R] [IsPrincipalIdealRing R], IsNoetherianRing R
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.integrable_prodLp_iff : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)},
  MeasureTheory.Integrable f μ ↔
    MeasureTheory.Integrable (fun x => (f x).fst) μ ∧ MeasureTheory.Integrable (fun x => (f x).snd) μ
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Reinterpret `f : α →ᵤ β` as an element of `α → β`.  -/
UniformFun.toFun : {α : Type u_1} → {β : Type u_2} → UniformFun α β ≃ (α → β)
-- Mathlib.Topology.NhdsWithin
mem_nhdsSet_subtype_iff_nhdsSetWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t u : Set ↑s},
  u ∈ nhdsSet t ↔ Subtype.val '' u ∈ nhdsSetWithin (Subtype.val '' t) s
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_iSup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_3}
  [Finite ι] (N : ι → Submodule R M), (∀ (i : ι), (N i).FG) → (iSup N).FG
-- Init.Control.Lawful.Basic
/-- `bind` is associative.

Changing the nesting of `bind` calls while maintaining the order of computations results in an
equivalent computation. This means that `bind` is not doing more than data-dependent sequencing.
 -/
LawfulMonad.bind_assoc : ∀ {m : Type u → Type v} {inst : Monad m} [self : LawfulMonad m] {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ),
  x >>= f >>= g = x >>= fun x => f x >>= g
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.measure_pos_of_nonempty_interior : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  {s : Set X}, (interior s).Nonempty → 0 < μ s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.homMk'_mk_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y Y' Y'' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y'),
  (CategoryTheory.CostructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.comp g' g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f)).homMk' g')
        ((CategoryTheory.CostructuredArrow.mk f).homMk' g))
-- Mathlib.Algebra.Star.BigOperators
isSelfAdjoint_sum : ∀ {R : Type u_1} {ι : Type u_2} [inst : AddCommMonoid R] [inst_1 : StarAddMonoid R] (s : Finset ι) {x : ι → R},
  (∀ i ∈ s, IsSelfAdjoint (x i)) → IsSelfAdjoint (∑ i ∈ s, x i)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.elementsFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  CategoryTheory.Functor.elementsFunctor.obj F = CategoryTheory.Cat.of F.Elements
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.smul_iff : ∀ {M₁ : Type u_3} {M₂ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {S : Type u_6} [inst_4 : Group S]
  [inst_5 : DistribMulAction S M₂] [ContinuousConstSMul S M₂] {f : M₁ → M₂} (c : S),
  IsCompactOperator (c • f) ↔ IsCompactOperator f