mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment : Bool → Std.Tactic.BVDecide.LRAT.Internal.Assignment → Bool
-- Mathlib.RingTheory.NormalClosure
Ring.instCommRingNormalClosure : (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] → CommRing (Ring.NormalClosure R S)
-- Mathlib.Analysis.Distribution.Support
Distribution.notMem_dsupport_iff : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} (x : α),
  x ∉ Distribution.dsupport f ↔ ∃ s, Distribution.IsVanishingOn f s ∧ IsOpen s ∧ x ∈ s
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
FormalMultilinearSeries.taylorComp.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G)
  (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ), q.taylorComp p n = ∑ c, q.compAlongOrderedFinpartition p c
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.logMessageIfAux : {α : Type} → [Std.ToFormat α] → Lean.Name → α → Lean.IR.CompilerM Unit
-- Mathlib.Algebra.Symmetrized
/-- The symmetrized algebra (denoted as `αˢʸᵐ`)
has the same underlying space as the original algebra `α`.  -/
«term_ˢʸᵐ» : Lean.TrailingParserDescr
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.iSup_eq_top : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {u : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover u → ⨆ i, u i = ⊤
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- Construct an `IsColimit` structure of cokernels given `Function.Exact`.  -/
ModuleCat.isColimitCokernelCofork : {R : Type u} →
  [inst : Ring R] →
    {M N P : ModuleCat R} →
      (f : M ⟶ N) →
        (g : N ⟶ P) →
          (H : Function.Exact ⇑(ModuleCat.Hom.hom f) ⇑(ModuleCat.Hom.hom g)) →
            Function.Surjective ⇑(ModuleCat.Hom.hom g) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g ⋯)
-- Mathlib.Tactic.ClickSuggestions.Unfold
/-- Return the consecutive unfoldings of `e`.  -/
_private.Mathlib.Tactic.ClickSuggestions.Unfold.0.Mathlib.Tactic.ClickSuggestions.unfolds : Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.comap_comap : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : NonAssocRing R] [inst_1 : NonAssocRing S]
  [inst_2 : NonAssocRing T] (I : TwoSidedIdeal T) (f : R →+* S) (g : S →+* T),
  (TwoSidedIdeal.comap f) ((TwoSidedIdeal.comap g) I) = (TwoSidedIdeal.comap (g.comp f)) I
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.tensorProdIsoPushout_app : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] (A : CategoryTheory.Under R),
  (R.tensorProdIsoPushout S).app A = CommRingCat.tensorProdObjIsoPushoutObj S A
-- Init.Data.Dyadic.Basic
Dyadic.toRat_natCast : ∀ (x : ℕ), (↑x).toRat = ↑x
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.t1Space : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  [T1Space F] (b : B), T1Space (E b)
-- Init.Data.Int.Order
Int.ofNat_lt : ∀ {n m : ℕ}, ↑n < ↑m ↔ n < m
-- Mathlib.NumberTheory.NumberField.House
NumberField.house_nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α : K), 0 ≤ NumberField.house α
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_inl : ∀ {R : Type u} (M : Type v) [inst : Zero M] (r : R), (TrivSqZeroExt.inl r).fst = r
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_map : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [inst : Star α] [inst_1 : Star β] {A : Matrix m n α}
  (f : α → β), Function.Semiconj f star star → A.conjTranspose.map f = (A.map f).conjTranspose
