mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.getKey!_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, m₁.Equiv m₂ → m₁.getKey! k = m₂.getKey! k
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_comp_mono_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z) [inst_3 : CategoryTheory.Mono h],
  CategoryTheory.IsIso
    ((CategoryTheory.Limits.kernelSubobject f).ofLE
      (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h)) ⋯)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, (t.erase k).get! k = default
-- Mathlib.Order.CompleteLattice.Lemmas
sup_eq_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] (x y : α), x ⊔ y = ⨆ b, bif b then x else y
-- Init.Data.UInt.Bitwise
UInt32.xor_zero : ∀ {a : UInt32}, a ^^^ 0 = a
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.PreservesColimits.preservesFilteredColimits : ∀ {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.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Batteries.Data.NameSet
Lean.NameSet.instSDiff_batteries : SDiff Lean.NameSet
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
_private.Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives.0.HomotopyCategory.Plus.isRightDerivabilityStructure.instIsInducedPlusInjectiveObjectInverseImageQuasiIsoMapCochainComplexPlusιIsomorphismsL : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.Plus.isRightDerivabilityStructure.L✝ C).IsInduced
-- Mathlib.Algebra.Ring.SumsOfSquares
NonUnitalSubsemiring.sumSq_toAddSubmonoid : ∀ {T : Type u_2} [inst : NonUnitalCommSemiring T], (NonUnitalSubsemiring.sumSq T).toAddSubmonoid = AddSubmonoid.sumSq T
-- Mathlib.Data.List.TakeDrop
List.takeI_left : ∀ {α : Type u} [inst : Inhabited α] (l₁ l₂ : List α), List.takeI l₁.length (l₁ ++ l₂) = l₁
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.halt.sizeOf_spec : sizeOf Turing.ToPartrec.Cont.halt = 1
-- Lean.Parser.Term
Lean.Parser.Term.optExprPrecedence : Lean.Parser.Parser
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued continuous maps, a version for a closed set. Let
`s` be a closed set in a normal topological space `Y`. Let `f` be a continuous real-valued function
on `s`. Let `t` be a nonempty convex set of real numbers (we use `OrdConnected` instead of `Convex`
to automatically deduce this argument by typeclass search) such that `f x ∈ t` for all `x : s`. Then
there exists a continuous real-valued function `g : C(Y, ℝ)` such that `g y ∈ t` for all `y` and
`g.restrict s = f`.  -/
ContinuousMap.exists_restrict_eq_forall_mem_of_closed : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : C(↑s, ℝ)) {t : Set ℝ} [t.OrdConnected],
  (∀ (x : ↑s), f x ∈ t) → t.Nonempty → IsClosed s → ∃ g, (∀ (y : Y), g y ∈ t) ∧ ContinuousMap.restrict s g = f
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A set of points, whose `vectorSpan` is finite-dimensional, is
collinear if and only if their `vectorSpan` has dimension at most
`1`.  -/
collinear_iff_finrank_le_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} [FiniteDimensional k ↥(vectorSpan k s)],
  Collinear k s ↔ Module.finrank k ↥(vectorSpan k s) ≤ 1
-- Mathlib.Order.Defs.PartialOrder
not_le_of_gt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.one_eq_lift_iff : ∀ {a : Cardinal.{u}}, 1 = Cardinal.lift.{v, u} a ↔ 1 = a
-- Mathlib.Tactic.CrossRefAttribute
/-- The environment extension storing all cross-references.
`addImportedFn` is a constant function to avoid a performance overhead during initialization.  -/
Mathlib.CrossRef.tagExt : Lean.SimplePersistentEnvExtension Mathlib.CrossRef.Tag (Array (Array Mathlib.CrossRef.Tag))
-- Init.Core
id.eq_1 : ∀ {α : Sort u} (a : α), id a = a
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
_private.Mathlib.AlgebraicGeometry.Morphisms.FlatRank.0.AlgebraicGeometry.IsAffine.finrank.eq_1 : ∀ {X S : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine S] (f : X ⟶ S) (s : ↥S),
  AlgebraicGeometry.IsAffine.finrank✝ f s =
    (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).finrank (S.isoSpec.hom s)
