mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_sub : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalRing 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] (f g : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) _auto_630✝ →
    autoParam (ContinuousOn g (spectrum R a)) _auto_632✝ → cfc (fun x => f x - g x) a = cfc f a - cfc g a
-- Mathlib.CategoryTheory.Filtered.Basic
/-- An arbitrary choice of object "to the left"
of a finite collection of objects `O` and morphisms `H`,
making all the triangles commute.
 -/
CategoryTheory.IsCofiltered.inf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofiltered C] →
      (O : Finset C) → Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) → C
-- Mathlib.Data.Rat.Floor
Rat.isInt_intFloor : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (r : R)
  (m : ℤ), Mathlib.Meta.NormNum.IsInt r m → Mathlib.Meta.NormNum.IsInt ⌊r⌋ m
-- Mathlib.Data.Sign.Defs
SignType.neg_eq_zero_iff : ∀ {a : SignType}, -a = 0 ↔ a = 0
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.of_subsingleton_dom : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [Subsingleton α], MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_of_lt : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i : ι} (hi : i < i0), toZ i0 i = -↑(Nat.find ⋯)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.integral_smul : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  {R : Type u_8} [inst_2 : NormedRing R] [inst_3 : Module R E] [IsBoundedSMul R E] [SMulCommClass ℝ R E] {f : ℝ → E}
  (r : R), IntervalIntegrable f μ a b → ∫ (x : ℝ) in a..b, r • f x ∂μ = r • ∫ (x : ℝ) in a..b, f x ∂μ
-- Init.Data.Nat.Div.Basic
Nat.mod_eq : ∀ (x y : ℕ), x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x
-- Batteries.Tactic.PrintOpaques
Batteries.Tactic.CollectOpaques.State.mk.sizeOf_spec : ∀ (visited : Lean.NameSet) (opaques : Array Lean.Name),
  sizeOf { visited := visited, opaques := opaques } = 1 + sizeOf visited + sizeOf opaques
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_bitVecToInt : ∀ (n : BitVec 8), Int8.ofIntLE n.toInt ⋯ ⋯ = Int8.ofBitVec n
-- Mathlib.Order.Bounds.Basic
IsLeast.isLeast_iff_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α}, IsLeast s a → (IsLeast s b ↔ a = b)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_C_ne_zero : ∀ {R : Type u_1} {n : ℕ} [inst : Semiring R] {a : R}, n ≠ 0 → (SkewPolynomial.C a).coeff n = 0
-- Mathlib.Topology.Algebra.ConstMulAction
IsOpen.smul_left : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] {s : Set G} {t : Set α}, IsOpen t → IsOpen (s • t)
-- Mathlib.LinearAlgebra.Dual.Defs
Module.dualMap_dualMap_eq_iff : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.IsReflexive R M] {M' : Type u_6} [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.IsReflexive R M']
  {f g : M →ₗ[R] M'}, f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Focus.left : ∀ {σs : List (Type u)} {P P' Q C R : Std.Do.SPred σs}, (P ⊣⊢ₛ P' ∧ R) → (P' ∧ Q ⊣⊢ₛ C) → P ∧ Q ⊣⊢ₛ C ∧ R
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.kernelForkBiproductToSubtype_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  (CategoryTheory.Limits.kernelForkBiproductToSubtype f p).isLimit =
    CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯
      (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f pᶜ)) ⋯ ⋯
-- Lean.Elab.DefView
Lean.Elab.DefKind.abbrev.sizeOf_spec : sizeOf Lean.Elab.DefKind.abbrev = 1
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.get?.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.eq = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.eq = Ordering.gt → motive Ordering.gt) (h_3 : Ordering.eq = Ordering.eq → motive Ordering.eq),
  (match h : Ordering.eq with
    | Ordering.lt => h_1 h
    | Ordering.gt => h_2 h
    | Ordering.eq => h_3 h) =
    h_3 ⋯
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.lift_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : Type u₁} [inst_1 : CategoryTheory.Groupoid G]
  (φ : CategoryTheory.Functor C G) (Φ : CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) G),
  (CategoryTheory.FreeGroupoid.of C).comp Φ = φ → Φ = CategoryTheory.FreeGroupoid.lift φ