-- Mathlib.Data.Nat.Prime.Nth
Nat.nth_prime_two_eq_five : Nat.nth Nat.Prime 2 = 5
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.height_sub : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R] {i j k : ι}, P.root k = P.root i - P.root j → b.height k = b.height i - b.height j
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The `NonUnitalStarSubalgebra` obtained from `S : NonUnitalSubalgebra R A` by taking the
smallest non-unital subalgebra containing both `S` and `star S`.  -/
NonUnitalSubalgebra.starClosure : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [StarModule R A] →
                [IsScalarTower R A A] → [SMulCommClass R A A] → NonUnitalSubalgebra R A → NonUnitalStarSubalgebra R A
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.arcosh_injOn : Set.InjOn Real.arcosh (Set.Ici 1)
-- Mathlib.Analysis.Convex.Basic
convex_of_nonneg_surjective_algebraMap : ∀ {R : Type u_5} [inst : CommSemiring R] (A : Type u_6) [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_7}
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [IsScalarTower R A M] [inst_7 : PartialOrder R]
  [inst_8 : PartialOrder A] [FaithfulSMul R A] {s : Set M},
  Set.Ici 0 ⊆ ⇑(algebraMap R A) '' Set.Ici 0 → Convex R s → Convex A s
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure'.brecOn : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure' x → Prop} {X Y : C} {x : X ⟶ Y}
  (t : W.multiplicativeClosure' x),
  (∀ ⦃X Y : C⦄ (x : X ⟶ Y) (t : W.multiplicativeClosure' x),
      CategoryTheory.MorphismProperty.multiplicativeClosure'.below t → motive x t) →
    motive x t
-- Mathlib.Algebra.Star.Module
toAddEquiv_starLinearEquiv : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A],
  (starLinearEquiv R).toAddEquiv = starAddEquiv
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionObj : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] (c : D) (d : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj c d =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (Opposite.op c) (Opposite.op d))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_mem_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∈ t.toList → k ∈ t
-- Init.Data.Int.Order
Int.toNat_sub_eq_zero_iff : ∀ (m n : ℤ), (m - n).toNat = 0 ↔ m ≤ n
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.Hom.eq_4 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (a : D) (a_1 : C), (CategoryTheory.Join.right a).Hom (CategoryTheory.Join.left a_1) = PEmpty.{max (v₁ + 1) (v₂ + 1)}
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- If there exists a pointwise left Kan extension of `F` along `L`,
then `L.lan.obj G` is a pointwise left Kan extension of `F`.  -/
CategoryTheory.Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit : {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] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseLeftKanExtension F] →
                  (CategoryTheory.Functor.LeftExtension.mk (L.leftKanExtension F)
                      (L.leftKanExtensionUnit F)).IsPointwiseLeftKanExtension
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
lt_or_lt_of_add_lt_add : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α] [AddLeftMono α] [AddRightMono α] {a₁ a₂ b₁ b₂ : α},
  a₁ + b₁ < a₂ + b₂ → a₁ < a₂ ∨ b₁ < b₂
-- Mathlib.Order.Basic
forall_gt_iff_le : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ ⦃c : α⦄, a < c → b < c) ↔ b ≤ a
-- Mathlib.RingTheory.Smooth.Quotient
/-- For flat ring homomorphism `f : R →+* S`, `I` an ideal of `R` which is square zero,
if `R ⧸ I →+* S ⧸ IS` is formally smooth, so is `f`.  -/
Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {R' : Type u_3} {S' : Type u_4}
  [inst_2 : CommRing R'] [inst_3 : CommRing S'] [inst_4 : Algebra R S] [inst_5 : Algebra R R'] [inst_6 : Algebra R' S']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [IsScalarTower R S S'] [IsScalarTower R R' S'] [Module.Flat R S],
  Function.Surjective ⇑(algebraMap R R') →
    Function.Surjective ⇑(algebraMap S S') →
      RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R')) →
        RingHom.ker (algebraMap R R') ^ 2 = ⊥ → Algebra.FormallySmooth R' S' → Algebra.FormallySmooth R S
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_of_isIso : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  [CategoryTheory.IsIso f] (i : ι) [inst_3 : K.HasHomology i] [inst_4 : L.HasHomology i], QuasiIsoAt f i
-- Mathlib.Data.ENNReal.Action
ENNReal.smul_one : ∀ (c : NNReal), c • 1 = ↑c
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filter : ∀ {α : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {β : Type w} [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Bool} {it : Std.IterM m β},
  (Std.IterM.filter f it).toArray = (fun as => Array.filter f as) <$> it.toArray
-- Mathlib.RingTheory.HahnSeries.Summable
/-- **Alias** of `HahnSeries.SummableFamily.hasFiniteSupport_smul`. -/
HahnSeries.SummableFamily.smul_support_finite : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  (s : HahnSeries.SummableFamily Γ R α) (t : HahnSeries.SummableFamily Γ' V β) (gh : Γ × Γ'),
  Function.HasFiniteSupport fun i => (s i.1).coeff gh.1 • (t i.2).coeff gh.2
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- The left-derived functors given by deriving the second argument of `A, B ↦ (A ⊗[k] B)_G`.  -/
Rep.Tor : (k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      ℕ → CategoryTheory.Functor (Rep.{u, u, u} k G) (CategoryTheory.Functor (Rep.{u, u, u} k G) (ModuleCat k))
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- Reindexing a matrix preserves double stochasticity.  -/
reindex_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {m : Type u_3} [inst_5 : Fintype m] [inst_6 : DecidableEq m]
  {M : Matrix n n R} {e₁ e₂ : n ≃ m}, M ∈ doublyStochastic R n → (Matrix.reindex e₁ e₂) M ∈ doublyStochastic R m
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => RingHom.Etale
-- Aesop.RuleTac.Basic
Aesop.Subgoal.mk.injEq : ∀ (diff diff_1 : Aesop.GoalDiff), ({ diff := diff } = { diff := diff_1 }) = (diff = diff_1)
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.algEquiv_X : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  ↑((RatFunc.Luroth.algEquiv h) RatFunc.X) = RatFunc.Luroth.generator E
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
MulAction.stabilizerEquivStabilizer_compTriple : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {g h k : G} {a b c : α} {hg : b = g • a}
  {hh : c = h • b} {hk : c = k • a},
  k = h * g →
    CompTriple ⇑(MulAction.stabilizerEquivStabilizer hg) ⇑(MulAction.stabilizerEquivStabilizer hh)
      ⇑(MulAction.stabilizerEquivStabilizer hk)
-- Mathlib.Data.Set.Prod
Set.prod_sub_preimage_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {W : Set γ} {f : α × β → γ},
  s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W
-- Init.Data.Iterators.Consumers.Monadic.Total
Std.IterM.Total.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {it it_1 : Std.IterM m β}, { it := it } = { it := it_1 } → it = it_1
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- Whiskering a 2-square with a natural transformation at the right side.  -/
CategoryTheory.TwoSquare.whiskerRight : {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₄} →
                        {R' : CategoryTheory.Functor C₂ C₄} →
                          CategoryTheory.TwoSquare T L R' B → (R ⟶ R') → CategoryTheory.TwoSquare T L R B
-- Std.Data.ByteSlice
/-- Runs a monadic action on each byte of a byte slice.

The bytes are processed starting at the lowest index and moving up.
 -/
ByteSlice.forM : {m : Type v → Type w} → [Monad m] → (UInt8 → m PUnit.{v + 1}) → ByteSlice → m PUnit.{v + 1}
-- Mathlib.Data.Rel
SetRel.image_univ_right : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.image Set.univ = R.cod
-- Mathlib.Algebra.Group.Ext
CancelCommMonoid.ext_iff : ∀ {M : Type u_1} {m₁ m₂ : CancelCommMonoid M}, m₁ = m₂ ↔ HMul.hMul = HMul.hMul
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.left_unitality_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.LaxMonoidal] {Z : C} (h : (F.obj n).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj n).map ((CategoryTheory.Functor.LaxMonoidal.ε F).app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit M) n).app X)
        (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor n).hom).app X)
          h)) =
    h
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.compare_maxKey!_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : β → β}, cmp (Std.ExtDTreeMap.Const.modify t k f).maxKey! t.maxKey! = Ordering.eq
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Presieve.functorPullback_map_overForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (S : CategoryTheory.Presieve Y),
  CategoryTheory.Presieve.functorPullback (CategoryTheory.Over.forget X)
      (CategoryTheory.Presieve.map (CategoryTheory.Over.forget X) S) =
    S
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.of_iso : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  [self : P.IsClosedUnderIsomorphisms] {X Y : C} (x : X ≅ Y), P X → P Y
-- Std.Time.Format.Modifier
/-- `L`: Stand-alone month of year as number or text (e.g., 7, 07, Jul, July, J).
Stand-alone means the month is used independently (e.g., a calendar header "July") rather than as part of a full date.
In practice the output is the same as `M`; the distinction is meaningful only in locale-aware contexts.
 -/
