mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Equiv.Sum
/-- The sum of `IsEmpty` with any type is equivalent to that type.  -/
Equiv.emptySum : (α : Type u_9) → (β : Type u_10) → [IsEmpty α] → α ⊕ β ≃ β
-- Mathlib.Algebra.Order.Module.Defs
/-- Binary strict **rearrangement inequality**.  -/
smul_add_smul_lt_smul_add_smul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_7 : Module α β]
  [PosSMulStrictMono α β] {a₁ a₂ : α} {b₁ b₂ : β}, a₂ < a₁ → b₂ < b₁ → a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckBinrelNoProp : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Algebra.Category.Grp.EpiMono
MonoidHom.ker_eq_bot_of_cancel : ∀ {A : Type u} {B : Type v} [inst : Group A] [inst_1 : Group B] {f : A →* B},
  (∀ (u v : ↥f.ker →* A), f.comp u = f.comp v → u = v) → f.ker = ⊥
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.finrank_corootSpanIn_int : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {L : Type u_8}
  [inst_2 : Field L] [inst_3 : Module L M] [inst_4 : Module L N] (Q : RootPairing ι L M N) [Q.IsRootSystem] [Finite ι]
  [CharZero L] [Q.IsCrystallographic], Module.finrank ℤ ↥(Q.corootSpan ℤ) = Module.finrank L N
-- Lean.Parser.Command
/-- `deprecated_module` marks the current module as deprecated.
When another module imports a deprecated module, a warning is emitted during elaboration.

```
deprecated_module "use NewModule instead" (since := "2026-03-19")
```

The warning message is optional but recommended.
The warning can be disabled with `set_option linter.deprecated.module false` or
`-Dlinter.deprecated.module=false`.
 -/
Lean.Parser.Command.deprecated_module : Lean.Parser.Parser
-- Mathlib.Order.Sublocale
Sublocale.carrier.instSemilatticeInf : {X : Type u_1} → [inst : Order.Frame X] → {S : Sublocale X} → SemilatticeInf ↥S
-- Mathlib.Logic.Relation
Relation.TransGen.tail' : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α}, Relation.ReflTransGen r a b → r b c → Relation.TransGen r a c
-- Mathlib.RingTheory.RingHom.PurelyInseparable
RingHom.IsPurelyInseparable.eq_1 : ∀ {F : Type u} {E : Type v} [inst : CommRing F] [inst_1 : CommRing E] (f : F →+* E),
  f.IsPurelyInseparable = IsPurelyInseparable F E
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], m₂.contains k = true → (m₁.inter m₂).get! k = m₁.get! k
-- Lean.Elab.Tactic.Induction
/-- If `stx` has a `with` clause, runs `m` within a tactic info node on `induction/cases ... with`.
The action `m` returns a list of metavariables to admit. The purpose of this is to let the remaining after goals be recorded
in the tactic info, while preserving the semantics that when there is a `with` clause, all unhandled alternatives are admitted.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.mkInitialTacticInfoForInduction : Lean.Syntax → Lean.Elab.Tactic.TacticM (Lean.Elab.Tactic.TacticM Lean.Elab.Info)
-- Mathlib.Topology.Bases
TopologicalSpace.countableBasis.congr_simp : ∀ (α : Type u) [t : TopologicalSpace α] [inst : SecondCountableTopology α] (a a_1 : Set α),
  a = a_1 → TopologicalSpace.countableBasis α a = TopologicalSpace.countableBasis α a_1
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- there exists a zero object  -/
CategoryTheory.Limits.HasZeroObject.zero : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasZeroObject C],
  ∃ X, CategoryTheory.Limits.IsZero X
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.append : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {lw rw : ℕ} → aig.RefVec lw → aig.RefVec rw → aig.RefVec (lw + rw)
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- `AdicCauchySequence I R` is an `R`-subalgebra of `ℕ → R`.  -/
AdicCompletion.AdicCauchySequence.subalgebra : {R : Type u_1} → [inst : CommRing R] → Ideal R → Subalgebra R (ℕ → R)
-- Mathlib.Tactic.ReduceModChar
/-- Given an expression of the form `a ^ b` in a ring of characteristic `n`, reduces `a`
modulo `n` recursively and then calculates `a ^ b` using fast modular exponentiation.  -/
Tactic.ReduceModChar.normPow : {u : Lean.Level} →
  {α : Q(Type u)} →
    (n n' : Q(ℕ)) →
      Q(Mathlib.Meta.NormNum.IsNat «$n» «$n'») →
        (e : Q(«$α»)) → (x : Q(Ring «$α»)) → Q(CharP «$α» «$n») → Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.GroupTheory.OrderOfElement
/-- If a direct product has finite order then so does each component.  -/
IsOfFinOrder.apply : ∀ {η : Type u_6} {Gs : η → Type u_7} [inst : (i : η) → Monoid (Gs i)] {x : (i : η) → Gs i},
  IsOfFinOrder x → ∀ (i : η), IsOfFinOrder (x i)
-- Mathlib.Tactic.Explode.Datatypes
/-- Simple list of `Expr`s.  -/
Mathlib.Explode.Entries.l : Mathlib.Explode.Entries → List Mathlib.Explode.Entry
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.coe_append : ∀ {α : Type u_1} {m n : ℕ} {x : Fin m ↪ α} {y : Fin n ↪ α} (h : Disjoint (Set.range ⇑x) (Set.range ⇑y)),
  ⇑(Fin.Embedding.append h) = Fin.append ⇑x ⇑y
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_of_injective' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2}
  {J : Type u_3} (X : I → C) (ι : J → I),
  Function.Injective ι →
    ∀ [inst_2 : CategoryTheory.Limits.HasCoproduct (X ∘ ι)] [inst_3 : CategoryTheory.Limits.HasCoproduct X]
      [CategoryTheory.Limits.HasCoproduct fun k => X ↑k],
      CategoryTheory.Mono (CategoryTheory.Limits.Sigma.desc fun j => CategoryTheory.Limits.Sigma.ι X (ι j))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.map_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  {δ : α → Type w'} {f : (a : α) → β a → γ a} {g : (a : α) → γ a → δ a},
  Std.ExtDTreeMap.map g (Std.ExtDTreeMap.map f t) = Std.ExtDTreeMap.map (fun k v => g k (f k v)) t
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
IicProdIoc_comp_restrict₂ : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] {a b : ι}, Finset.restrict₂ ⋯ ∘ IicProdIoc a b = Prod.snd
-- Init.Data.List.Erase
List.erase_cons_head : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) (l : List α), (a :: l).erase a = l
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.val_mkOfDetNeZero : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {K : Type u_1} [inst_2 : Field K] (A : Matrix n n K)
  (h : A.det ≠ 0), ↑(Matrix.GeneralLinearGroup.mkOfDetNeZero A h) = A
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eraseKey_eq_iff_beq_maxKey?_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.maxKey? (Std.Internal.List.eraseKey k l) = Std.Internal.List.maxKey? l ↔
      ∀ {km : α}, Std.Internal.List.maxKey? l = some km → (k == km) = false)
