mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.DiscrTree.Types
/-- Discrimination tree trie. See `DiscrTree`.
 -/
Lean.Meta.DiscrTree.Trie : Type → Type
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Given `w : TwoSquare T L R B` and `X₃ : C₃`, this is the obvious functor
`CostructuredArrow L X₃ ⥤ CostructuredArrow R (B.obj X₃)`.  -/
CategoryTheory.TwoSquare.costructuredArrowRightwards : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        CategoryTheory.TwoSquare T L R B →
                          (X₃ : C₃) →
                            CategoryTheory.Functor (CategoryTheory.CostructuredArrow L X₃)
                              (CategoryTheory.CostructuredArrow R (B.obj X₃))
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
/-- **First mean value theorem for interval integrals (arbitrary measure, a.e. nonnegativity).**
Let `f g : ℝ → ℝ` and let `μ` be a measure on `ℝ`. Assume that `f` is continuous on `uIcc a b`,
that `g` is interval integrable on `a..b` w.r.t. `μ`, and that `g ≥ 0` a.e. on `Ι a b` w.r.t.
`μ.restrict (Ι a b)`. Then
`∃ c ∈ uIcc a b, (∫ x in a..b, f x * g x ∂μ) = f c * (∫ x in a..b, g x ∂μ)`.  -/
exists_eq_const_mul_intervalIntegral_of_ae_nonneg : ∀ {a b : ℝ} {f g : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ},
  ContinuousOn f (Set.uIcc a b) →
    IntervalIntegrable g μ a b →
      (∀ᵐ (x : ℝ) ∂μ.restrict (Set.uIoc a b), 0 ≤ g x) →
        ∃ c ∈ Set.uIcc a b, ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset : ∀ {A B : GrpCat} (f : A ⟶ B),
  (Equiv.symm (GrpCat.SurjectiveOfEpiAuxs.tau f))
      (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩) =
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, k ∉ m₂ → (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
-- Init.Data.Int.Gcd
Int.gcd_le_left : ∀ {a : ℤ} (b : ℤ), 0 < a → ↑(a.gcd b) ≤ a
-- Mathlib.Data.List.Rotate
/-- The relation `List.IsRotated l l'` forms a `Setoid` of cycles.  -/
List.IsRotated.setoid : (α : Type u_1) → Setoid (List α)
-- Mathlib.RingTheory.NormalClosure
Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S],
  IsScalarTower R (FractionRing S)
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] (f : α → C) [inst_2 : CategoryTheory.Limits.HasProduct f],
  (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).pt = ∏ᶜ f
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type.congr_simp : ∀ {α : Type u} (r r_1 : α → α → Prop) (e_r : r = r_1) [wo : IsWellOrder α r], Ordinal.type r = Ordinal.type r_1
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_mul : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : StrongNormalizedGCDMonoid R] {p q : Polynomial R},
  (p * q).content = p.content * q.content
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injective : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [IsDomain S] {φ : R →+* S},
  Function.Injective ⇑φ → ∀ {f : Polynomial R}, f.IsPrimitive → Irreducible (Polynomial.map φ f) → Irreducible f
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.mk : Lean.Syntax →
  Lean.FVarId →
    Array Lean.Elab.Attribute →
      Lean.Name →
        Lean.Name →
          Option Lean.Name →
            Lean.LocalContext →
              Lean.LocalInstances →
                Lean.Expr →
                  Lean.Expr →
                    Lean.MVarId →
                      Lean.Elab.TerminationHints →
                        Lean.Syntax →
                          Option (Lean.TSyntax `Lean.Parser.Command.docComment) → Lean.Elab.Term.LetRecToLift
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instIsScalarTower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {a b : R} [inst : SMul S R] [inst_1 : SMul T R] [inst_2 : SMul S T]
  [IsScalarTower S T R], IsScalarTower S T (QuadraticAlgebra R a b)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k fallback : α}, k ∈ m → (m.insertManyIfNewUnit l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Relation between `ValueDistribution.logCounting` and `locallyFinsuppWithin.logCounting`.
 -/
locallyFinsuppWithin.logCounting_divisor : ∀ {f : ℂ → ℂ},
  Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ) =
    ValueDistribution.logCounting f 0 - ValueDistribution.logCounting f ⊤
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instTopologicalSpace : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {E : Type u_3} →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        [inst_7 : TopologicalSpace F] →
                          [IsTopologicalAddGroup F] → (𝔖 : Set (Set E)) → TopologicalSpace (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.instPartialOrder : PartialOrder BoxIntegral.IntegrationParams
-- Aesop.Script.StructureStatic
Aesop.Script.structureStaticCore : Aesop.Script.TacticState → Aesop.Script.UScript → Lean.CoreM (Aesop.Script.UScript × Bool)
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradientWithin.congr_simp : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (f f_1 : F → 𝕜),
  f = f_1 → ∀ (s s_1 : Set F), s = s_1 → ∀ (x x_1 : F), x = x_1 → gradientWithin f s x = gradientWithin f_1 s_1 x_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_zero : ∀ {α : Type u} [inst : Zero α], ↑0 = 0
-- Mathlib.Topology.Maps.Proper.UniversallyClosed
/-- A map `f : X → Y` is proper if and only if it is continuous and the map
`(Prod.map f id : X × Filter X → Y × Filter X)` is closed. This is stronger than
`isProperMap_iff_universally_closed` since it shows that there's only one space to check to get
properness, but in most cases it doesn't matter.  -/
isProperMap_iff_isClosedMap_filter : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.map_map : ∀ {K : Type u_4} {L₁ : Type u_5} {L₂ : Type u_6} {L₃ : Type u_7} [inst : Field K] [inst_1 : Field L₁]
  [inst_2 : Algebra K L₁] [inst_3 : Field L₂] [inst_4 : Algebra K L₂] [inst_5 : Field L₃] [inst_6 : Algebra K L₃]
  (E : IntermediateField K L₁) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃),
  IntermediateField.map g (IntermediateField.map f E) = IntermediateField.map (g.comp f) E
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflQuiver.toQuiver : {obj : Type u} → [self : CategoryTheory.ReflQuiver obj] → Quiver obj
-- Init.Data.Range.Polymorphic.PRange
Std.Rcc.instDecidableMemOfDecidableLE : {α : Type u} → {r : Std.Rcc α} → {a : α} → [inst : LE α] → [DecidableLE α] → Decidable (a ∈ r)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented
angle-at-point form where the apex is given as the center of a circle.  -/
EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s →
    p₂ ∈ s → p₁ ≠ p₂ → EuclideanGeometry.oangle p₁ s.center p₂ = ↑Real.pi - 2 • EuclideanGeometry.oangle p₂ p₁ s.center
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁ : a ∈ m.insert k v},
  (m.insert k v)[a] = if h₂ : (k == a) = true then v else m[a]
-- Mathlib.Computability.Ackermann
ack_three : ∀ (n : ℕ), ack 3 n = 2 ^ (n + 3) - 3
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.forget₂_map : ∀ {R : Type u} [inst : CommRing R] (X Y : CoalgCat R) (f : X ⟶ Y),
  (CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).map f = ModuleCat.ofHom ↑(CoalgCat.Hom.toCoalgHom f)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.mapAlgHom_apply : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] [inst_3 : Algebra R S₁] [inst_4 : Algebra R S₂] (f : S₁ →ₐ[R] S₂) (x : MvPolynomial σ S₁),
  (MvPolynomial.mapAlgHom f) x = (MvPolynomial.map ↑f) x
-- Mathlib.MeasureTheory.Measure.Tight
MeasureTheory.IsTightMeasureSet.union : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S T : Set (MeasureTheory.Measure 𝓧)} [inst : TopologicalSpace 𝓧],
  MeasureTheory.IsTightMeasureSet S → MeasureTheory.IsTightMeasureSet T → MeasureTheory.IsTightMeasureSet (S ∪ T)
-- Mathlib.Logic.Equiv.Set
/-- If `f` is an injective function, then `s` is equivalent to `f '' s`.  -/
Equiv.Set.image : {α : Type u_3} → {β : Type u_4} → (f : α → β) → (s : Set α) → Function.Injective f → ↑s ≃ ↑(f '' s)
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_fun_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) →
    deriv (fun x => ∏ i ∈ u, f i x) x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • deriv (f i) x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.map_smul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  (X : Cᵒᵖ) {Y : Cᵒᵖ} (π : X ⟶ Y) (r : ↑(R.obj.obj X)) (m : ↑(A.obj.obj X)),
  (CategoryTheory.ConcreteCategory.hom (A.obj.map π)) (PresheafOfModules.Sheafify.smul α φ r m) =
    PresheafOfModules.Sheafify.smul α φ ((CategoryTheory.ConcreteCategory.hom (R.obj.map π)) r)
      ((CategoryTheory.ConcreteCategory.hom (A.obj.map π)) m)
-- Mathlib.Probability.Density
MeasureTheory.pdf_def : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {X : Ω → E}, MeasureTheory.pdf X ℙ μ = (MeasureTheory.Measure.map X ℙ).rnDeriv μ
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.coeff_regularizedGaussHGFunSeries : ∀ {n : ℕ} {a b c : ℂ},
  (a.regularizedGaussHGFunSeries b c).coeff n =
    Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) /
      (↑n.factorial * Complex.Gamma (c + ↑n))
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
/-- The `completeEquipartiteGraph r t` is always `r`-colorable.  -/
SimpleGraph.completeEquipartiteGraph_colorable : ∀ {r t : ℕ}, (SimpleGraph.completeEquipartiteGraph r t).Colorable r
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.toPreGNS_ofPreGNS : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) (a : f.PreGNS),
  f.toPreGNS (f.ofPreGNS a) = a
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.mapDomainLinearMap_single : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (f : M → N) (s : S) (m : M),
  (AddMonoidAlgebra.mapDomainLinearMap R S f) (AddMonoidAlgebra.single m s) = AddMonoidAlgebra.single (f m) s
-- Mathlib.Order.Atoms
/-- **Alias** of the reverse direction of `isAtom_compl`. -/
IsCoatom.compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α}, IsCoatom a → IsAtom aᶜ
-- Mathlib.Logic.Function.Basic
Function.Surjective.forall₃ : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
  Function.Surjective f →
    ∀ {p : β → β → β → Prop}, (∀ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ↔ ∀ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)
-- Mathlib.AlgebraicGeometry.RelativeGluing
/-- The schemes `Xᵢ`.  -/
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor : {S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰 → CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Group.Subgroup.Defs
add_mem_cancel_right : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [AddSubgroupClass S G] {x y : G},
  x ∈ H → (y + x ∈ H ↔ y ∈ H)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (iso : F ≅ F') {X : C} {Y : D} (g : F'.obj X ⟶ Y),
  (CategoryTheory.Adjunction.equivHomsetLeftOfNatIso iso).symm g = CategoryTheory.CategoryStruct.comp (iso.hom.app X) g
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.compProj_mem_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L : NNReal}
  (α : ODE.FunSpace t₀ x₀ r L),
  ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r → ∀ {t : ℝ}, α.compProj t ∈ Metric.closedBall x₀ ↑a
-- Mathlib.Algebra.Lie.LieTheorem
_private.Mathlib.Algebra.Lie.LieTheorem.0.LieModule.T.congr_simp : ∀ {R : Type u_1} {A : Type u_3} {V : Type u_4} [inst : CommRing R] [inst_1 : LieRing A] [inst_2 : LieAlgebra R A]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : LieRingModule A V] [inst_6 : LieModule R A V]
  (χ χ_1 : A → R), χ = χ_1 → ∀ (w w_1 : A), w = w_1 → LieModule.T✝ χ w = LieModule.T✝ χ_1 w_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanCompIso_hom_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospanCompIso F f g).hom.app CategoryTheory.Limits.WalkingCospan.one =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Limits.cospan f g).comp F).obj CategoryTheory.Limits.WalkingCospan.one)
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.Ico_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico ↑a ↑b = WithTop.some '' Set.Ico a b
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeTR.go.eq_3 : ∀ {α : Type u_1} (l : List α) (a : Array α) (x_3 : α) (xs : List α) (n : ℕ),
  List.takeTR.go✝ l (x_3 :: xs) n.succ a = List.takeTR.go✝ l xs n (a.push x_3)
-- Mathlib.Order.Atoms
IsCoatomistic.instIsCoatomic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] [IsCoatomistic α], IsCoatomic α
-- Mathlib.Data.Num.ZNum
ZNum.cast_le : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {m n : ZNum}, ↑m ≤ ↑n ↔ m ≤ n
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualAnnihilator_anti : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {U V : Submodule R M}, U ≤ V → V.dualAnnihilator ≤ U.dualAnnihilator
-- Std.Data.String.ToInt
String.Slice.isInt_of_toInt?_eq_some : ∀ {a : ℤ} {s : String.Slice}, s.toInt? = some a → s.isInt = true
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.resCongr_inv : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] (f f' : G →ₜ* H) (h : f = f'),
  (ContAction.resCongr V f f' h).inv =
    { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (CategoryTheory.Iso.refl X.obj.V) ⋯).inv,
      naturality := ⋯ }
-- Mathlib.Topology.UniformSpace.Equiv
/-- Uniform equivalence between `ULift α` and `α`.  -/
UniformEquiv.ulift : (α : Type u) → [inst : UniformSpace α] → ULift.{v, u} α ≃ᵤ α
-- Mathlib.Data.DFinsupp.Submonoid
/-- The supremum of a family of commutative additive submonoids is equal to the range of
`DFinsupp.sumAddHom`; that is, every element in the `iSup` can be produced from taking a finite
number of non-zero elements of `S i`, coercing them to `γ`, and summing them.  -/
AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom : ∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] [inst_1 : AddCommMonoid γ] (S : ι → AddSubmonoid γ),
  iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun i => (S i).subtype)
-- Mathlib.Data.Fin.VecNotation
Matrix.range_cons_cons_empty : ∀ {α : Type u} (x y : α) (u : Fin 0 → α), Set.range (Matrix.vecCons x (Matrix.vecCons y u)) = {x, y}
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'_self : ∀ (c : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ⊆ Turing.PartrecToTM2.codeSupp' c k
-- Std.Sync.SharedMutex
/-- Locks a `BaseSharedMutex` for exclusive write access. This function blocks until no other
writers or readers have access to the lock.

The current thread must not have already locked the mutex.
Reentrant locking is undefined behavior (inherited from the C++ implementation).
 -/
Std.BaseSharedMutex.write : Std.BaseSharedMutex → BaseIO Unit
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred
Std.Tactic.BVDecide.BVPred.bitblast_Inv_of_Inv : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {assign : Std.Tactic.BVDecide.BVExpr.Assignment}
  (input : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig input.cache →
    Std.Tactic.BVDecide.BVExpr.Cache.Inv assign (↑(Std.Tactic.BVDecide.BVPred.bitblast aig input).result).aig
      (Std.Tactic.BVDecide.BVPred.bitblast aig input).cache
-- Mathlib.Topology.Inseparable
SeparationQuotient.isClosedMap_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsClosedMap SeparationQuotient.mk
-- Init.Meta.Defs
Lean.version.getIsRelease : Unit → Bool
-- Mathlib.Geometry.Manifold.Notation
/-- Expression describing the model with corners found.  -/
Manifold.Elab.FindModelResult.model : Manifold.Elab.FindModelResult → Lean.Expr
-- Mathlib.Topology.Instances.CantorSet
cantorStep.eq_1 : ∀ (x : ℝ), cantorStep x = if x ∈ Set.Icc 0 (1 / 3) then 3 * x else 3 * x - 2
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_zpow : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield 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] [inst_9 : ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] (a : Aˣ)
  (n : ℤ), autoParam (p ↑a) cfc_zpow._auto_1 → cfc (fun x => x ^ n) ↑a = ↑(a ^ n)
-- Mathlib.Algebra.Algebra.Opposite
/-- A commutative algebra is isomorphic to its opposite.  -/
AlgEquiv.toOpposite : (R : Type u_1) →
  (A : Type u_3) → [inst : CommSemiring R] → [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → A ≃ₐ[R] Aᵐᵒᵖ
-- Init.Sym.Simp.SimprocDSL
Lean.Parser.Category.sym_simp_field : Lean.Parser.Category
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.mk.injEq : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (coeff : Γ → R)
  (isPWO_support' : (Function.support coeff).IsPWO) (coeff_1 : Γ → R)
  (isPWO_support'_1 : (Function.support coeff_1).IsPWO),
  ({ coeff := coeff, isPWO_support' := isPWO_support' } = { coeff := coeff_1, isPWO_support' := isPWO_support'_1 }) =
    (coeff = coeff_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- For an edge `hom`, `InvStruct hom` encodes the data of a backward edge `inv`, and
2-simplices witnessing that `hom` and `inv` compose to the identity on their endpoints.
This implies that `hom` becomes an isomorphism in the homotopy category.  -/
SSet.Edge.InvStruct : {X : SSet} → {x₀ x₁ : X.obj (Opposite.op { len := 0 })} → SSet.Edge x₀ x₁ → Type u
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.Const.beq_of_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : BEq β] [ReflBEq β] (m₁ m₂ : Std.ExtDHashMap α fun x => β), m₁ = m₂ → Std.ExtDHashMap.Const.beq m₁ m₂ = true
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.measurable_of_measurable_nnreal_nnreal : ∀ {β : Type u_2} {x : MeasurableSpace β} {f : ENNReal × ENNReal → β},
  (Measurable fun p => f (↑p.1, ↑p.2)) →
    (Measurable fun r => f (⊤, ↑r)) → (Measurable fun r => f (↑r, ⊤)) → Measurable f
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_mul_iff : ∀ {a b c : Ordinal.{u_4}}, a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The colimit of a functor out of the walking reflexive pair is the same as the colimit of the
underlying parallel pair.  -/
CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) →
      [inst_1 :
          CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
            (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)] →
        CategoryTheory.Limits.colimit F ≅
          CategoryTheory.Limits.coequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
            (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
-- Mathlib.RingTheory.Multiplicity
Int.finiteMultiplicity_iff : ∀ {a b : ℤ}, FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0
-- Mathlib.Data.Setoid.Basic
/-- The map from the quotient of the infimum of a set of setoids into the quotient
by an element of this set.  -/
Setoid.map_sInf : {α : Type u_1} → {S : Set (Setoid α)} → {s : Setoid α} → s ∈ S → Quotient (sInf S) → Quotient s