mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.Const.get!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited β] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.Const.get! ⟨{ size := size, buckets := buckets }, hm⟩ a =
    Std.DHashMap.Internal.AssocList.get! a buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_bot : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : LieAlgebra R L] (I : LieIdeal R L), ⁅I, ⊥⁆ = ⊥
-- Mathlib.Data.Nat.ChineseRemainder
/-- The natural number less than `∏ i ∈ t, s i` congruent to
`a i` mod `s i` for all  `i ∈ t`.  -/
Nat.chineseRemainderOfFinset : {ι : Type u_1} →
  (a s : ι → ℕ) →
    (t : Finset ι) →
      (∀ i ∈ t, s i ≠ 0) → (↑t).Pairwise (Function.onFun Nat.Coprime s) → { k // ∀ i ∈ t, k ≡ a i [MOD s i] }
-- Mathlib.Algebra.Ring.GrindInstances
Semiring.toGrindSemiring : (α : Type u_1) → [s : Semiring α] → Lean.Grind.Semiring α
-- Init.SizeOfLemmas
UInt32.sizeOf : ∀ (a : UInt32), sizeOf a = a.toNat + 3
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.coe_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup N) (f : M →ₙ+ N),
  ↑(AddSubsemigroup.comap f S) = ⇑f ⁻¹' ↑S
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- If `C` is a monoidal category, we say that `P : ObjectProperty C`
is monoidal if it is stable by tensor product and holds for the unit.  -/
CategoryTheory.ObjectProperty.IsMonoidal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_revPerm_Ici : ∀ {n : ℕ} (i : Fin n), Finset.map (Equiv.toEmbedding Fin.revPerm) (Finset.Ici i) = Finset.Iic i.rev
-- Mathlib.Data.Finset.Sym
Finset.strictMono_sym2 : ∀ {α : Type u_1}, StrictMono Finset.sym2
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.instRingHomClass : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, RingHomClass (α →+* β) α β
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- The hom relation that identifies the specified reflexivity arrows with the nil paths  -/
CategoryTheory.Cat.FreeReflRel : (V : Type u_1) → [inst : CategoryTheory.ReflQuiver V] → (X Y : CategoryTheory.Paths V) → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.induct_unfolding : ∀ (motive : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly → Prop),
  (∀ (n : ℤ), motive (Lean.Grind.CommRing.Expr.num n) (Lean.Grind.CommRing.Poly.num ↑n.natAbs)) →
    (∀ (x : Lean.Grind.CommRing.Var), motive (Lean.Grind.CommRing.Expr.var x) (Lean.Grind.CommRing.Poly.ofVar x)) →
      (∀ (a b : Lean.Grind.CommRing.Expr),
          motive a a.toPolyS → motive b b.toPolyS → motive (a.add b) (a.toPolyS.combine b.toPolyS)) →
        (∀ (a b : Lean.Grind.CommRing.Expr),
            motive a a.toPolyS → motive b b.toPolyS → motive (a.mul b) (a.toPolyS.mul b.toPolyS)) →
          (∀ (k : ℕ) (n : ℤ),
              motive ((Lean.Grind.CommRing.Expr.num n).pow k) (Lean.Grind.CommRing.Poly.num (↑n.natAbs ^ k))) →
            (∀ (k : ℕ) (x : Lean.Grind.CommRing.Var),
                motive ((Lean.Grind.CommRing.Expr.var x).pow k)
                  (Lean.Grind.CommRing.Poly.ofMon
                    (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit))) →
              (∀ (a : Lean.Grind.CommRing.Expr) (k : ℕ),
                  (∀ (n : ℤ), a = Lean.Grind.CommRing.Expr.num n → False) →
                    (∀ (x : Lean.Grind.CommRing.Var), a = Lean.Grind.CommRing.Expr.var x → False) →
                      motive a a.toPolyS → motive (a.pow k) (a.toPolyS.pow k)) →
                (∀ (n : ℕ), motive (Lean.Grind.CommRing.Expr.natCast n) (Lean.Grind.CommRing.Poly.num ↑n)) →
                  (∀ (a b : Lean.Grind.CommRing.Expr), motive (a.sub b) (Lean.Grind.CommRing.Poly.num 0)) →
                    (∀ (a : Lean.Grind.CommRing.Expr), motive a.neg (Lean.Grind.CommRing.Poly.num 0)) →
                      (∀ (k : ℤ), motive (Lean.Grind.CommRing.Expr.intCast k) (Lean.Grind.CommRing.Poly.num 0)) →
                        ∀ (a : Lean.Grind.CommRing.Expr), motive a a.toPolyS
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.acyclic_of_isZero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c), CategoryTheory.Limits.IsZero K → K.Acyclic
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.one_div_eq : ∀ {p q r : NNReal}, p.HolderTriple q r → 1 / r = 1 / p + 1 / q
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.const_mul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Mul β]
  [ContinuousMul β], MeasureTheory.StronglyMeasurable f → ∀ (c : β), MeasureTheory.StronglyMeasurable fun x => c * f x
