mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- The inf of two subsemirings is their intersection.  -/
Subsemiring.instMin : {R : Type u} → [inst : NonAssocSemiring R] → Min (Subsemiring R)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- A discrete valuation ring `R` is not a field.  -/
IsDiscreteValuationRing.not_isField : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R], ¬IsField R
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.coe_injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Function.Injective DFunLike.coe
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, k ∈ (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl
-- Init.Data.Sum.Basic
/-- Retrieves the contents from a sum known to be `inl`. -/
Sum.getLeft : {α : Type u_1} → {β : Type u_2} → (ab : α ⊕ β) → ab.isLeft = true → α
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint32.inj : ∀ {val val_1 : UInt32}, Lean.Compiler.LCNF.LitValue.uint32 val = Lean.Compiler.LCNF.LitValue.uint32 val_1 → val = val_1
-- Init.Data.Nat.Dvd
Nat.dvd_of_mul_dvd_mul_left : ∀ {k m n : ℕ}, 0 < k → k * m ∣ k * n → m ∣ n
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.instMonadHetT : {m : Type w → Type w'} → [Monad m] → Monad (Std.Iterators.HetT m)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  [inst_3 : DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [inst_4 : NeZero i] (hi : Even i)
  (x y : ↥(LinearMap.ker A.ρ.norm)),
  (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) x =
      (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) y ↔
    ↑x - ↑y ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.DegeneraciesVanish.σ_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {n : ℕ} {T : C} {f : X.obj (Opposite.op { len := n + 1 }) ⟶ T},
  AlgebraicTopology.DoldKan.DegeneraciesVanish f →
    ∀ (i : Fin (n + 1)) {Z : C} (h : T ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp f h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.desc_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (j k : ι)
  (hjk : c.Rel j k),
  (HomologicalComplex.homotopyCofiber.desc φ α hα).f j =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ j k hjk) (hα.hom k j) +
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ j) (α.f j)
-- Init.Data.Array.Count
Array.countP_replace : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {xs : Array α} {p : α → Bool},
  Array.countP p (xs.replace a b) =
    if xs.contains a = true then (Array.countP p xs + if p b = true then 1 else 0) - if p a = true then 1 else 0
    else Array.countP p xs
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.comp_right_iff_of_isEquivalence : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D C') [G.IsEquivalence], (F.comp G).IsDense ↔ F.IsDense
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R),
  IsLocalization.coeSubmodule S I = Submodule.map (Algebra.linearMap R S) I
-- Lean.Elab.ConfigEval.Types
/-- Ref for the option name itself.  -/
Lean.Elab.ConfigEval.ConfigItem.option : Lean.Elab.ConfigEval.ConfigItem → Lean.Ident
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedTZifV2 : Inhabited Std.Time.TimeZone.TZif.TZifV2
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_naturality_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)) {m n : M}
  {X Y : C} (f : X ⟶ Y) [inst_3 : F.LaxMonoidal] {Z : C}
  (h : (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m n)).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.obj m).map f))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app Y) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app X)
      (CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj m n)).map f) h)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category with finite biproducts and finite limits is AB4 if it is AB5.  -/
CategoryTheory.AB4Star.of_AB5Star : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C]
  [inst_4 : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C]
  [CategoryTheory.AB5StarOfSize.{w, w, v, u} C], CategoryTheory.AB4StarOfSize.{w, v, u} C