-- Init.Data.List.Pairwise
List.Pairwise.iff : ∀ {α : Type u_1} {R S : α → α → Prop},
  (∀ (a b : α), R a b ↔ S a b) → ∀ {l : List α}, List.Pairwise R l ↔ List.Pairwise S l
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
MonomialOrder.degLex.congr_simp : ∀ {σ : Type u_2} [inst : LinearOrder σ] [inst_1 : WellFoundedGT σ], MonomialOrder.degLex = MonomialOrder.degLex
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.ofList_equiv_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {l : List (α × β)},
  (Std.DHashMap.Raw.Const.ofList l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l)
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.mk_factors_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  (CategoryTheory.Subobject.mk f).Factors f
-- Lean.Message
Lean.MessageData.ofOriginatingSyntax.inj : ∀ {a : Lean.Syntax} {a_1 : Lean.MessageData} {a_2 : Lean.Syntax} {a_3 : Lean.MessageData},
  Lean.MessageData.ofOriginatingSyntax a a_1 = Lean.MessageData.ofOriginatingSyntax a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.split.eq_1 : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} (firstRejected curr : s.Pos)
  (hle : firstRejected ≤ curr),
  String.Slice.Pattern.Model.split pat firstRejected curr hle =
    if h : curr = s.endPos then [s.subslice firstRejected curr hle]
    else
      match hd : String.Slice.Pattern.Model.matchAt? pat curr with
      | some pos =>
        have this := ⋯;
        s.subslice firstRejected curr hle :: String.Slice.Pattern.Model.split pat pos pos ⋯
      | none => String.Slice.Pattern.Model.split pat firstRejected (curr.next h) ⋯
-- Mathlib.LinearAlgebra.Matrix.Gershgorin
/-- If `A` is a column strictly dominant diagonal matrix, then its determinant is nonzero.  -/
det_ne_zero_of_sum_col_lt_diag : ∀ {K : Type u_1} {n : Type u_2} [inst : NormedField K] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n K},
  (∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖) → A.det ≠ 0
-- Mathlib.Analysis.InnerProductSpace.Basic
instSymmEqInnerOfNat : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Sort u_4} (v : ι → E), Std.Symm fun i j => inner 𝕜 (v i) (v j) = 0
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.lift.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] {S : Type u_4} [inst_6 : CommRing S]
  [inst_7 : Algebra R S] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R S B] [inst_10 : Algebra R A]
  [inst_11 : IsScalarTower R A B] [isIntegral : Algebra.IsIntegral R S],
  IsIntegralClosure.lift R A B = IsIntegralClosure.lift R A B
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (s : Set α),
  SubMulAction.ofFixingSubgroup M s = { carrier := sᶜ, smul_mem' := ⋯ }
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- If the `d` from `Ideal.exists_mul_add_mem_pow_succ` is unique, up to `P`,
then so are the `c`s, up to `P ^ (i + 1)`.
Inspired by [Neukirch], proposition 6.1  -/
Ideal.mul_add_mem_pow_succ_inj : ∀ {S : Type u_1} [inst : CommRing S] (P : Ideal S) {i : ℕ} (a d d' e e' : S),
  a ∈ P ^ i → e ∈ P ^ (i + 1) → e' ∈ P ^ (i + 1) → d - d' ∈ P → a * d + e - (a * d' + e') ∈ P ^ (i + 1)
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.RecurringRule.mk.injEq : ∀ (stdName : String) (stdOffset : Std.Time.TimeZone.Offset) (dst : Option Std.Time.TimeZone.DaylightSavingRule)
  (stdName_1 : String) (stdOffset_1 : Std.Time.TimeZone.Offset) (dst_1 : Option Std.Time.TimeZone.DaylightSavingRule),
  ({ stdName := stdName, stdOffset := stdOffset, dst := dst } =
      { stdName := stdName_1, stdOffset := stdOffset_1, dst := dst_1 }) =
    (stdName = stdName_1 ∧ stdOffset = stdOffset_1 ∧ dst = dst_1)
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.ofHom_apply : ∀ {R S : Type u} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (r : R),
  (CategoryTheory.ConcreteCategory.hom (SemiRingCat.ofHom f)) r = f r
-- Mathlib.GroupTheory.Index
/-- Relative version of `AddSubgroup.index_eq_two_iff_exists_notMem_and'`.  -/
AddSubgroup.relIndex_eq_two_iff_exists_notMem_and' : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a + b ∈ H ∨ b ∈ H
-- Init.Notation
/-- `max:prec` as a term. It is equivalent to `eval_prec max` for `eval_prec` defined at `Meta.lean`.
We use `max_prec` to workaround bootstrapping issues.
 -/
termMax_prec : Lean.ParserDescr
-- Mathlib.Topology.Order.IsLUB
exists_seq_strictAnti_tendsto' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [FirstCountableTopology α] {x y : α},
  x < y → ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo x y) ∧ Filter.Tendsto u Filter.atTop (nhds x)