-- Lean.Widget.InteractiveGoal
/-- Extend an array of hypothesis bundles with another bundle.  -/
Lean.Widget.addInteractiveHypothesisBundle : Array Lean.Widget.InteractiveHypothesisBundle →
  Array (String × Lean.FVarId) →
    Lean.Expr →
      optParam (Option Lean.Expr) none →
        optParam Bool false → Lean.MetaM (Array Lean.Widget.InteractiveHypothesisBundle)
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_sup_left : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) [K.Normal], K.relIndex (K ⊔ H) = K.relIndex H
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_eq : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  (↑m).WF → ∀ {a : α} (h' : m.contains a = true), m.getKey a h' = a
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedAlgebra.proj_recompose : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜]
  (a : DirectSum ι fun i => ↥(𝒜 i)) (i : ι),
  (GradedAlgebra.proj 𝒜 i) ((DirectSum.decompose 𝒜).symm a) =
    (DirectSum.decompose 𝒜).symm ((DirectSum.of (fun i => ↥(𝒜 i)) i) (a i))
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- The inverse to `spine X n`.  -/
SSet.StrictSegal.spineToSimplex : {X : SSet} → X.StrictSegal → {n : ℕ} → X.Path n → X.obj (Opposite.op { len := n })
-- Mathlib.Data.Sym.Sym2
Eq.ndrecOn.congr_simp : ∀ {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m m_1 : motive a),
  m = m_1 → Eq.ndrecOn h m = Eq.ndrecOn h m_1
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a (-b) = p - toIcoMod hp (-a) b
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_eval_succ : ∀ (S : Type u_1) [inst : Semiring S] (r n : ℕ),
  ↑n * Polynomial.eval (↑n + 1) (ascPochhammer S r) = (↑n + ↑r) * Polynomial.eval (↑n) (ascPochhammer S r)
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- A locally convex space is quasi-complete if every closed and von Neumann bounded set is
complete.  -/
QuasiCompleteSpace : (𝕜 : Type u_6) → (E : Type u_7) → [Zero E] → [UniformSpace E] → [SeminormedRing 𝕜] → [SMul 𝕜 E] → Prop
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
MonoidAlgebra.antipode_single : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] {G : Type u_3}
  [inst_3 : Group G] (g : G) (a : A),
  (HopfAlgebraStruct.antipode R) (MonoidAlgebra.single g a) =
    MonoidAlgebra.single g⁻¹ ((HopfAlgebraStruct.antipode R) a)
-- Mathlib.Data.Set.Image
Prod.range_snd : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α], Set.range Prod.snd = Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Given `F : WalkingParallelFamily ⥤ C`, which is really the same as
`parallelFamily (fun j ↦ F.map (line j))` and a cone on `F`, we get a trident on
`fun j ↦ F.map (line j)`.  -/
CategoryTheory.Limits.Trident.ofCone : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} →
        CategoryTheory.Limits.Cone F →
          CategoryTheory.Limits.Trident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)