-- Mathlib.Order.Filter.Map
Filter.map_inl_inf_map_inr : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, Filter.map Sum.inl f ⊓ Filter.map Sum.inr g = ⊥
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.universally_inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C),
  (P ⊓ Q).universally = P.universally ⊓ Q.universally
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_empty : ∀ (R : Type u_1) {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X], (Convexity.convexHull R) ∅ = ∅
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
CategoryTheory.Functor.EffectivePresentation.mk.inj : ∀ {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} {X : D} {p : C} {f : F.obj p ⟶ X}
  {effectiveEpi : CategoryTheory.EffectiveEpi f} {p_1 : C} {f_1 : F.obj p_1 ⟶ X}
  {effectiveEpi_1 : CategoryTheory.EffectiveEpi f_1},
  { p := p, f := f, effectiveEpi := effectiveEpi } = { p := p_1, f := f_1, effectiveEpi := effectiveEpi_1 } →
    p = p_1 ∧ f ≍ f_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂)[k]? = t₁[k]?
-- Init.SimpLemmas
beq_false : ∀ (b : Bool), (b == false) = !b
-- Lean.Parser.Do
Lean.Parser.Term.doNested : Lean.Parser.Parser
-- Lean.Meta.SynthInstance
/-- Remark: `mkTableKey` assumes `e` does not contain assigned metavariables.  -/
Lean.Meta.SynthInstance.mkTableKey : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Expr → m Lean.Expr
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.mapEquiv_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] (f : R ≃+* S) (a : IsLocalRing.ResidueField R),
  (IsLocalRing.ResidueField.mapEquiv f) a = (IsLocalRing.ResidueField.map ↑f) a
-- Lean.Meta.Sym.AlphaShareCommon
/-- Monad for hash-consing expressions up to alpha-equivalence.

When checks are enabled in the context, hash-consing throws if a **new** term
violates the `SymM` representation invariants (reducible constants unfolded,
kernel projections folded). Terms already in the state are never re-checked:
membership certifies that a term was admitted before. On a throw, the state
contains every term hash-consed before the failure; these terms individually
satisfy the invariants, so callers should keep the partial state and retry after
repairing the input term. The error value is the `Cache` accumulated before the
failure (empty for `shareCommonAlphaInc`, which does not use one); the retry can
be seeded with it to avoid revisiting the subterms processed before the failure.
 -/
Lean.Meta.Sym.AlphaShareCommonM : Type → Type
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- Given two commutative rings `R S : CommRingCat` and a surjective morphism
`f : R ⟶ S`, the induced scheme morphism `specObj S ⟶ specObj R` is a
closed immersion.  -/
AlgebraicGeometry.IsClosedImmersion.spec_of_surjective : ∀ {R S : CommRingCat} (f : R ⟶ S),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f) →
    AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Spec.map f)
-- Mathlib.Topology.ContinuousMap.Weierstrass
/-- Another alternative statement of Weierstrass's theorem,
for those who like epsilons, but not bundled continuous functions.

Every real-valued function `ℝ → ℝ` which is continuous on `[a,b]`
can be approximated to within any `ε > 0` on `[a,b]` by some polynomial.
 -/
exists_polynomial_near_of_continuousOn : ∀ (a b : ℝ) (f : ℝ → ℝ),
  ContinuousOn f (Set.Icc a b) → ∀ (ε : ℝ), 0 < ε → ∃ p, ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAt_iff_extract : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  pat.isEmpty = false →
    (String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ ↔
      s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.copy.toByteArray)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.forIn'.loop.match_3.eq_2 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (i : ℕ) (h : i + 1 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.nondegComplex_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (i j : ℕ), s.nondegComplex.d i j = s.d i j
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.push : Std.Format → Lean.PrettyPrinter.FormatterM Unit
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.homotopyEquiv_homotopyInvHomId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  (hc : ∀ (j : ι), ∃ i, c.Rel i j), (HomologicalComplex.cylinder.homotopyEquiv K hc).homotopyInvHomId = Homotopy.ofEq ⋯
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
continuous_dist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α], Continuous fun p => dist p.1 p.2
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Constructs the list of values of the map.  -/
RBTree.RBMap.Values.toList : {α : Type u_1} → {β : Type u_2} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → List β
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instPosSMulMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : SMul α β] [inst_3 : Zero α]
  [PosSMulMono α β], PosSMulMono α βᵒᵈ
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_aux.invFun.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] (p : (i : ι) → Submodule R (Ms i)) [inst_3 : Fintype ι] [inst_4 : DecidableEq ι],
  Submodule.quotientPi_aux.invFun p = ⇑(Submodule.piQuotientLift p (Submodule.pi Set.univ p) (LinearMap.single R Ms) ⋯)