-- Mathlib.Order.Filter.Basic
Filter.iSup_join : ∀ {α : Type u} {ι : Sort w} {f : ι → Filter (Filter α)}, ⨆ x, (f x).join = (⨆ x, f x).join
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.ofNat_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : ContinuousAdd M₁] (n : ℕ) [inst_5 : n.AtLeastTwo] (m : M₁),
  (OfNat.ofNat n) m = OfNat.ofNat n • m
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The free functor from the Eilenberg-Moore category, constructing an algebra for any object.  -/
CategoryTheory.Monad.free : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (T : CategoryTheory.Monad C) → CategoryTheory.Functor C T.Algebra
-- Init.MetaTypes
Lean.Meta.LiftLetsConfig.mk.inj : ∀ {toExtractLetsConfig toExtractLetsConfig_1 : Lean.Meta.ExtractLetsConfig},
  { toExtractLetsConfig := toExtractLetsConfig } = { toExtractLetsConfig := toExtractLetsConfig_1 } →
    toExtractLetsConfig = toExtractLetsConfig_1
-- Mathlib.GroupTheory.Coset.Basic
AddMonoidHom.fiberEquivOfSurjective.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] {f : α →+ H} (hf : Function.Surjective ⇑f)
  (h h' : H),
  AddMonoidHom.fiberEquivOfSurjective hf h h' =
    (AddMonoidHom.fiberEquivKerOfSurjective hf h).trans (AddMonoidHom.fiberEquivKerOfSurjective hf h').symm
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instMax : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] → [inst_1 : Field K] → [inst_2 : Algebra k K] → Max (FiniteGaloisIntermediateField k K)
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- **Alias** of `Topology.RelCWComplex.finite_cells_of_finite`.

---

If `C` is finite as a CW complex then the collection of all cells (of any dimension) is
finite.  -/
Topology.CWComplex.finite_cells_of_finite : ∀ {X : Type u_2} [inst : TopologicalSpace X] {C D : Set X} [inst_1 : Topology.RelCWComplex C D]
  [finite : Topology.RelCWComplex.Finite C], Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)
-- Init.Data.SInt.Basic
/-- Obtains the `ISize` whose 2's complement representation is the given `BitVec`.  -/
ISize.ofBitVec : BitVec System.Platform.numBits → ISize
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedElabInfo : Inhabited Lean.Elab.ElabInfo
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_eq_natCast_iff : ∀ (a b c : ℕ), ↑a = ↑b ↔ a ≡ b [MOD c]
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.get? k = (t.get? k).bind (f k)
-- Std.Do.SPred.DerivedLaws
/-- A mapping from `SPred` to pure propositions that are known to be equivalent.
 -/
Std.Do.SPred.Tactic.IsPure : {σs : List (Type u)} → Std.Do.SPred σs → outParam Prop → Prop
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.epi_of_isZero_cokernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Limits.HasCokernel f],
  CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel f) → CategoryTheory.Epi f
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.unop_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Dᵒᵖ Cᵒᵖ} (h : G ⊣ F),
  h.unop.counit = CategoryTheory.NatTrans.unop h.unit
-- Mathlib.Order.WithBot
WithBot.bot_ne_coe : ∀ {α : Type u_1} {a : α}, ⊥ ≠ ↑a
-- Mathlib.Order.KrullDimension
Order.height_eq_coe_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
  Order.height x = ↑n ↔ Order.height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, Order.height y = ↑n - 1) ∧ ∀ y < x, Order.height y < ↑n