-- Mathlib.Algebra.Group.End
Equiv.swap_mul_eq_iff : ∀ {α : Type u_4} [inst : DecidableEq α] {i j : α} {σ : Equiv.Perm α}, Equiv.swap i j * σ = σ ↔ i = j
-- Mathlib.RingTheory.Spectrum.Prime.Topology
StableUnderSpecialization.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X),
  StableUnderSpecialization s = ∀ ⦃x y : X⦄, x ⤳ y → x ∈ s → y ∈ s
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverXPullbackCoverOver : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      (j : 𝒰.I₀) → ((AlgebraicGeometry.Scheme.Cover.pullbackCoverOver S 𝒰 f).X j).Over S
-- Mathlib.MeasureTheory.Function.EssSup
essSup_le_of_ae_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f : α → β} (c : β),
  (f ≤ᵐ[μ] fun x => c) →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f) essSup_le_of_ae_le._auto_1 →
      essSup f μ ≤ c
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.addEmptyConstants_is_expansion_on' : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M],
  (FirstOrder.Language.LEquiv.addEmptyConstants L ↑∅).toLHom.IsExpansionOn M
-- Mathlib.Data.Int.Bitwise
/-- Connection of `HShiftRight Int Int Int` and `HShiftRight Int Nat Int`.  -/
Int.shiftRight_natCast_right : ∀ (m : ℤ) (n : ℕ), m >>> ↑n = m >>> n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
/-- The equalizer of `f g : X ⟶ Y` is the pullback of the diagonal map `Y ⟶ Y × Y`
along the map `(f, g) : X ⟶ Y × Y`.  -/
CategoryTheory.Limits.isPullback_equalizer_prod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Y],
  CategoryTheory.IsPullback (CategoryTheory.Limits.equalizer.ι f g)
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) f) (CategoryTheory.Limits.prod.lift f g)
    (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y))
-- Mathlib.CategoryTheory.Preadditive.Schur
CategoryTheory.mono_of_nonzero_from_simple : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasKernels C] {X Y : C} [CategoryTheory.Simple X] {f : X ⟶ Y}, f ≠ 0 → CategoryTheory.Mono f
-- Mathlib.Topology.FiberBundle.Basic
/-- Characterization of continuous functions (at a point) into a fiber bundle.  -/
FiberBundle.continuousAt_totalSpace : ∀ {B : Type u_2} (F : Type u_3) {X : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace B]
  [inst_2 : TopologicalSpace F] {E : B → Type u_5} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (b : B) → TopologicalSpace (E b)] [inst_5 : FiberBundle F E] (f : X → Bundle.TotalSpace F E) {x₀ : X},
  ContinuousAt f x₀ ↔
    ContinuousAt (fun x => (f x).proj) x₀ ∧ ContinuousAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.allM_filterMap : ∀ {α β β' : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α Id m] [LawfulMonad m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β}
  {f : β → Option β'} {p : β' → m Bool},
  Std.Iter.allM p (Std.Iter.filterMap f it) =
    Std.Iter.allM
      (fun x =>
        match f x with
        | some fx => p fx
        | none => pure true)
      it
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_add_le_of_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {a b : WithBot ℕ},
  p.degree ≤ a → q.degree ≤ b → (p + q).degree ≤ max a b
-- Init.Data.Float.Model.Unpacked.Round
Float.Model.UnpackedFloat.ExtendedMantissa.instHShiftRightNat : HShiftRight Float.Model.UnpackedFloat.ExtendedMantissa ℕ Float.Model.UnpackedFloat.ExtendedMantissa
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Transport the property of being monoidal closed across a monoidal equivalence of categories  -/
CategoryTheory.MonoidalClosed.ofEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              {G : CategoryTheory.Functor D C} →
                (F ⊣ G) →
                  [F.Monoidal] → [F.IsEquivalence] → [CategoryTheory.MonoidalClosed D] → CategoryTheory.MonoidalClosed C
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasStrongEpiMonoFactorisations.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (d : {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.StrongEpiMonoFactorisation f),
  CategoryTheory.Limits.HasStrongEpiMonoFactorisations C
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z)
  [CategoryTheory.Epi f] [CategoryTheory.Epi g] [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct W X]
  [inst_4 : CategoryTheory.Limits.HasBinaryCoproduct Y Z], CategoryTheory.Epi (CategoryTheory.Limits.coprod.map f g)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Neg α] [inst_1 : Neg β] (s : Set α) (t : Set β), -s ×ˢ t = (-s) ×ˢ (-t)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δ_toCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_toCycles._auto_1),
  CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