-- Mathlib.Analysis.Complex.Basic
_private.Mathlib.Analysis.Complex.Basic.0.RCLike.termImC : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.toAddGroup.eq_1 : ∀ {G : Type u_3} [inst : AddGroup G] (H : AddSubgroup G), H.toAddGroup = AddSubgroupClass.toAddGroup H
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instTopologicalSpaceCarrier : (R : Type u) → [inst : Ring R] → [inst_1 : TopologicalSpace R] → (M : TopModuleCat R) → TopologicalSpace ↑M.toModuleCat
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne.match_1.eq_3 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (h_1 : Unit → motive none)
  (h_2 :
    (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l]) →
        (nodup : [l].Nodup) → motive (some { clause := [l], nodupkey := nodupkey, nodup := nodup }))
  (h_3 : (val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some val)),
  (∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
      (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l])
      (nodup : [l].Nodup), val = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False) →
    (match some val with
      | none => h_1 ()
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } => h_2 l nodupkey nodup
      | some val => h_3 val) =
      h_3 val
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.getUnusedNames.go : Array Lean.Name → ℕ → Array Lean.Name → Lean.LocalContext → Array Lean.Name × Lean.LocalContext
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.mem_range_iff_of_surjective : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y) [AlgebraicGeometry.Surjective e],
  CategoryTheory.CategoryStruct.comp e g = f → ∀ (s : ↥S), s ∈ Set.range ⇑f ↔ s ∈ Set.range ⇑g
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.center_le_centralizer : ∀ {M : Type u_1} [inst : AddMonoid M] (s : Set M), AddSubmonoid.center M ≤ AddSubmonoid.centralizer s
-- Init.Data.BitVec.Lemmas
BitVec.instAssociativeHOr : ∀ {n : ℕ}, Std.Associative fun x1 x2 => x1 ||| x2
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.IsStableUnderComposition] [inst_2 : J.IsStableUnderBaseChange]
  [inst_3 : CategoryTheory.Limits.HasPullbacks C] [inst_4 : J.HasIsos],
  (CategoryTheory.Precoverage.toPretopology C J).toGrothendieck = J.toGrothendieck
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_lt_veblen_iff_right : ∀ {o a b : Ordinal.{u}}, Ordinal.veblen o a < Ordinal.veblen o b ↔ a < b
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.mk : {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] →
        (functor : CategoryTheory.Functor C D) →
          (inverse : CategoryTheory.Functor D C) →
            CategoryTheory.Functor.id C = functor.comp inverse →
              inverse.comp functor = CategoryTheory.Functor.id D → CategoryTheory.IsoCat C D
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_zero : ∀ (m k : ℕ), hyperoperation 0 m k = k + 1
-- Mathlib.Topology.Bornology.Absorbs
Absorbent.absorbs_finite : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t : Set α},
  Absorbent M s → t.Finite → Absorbs M s t
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString : ToString Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- An abbreviation for indexed families of seminorms. This is mainly to allow for dot-notation.  -/
SeminormFamily : (R : Type u_1) →
  (E : Type u_6) → Type u_9 → [inst : SeminormedRing R] → [inst_1 : AddCommGroup E] → [Module R E] → Type (max u_9 u_6)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{v', u', v, u} C],
  CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- The transpose of a matrix is column stochastic matrix if it is row stochastic.  -/
Matrix.transpose_mem_colStochastic_iff_mem_rowStochastic : ∀ {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 : Matrix n n R},
  M.transpose ∈ Matrix.colStochastic R n ↔ M ∈ Matrix.rowStochastic R n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_eq_some_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {fallback : α}, t.isEmpty = false → t.minKey? = some (t.minKeyD fallback)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.val_mk'' : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  (h : IsUnit A.det), ↑(Matrix.GeneralLinearGroup.mk'' A h) = A
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.sub'.match_1.eq_3 : ∀ (motive : PosNum → PosNum → Sort u_1) (a b : PosNum) (h_1 : (a : PosNum) → motive a PosNum.one)
  (h_2 : (b : PosNum) → motive PosNum.one b) (h_3 : (a b : PosNum) → motive a.bit0 b.bit0)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit1) (h_5 : (a b : PosNum) → motive a.bit1 b.bit0)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match a.bit0, b.bit0 with
    | a, PosNum.one => h_1 a
    | PosNum.one, b => h_2 b
    | a.bit0, b.bit0 => h_3 a b
    | a.bit0, b.bit1 => h_4 a b
    | a.bit1, b.bit0 => h_5 a b
    | a.bit1, b.bit1 => h_6 a b) =
    h_3 a b