Std.Time.Modifier.L : Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_union_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → Set.Ico b a ∪ {a} = Set.Icc b a
-- Std.Time.Date.Unit.Week
/-- Creates an `Offset` from a natural number.
 -/
Std.Time.Week.Offset.ofNat : ℕ → Std.Time.Week.Offset
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_cert : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Poly → Bool
-- Mathlib.Order.Concept
Concept.surjective_ofObjects : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, Function.Surjective (Concept.ofObjects r)
-- Mathlib.Order.Directed
/-- Local notation for a relation  -/
_private.Mathlib.Order.Directed.0.«term_≼_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.codisjoint_restrictScalars_iff : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {s t : Submodule R M},
  Codisjoint (Submodule.restrictScalars S s) (Submodule.restrictScalars S t) ↔ Codisjoint s t
-- Mathlib.Algebra.Regular.Defs
IsAddRegular.mk : ∀ {R : Type u_2} [inst : Add R] {c : R}, IsAddLeftRegular c → IsAddRightRegular c → IsAddRegular c
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.instFinalOppositeLeftOpOfInitial : ∀ {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] (F : CategoryTheory.Functor C Dᵒᵖ) [F.Initial], F.leftOp.Final
-- Mathlib.CategoryTheory.Yoneda
/-- If `C` is a category with `[Category.{max w v₁} C]`, this is the isomorphism
`uliftYoneda.{w} (C := C) ≅ yoneda`.  -/
CategoryTheory.uliftYonedaIsoYoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{max w v₁, u₁} C] →
    CategoryTheory.uliftYoneda.{w, max v₁ w, u₁} ≅ CategoryTheory.yoneda
