mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Quiver.Symmetric
Prefunctor.symmetrify_mapReverse : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (φ : U ⥤q V), φ.symmetrify.MapReverse
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.isDefiniteRef : Lean.IR.IRType → Bool
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.instProd_2 : ∀ {R : Type u} [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S], Algebra.Etale (R × S) S
-- Mathlib.Order.Monotone.Basic
/-- If `α` is a nonempty preorder with no maximal elements, then there exists a strictly monotone
function `ℕ → α`.  -/
Nat.exists_strictMono : ∀ (α : Type u) [inst : Preorder α] [Nonempty α] [NoMaxOrder α], ∃ f, StrictMono f
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to a set is bounded by the distance to any point in this set.  -/
Metric.infDist_le_dist_of_mem : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α}, y ∈ s → Metric.infDist x s ≤ dist x y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- `X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃)` is the pushout `(X₁ ⨿[Z₁] X₂) ×[X₂] (X₂ ⨿[Z₂] X₃)`.  -/
CategoryTheory.Limits.pushoutPushoutRightIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Z₁ Z₂ : C} →
      (g₁ : Z₁ ⟶ X₁) →
        (g₂ : Z₁ ⟶ X₂) →
          (g₃ : Z₂ ⟶ X₂) →
            (g₄ : Z₂ ⟶ X₃) →
              [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂] →
                [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPushout g₁
                        (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] →
                    CategoryTheory.Limits.IsColimit
                      (CategoryTheory.Limits.PushoutCocone.mk
                        (CategoryTheory.Limits.pushout.desc
                          (CategoryTheory.Limits.pushout.inl g₁
                            (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄)
                            (CategoryTheory.Limits.pushout.inr g₁
                              (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))))
                          ⋯)
                        (CategoryTheory.Limits.pushout.inr g₁
                          (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
                        ⋯)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exsphere_compl : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.exsphere signsᶜ = s.exsphere signs
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- For any vector space, `dualAnnihilator` and `dualCoannihilator` gives an antitone order
isomorphism between the finite-codimensional subspaces in the vector space and the
finite-dimensional subspaces in its dual.  -/
Subspace.orderIsoFiniteCodimDim : {K : Type u_4} →
  {V : Type u_5} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → { W // FiniteDimensional K (V ⧸ W) } ≃o { W // FiniteDimensional K ↥W }ᵒᵈ
-- Mathlib.Order.Hom.Set
OrderIso.setCongr_symm_apply : ∀ {α : Type u_1} [inst : Preorder α] (s t : Set α) (h : s = t) (b : { b // (fun x => x ∈ t) b }),
  (RelIso.symm (OrderIso.setCongr s t h)) b = ⟨↑b, ⋯⟩
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.ae_le_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {β : ι → Type u_4}
  [inst_3 : (i : ι) → Preorder (β i)] {f f' : (i : ι) → α i → β i},
  (∀ (i : ι), f i ≤ᵐ[μ i] f' i) → (fun x i => f i (x i)) ≤ᵐ[MeasureTheory.Measure.pi μ] fun x i => f' i (x i)
-- Mathlib.Data.Num.Basic
/-- The successor of a `PosNum`.  -/
PosNum.succ : PosNum → PosNum
-- Aesop.Rule.Forward
Aesop.ForwardRulePriority.normSafe.sizeOf_spec : ∀ (n : ℤ), sizeOf (Aesop.ForwardRulePriority.normSafe n) = 1 + sizeOf n
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- Given `x : X` and `y : Y` such that `f x = s = g y`, this is the
canonical map `κ(x) ⟶ κ(x) ⊗[κ(s)] κ(y)`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInl : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} → {g : Y ⟶ S} → (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) → X.residueField T.x ⟶ T.tensor
-- Init.Data.String.Defs
String.Pos.mk.inj : ∀ {s : String} {offset : String.Pos.Raw} {isValid : String.Pos.Raw.IsValid s offset} {offset_1 : String.Pos.Raw}
  {isValid_1 : String.Pos.Raw.IsValid s offset_1},
  { offset := offset, isValid := isValid } = { offset := offset_1, isValid := isValid_1 } → offset = offset_1
-- Lean.Expr
Lean.Expr.letE.sizeOf_spec : ∀ (declName : Lean.Name) (type value body : Lean.Expr) (nondep : Bool),
  sizeOf (Lean.Expr.letE declName type value body nondep) =
    1 + sizeOf declName + sizeOf type + sizeOf value + sizeOf body + sizeOf nondep
-- Mathlib.Logic.Function.Basic
Function.Bijective.existsUnique_iff : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → ∀ {p : β → Prop}, (∃! y, p y) ↔ ∃! x, p (f x)
-- Init.Data.BitVec.Bitblast
BitVec.msb_neg_of_ne_intMin_of_ne_zero : ∀ {w : ℕ} {x : BitVec w}, x ≠ BitVec.intMin w → x ≠ 0#w → (-x).msb = !x.msb
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- Eta-expanded form of `AbsolutelyContinuousOnInterval.smul`

---

If `f` and `g` are absolutely continuous on `uIcc a b`, then `f • g` is absolutely continuous
on `uIcc a b`.  -/
AbsolutelyContinuousOnInterval.fun_smul : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {M : Type u_3} [inst_1 : SeminormedRing M]
  [inst_2 : Module M F] [NormSMulClass M F] {f : ℝ → M} {g : ℝ → F},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (fun i => f i • g i) a b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey? k = none
-- Mathlib.Algebra.CharP.Two
CharTwo.natCast_cases : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] [CharP R 2] (n : ℕ), ↑n = 0 ∨ ↑n = 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_filter_not_contains_map_fst_of_contains_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getValue? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = none
-- Lean.Server.ServerTask
Lean.Server.ServerTask.waitAny : {α : Type} →
  (tasks : List (Lean.Server.ServerTask α)) →
    autoParam (tasks.length > 0) Lean.Server.ServerTask.waitAny._auto_1 → BaseIO α
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.get? k = t.get? k'
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
/-- Given trivializations `e₁`, `e₂` for vector bundles `E₁`, `E₂` over a base `B`,
`Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂` is the induced pretrivialization for the
continuous `σ`-semilinear maps from `E₁` to `E₂`. That is, the map which will later become a
trivialization, after the bundle of continuous semilinear maps is equipped with the right
topological vector bundle structure.  -/
Bundle.Pretrivialization.continuousAlternatingMap : (𝕜 : Type u_1) →
  (ι : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      {B : Type u_3} →
        [inst_1 : TopologicalSpace B] →
          {F₁ : Type u_4} →
            [inst_2 : NormedAddCommGroup F₁] →
              [inst_3 : NormedSpace 𝕜 F₁] →
                {E₁ : B → Type u_5} →
                  [inst_4 : (x : B) → AddCommGroup (E₁ x)] →
                    [inst_5 : (x : B) → Module 𝕜 (E₁ x)] →
                      [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                        {F₂ : Type u_6} →
                          [inst_7 : NormedAddCommGroup F₂] →
                            [inst_8 : NormedSpace 𝕜 F₂] →
                              {E₂ : B → Type u_7} →
                                [inst_9 : (x : B) → AddCommGroup (E₂ x)] →
                                  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] →
                                    [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                      [inst_12 : (x : B) → TopologicalSpace (E₁ x)] →
                                        [FiberBundle F₁ E₁] →
                                          [inst_14 : (x : B) → TopologicalSpace (E₂ x)] →
                                            [FiberBundle F₂ E₂] →
                                              (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) →
                                                (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) →
                                                  [Bundle.Trivialization.IsLinear 𝕜 e₁] →
                                                    [Bundle.Trivialization.IsLinear 𝕜 e₂] →
                                                      Bundle.Pretrivialization (F₁ [⋀^ι]→L[𝕜] F₂) Bundle.TotalSpace.proj
-- Mathlib.Data.Int.Log
Int.log_zpow : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, 1 < b → ∀ (z : ℤ), Int.log b (↑b ^ z) = z
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExpKernel_ae_eq_condExp : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  m ≤ mΩ →
    ∀ {s : Set Ω},
      MeasurableSet s → (fun ω => ((ProbabilityTheory.condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun ω => 1 | m]
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mk.injEq : ∀ {K : Type u} [inst : DivisionRing K] (toSubring : Subring K)
  (inv_mem' : ∀ x ∈ toSubring.carrier, x⁻¹ ∈ toSubring.carrier) (toSubring_1 : Subring K)
  (inv_mem'_1 : ∀ x ∈ toSubring_1.carrier, x⁻¹ ∈ toSubring_1.carrier),
  ({ toSubring := toSubring, inv_mem' := inv_mem' } = { toSubring := toSubring_1, inv_mem' := inv_mem'_1 }) =
    (toSubring = toSubring_1)
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangle_mor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangle comm h₁₂ h₂₃ h₁₃ h).mor₁ = h.m₁
-- Mathlib.Logic.Relation
Relation.transGen_eq_self : ∀ {α : Type u_1} {r : α → α → Prop} [IsTrans α r], Relation.TransGen r = r
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.coe_compl : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} (s : L.DefinableSet A α),
  ↑sᶜ = (↑s)ᶜ
-- Mathlib.ModelTheory.Substructures
/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective.  -/
FirstOrder.Language.Substructure.gciMapComap : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          {f : L.Hom M N} →
            Function.Injective ⇑f →
              GaloisCoinsertion (FirstOrder.Language.Substructure.map f) (FirstOrder.Language.Substructure.comap f)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instTransOrdOffset : Std.TransOrd Std.Time.Month.Offset
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.instContinuousEval : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [LocallyCompactPair A B], ContinuousEval (A →ₜ* B) A B
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.neg : ∀ {R : Type u_1} [inst : Ring R] {f : Polynomial R}, f.Splits → (-f).Splits
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.liftCover_coe' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {A : Set (Set α)}
  {F : (s : Set α) → s ∈ A → C(↑s, β)}
  {hF :
    ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
      (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩}
  {hA : ∀ (x : α), ∃ i ∈ A, i ∈ nhds x} {s : Set α} {hs : s ∈ A} (x : ↑s),
  (ContinuousMap.liftCover' A F hF hA) ↑x = (F s hs) x
-- Mathlib.Algebra.GroupWithZero.Regular
/-- In a non-trivial ring, the element `0` is not left-regular -- with typeclasses.  -/
not_isLeftRegular_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] [nR : Nontrivial R], ¬IsLeftRegular 0
-- Mathlib.Algebra.FreeAlgebra.Cardinality
FreeAlgebra.cardinalMk_le_max_lift : ∀ (R : Type u) [inst : CommSemiring R] (X : Type v),
  Cardinal.mk (FreeAlgebra R X) ≤
    max (max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk X))) Cardinal.aleph0
-- Mathlib.Algebra.Group.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
CommMonoid.mul_comm : ∀ {M : Type u} [self : CommMonoid M] (a b : M), a * b = b * a
-- Lean.SubExpr
/-- The coordinate `3 = maxChildren - 1` is
reserved to denote the type of the expression.  -/
Lean.SubExpr.Pos.typeCoord : ℕ
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.antitone_rpow_of_base_le_one : ∀ {b : ℝ}, 0 < b → b ≤ 1 → Antitone fun x => b ^ x
-- Lean.Widget.InteractiveGoal
/-- An interactive tactic-mode goal.  -/
Lean.Widget.InteractiveGoal : Type
-- Init.Data.Float.Model.Unpacked.Round
/-- Extract the accuracy of the mantissa.  -/
Float.Model.UnpackedFloat.ExtendedMantissa.accuracy : Float.Model.UnpackedFloat.ExtendedMantissa → Float.Model.UnpackedFloat.Accuracy
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The morphism property on `Under X` induced by a morphism property on `C`.  -/
CategoryTheory.MorphismProperty.under : {T : Type u_3} →
  [inst : CategoryTheory.Category.{v_3, u_3} T] →
    CategoryTheory.MorphismProperty T → {X : T} → CategoryTheory.MorphismProperty (CategoryTheory.Under X)
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.hasLimits : CategoryTheory.Limits.HasLimits AddGrpCat
-- Mathlib.Order.Interval.Basic
Interval.coe_le_coe : ∀ {α : Type u_1} [inst : Preorder α] {s t : NonemptyInterval α}, ↑s ≤ ↑t ↔ s ≤ t
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.instIsStrictlySupportedTruncLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], (K.truncLE e).IsStrictlySupported e
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.epsilon_ne_zero : Hyperreal.epsilon ≠ 0
-- Init.Data.String.Iterate
String.Slice.ByteIterator.s : String.Slice.ByteIterator → String.Slice
-- Mathlib.Analysis.Complex.Circle
Circle.instIsTopologicalGroup : IsTopologicalGroup Circle
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.full_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C), P.ι.Full
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_arrow_apply : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [inst_3 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0) {F : V → V → Type uF} {carrier : V → Type w}
  {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_4 : CategoryTheory.ConcreteCategory V F]
  (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f))),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject g).arrow)
      ((CategoryTheory.ConcreteCategory.hom (imageToKernel f g w)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.imageSubobject f).arrow) x
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.instMulEquivClass : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N], MulEquivClass (M ≃* N) M N
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseQuarterNumber : Std.Internal.Parsec.String.Parser Std.Time.Month.Quarter
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.functor_map_eq_inf : ∀ {X : TopCat} (U V : TopologicalSpace.Opens ↑X),
  ⋯.functor.obj ((TopologicalSpace.Opens.map U.inclusion').obj V) = V ⊓ U
-- Mathlib.Order.SetAccumulate
Set.subset_accumulate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α] {x : α}, s x ⊆ Set.accumulate s x
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.map_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {T : Type u_3} [inst_3 : Semiring T] (w : AbsoluteValue T S) (f : R →+* T) (x : WithAbs v),
  (WithAbs.map v w f) x = WithAbs.toAbs w (f x.ofAbs)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_prodMk_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (e₀ : E), ContDiff 𝕜 n fun f => (e₀, f)
-- Init.Data.Vector.Lemmas
_private.Init.Data.Vector.Lemmas.0.Array.eraseIdx!.eq_1 : ∀ {α : Type u} (xs : Array α) (i : ℕ),
  xs.eraseIdx! i =
    if h : i < xs.size then xs.eraseIdx i h
    else panicWithPosWithDecl "Init.Data.Array.Basic" "Array.eraseIdx!" 1842 47 "invalid index"
-- Mathlib.Data.Fintype.Defs
Finset.mem_filter_univ : ∀ {α : Type u_1} [inst : Fintype α] {p : α → Prop} [inst_1 : DecidablePred p] (x : α),
  x ∈ Finset.filter p Finset.univ ↔ p x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
/-- In the category of simplicial sets, an anodyne extension is a morphism
that has the left lifting property with respect to fibrations, where
a fibration is a morphism that has the right lifting property with respect
to horn inclusions. We do not introduce a typeclass for anodyne extensions
because when the Quillen model structure is fully upstreamed (TODO @joelriou),
the assumption `anodyneExtensions f` can be spelled as
`[Cofibration f] [WeakEquivalence f]`.  -/
SSet.anodyneExtensions : CategoryTheory.MorphismProperty SSet
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- The iterates of `C^n` functions on domains are `C^n`.  -/
ContMDiffOn.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {n : WithTop ℕ∞} {f : M → M},
  ContMDiffOn I I n f s → Set.MapsTo f s s → ∀ (k : ℕ), ContMDiffOn I I n f^[k] s
-- Mathlib.Data.PEquiv
PEquiv.mk.inj : ∀ {α : Type u} {β : Type v} {toFun : α → Option β} {invFun : β → Option α}
  {inv : ∀ (a : α) (b : β), invFun b = some a ↔ toFun a = some b} {toFun_1 : α → Option β} {invFun_1 : β → Option α}
  {inv_1 : ∀ (a : α) (b : β), invFun_1 b = some a ↔ toFun_1 a = some b},
  { toFun := toFun, invFun := invFun, inv := inv } = { toFun := toFun_1, invFun := invFun_1, inv := inv_1 } →
    toFun = toFun_1 ∧ invFun = invFun_1
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The bicategory of comonads in `B`.  -/
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat : (B : Type u) → [CategoryTheory.Bicategory B] → Type (max (max (max (max 0 u) v) 0) w)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The object property on `Over X` induced by a morphism property.  -/
CategoryTheory.MorphismProperty.overObj : {T : Type u_3} →
  [inst : CategoryTheory.Category.{v_3, u_3} T] →
    CategoryTheory.MorphismProperty T → {X : T} → CategoryTheory.ObjectProperty (CategoryTheory.Over X)
-- Mathlib.Analysis.Matrix.Normed
_private.Mathlib.Analysis.Matrix.Normed.0.Matrix.norm_unitOf : ∀ {α : Type u_5} [inst : NormedDivisionRing α] [inst_1 : NormedAlgebra ℝ α] (a : α), ‖Matrix.unitOf✝ a‖₊ = 1
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.cylinder_eq_pi : ∀ {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ), PiNat.cylinder x n = (↑(Finset.range n)).pi fun i => {x i}
-- Mathlib.Topology.Connected.TotallyDisconnected
instTotallyDisconnectedSpaceSum : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [TotallyDisconnectedSpace α]
  [TotallyDisconnectedSpace β], TotallyDisconnectedSpace (α ⊕ β)
-- Mathlib.NumberTheory.Fermat
/-- Fermat numbers: the `n`-th Fermat number is defined as `2^(2^n) + 1`.  -/
Nat.fermatNumber : ℕ → ℕ
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset : HAdd Std.Time.Nanosecond.Offset Std.Time.Millisecond.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.nnnorm_def : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)]
  (f : (i : ι) → G i), ‖f‖₊ = Finset.univ.sup fun b => ‖f b‖₊
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.chromaticNumber_le_sum_right : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W}, H.chromaticNumber ≤ (G ⊕g H).chromaticNumber
-- Mathlib.GroupTheory.GroupAction.Defs
/-- `fixedBy m` is the set of elements fixed by `m`.  -/
MulAction.fixedBy : {M : Type u_1} → (α : Type u_3) → [inst : Monoid M] → [MulAction M α] → M → Set α
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSESδ_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS₁ : S₁.ShortExact)
  (hS₂ : S₂.ShortExact) (f : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.triangleOfSESδ hS₁)
      ((CategoryTheory.shiftFunctor (DerivedCategory C) 1).map (DerivedCategory.Q.map f.τ₁)) =
    CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map f.τ₃) (DerivedCategory.triangleOfSESδ hS₂)
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.isClosed : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] [inst_8 : TopologicalSpace A] [inst_9 : IsSemitopologicalSemiring A]
  [inst_10 : ContinuousConstSMul R A] [inst_11 : ContinuousStar A] (x : A),
  IsClosed ↑(NonUnitalStarAlgebra.elemental R x)