-- Mathlib.Topology.Algebra.ConstMulAction
closure_smul₀' : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {c : G₀}, c ≠ 0 → ∀ (s : Set α), closure (c • s) = c • closure s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_le_arccos : ∀ {x y : ℝ}, x ≤ y → Real.arccos y ≤ Real.arccos x
-- Mathlib.Analysis.MeanInequalitiesPow
ENNReal.LpAddConst_lt_top : ∀ (p : ENNReal), p.LpAddConst < ⊤
-- Mathlib.AlgebraicGeometry.Limits
/-- The canonical map `∐ Spec Rᵢ ⟶ Spec (Π Rᵢ)`.
This is an isomorphism when the product is finite.  -/
AlgebraicGeometry.sigmaSpec : {ι : Type u} →
  (R : ι → CommRingCat) →
    (∐ fun i => AlgebraicGeometry.Spec (R i)) ⟶ AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i)))
-- Init.Data.List.ToArray
List.foldlM_toArray : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β) (l : List α),
  Array.foldlM f init l.toArray = List.foldlM f init l
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.forIn_mapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} {β₂ : Type w}
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o] [inst_5 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [Std.Iterators.Finite α Id] [inst_8 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β}
  {f : β → Std.Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)},
  forIn (Std.Iter.mapWithPostcondition f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out).run
      g __do_lift acc
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom_apply : ∀ (X Y : Type u) (x : X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom)
      ((CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.coprod.inl) x) =
    Sum.inl x
-- Mathlib.Probability.Moments.CovarianceBilinDual
StrongDual.toLpₗ_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal}
  {𝕜 : Type u_2} [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedSpace 𝕜 E] (h_Lp : MeasureTheory.MemLp id p μ)
  (L : StrongDual 𝕜 E), (StrongDual.toLpₗ μ p) L = MeasureTheory.MemLp.toLp ⇑L ⋯
-- Aesop.Search.ExpandSafePrefix
Aesop.safeExpansionFailedException : Lean.Exception
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_le_one : ∀ {x : ℝ}, √x ≤ 1 ↔ x ≤ 1
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubring.instIsSemitopologicalRing : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalRing R] [IsSemitopologicalRing R]
  (S : NonUnitalSubring R), IsSemitopologicalRing ↥S
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_sInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (P : Set (CategoryTheory.MorphismProperty D)),
  (sInf P).inverseImage F = ⨅ P' ∈ P, P'.inverseImage F
-- Mathlib.Logic.Relation
Relation.ReflTransGen.single : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, r a b → Relation.ReflTransGen r a b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂).getKey! k = default
-- Mathlib.Order.PrimeIdeal
Order.Ideal.IsPrime.mk : ∀ {P : Type u_1} [inst : Preorder P] {I : Order.Ideal P} [toIsProper : I.IsProper], Order.IsPFilter (↑I)ᶜ → I.IsPrime
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_image2_eq_csSup_csSup : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
  {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) →
    (∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)) →
      s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sSup s) (sSup t)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.mem_weakEquivalences : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.weakEquivalences C f
-- Mathlib.Tactic.Choose
/-- A `choose` argument is either a bare identifier or a parenthesized extended binder  -/
Mathlib.Tactic.Choose.chooseBinder : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `DifferentiableOn.pow` -/
DifferentiableOn.fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {s : Set E},
  DifferentiableOn 𝕜 f s → ∀ (n : ℕ), DifferentiableOn 𝕜 (fun i => f i ^ n) s
-- Std.Time.Format.Basic
Std.Time.FormatType.eq_2 : ∀ (result : Type) (val : String) (xs : List Std.Time.FormatPart),
  Std.Time.FormatType result (Std.Time.FormatPart.string val :: xs) = Std.Time.FormatType result xs