-- Mathlib.Algebra.Group.Semiconj.Basic
/-- **Alias** of the reverse direction of `SemiconjBy.inv_symm_left_iff`. -/
SemiconjBy.inv_symm_left : ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x y → SemiconjBy a⁻¹ y x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instHasDistribNeg : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [inst : Mul G] → [HasDistribNeg G] → HasDistribNeg (l.Germ G)
-- Mathlib.Topology.FiberBundle.Constructions
Pullback.continuous_lift : ∀ {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] (f : B' → B), Continuous (Bundle.Pullback.lift f)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isIso_iff₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1} (f : F ⟶ G),
  CategoryTheory.IsIso f ↔ CategoryTheory.IsIso (f.app 0) ∧ CategoryTheory.IsIso (f.app 1)
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.fintypeCatAsCofanIsColimit.congr_simp : ∀ (X : LightProfinite) [inst : Finite ↑X.toTop],
  LightCondensed.fintypeCatAsCofanIsColimit X = LightCondensed.fintypeCatAsCofanIsColimit X
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsIntTangentAt.mk : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  p ∈ s₁ → p ∈ s₂ → Wbtw ℝ s₂.center s₁.center p → s₁.IsIntTangentAt s₂ p
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean : Coe (Lean.TSyntax `Lean.Parser.Tactic.rcasesPatMed) (Lean.TSyntax `Lean.Parser.Tactic.rcasesPatLo)
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Relations.Solution.IsPresentation.directSum : ∀ {A : Type u} [inst : Ring A] {ι : Type w} [inst_1 : DecidableEq ι] {relations : ι → Module.Relations A}
  {M : ι → Type v} [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module A (M i)]
  {solution : (i : ι) → (relations i).Solution (M i)},
  (∀ (i : ι), (solution i).IsPresentation) → (Module.Relations.Solution.directSum solution).IsPresentation
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_keysArray_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp},
  t₁.keysArray.Perm t₂.keysArray → t₁.Equiv t₂
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_inter_le_size_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (m₁ ∩ m₂).size ≤ m₂.size
-- Mathlib.RingTheory.LocalProperties.Semilocal
Submodule.fg_of_localized_maximal : ∀ {R : Type u_1} [inst : CommSemiring R] [Finite (MaximalSpectrum R)] {M : Type u_2} [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (N : Submodule R M),
  (∀ (P : Ideal R) [inst_4 : P.IsMaximal], (Submodule.localized P.primeCompl N).FG) → N.FG
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableWithinAt_sub_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x}
  {u : Set B} {x₀ : B}, MDiffAt[u] (T% s) x₀ → MDiffAt[u] (T% t) x₀ → (MDiffAt[u] fun x => ⟨x, (s - t) x⟩) x₀
-- Lean.Server.InfoUtils
/-- For every branch of the `InfoTree`, find the deepest node in that branch for which `p` returns
`some _`  and return the union of all such nodes. The visitor `p` is given a node together with
its innermost surrounding `ContextInfo`.  -/
Lean.Elab.InfoTree.deepestNodes : {α : Type} →
  (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → Option α) →
    Lean.Elab.InfoTree → List α
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_hull : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (s : Set M), PointedCone.dual p ↑(PointedCone.hull R s) = PointedCone.dual p s
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The top right map in the forward hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip) →
        (CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ C)
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.range_comp : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} {P : Type u_6} [inst_1 : Group N] [inst_2 : Group P] (g : N →* P)
  (f : G →* N), (g.comp f).range = Subgroup.map g f.range
-- Mathlib.Computability.DFA
DFA.union_step : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2) (s : σ1 × σ2) (a : α),
  (M1.union M2).step s a = (M1.step s.1 a, M2.step s.2 a)
