mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.ReduceOption
List.reduceOption_mem_iff : ∀ {α : Type u_1} {l : List (Option α)} {x : α}, x ∈ l.reduceOption ↔ some x ∈ l
-- Mathlib.Algebra.Homology.Augment
ChainComplex.augmentTruncate_hom_f_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) (i : ℕ), C.augmentTruncate.hom.f (i + 1) = CategoryTheory.CategoryStruct.id (C.X (i + 1))
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryGE? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → Option (α × β)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.eval₂_toLaurent : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] (f : R →+* S) (x : Sˣ)
  (p : Polynomial R), (LaurentPolynomial.eval₂ f x) (Polynomial.toLaurent p) = Polynomial.eval₂ f (↑x) p
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instIsStableUnderTransfiniteCompositionAnodyneExtensions : SSet.anodyneExtensions.IsStableUnderTransfiniteComposition
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.floor.congr_simp : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m m_1 : E), m = m_1 → ZSpan.floor b m = ZSpan.floor b m_1
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.min : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : LinearOrder M] {f g : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → Function.HasFiniteSupport fun a => min (f a) (g a)
-- Mathlib.RingTheory.Invariant.Basic
/-- If `G` acts on `B/A` with `A` as the fixed subring, then `G` also acts on `L/K` with `K` as
the fixed subfield, where `K` and `L` are the fraction fields of `A` and `B` respectively.  -/
IsFractionRing.isInvariant : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [inst : Group G] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : Algebra A B] [inst_4 : Field K] [inst_5 : Field L] [inst_6 : Algebra K L]
  [inst_7 : Algebra A K] [inst_8 : Algebra B L] [inst_9 : Algebra A L] [IsFractionRing A K] [IsFractionRing B L]
  [IsScalarTower A K L] [IsScalarTower A B L] [inst_14 : MulSemiringAction G B] [inst_15 : MulSemiringAction G L]
  [SMulDistribClass G B L] [hAB : Algebra.IsInvariant A B G] [SMulCommClass G A B] [Finite G], Algebra.IsInvariant K L G
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Decomp.0.SimpleGraph.Walk.takeUntil.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V}
  (motive : (w : V) → (x : G.Walk v w) → (x_1 : V) → x_1 ∈ x.support → Sort u_2) (u : V)
  (h : u ∈ SimpleGraph.Walk.nil.support)
  (h_1 : (u : V) → (h : u ∈ SimpleGraph.Walk.nil.support) → motive v SimpleGraph.Walk.nil u h)
  (h_2 :
    (w v_1 : V) →
      (r : G.Adj v v_1) →
        (p : G.Walk v_1 w) →
          (u : V) → (h : u ∈ (SimpleGraph.Walk.cons r p).support) → motive w (SimpleGraph.Walk.cons r p) u h),
  (match v, SimpleGraph.Walk.nil, u, h with
    | .(v), SimpleGraph.Walk.nil, u, h => h_1 u h
    | w, SimpleGraph.Walk.cons r p, u, h => h_2 w v_1 r p u h) =
    h_1 u h
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
  [inst_4 : S₃.HasLeftHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) {Z : C} (h : S₃.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ₂) h)
-- Init.Try
/-- Maximum number of suggestions.  -/
Lean.Try.Config.max : Lean.Try.Config → ℕ
-- Init.Data.List.TakeDrop
List.take_of_length_le : ∀ {α : Type u_1} {i : ℕ} {l : List α}, l.length ≤ i → List.take i l = l
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_rat_le_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ}, ¬p ∣ q.den → ‖↑q‖ ≤ 1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.foldl_eq_foldl_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} {δ : Type w} [inst : Std.TransCmp cmp]
  {f : δ → α → δ} {init : δ}, Std.ExtTreeSet.foldl f init t = List.foldl f init t.toList
-- Mathlib.RingTheory.NormalClosure
Ring.instFiniteNormalClosure_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S] [Module.Finite R S] [PerfectField (FractionRing R)]
  [IsDedekindDomain S], Module.Finite R (Ring.NormalClosure R S)