-- Mathlib.Algebra.Lie.Loop
LieAlgebra.LoopAlgebra.residuePairing.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup A] [inst_4 : DistribSMul A R] [inst_5 : SMulCommClass A R R] (Φ Φ_1 : LinearMap.BilinForm R L),
  Φ = Φ_1 → LieAlgebra.LoopAlgebra.residuePairing R A L Φ = LieAlgebra.LoopAlgebra.residuePairing R A L Φ_1
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.dist_le_mul : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f → ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.coe_id : ∀ {X : PartOrdEmb}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Init.Data.List.Impl
/-- Replaces the first element of the list `l` that is equal to `a` with `b`. If no element is equal to
`a`, then the list is returned unchanged.

`O(|l|)`. This is a tail-recursive version of `List.replace` that's used in runtime code.

Examples:
* `[1, 4, 2, 3, 3, 7].replaceTR 3 6 = [1, 4, 2, 6, 3, 7]`
* `[1, 4, 2, 3, 3, 7].replaceTR 5 6 = [1, 4, 2, 3, 3, 7]`
 -/
List.replaceTR : {α : Type u_1} → [BEq α] → List α → α → α → List α
-- Mathlib.Algebra.DualNumber
/-- `ε` commutes with every element of the algebra.  -/
DualNumber.commute_eps_right : ∀ {R : Type u_1} [inst : Semiring R] (x : DualNumber R), Commute x DualNumber.eps
-- Mathlib.Order.RelClasses
wellFoundedLT_dual_iff : ∀ (α : Type u_1) [inst : LT α], WellFoundedLT αᵒᵈ ↔ WellFoundedGT α
-- Mathlib.CategoryTheory.Sites.Continuous
/-- The induced functor `Sheaf K A ⥤ Sheaf J A` given by `F.op ⋙ _`
if `F` is a continuous functor.
 -/
CategoryTheory.Functor.sheafPushforwardContinuous : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (A : Type u) →
            [inst_2 : CategoryTheory.Category.{t, u} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [F.IsContinuous J K] → CategoryTheory.Functor (CategoryTheory.Sheaf K A) (CategoryTheory.Sheaf J A)
-- Mathlib.Probability.Process.HittingTime
/-- Hitting time: given a stochastic process `u` and a set `s`, `hittingBtwn u s n m` is
the first time `u` is in `s` after time `n` and before time `m` (if `u` does not hit `s`
after time `n` and before `m` then the hitting time is simply `m`).

The hitting time is a stopping time if the process is strongly adapted and discrete.  -/
MeasureTheory.hittingBtwn : {Ω : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [Preorder ι] → [InfSet ι] → (ι → Ω → β) → Set β → ι → ι → Ω → ι
-- Aesop.Search.Queue.Class
Aesop.Queue.popGoal : {Q : Type} → [self : Aesop.Queue Q] → Q → BaseIO (Option Aesop.GoalRef × Q)
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.Nonempty.inr : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, t.Nonempty → (s ∪ t).Nonempty
-- Batteries.Tactic.Lint.Simp
Batteries.Tactic.Lint.SimpTheoremInfo.mk.injEq : ∀ (hyps : Array Lean.Expr) (lhs rhs : Lean.Expr) (hyps_1 : Array Lean.Expr) (lhs_1 rhs_1 : Lean.Expr),
  ({ hyps := hyps, lhs := lhs, rhs := rhs } = { hyps := hyps_1, lhs := lhs_1, rhs := rhs_1 }) =
    (hyps = hyps_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Data.W.Basic
/-- The canonical map to the corresponding sigma type, returning the label of a node as an
element `a` of `α`, and the children of the node as a function `β a → WType β`.  -/
WType.toSigma : {α : Type u_1} → {β : α → Type u_2} → WType β → (a : α) × (β a → WType β)
-- Mathlib.Topology.MetricSpace.Polish
CompletePseudometrizable.iInf : ∀ {α : Type u_1} {ι : Type u_3} [Countable ι] {t : ι → TopologicalSpace α},
  (∃ t₀, T2Space α ∧ ∀ (i : ι), t i ≤ t₀) →
    (∀ (i : ι), ∃ u, CompleteSpace α ∧ (uniformity α).IsCountablyGenerated ∧ u.toTopologicalSpace = t i) →
      ∃ u, CompleteSpace α ∧ (uniformity α).IsCountablyGenerated ∧ u.toTopologicalSpace = ⨅ i, t i