-- Mathlib.Order.Hom.Lattice
LatticeHom.fst_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (x : α × β), LatticeHom.fst x = x.1
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typeEquiv_functor_map_hom_app_hom_apply_hom_apply : ∀ {X Y : Type u} (f : X ⟶ Y) (x : Type uᵒᵖ)
  (g :
    { obj := fun Y => Opposite.unop Y ⟶ X,
          map := fun {X_1 Y} f => TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp f.unop g, map_id := ⋯,
          map_comp := ⋯ }.obj
      x)
  (a : Opposite.unop x),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.typeEquiv.functor.map f).hom.app x)) g))
      a =
    f.hom' (g.hom' a)
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
uliftPowersHom_symm_apply : ∀ (M : Type u) [inst : Monoid M] (a : ULift.{u, 0} (Multiplicative ℕ) →* M),
  (uliftPowersHom M).symm a = a (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instNontrivialValueGroup : ∀ (A : Type u) [inst : CommRing A] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra A K],
  Nontrivial (ValuationRing.ValueGroup A K)
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- If `χ` is a Dirichlet character and its level `M` divides `N`, then we obtain the L-series
of `χ` considered as a Dirichlet character of level `N` from the L-series of `χ` by multiplying
with `∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))`.  -/
DirichletCharacter.LSeries_changeLevel : ∀ {M N : ℕ} [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ},
  1 < s.re →
    LSeries (fun n => ((DirichletCharacter.changeLevel hMN) χ) ↑n) s =
      LSeries (fun n => χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- `affineCombination` gives equal results for two families of weights and two families of
points that are equal on `s`.  -/
Finset.affineCombination_congr : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w₁ w₂ : ι → k},
  (∀ i ∈ s, w₁ i = w₂ i) →
    ∀ {p₁ p₂ : ι → P},
      (∀ i ∈ s, p₁ i = p₂ i) → (Finset.affineCombination k s p₁) w₁ = (Finset.affineCombination k s p₂) w₂
-- Mathlib.Algebra.Group.Commute.Basic
/-- **Alias** of the reverse direction of `Commute.inv_left_iff`. -/
Commute.inv_left : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → Commute a⁻¹ b
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.stronglyMeasurable_coeFn : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : ↥(MeasureTheory.Lp β 1 μ)), MeasureTheory.StronglyMeasurable ↑↑f
-- Std.Async.System
Std.Async.System.instReprGroupInfo : Repr Std.Async.System.GroupInfo
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.image_coe_inj : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {s t : Set G},
  QuotientAddGroup.mk '' s = QuotientAddGroup.mk '' t ↔ ↑N + s = ↑N + t
-- Mathlib.Algebra.Group.Center
Set.decidableMemCenter : {M : Type u_1} →
  [inst : Semigroup M] → [(a : M) → Decidable (∀ (b : M), b * a = a * b)] → DecidablePred fun x => x ∈ Set.center M
-- Mathlib.NumberTheory.FermatPsp
/-- If `n` is a Fermat pseudoprime to base `b`, then `n` is coprime with `b`, assuming that `b` is
positive.

This lemma is a small wrapper based on `coprime_of_probablePrime`
 -/