-- Lean.Attributes
Lean.EnumAttributes.mk.injEq : ∀ {α : Type} (attrs : List Lean.AttributeImpl)
  (ext : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α))
  (attrs_1 : List Lean.AttributeImpl)
  (ext_1 : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)),
  ({ attrs := attrs, ext := ext } = { attrs := attrs_1, ext := ext_1 }) = (attrs = attrs_1 ∧ ext = ext_1)
-- Batteries.Data.Fin.Coding
Fin.encodeSum.eq_1 : ∀ {n m : ℕ} (x_1 : Fin n), Fin.encodeSum (Sum.inl x_1) = Fin.castAdd m x_1
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves limits, then `F : Cᵒᵖ ⥤ D` preserves colimits.  -/
CategoryTheory.Limits.preservesColimitsOfSize_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
span_range_eq_top_iff_surjective_fintypeLinearCombination : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : α → M),
  Submodule.span R (Set.range v) = ⊤ ↔ Function.Surjective ⇑(Fintype.linearCombination R v)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_eq_some_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {km : α},
  t.max? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `div_lt_iff₀'` for a version with multiplication on the other side.  -/
div_lt_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 < c → (b / c < a ↔ b < a * c)
-- Mathlib.Order.Hom.Bounded
BotHom.instInhabited.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β],
  BotHom.instInhabited = { default := { toFun := fun x => ⊥, map_bot' := ⋯ } }
-- Mathlib.Algebra.Polynomial.Degree.Defs
/-- The second-highest coefficient, or 0 for constants  -/
Polynomial.nextCoeff : {R : Type u} → [inst : Semiring R] → Polynomial R → R
-- Mathlib.Analysis.Calculus.Deriv.Linear
ContinuousLinearMap.hasStrictDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} (e : 𝕜 →L[𝕜] F), HasStrictDerivAt (⇑e) (e 1) x
-- Init.Data.Int.Gcd
Int.gcd_pow_left_of_gcd_eq_one : ∀ {n m : ℤ} {k : ℕ}, n.gcd m = 1 → (n ^ k).gcd m = 1
-- Mathlib.ModelTheory.DirectLimit
/-- Alias for `Σ i, G i`.

Instead of `Σ i, G i`, we use the alias `Language.Structure.Sigma` which depends on `f`.
This way, Lean can infer what `L` and `f` are in the `Setoid` instance.
Otherwise we have a "cannot find synthesization order" error.
See also the discussion at
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/local.20instance.20cannot.20find.20synthesization.20order.20in.20porting
 -/
FirstOrder.Language.Structure.Sigma : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      {G : ι → Type w} →
        [inst_1 : (i : ι) → L.Structure (G i)] → ((i j : ι) → i ≤ j → L.Embedding (G i) (G j)) → Type (max v w)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Insert an element above all the others, without any comparisons.
(Assumes that the element is in fact above all the others).

```
insertMax {1, 2} 4 = {1, 2, 4}
insertMax {1, 2} 0 = precondition violation
```  -/
Ordnode.insertMax : {α : Type u_1} → Ordnode α → α → Ordnode α
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_eq_of_finiteDimensional : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {k : Type u_3}
  [inst_2 : DivisionRing k] [inst_3 : Module k M] [inst_4 : Module k N] {f : M →ₗ[k] N} [FiniteDimensional k M]
  [FiniteDimensional k N], f.index = ↑(Module.finrank k M) - ↑(Module.finrank k N)
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.degenerate_eq_iUnion_range_σ : ∀ (X : SSet) {n : ℕ},
  X.degenerate (n + 1) = ⋃ i, Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i))
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instInhabitedExpr : Inhabited Lean.Grind.Linarith.Expr
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If the left extension defined by `α : F₀ ⟶ L ⋙ F₁` is universal,
then for every `L' : D ⥤ D'`, `F₁ : D ⥤ H`, if an extension
`b : L'.LeftExtension F₁` is such that the "pasted" extension
`(LeftExtension.precomp₂ L' α).obj b` is universal, then `b` is itself
universal.  -/
CategoryTheory.Functor.LeftExtension.isUniversalOfPrecomp₂ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {L' : CategoryTheory.Functor D D'} →
                    {F₀ : CategoryTheory.Functor C H} →
                      {F₁ : CategoryTheory.Functor D H} →
                        (α : F₀ ⟶ L.comp F₁) →
                          CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F₁ α) →
                            {b : L'.LeftExtension F₁} →
                              CategoryTheory.StructuredArrow.IsUniversal
                                  ((CategoryTheory.Functor.LeftExtension.precomp₂ L' α).obj b) →
                                CategoryTheory.StructuredArrow.IsUniversal b
-- Init.Data.SInt.Basic
/-- Negates 8-bit signed integers. Usually accessed via the `-` prefix operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.neg : Int8 → Int8
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.of_card_le_two : ∀ {V : Type u_1} {G : SimpleGraph V}, ENat.card V ≤ 2 → G.IsAcyclic
-- Lean.Parser.Basic
Lean.Parser.sepByInfo : Lean.Parser.ParserInfo → Lean.Parser.ParserInfo → Lean.Parser.ParserInfo
-- Init.Data.List.Attach
List.mem_unattach : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {a : α}, a ∈ l.unattach ↔ ∃ (h : p a), ⟨a, h⟩ ∈ l
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.refl_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (x : A), (CoalgEquiv.refl R A) x = x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- Implementation of the functor `PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X)`
when `X` is initial.

The functor is implemented as, on object level `M ↦ (c ↦ M(c))` where the `R(X)`-module structure
on `M(c)` is given by restriction of scalars along the unique morphism `R(c) ⟶ R(X)`; and on
morphism level `(f : M ⟶ N) ↦ (c ↦ f(c))`.
 -/
PresheafOfModules.forgetToPresheafModuleCatObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (X : Cᵒᵖ) →
        CategoryTheory.Limits.IsInitial X → PresheafOfModules R → CategoryTheory.Functor Cᵒᵖ (ModuleCat ↑(R.obj X))
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.isRkFinite_sdiff_iff : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.IsRkFinite X → (M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.piecewise_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {s : Set α} {hs : MeasurableSet s} [inst : DecidablePred fun x => x ∈ s] (a : α),
  (ProbabilityTheory.Kernel.piecewise hs κ η) a = if a ∈ s then κ a else η a
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- Given a t-structure `t` on a pretriangulated category `C`, the property `t.IsGE X n`
holds if `X : C` is `≥ n` for the t-structure.  -/
CategoryTheory.Triangulated.TStructure.IsGE : {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] → CategoryTheory.Triangulated.TStructure C → C → ℤ → Prop
-- Mathlib.Analysis.RCLike.Basic
RCLike.ratCast_im : ∀ {K : Type u_1} [inst : RCLike K] (q : ℚ), RCLike.im ↑q = 0