-- Mathlib.Topology.Constructions
Topology.isEmbedding_sigmaMap : ∀ {ι : Type u_5} {κ : Type u_6} {σ : ι → Type u_7} {τ : κ → Type u_8} [inst : (i : ι) → TopologicalSpace (σ i)]
  [inst_1 : (k : κ) → TopologicalSpace (τ k)] {f₁ : ι → κ} {f₂ : (i : ι) → σ i → τ (f₁ i)},
  Function.Injective f₁ → (Topology.IsEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Topology.IsEmbedding (f₂ i))
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- The canonical isomorphism `X K.op i ≅ Opposite.op (X K i)`.  -/
HomologicalComplex.extend.XOpIso : {ι : Type u_1} →
  {c : ComplexShape ι} →
    {C : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_3} C] →
        [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
            (K : HomologicalComplex C c) →
              (i : Option ι) → HomologicalComplex.extend.X K.op i ≅ Opposite.op (HomologicalComplex.extend.X K i)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm_self : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, CliffordAlgebra.changeForm ⋯ = LinearMap.id
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_eq_zpow_log_mulValuation : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℚ_[p]}, x ≠ 0 → ‖x‖ = ↑p ^ (Padic.mulValuation x).log
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β k} {kmi : α}, (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.coe_taylorAlgHom : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R), ↑(Polynomial.taylorAlgHom r) = Polynomial.taylor r
-- Mathlib.Algebra.Free
FreeSemigroup.recOnMul.eq_1 : ∀ {α : Type u} {C : FreeSemigroup α → Sort l} (x : FreeSemigroup α) (ih1 : (x : α) → C (FreeSemigroup.of x))
  (ih2 : (x : α) → (y : FreeSemigroup α) → C (FreeSemigroup.of x) → C y → C (FreeSemigroup.of x * y)),
  x.recOnMul ih1 ih2 =
    FreeSemigroup.recOn x fun f s =>
      List.recOn (motive := fun x => (x_1 : α) → C { head := x_1, tail := x }) s ih1
        (fun hd tl ih f => ih2 f { head := hd, tail := tl } (ih1 f) (ih hd)) f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {fallback : β}, Std.ExtDTreeMap.Const.getD (t.erase k) k fallback = fallback
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α},
  (Std.ExtHashMap.filter f m)[k]? = m[k]?.pfilter fun x_2 h' => f (m.getKey k ⋯) x_2
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.le_nhds_infty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : Filter (OnePoint X)},
  f ≤ nhds OnePoint.infty ↔ ∀ (s : Set X), IsClosed s → IsCompact s → OnePoint.some '' sᶜ ∪ {OnePoint.infty} ∈ f
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.nonempty_interior' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (self : ModelWithCorners 𝕜 E H),
  (interior (Set.range ↑self.toPartialEquiv)).Nonempty
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasOxfordStrings.comma : {α : Sort u_1} → [self : Lean.HasOxfordStrings✝ α] → α
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- **Alias** of `Module.Flat.exists_factorization_of_finitePresentation`.

---

Every homomorphism from a finitely presented module to a flat module factors through a finite
free module.  -/
Module.Flat.exists_factorization_of_isFinitelyPresented : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  {P : Type u_3} [inst_4 : AddCommGroup P] [inst_5 : Module R P] [Module.FinitePresentation R P] (h₁ : P →ₗ[R] M),
  ∃ k h₂ h₃, h₁ = h₃ ∘ₗ h₂
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_roc_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi + 1
-- Lean.Meta.Tactic.Simp.Types
/-- Given a simplified function result `r` and arguments `args`, simplify arguments using `simp` and `dsimp`.
The resulting proof is built using `congr` and `congrFun` theorems.
 -/
Lean.Meta.Simp.congrArgs : Lean.Meta.Simp.Result → Array Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Std.Time.DateTime.Timestamp
/-- Subtracts a `Nanosecond.Offset` from the given `Timestamp`.
 -/