Nat.coprime_of_fermatPsp : ∀ {n b : ℕ}, n.FermatPsp b → 1 ≤ b → n.Coprime b
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_nonneg : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E}, 0 ≤ MeasureTheory.lpNorm f p μ
-- Batteries.Data.Vector.Lemmas
Vector.finIdxOf?_empty : ∀ {α : Type u_1} {a : α} [inst : BEq α] (v : Vector α 0), v.finIdxOf? a = none
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instRespectsIsoAnodyneExtensions : SSet.anodyneExtensions.RespectsIso
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instIsVeryGoodSymmOfRespectsIsoCofibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).RespectsIso] [inst_5 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [P.IsVeryGood], P.symm.IsVeryGood
-- Mathlib.Order.JordanHolder
CompositionSeries.Equivalent.refl : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X), s.Equivalent s
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.values : Lean.Json.CompressWorkItemQueue✝ → Array Lean.Json
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_alter!_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)} {fallback : α},
      (Std.DTreeMap.Internal.Impl.alter! k f t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.alter! k f t).maxKeyD fallback = k ↔
          (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.union_mem_iff : ∀ {α : Type u} {f : Ultrafilter α} {s t : Set α}, s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.spine_surjective : ∀ {n : ℕ} (X : SSet.Truncated (n + 1)) [X.IsStrictSegal] {m : ℕ} (p : X.Path m)
  (h : autoParam (m ≤ n + 1) SSet.Truncated.spine_surjective._auto_1), ∃ x, X.spine m h x = p
-- Mathlib.Data.BitVec
BitVec.toNat_injective : ∀ {n : ℕ}, Function.Injective BitVec.toNat
-- Init.Data.List.MinMaxOn
List.maxOn_eq_head : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} (h : xs ≠ []), (∀ x ∈ xs, f x ≤ f (xs.head h)) → List.maxOn f xs h = xs.head h
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.triangle_obj₁ : ∀ {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.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  (X.triangle f g).obj₁ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Init.Prelude
/-- A decision procedure for strict inequality of natural numbers, usually accessed via the
`DecidableLT Nat` instance.

Examples:
 * `(if 3 < 4 then "yes" else "no") = "yes"`
 * `(if 4 < 4 then "yes" else "no") = "no"`
 * `(if 6 < 4 then "yes" else "no") = "no"`
 * `show 5 < 12 by decide`
 -/
Nat.decLt : (n m : ℕ) → Decidable (n < m)
-- Mathlib.Order.Filter.Pi
Filter.mem_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : Set ((i : ι) → α i)},
  s ∈ Filter.pi f ↔ ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Dependent recursion principle for `AddLocalizations`: given elements `f a b : p (mk a b)`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d` (with the correct coercions),
then `f` is defined on the whole `AddLocalization S`.  -/
AddLocalization.rec : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {p : AddLocalization S → Sort u} →
        (f : (a : M) → (b : ↥S) → p (AddLocalization.mk a b)) →
          (∀ {a c : M} {b d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) →
            (x : AddLocalization S) → p x
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.absolutelyContinuous_sum_right : ∀ {α : Type u_1} {ι : Type u_4} {mα : MeasurableSpace α} {ν : MeasureTheory.Measure α}
  {μs : ι → MeasureTheory.Measure α} (i : ι),
  ν.AbsolutelyContinuous (μs i) → ν.AbsolutelyContinuous (MeasureTheory.Measure.sum μs)
-- Std.Async.System
Std.Async.System.instDecidableEqSystemUser.decEq : (x x_1 : Std.Async.System.SystemUser) → Decidable (x = x_1)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.IsFiniteKernel.piecewise : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {s : Set α} {hs : MeasurableSet s} [inst : DecidablePred fun x => x ∈ s] [ProbabilityTheory.IsFiniteKernel κ]
  [ProbabilityTheory.IsFiniteKernel η], ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.piecewise hs κ η)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q)
  (hq' : q = q'), CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' ⋯
-- Init.Data.SInt.Lemmas
Int8.toInt64_ne_neg_one : ∀ (a : Int8), a ≠ -1 → a.toInt64 ≠ -1
-- Mathlib.Topology.Bases
TopologicalSpace.exists_seq_basis : ∀ (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α],
  ∃ b, TopologicalSpace.IsTopologicalBasis (Set.range b)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A telescoping product along `{0, ..., n - 1}` of a commutative-group-valued function reduces to
the ratio of the last and first factors.  -/
Finset.prod_range_div : ∀ {G : Type u_3} [inst : CommGroup G] (f : ℕ → G) (n : ℕ), ∏ i ∈ Finset.range n, f (i + 1) / f i = f n / f 0
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Subtype.preimage_eball`. -/
Subtype.preimage_emetricBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ENNReal),
  Subtype.val ⁻¹' Metric.eball (↑a) r = Metric.eball a r
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.splitter : {J : CategoryTheory.Limits.MulticospanShape} →
  (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3) →
    (j : CategoryTheory.Limits.WalkingMulticospan J) →
      ((i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i)) →
        ((i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)) → motive j
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
AddSubgroup.properlyDiscontinuousVAdd_of_le : ∀ {Γ : Type u_1} {α : Type u_2} [inst : AddGroup Γ] [inst_1 : TopologicalSpace α] [inst_2 : VAdd Γ α]
  {G H : AddSubgroup Γ}, ProperlyDiscontinuousVAdd (↥G) α → H ≤ G → ProperlyDiscontinuousVAdd (↥H) α
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.toNonUnitalSubalgebra_eq_top : ∀ {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] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S : NonUnitalStarSubalgebra R A}, S.toNonUnitalSubalgebra = ⊤ ↔ S = ⊤
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.many : {α ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] →
      [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι α → Std.Internal.Parsec ι (Array α)