-- Std.Time.Format.Modifier
Std.Time.Modifier.b.sizeOf_spec : ∀ (presentation : Std.Time.Text), sizeOf (Std.Time.Modifier.b presentation) = 1 + sizeOf presentation
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_alter_eq_sub_one : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  k ∈ t → (f (t.get? k)).isNone = true → (t.alter k f).size = t.size - 1
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instRing : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Ring β] → [IsTopologicalRing β] → Ring C(α, β)
-- Mathlib.Condensed.Module
/-- The forgetful functor from condensed abelian groups to condensed sets.  -/
Condensed.abForget : CategoryTheory.Functor CondensedAb CondensedSet
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
AlgebraicTopology.DoldKan.hσ'_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {q n m : ℕ},
  n < q → ∀ (hnm : AlgebraicTopology.DoldKan.c.Rel m n), AlgebraicTopology.DoldKan.hσ' q n m hnm = 0
-- Mathlib.Tactic.Translate.Core
/-- Linter used by translate attributes that checks if the given declaration name is
equal to the automatically generated name  -/
Mathlib.Tactic.Translate.linter.translateGenerateName : Lean.Option Bool
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_natCast : ∀ (a : Ordinal.{u_1}) (n : ℕ), a ^ ↑n = a ^ n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sieve₀_trivial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C), (CategoryTheory.PreOneHypercover.trivial S).sieve₀ = ⊤
-- Std.Data.HashMap.Lemmas
Std.HashMap.map_map_equiv : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type w'} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β}
  {f : α → β → γ} {g : α → γ → δ},
  (Std.HashMap.map g (Std.HashMap.map f m)).Equiv (Std.HashMap.map (fun k v => g k (f k v)) m)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
fourier_gaussian_pi' : ∀ {b : ℂ},
  0 < b.re →
    ∀ (c : ℂ),
      (FourierTransform.fourier fun x => Complex.exp (-↑Real.pi * b * ↑x ^ 2 + 2 * ↑Real.pi * c * ↑x)) = fun t =>
        1 / b ^ (1 / 2) * Complex.exp (-↑Real.pi / b * (↑t + Complex.I * c) ^ 2)