Std.Time.Timestamp.subNanoseconds : Std.Time.Timestamp → Std.Time.Nanosecond.Offset → Std.Time.Timestamp
-- Init.Data.Dyadic.Basic
/-- The "precision" of a dyadic number, i.e. in `n * 2^(-p)` with `n` odd the precision is `p`.  -/
Dyadic.precision : Dyadic → Option ℤ
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseFormatPart : Std.Internal.Parsec.String.Parser Std.Time.FormatPart
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.IsPullback.iff_of_equiv : ∀ (sq₁ : CategoryTheory.Square (Type v)) (sq₂ : CategoryTheory.Square (Type u)) (e₁ : sq₁.X₁ ≃ sq₂.X₁)
  (e₂ : sq₁.X₂ ≃ sq₂.X₂) (e₃ : sq₁.X₃ ≃ sq₂.X₃) (e₄ : sq₁.X₄ ≃ sq₂.X₄),
  ⇑e₂ ∘ ⇑(CategoryTheory.ConcreteCategory.hom sq₁.f₁₂) = ⇑(CategoryTheory.ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁ →
    ⇑e₃ ∘ ⇑(CategoryTheory.ConcreteCategory.hom sq₁.f₁₃) = ⇑(CategoryTheory.ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁ →
      ⇑e₄ ∘ ⇑(CategoryTheory.ConcreteCategory.hom sq₁.f₂₄) = ⇑(CategoryTheory.ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂ →
        ⇑e₄ ∘ ⇑(CategoryTheory.ConcreteCategory.hom sq₁.f₃₄) = ⇑(CategoryTheory.ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃ →
          (sq₁.IsPullback ↔ sq₂.IsPullback)
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_iff_bmod_eq_zero : ∀ {a : ℕ} {b : ℤ}, ↑a ∣ b ↔ b.bmod a = 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edges_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w),
  (p.concat h).edges = p.edges.concat s(v, w)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.hom_ext_iff : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  {f g : Monoid.Coprod M N →* P},
  f = g ↔ f.comp Monoid.Coprod.inl = g.comp Monoid.Coprod.inl ∧ f.comp Monoid.Coprod.inr = g.comp Monoid.Coprod.inr
-- Init.Data.List.Find
List.findIdx?_eq_some_of_exists : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, (∃ x ∈ xs, p x = true) → List.findIdx? p xs = some (List.findIdx p xs)
-- Lean.Language.Lean.Types
/-- Syntax tree of the command.  -/
Lean.Language.Lean.CommandParsedSnapshot.stx : Lean.Language.Lean.CommandParsedSnapshot → Lean.Syntax
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filter_le_size : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  {f : (a : α) → β a → Bool} (h : t.WF), (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.size ≤ t.size
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Collector.Cache : Type
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
UniformCauchySeqOn.inv : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {s : Set β}, UniformCauchySeqOn f l s → UniformCauchySeqOn f⁻¹ l s
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The ring homomorphism `(R/I)/J' -> R/(I ⊔ J)` induced by `quotLeftToQuotSup` where `J'`
is the image of `J` in `R/I`  -/
DoubleQuot.quotQuotToQuotSup : {R : Type u} → [inst : CommRing R] → (I J : Ideal R) → (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →+* R ⧸ I ⊔ J
-- Init.Data.Int.Order
Int.mul.eq_1 : ∀ (m_2 n_2 : ℕ), (Int.ofNat m_2).mul (Int.ofNat n_2) = Int.ofNat (m_2 * n_2)
-- Std.Time.Format.Modifier
/-- 18:00–21:00
 -/
Std.Time.ExtendedDayPeriod.evening : Std.Time.ExtendedDayPeriod
-- Mathlib.Order.BoundedOrder.Basic
/-- A bottom element can be replaced with `⊥`.

Prefer `IsBot.eq_bot` if `α` already has a bottom element.  -/
IsBot.rec : {α : Type u} →
  [inst : LE α] →
    {motive : (x : α) → IsBot x → Sort u_1} →
      ([inst_1 : OrderBot α] → motive ⊥ ⋯) → (x : α) → (hx : IsBot x) → motive x hx
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Two linear isometries are equal if they are equal on basis vectors.  -/
Module.Basis.ext_linearIsometry : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] {ι : Type u_11} (b : Module.Basis ι R E) {f₁ f₂ : E →ₛₗᵢ[σ₁₂] E₂},
  (∀ (i : ι), f₁ (b i) = f₂ (b i)) → f₁ = f₂
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.ofReal_setIntegral_one : ∀ {X : Type u_5} {x : MeasurableSpace X} (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (s : Set X),
  ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_preimage_mul_left : ∀ {a : ℝ},
  a ≠ 0 → ∀ (s : Set ℝ), MeasureTheory.volume ((fun x => a * x) ⁻¹' s) = ENNReal.ofReal |a⁻¹| * MeasureTheory.volume s
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- If the topology on `α` is generated by its restrictions to compact sets, then the space of
continuous maps `C(α, β)` is complete (w.r.t. the compact convergence uniformity).

Sufficient conditions on `α` to satisfy this condition are (weak) local compactness and sequential
compactness.  -/
ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] [CompleteSpace β]
  [CompactlyCoherentSpace α], CompleteSpace C(α, β)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_min : ∀ (x y : ℝ), ↑(min x y) = min ↑x ↑y
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.OuterRegular.comap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [BorelSpace α]
  {mβ : MeasurableSpace β} [inst_3 : TopologicalSpace β] [BorelSpace β] (μ : MeasureTheory.Measure β) [μ.OuterRegular]
  (f : α ≃ₜ β), (MeasureTheory.Measure.comap (⇑f) μ).OuterRegular
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.hasSum_aeval : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : MvPowerSeries.HasEval a)
  (f : MvPowerSeries σ R),
  HasSum (fun d => (MvPowerSeries.coeff d) f • d.prod fun s e => a s ^ e) ((MvPowerSeries.aeval ha) f)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_const : ∀ {ι : Type u_3} [Nonempty ι] (o : Ordinal.{max u_4 u_3}), (Ordinal.lsub fun x => o) = Order.succ o
-- Lean.Parser.Extension
Lean.Parser.ensureConstantParserAlias : Lean.Name → IO Unit
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, t.contains k = true → (cmp t.minKey! k).isLE = true
-- Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
/-- The restriction of a reflexive bilinear map `B` onto a submodule `W` is
nondegenerate if `W` has trivial intersection with its orthogonal complement,
that is `Disjoint W (W.orthogonalBilin B)`.  -/
LinearMap.nondegenerate_restrict_of_disjoint_orthogonal : ∀ {R : Type u_1} {M : Type u_4} {M₁ : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] {B : M →ₗ[R] M →ₗ[R] M₁},
  B.IsRefl → ∀ {W : Submodule R M}, Disjoint W (Submodule.orthogonalBilin B W) → (B.domRestrict₁₂ W W).Nondegenerate
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratioHom_apply : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (f : α →ᵈ α), Dilation.ratioHom f = Dilation.ratio f
-- Mathlib.CategoryTheory.Limits.Types.Equalizers
CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype : ∀ {Y Z : Type u} (g h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.equalizerIso g h).hom (TypeCat.ofHom Subtype.val) =
    CategoryTheory.Limits.equalizer.ι g h
-- Mathlib.MeasureTheory.Order.UpperLower
/-- If we can fit a small ball inside a set `sᶜ` intersected with any neighborhood of `x`, then the
density of `s` near `x` is not `1`.

Along with `aux₀`, this proves that `x` is not a Lebesgue point of `s`. This will be used to prove
that the frontier of an order-connected set is null.  -/
_private.Mathlib.MeasureTheory.Order.UpperLower.0.aux₁ : ∀ {ι : Type u_1} [inst : Fintype ι] {s : Set (ι → ℝ)} {x : ι → ℝ},
  (∀ (δ : ℝ),
      0 < δ → ∃ y, Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior sᶜ) →
    ¬Filter.Tendsto
        (fun r =>
          MeasureTheory.volume (closure s ∩ Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall x r))
        (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_obj_none : ∀ {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι'),
  (CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv ι' e).functor.obj none = none
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- The `pattern` of the first lemma in a section is shown as the header of that section.  -/
Mathlib.Tactic.ClickSuggestions.Result.pattern : {α : Type} → Mathlib.Tactic.ClickSuggestions.Result α → ProofWidgets.Html
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.eraseList.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (toErase : List α),
  Std.Internal.List.eraseList l toErase =
    match toErase with
    | [] => l
    | k :: toErase => Std.Internal.List.eraseList (Std.Internal.List.eraseKey k l) toErase
-- Lean.Meta.Basic
Lean.Meta.isListLevelDefEqAux : List Lean.Level → List Lean.Level → Lean.MetaM Bool
-- Mathlib.NumberTheory.FermatPsp
/-- This is a proof that the number produced using `psp_from_prime` is greater than the prime `p` used
to create it. The primary purpose of this lemma is to help prove `exists_infinite_pseudoprimes`.
 -/
_private.Mathlib.NumberTheory.FermatPsp.0.Nat.psp_from_prime_gt_p : ∀ {b : ℕ}, 2 ≤ b → ∀ {p : ℕ}, 2 < p → p < Nat.psp_from_prime✝ b p
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Reinterpret a `ContinuousMonoidHom` as a `MonoidHom`.  -/
ContinuousMonoidHom.toMonoidHom : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → (A →ₜ* B) → A →* B
-- Mathlib.Algebra.Symmetrized
SymAlg.instSMul : {α : Type u_1} → (R : Type u_2) → [SMul R α] → SMul R αˢʸᵐ
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The sieve of `X` generated by family of morphisms `Y i ⟶ X`.  -/
CategoryTheory.Sieve.ofArrows : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {I : Type u_1} → {X : C} → (Y : I → C) → ((i : I) → Y i ⟶ X) → CategoryTheory.Sieve X
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase_dup.injEq : ∀ (c c_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.erase_dup c = Lean.Meta.Grind.AC.EqCnstrProof.erase_dup c_1) = (c = c_1)
-- Mathlib.Algebra.Category.Grp.Basic
mulEquivIsoGroupIso.eq_1 : ∀ {X Y : GrpCat},
  mulEquivIsoGroupIso =
    { hom := TypeCat.ofHom fun e => e.toGrpIso, inv := TypeCat.ofHom fun i => i.groupIsoToMulEquiv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.Computability.EpsilonNFA
εNFA.εClosure.below.base : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} {motive : (a : σ) → M.εClosure S a → Prop} (s : σ) (a : s ∈ S),
  εNFA.εClosure.below ⋯
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.separatingLeft_toLinearMap₂_iff : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R}
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂),
  ((Matrix.toLinearMap₂ b₁ b₂) M).SeparatingLeft ↔ M.SeparatingLeft
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State.mk.injEq : ∀ (visitedLevel : Lean.LevelSet) (visitedExpr : Lean.ExprSet) (params : Array Lean.Name)
  (visitedLevel_1 : Lean.LevelSet) (visitedExpr_1 : Lean.ExprSet) (params_1 : Array Lean.Name),
  ({ visitedLevel := visitedLevel, visitedExpr := visitedExpr, params := params } =
      { visitedLevel := visitedLevel_1, visitedExpr := visitedExpr_1, params := params_1 }) =
    (visitedLevel = visitedLevel_1 ∧ visitedExpr = visitedExpr_1 ∧ params = params_1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).getKey? k = some k
-- Mathlib.Tactic.Order.Graph.Tarjan
/-- `lowlink[v]` is the smallest index of any node on the stack that is reachable from `v`
through `v`'s DFS subtree.  -/
Mathlib.Tactic.Order.Graph.TarjanState.lowlink : Mathlib.Tactic.Order.Graph.TarjanState → Std.HashMap ℕ ℕ
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.sUnion_sdiff_singleton_empty`. -/
Set.sUnion_diff_singleton_empty : ∀ {α : Type u_1} (s : Set (Set α)), ⋃₀ (s \ {∅}) = ⋃₀ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertMany_append : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l₁ l₂ : List (α × β)},
  Std.ExtDTreeMap.Const.insertMany t (l₁ ++ l₂) =
    Std.ExtDTreeMap.Const.insertMany (Std.ExtDTreeMap.Const.insertMany t l₁) l₂
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.coe_resLE_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (x : ↥V), ↑((AlgebraicGeometry.Scheme.Hom.resLE f U V e) x) = f ↑x
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyoneda_obj_map : ∀ (M : AddCommMonCatᵒᵖ) {X Y : AddCommMonCat} (f : X ⟶ Y),
  (AddCommMonCat.coyoneda.obj M).map f = AddCommMonCat.ofHom (AddMonoidHom.compHom (AddCommMonCat.Hom.hom f))
-- Mathlib.Order.Iterate
Function.Commute.iterate_le_of_map_le : ∀ {α : Type u_1} [inst : Preorder α] {f g : α → α},
  Function.Commute f g → Monotone f → Monotone g → ∀ {x : α}, f x ≤ g x → ∀ (n : ℕ), f^[n] x ≤ g^[n] x