-- Mathlib.Data.Finset.Dedup
Finset.exists_list_nodup_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), ∃ l, l.Nodup ∧ l.toFinset = s
-- Mathlib.NumberTheory.Padics.Complex
PadicComplex.RankOne.hom_eq_embedding : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], Valuation.RankOne.hom Valued.v = MonoidWithZeroHom.ValueGroup₀.embedding
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.contains_ofEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} {k' : α} {v' : β k'}
  {h : ∀ [Std.OrientedOrd α], k k' = Ordering.eq}, (Std.DTreeMap.Internal.Cell.ofEq k' v' h).contains = true
-- Mathlib.Algebra.Notation.Lemmas
dite_nonneg : ∀ {α : Type u_1} [inst : Zero α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α} [inst_2 : LE α],
  (∀ (h : p), 0 ≤ a h) → (∀ (h : ¬p), 0 ≤ b h) → 0 ≤ dite p a b
-- Mathlib.Order.CompleteLatticeIntervals
/-- Complete linear order structure on `Set.Icc`  -/
instCompleteLinearOrderElemIccOfFactLe : {α : Type u_2} →
  [inst : ConditionallyCompleteLinearOrder α] → {a b : α} → [Fact (a ≤ b)] → CompleteLinearOrder ↑(Set.Icc a b)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
isClosed_closedAbsConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] {s : Set E}, IsClosed ((closedAbsConvexHull 𝕜) s)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `α ≫ β`.  -/
Mathlib.Tactic.BicategoryLike.MkEvalComp : (Type → Type) → Type
-- Batteries.Data.List.Lemmas
List.findIdx_eq_findIdx? : ∀ {α : Type u_1} (p : α → Bool) (l : List α),
  List.findIdx p l =
    match List.findIdx? p l with
    | some i => i
    | none => l.length
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_eq_ofIntTruncate : ∀ {x : ℤ} {h₁ : Int16.minValue.toInt ≤ x} {h₂ : x ≤ Int16.maxValue.toInt}, Int16.ofIntLE x h₁ h₂ = Int16.ofIntClamp x
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.functorEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (G : CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) D),
  CategoryTheory.FreeGroupoid.functorEquiv G = (CategoryTheory.FreeGroupoid.of C).comp G
-- Mathlib.CategoryTheory.Limits.Final
/-- If `H` creates colimits of shape `C` and `F : C ⥤ D` is final, then `H` creates colimits of
shape `D`.  -/
CategoryTheory.Functor.Final.createsColimitsOfShapeOfFinal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {B : Type u₄} →
                  [inst_4 : CategoryTheory.Category.{v₄, u₄} B] →
                    (H : CategoryTheory.Functor E B) →
                      [CategoryTheory.CreatesColimitsOfShape C H] → CategoryTheory.CreatesColimitsOfShape D H
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.equicontinuousWithinAt_iff : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {κ₁ : Type u_11}
  {κ₂ : Type u_12} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α}
  {S : Set X} {x₀ : X},
  (nhdsWithin x₀ S).HasBasis p₁ s₁ →
    (uniformity α).HasBasis p₂ s₂ →
      (EquicontinuousWithinAt F S x₀ ↔
        ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂)
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instMul : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → Mul (LowerSet α)
-- Mathlib.Data.Finite.Perm
Equiv.Perm.isMulCommutative_iff_card_le_two : ∀ {α : Type u_1} [Finite α], IsMulCommutative (Equiv.Perm α) ↔ Nat.card α ≤ 2
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.yoneda_preservesLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : CategoryTheory.Category.{t, w} J]
  (X : C), CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.yoneda.obj X)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Stmt.write.sizeOf_spec : ∀ {Γ : Type u_1} [inst : SizeOf Γ] (a : Γ), sizeOf (Turing.TM0.Stmt.write a) = 1 + sizeOf a
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.IsMulSpanning.of_le : ∀ {G : Type u_1} [inst : Group G] {M N : Submonoid G}, M.IsMulSpanning → M ≤ N → N.IsMulSpanning
-- Mathlib.Algebra.Group.Defs
CommGroup.toCancelCommMonoid : {G : Type u_1} → [CommGroup G] → CancelCommMonoid G
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.iUnionNotConvergentSeq_measurableSet : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι]
  [inst_2 : Nonempty ι] [inst_3 : Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), Measurable fun a => edist (f n a) (g a))
  (hsm : MeasurableSet s) (hs : μ s ≠ ⊤)
  (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))),
  MeasurableSet (MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hsm hs hfg)
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_mul_left_eball`. -/
EMetric.preimage_mul_left_ball : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ENNReal),
  (fun x => a * x) ⁻¹' Metric.eball b r = Metric.eball (a⁻¹ * b) r
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.ext : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} {f g : CauSeq β abv}, (∀ (i : ℕ), ↑f i = ↑g i) → f = g
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_eq_submodule_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) [h : RingHomSurjective f]
  (I : Ideal R), Ideal.map f I = Submodule.map f.toSemilinearMap I