-- Mathlib.Order.Concept
/-- The concept generated by a single attribute.  -/
Concept.ofAttribute : {α : Type u_2} → {β : Type u_3} → (r : α → β → Prop) → β → Concept α β r
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instDistribSMul : {k : Type u_1} →
  {G : Type u_2} → {S : Type u_3} → [inst : AddMonoid k] → [DistribSMul S k] → DistribSMul S (SkewMonoidAlgebra k G)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.homMk_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (φ : f ⟶ f'),
  ∃ ψ,
    ∃ (hψ : CategoryTheory.CategoryStruct.comp (S.map ψ) f'.hom = f.hom),
      φ = CategoryTheory.CostructuredArrow.homMk ψ hψ
-- Mathlib.Condensed.Light.Epi
LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite : ∀ (A : Type u') [inst : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w}
  [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_2 : CategoryTheory.ConcreteCategory A FA]
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)] {X Y : LightCondensed A} (f : X ⟶ Y),
  CategoryTheory.Sheaf.IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : CategoryTheory.ToType (Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x =
              (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y
-- Init.MetaTypes
/-- If `locals` is `true`, `dsimp` will unfold all definitions from the current file.
For local theorems, use `+suggestions` instead.
 -/
Lean.Meta.DSimp.Config.locals : Lean.Meta.DSimp.Config → Bool
-- Mathlib.Data.Finmap
Finmap.mem_of_lookup_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s : Finmap β},
  Finmap.lookup a s = some b → a ∈ s
-- Mathlib.Topology.Constructions
/-- **Alias** of `Pi.continuous_domRestrict_apply`. -/
Pi.continuous_restrict_apply : ∀ {X : Type u} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] (s : Set X) {f : X → Z},
  Continuous f → Continuous (s.domRestrict f)
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_ai_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.AC.Expr) (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_ai_cert lhs rhs lhs' rhs' = (lhs.toSeq.erase0.beq' lhs').and' (rhs.toSeq.erase0.beq' rhs')
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_lt : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b c : CauSeq α abs},
  a < c → b < c → a ⊔ b < c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).get? k = if t₂.contains k = true then none else t₁.get? k
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.WithBot.completeLattice : {α : Type u_5} → [ConditionallyCompleteLattice α] → CompleteLattice (WithTop (WithBot α))
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- If `𝒰` is an open cover of `X` that is locally directed, `X` is
the colimit of the components of `𝒰`.  -/
AlgebraicGeometry.Scheme.OpenCover.isColimitCoconeOfLocallyDirected : {X : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        CategoryTheory.Limits.IsColimit (AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected 𝒰)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.inj.inj : ∀ {thm thm_1 : Lean.Meta.Grind.InjectiveTheorem},
  Lean.Meta.Grind.Entry.inj thm = Lean.Meta.Grind.Entry.inj thm_1 → thm = thm_1
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.finrank_le_of_le_left : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [FiniteDimensional (↥F) L], F ≤ E → Module.finrank (↥E) L ≤ Module.finrank (↥F) L
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.PreInstance.assignment : Lean.Meta.Grind.PreInstance → Array Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.ext_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v}, p.support = q.support → p = q
-- Init.Data.Vector.Attach
Vector.count_attach : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Vector α n} {a : { x // x ∈ xs }},
  Vector.count a xs.attach = Vector.count (↑a) xs
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_iUnion : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_2} (s : ι → Set G),
  Subgroup.closure (⋃ i, s i) = ⨆ i, Subgroup.closure (s i)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.braiding_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t)
  {Z : C} (h : (CategoryTheory.Limits.pair Y X).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom
      (CategoryTheory.CategoryStruct.comp t.fst h) =
    CategoryTheory.CategoryStruct.comp s.snd h
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.injOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  Set.InjOn (↑e) e.source
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.Smooth.stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => RingHom.Smooth
-- Mathlib.RingTheory.Localization.Rat
Rat.associated_num_den : ∀ (q : ℚ), Associated (IsFractionRing.num ℤ q) q.num ∧ Associated ↑(IsFractionRing.den ℤ q) ↑q.den
-- Mathlib.Analysis.Normed.Ring.Int
Int.nnnorm_coe_units : ∀ (e : ℤˣ), ‖↑e‖₊ = 1
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.reindex_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {J' : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [inst_3 : F.Final],
  (P.reindex F).ι = F.whiskerLeft P.ι
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.NoetherianSpace.discrete : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] [T2Space α], DiscreteTopology α
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.edist_lt_mul_of_lt : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
  {x y : α} {r : ENNReal}, LipschitzWith K f → K ≠ 0 → edist x y < r → edist (f x) (f y) < ↑K * r
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess.0.Finset.orderEmbOfFinWithBot_of_ne_zero : ∀ {T : Type u_1} [inst : LinearOrder T] (I : Finset T) [inst_1 : Bot T] (i : Fin (I.card + 1)) (hi : i ≠ 0),
  Finset.orderEmbOfFinWithBot✝ I i = (I.orderEmbOfFin ⋯) (i.pred hi)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_toWalk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk.reverse = ⋯.toWalk
-- Mathlib.Combinatorics.KatonaCircle
/-- Decompose a numbering of which `s` is a prefix into a numbering of `s` and a numbering on `sᶜ`.
 -/
Numbering.prefixedEquiv : {X : Type u_1} →
  [inst : Fintype X] →
    [inst_1 : DecidableEq X] → (s : Finset X) → ↥(Numbering.prefixed s) ≃ Numbering ↥s × Numbering ↥sᶜ
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of a measurable function is smaller than its integral,
while avoiding a null set.  -/
MeasureTheory.exists_notMem_null_le_lintegral : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ENNReal}
  [MeasureTheory.IsProbabilityMeasure μ], AEMeasurable f μ → μ N = 0 → ∃ x ∉ N, f x ≤ ∫⁻ (a : α), f a ∂μ
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `AddEquivClass F A B` states that `F` is a type of addition-preserving morphisms.
You should extend this class when you extend `AddEquiv`.  -/
AddEquivClass : (F : Type u_9) → (A : outParam (Type u_10)) → (B : outParam (Type u_11)) → [Add A] → [Add B] → [EquivLike F A B] → Prop
-- Init.Data.Iterators.Basic
/-- Asserts that an iterator `it'` could plausibly produce `it'` as a successor iterator after
finitely many steps. This relation is reflexive.
 -/