-- Mathlib.Algebra.Group.Commute.Basic
Commute.div_div_div_comm : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
  Commute b c → Commute b⁻¹ d → Commute c⁻¹ d → a / b / (c / d) = a / c / (b / d)
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Context.dischargeDepth : Lean.Meta.Sym.Simp.Context → ℕ
-- Mathlib.Analysis.Normed.Group.Uniform
locallyLipschitz_inv_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E},
  LocallyLipschitz f⁻¹ ↔ LocallyLipschitz f
-- Init.Data.List.Sublist
List.eq_nil_of_prefix_nil : ∀ {α : Type u_1} {l : List α}, l <+: [] → l = []
-- Mathlib.Topology.Order.HullKernel
PrimitiveSpectrum.gc_closureOperator : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α} (S : Set ↑T),
  ⋯.closureOperator S = PrimitiveSpectrum.hull T (PrimitiveSpectrum.kernel S)
-- Mathlib.Data.Real.Basic
Real.cauchy_natCast : ∀ (n : ℕ), (↑n).cauchy = ↑n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.comp_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y Z : CategoryTheory.PreOneHypercover S}
  (f : X.Hom Y) (g : Y.Hom Z) {i j : X.I₀} (i_1 : X.I₁ i j),
  (CategoryTheory.CategoryStruct.comp f g).h₁ i_1 = CategoryTheory.CategoryStruct.comp (f.h₁ i_1) (g.h₁ (f.s₁ i_1))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone morphism between two binary bicones for the same diagram is a morphism of the
binary bicone points which commutes with the cone and cocone legs.  -/
CategoryTheory.Limits.BinaryBiconeMorphism : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → CategoryTheory.Limits.BinaryBicone P Q → CategoryTheory.Limits.BinaryBicone P Q → Type uC'
-- Std.Data.HashSet.Basic
Std.HashSet.instForMOfMonad : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → {m : Type v → Type w} → [Monad m] → ForM m (Std.HashSet α) α
-- Lean.Data.Lsp.Basic
Lean.Lsp.PartialResultParams.mk : Option Lean.Lsp.ProgressToken → Lean.Lsp.PartialResultParams
-- Lean.Elab.Deriving.Basic
Lean.Elab.getOptDerivingClasses : Lean.Syntax → Lean.CoreM (Array Lean.Elab.DerivingClassView)
-- Mathlib.Data.Nat.Choose.Central
Nat.centralBinom_lt_four_pow : ∀ {n : ℕ}, n ≠ 0 → n.centralBinom < 4 ^ n
-- Mathlib.Algebra.Lie.Derivation.Killing
LieDerivation.IsKilling.rangeAdOrthogonal_carrier : ∀ (R : Type u_1) (L : Type u_2) [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  ↑(LieDerivation.IsKilling.rangeAdOrthogonal R L) =
    {y | ∀ (a : L), ((killingForm R (LieDerivation R L L)) ((LieDerivation.ad R L) a)) y = 0}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKey! k' =
    if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else default else t.getKey! k'
-- Mathlib.MeasureTheory.Constructions.SimpleGraph
SimpleGraph.measurable_fromEdgeSet : ∀ {V : Type u_1}, Measurable SimpleGraph.fromEdgeSet
-- Mathlib.Tactic.GrindAttrs
/-- `closedness` is a simple tactic that tries various lemmas to prove that a set is closed,
and reasoning about the closure of sets.
It is implemented using `grind`, and has the same configuration options as `grind`.

It also exists as a grind attribute, and can be combined with other grind attributes using
`grind only [closedness, ...]`.
 -/
closednessTac : Lean.ParserDescr
-- Init.Data.List.ToArray
List.findSomeM?_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → m (Option β))
  (l : List α), Array.findSomeM? f l.toArray = List.findSomeM? f l
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestSimpAllTrace : Lean.Elab.Tactic.Try.TryTactic
-- Mathlib.Logic.Equiv.Prod
Equiv.sigmaUnique_apply : ∀ {α : Type u_10} {β : α → Type u_9} [inst : (a : α) → Unique (β a)] (x : (a : α) × β a),
  (Equiv.sigmaUnique α β) x = x.fst
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnion.eq_1 : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J),
  π.biUnion πi = { boxes := π.boxes.biUnion fun J => (πi J).boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.CostructuredArrow.toOverCompCoyoneda.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)),
  CategoryTheory.CostructuredArrow.toOverCompCoyoneda A =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.NatIso.ofComponents
          (fun Y =>
            (CategoryTheory.overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
              (((CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).app
                      (Opposite.unop X)).homCongr
                  (CategoryTheory.Iso.refl
                    ((CategoryTheory.overEquivPresheafCostructuredArrow A).functor.obj Y))).toIso)
          ⋯)
      ⋯
-- Mathlib.Order.Disjointed
Fintype.sup_disjointed : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : PartialOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : Fintype ι] (f : ι → α),
  Finset.univ.sup (disjointed f) = Finset.univ.sup f