Std.Iter.IsPlausibleIndirectSuccessorOf : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → Std.Iter β → Prop
-- Batteries.Data.MLList.Basic
/-- Repeatedly apply a function `f : α → m (α × List β)` to an initial `a : α`,
accumulating the elements of the resulting `List β` as a single monadic lazy list.

(This variant allows starting with a specified `List β` of elements, as well. ) -/
MLList.fixlWith : {m : Type u → Type u} → [Monad m] → {α β : Type u} → (α → m (α × List β)) → α → List β → MLList m β
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.exists_eq_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Sieve X),
  ∃ I Y f, R = CategoryTheory.Sieve.ofArrows Y f
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `L` and `M` are both perfect closures of `K`, then there is a ring isomorphism `L ≃+* M`.
This is similar to `IsAlgClosure.equiv` and `IsSepClosure.equiv`.  -/
IsPerfectClosure.equiv : {K : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing K] →
        [inst_1 : CommRing L] →
          [inst_2 : CommRing M] →
            (i : K →+* L) →
              (j : K →+* M) →
                (p : ℕ) →
                  [inst_3 : ExpChar M p] →
                    [ExpChar K p] →
                      [inst_5 : ExpChar L p] →
                        [inst_6 : PerfectRing L p] →
                          [IsPerfectClosure i p] → [inst_8 : PerfectRing M p] → [IsPerfectClosure j p] → L ≃+* M
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.linearMap_repr_symm_apply : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (a : ι₂ × ι₁ →₀ R),
  (b₁.linearMap b₂).repr.symm a = (Matrix.toLin b₁ b₂) ((Finsupp.linearCombination R ⇑(Matrix.stdBasis R ι₂ ι₁)) a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insertMany_list_singleton : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {k : α} {v : β},
  t.insertMany [(k, v)] = t.insert k v
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMonoidMorphism.contMDiff_toFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {H' : Type u_5} [inst_4 : TopologicalSpace H']
  {E' : Type u_6} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_8} [inst_7 : TopologicalSpace G]
  [inst_8 : ChartedSpace H G] [inst_9 : Monoid G] {G' : Type u_9} [inst_10 : TopologicalSpace G']
  [inst_11 : ChartedSpace H' G'] [inst_12 : Monoid G'] (self : ContMDiffMonoidMorphism I I' n G G'),
  ContMDiff I I' n (↑self.toMonoidHom).toFun
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Iio' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Iic a) → Filter.Tendsto f Filter.atBot Filter.atTop → Set.Ioi (f a) ⊆ f '' Set.Iio a
-- Mathlib.Topology.ContinuousMap.Polynomial
Polynomial.toContinuousMap_X_eq_id : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R],
  Polynomial.X.toContinuousMap = ContinuousMap.id R
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.ofList_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, Std.ExtDHashMap.ofList l = ∅ ↔ l = []
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.mk : {𝕜 : 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] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            (toFun : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) →
                                              IsCovariantDerivativeOn F toFun → CovariantDerivative I F V
-- Mathlib.Data.Prod.Basic
Prod.Lex.refl_right : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Refl s] (x : α × β), Prod.Lex r s x x