mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.mk.inj : ∀ {H : Type u_2} {inst : TopologicalSpace H} {members : Set (OpenPartialHomeomorph H H)}
  {trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e.trans e' ∈ members}
  {symm' : ∀ e ∈ members, e.symm ∈ members} {id_mem' : OpenPartialHomeomorph.refl H ∈ members}
  {locality' :
    ∀ (e : OpenPartialHomeomorph H H), (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members}
  {mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members}
  {members_1 : Set (OpenPartialHomeomorph H H)}
  {trans'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ∈ members_1 → e.trans e' ∈ members_1}
  {symm'_1 : ∀ e ∈ members_1, e.symm ∈ members_1} {id_mem'_1 : OpenPartialHomeomorph.refl H ∈ members_1}
  {locality'_1 :
    ∀ (e : OpenPartialHomeomorph H H), (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ members_1) → e ∈ members_1}
  {mem_of_eqOnSource'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ≈ e → e' ∈ members_1},
  { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' } =
      { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
        mem_of_eqOnSource' := mem_of_eqOnSource'_1 } →
    members = members_1
-- Mathlib.Algebra.Homology.ShortComplex.Ab
/-- **Alias** of the forward direction of `CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker`. -/
CategoryTheory.ShortComplex.Exact.ab_range_eq_ker : ∀ {S : CategoryTheory.ShortComplex Ab}, S.Exact → (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Subtype.instMeasurableSingletonClass : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop} [MeasurableSingletonClass α],
  MeasurableSingletonClass (Subtype p)
-- Lean.Expr
Lean.Expr.Data.approxDepth : Lean.Expr.Data → UInt8
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.four_zero_nine_six_lt_exp_sixteen : 4096 < Real.exp 16
-- Batteries.Data.Fin.Fold
Fin.dfoldl_succ_last : ∀ {n : ℕ} {α : Fin (n + 1 + 1) → Type u_1} (f : (i : Fin (n + 1)) → α i.castSucc → α i.succ) (x : α 0),
  Fin.dfoldl (n + 1) α f x = f (Fin.last n) (Fin.dfoldl n (α ∘ Fin.castSucc) (fun x1 x2 => f x1.castSucc x2) x)
-- Mathlib.RingTheory.Ideal.Pure
/-- If `I` is pure, `I ^ 2 = I`. The converse holds if `I` is finitely generated, see
`Ideal.Pure.of_isIdempotentElem`.  -/
Ideal.isIdempotentElem_of_pure : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [I.Pure], IsIdempotentElem I
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.iff_formallyUnramified_and_smooth : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.Etale R A ↔ Algebra.FormallyUnramified R A ∧ Algebra.Smooth R A
-- Mathlib.Topology.Constructions.SumProd
Continuous.comp₂ : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {g : X × Y → Z},
  Continuous g → ∀ {e : W → X}, Continuous e → ∀ {f : W → Y}, Continuous f → Continuous fun w => g (e w, f w)
-- Mathlib.Order.UpperLower.Relative
isRelLowerSet_self : ∀ {α : Type u_1} {s : Set α} [inst : LE α], IsRelLowerSet s fun x => x ∈ s
-- Mathlib.RingTheory.Localization.Module
span_eq_top_localization_localization : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [IsLocalization S Rₛ] {A : Type u_3} [inst_4 : CommSemiring A] [inst_5 : Algebra R A]
  (Aₛ : Type u_4) [inst_6 : CommSemiring Aₛ] [inst_7 : Algebra A Aₛ] [inst_8 : Algebra Rₛ Aₛ] [inst_9 : Algebra R Aₛ]
  [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {v : Set A},
  Submodule.span R v = ⊤ → Submodule.span Rₛ (⇑(algebraMap A Aₛ) '' v) = ⊤
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rco_ne_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m...n).toArray[i]! ≠ 0 ↔ i < (n - m).toNat ∧ m + ↑i ≠ 0
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.next : {α : Type u} → Std.Rxo.Iterator α → Option α
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose.eq_1 : ∀ (x : ℕ), x.multichoose 0 = 1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rcc_eq_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toArray[i]! = 0 ↔ (n + 1 - m).toNat ≤ i ∨ m + ↑i = 0
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionLiteralSupport.toJson : Lean.Lsp.CodeActionLiteralSupport → Lean.Json
-- Mathlib.Algebra.Group.Opposite
AddSemiconjBy.op : ∀ {α : Type u_1} [inst : Add α] {a x y : α},
  AddSemiconjBy a x y → AddSemiconjBy (AddOpposite.op a) (AddOpposite.op y) (AddOpposite.op x)
-- Std.Time.Zoned.Database.TzIf
/-- The GMT offset in seconds for this local time type.
 -/
Std.Time.TimeZone.TZif.LocalTimeType.gmtOffset : Std.Time.TimeZone.TZif.LocalTimeType → ℤ
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_right_le_mk_add : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk b ≤ ArchimedeanClass.mk a → ArchimedeanClass.mk b ≤ ArchimedeanClass.mk (a + b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toList_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp} {f : α → β → γ},
  Std.DTreeMap.Const.toList (Std.DTreeMap.map f t) = List.map (fun p => (p.1, f p.1 p.2)) (Std.DTreeMap.Const.toList t)
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The dual of a reflexive module is reflexive.  -/
Module.Dual.instIsReflecive : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.IsReflexive R M], Module.IsReflexive R (Module.Dual R M)
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_univ_singleton : ∀ {G : Type u_1} [inst : AddGroup G] {g : G}, AddSubgroup.IsComplement Set.univ {g}
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldr_eq_foldr_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {f : α → β → δ → δ}
  {init : δ}, Std.TreeMap.foldr f init t = List.foldr (fun a b => f a.1 a.2 b) init t.toList
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_eventuallyEq_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), ↑hf.localInverse.toPartialEquiv ∘ f =ᶠ[nhds x] id
-- Lean.Level
Lean.Level.PP.Result.offset.sizeOf_spec : ∀ (a : Lean.Level.PP.Result) (a_1 : ℕ), sizeOf (a.offset a_1) = 1 + sizeOf a + sizeOf a_1
-- Lean.Declaration
Lean.TheoremVal.mk.sizeOf_spec : ∀ (toConstantVal : Lean.ConstantVal) (value : Lean.Expr) (all : List Lean.Name),
  sizeOf { toConstantVal := toConstantVal, value := value, all := all } =
    1 + sizeOf toConstantVal + sizeOf value + sizeOf all
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.closure : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite X → M.IsRkFinite (M.closure X)
-- Mathlib.Algebra.Group.Commute.Hom
SemiconjBy.of_map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {a x y : M} [inst_2 : FunLike F M N]
  [MulHomClass F M N] {f : F}, Function.Injective ⇑f → SemiconjBy (f a) (f x) (f y) → SemiconjBy a x y
-- Std.Time.DateTime.WallTime
Std.Time.instOrdWallTime : Ord Std.Time.WallTime
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Directed.sequence.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match none with
    | none => h_1 ()
    | some a => h_2 a) =
    h_1 ()
-- Mathlib.Algebra.Module.Hom
AddMonoid.End.instDistribMulAction : {R : Type u_1} →
  {A : Type u_4} →
    [inst : Monoid R] → [inst_1 : AddCommMonoid A] → [DistribMulAction R A] → DistribMulAction R (AddMonoid.End A)
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.unifyEqs? : ℕ →
  Lean.MVarId →
    Lean.Meta.FVarSubst → optParam (Option Lean.Name) none → Lean.MetaM (Option (Lean.MVarId × Lean.Meta.FVarSubst))
-- Mathlib.LinearAlgebra.Multilinear.Basis
Fintype.ofFinite.congr_simp : ∀ (α : Type u_4) [inst : Finite α], Fintype.ofFinite α = Fintype.ofFinite α
-- Lean.Parser.Term
Lean.Parser.Term.matchDiscr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Prelude
/-- The `` `choice `` kind is used to represent ambiguous parse results.

The parser prioritizes longer matches over shorter ones, but there is not always a unique longest
match. All the parse results are saved, and the determination of which to use is deferred
until typing information is available.
 -/
Lean.choiceKind : Lean.SyntaxNodeKind
-- Mathlib.Algebra.Module.GradedModule
DirectSum.Gmodule.smulAddMonoidHom_apply_of_of : ∀ {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [inst : AddMonoid ιA] [inst_1 : VAdd ιA ιB]
  [inst_2 : (i : ιA) → AddCommMonoid (A i)] [inst_3 : (i : ιB) → AddCommMonoid (M i)] [inst_4 : DecidableEq ιA]
  [inst_5 : DecidableEq ιB] [inst_6 : GradedMonoid.GMonoid A] [inst_7 : DirectSum.Gmodule A M] {i : ιA} {j : ιB}
  (x : A i) (y : M j),
  ((DirectSum.Gmodule.smulAddMonoidHom A M) ((DirectSum.of A i) x)) ((DirectSum.of M j) y) =
    (DirectSum.of M (i +ᵥ j)) (GradedMonoid.GSMul.smul x y)
-- Mathlib.Combinatorics.Graph.Basic
/-- An edge `e` is incident to something if and only if `e` is in the edge set.  -/
Graph.edge_mem_iff_exists_isLink : ∀ {α : Type u_3} {β : Type u_4} (self : Graph α β) (e : β), e ∈ self.edgeSet ↔ ∃ x y, self.IsLink e x y
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIicIoi_apply_inl : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α} (a : ↑(Set.Iic x)), (OrderIso.sumLexIicIoi x) (toLex (Sum.inl a)) = ↑a
-- Lean.Compiler.IR.Basic
Lean.IR.Arg.var.inj : ∀ {id id_1 : Lean.IR.VarId}, Lean.IR.Arg.var id = Lean.IR.Arg.var id_1 → id = id_1
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_eq_mulEquivOfLocalizations : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P},
  (k.mulEquivOfLocalizations f).symm = f.mulEquivOfLocalizations k
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_3.eq_3 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → Sort u_1) (h_1 : (f : ℕ → ONote) → motive (Sum.inr f))
  (h_2 : (b' : ONote) → motive (Sum.inl (some b'))) (h_3 : Unit → motive (Sum.inl none)),
  (match Sum.inl none with
    | Sum.inr f => h_1 f
    | Sum.inl (some b') => h_2 b'
    | Sum.inl none => h_3 ()) =
    h_3 ()
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.filter f m) k fallback =
    ((Std.ExtDHashMap.Const.get? m k).pfilter fun x_2 h' => f (m.getKey k ⋯) x_2).getD fallback
-- Mathlib.RingTheory.RingHom.Surjective
_private.Mathlib.RingTheory.RingHom.Surjective.0.RingHom.termSurjective : Lean.ParserDescr
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.card_right : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G}, Subgroup.IsComplement (↑H) T → Nat.card ↑T = H.index
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.between_adj : ∀ {V : Type u_1} {v w : V} {G : SimpleGraph V} {s t : Set V},
  (SimpleGraph.between s t G).Adj v w ↔ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)
-- Mathlib.Algebra.Lie.Prod
LieHom.inl_eq_prod : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], LieHom.inl R L₁ L₂ = LieHom.id.prod 0
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.instHasGoodTensor₁₂OfHasGoodTensor₁₂TensorX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] {I : Type u_2} [inst_3 : AddMonoid I] {c : ComplexShape I}
  [inst_4 : c.TensorSigns] (K₁ K₂ K₃ : HomologicalComplex C c)
  [CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor K₁.X K₂.X K₃.X], K₁.HasGoodTensor₁₂ K₂ K₃
-- Mathlib.Algebra.Category.Grp.Shrink
/-- A functor `F : C ⥤ GrpCat.{w'}` factors through `GrpCat.{w}` if all the
monoids are `w`-small.  -/
GrpCat.shrinkFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C GrpCat) → [∀ (X : C), Small.{w, w'} ↑(F.obj X)] → CategoryTheory.Functor C GrpCat
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.GeneralTheorems.mk.inj : ∀ {theorems theorems_1 : Lean.Meta.RefinedDiscrTree Mathlib.Meta.FunProp.GeneralTheorem},
  { theorems := theorems } = { theorems := theorems_1 } → theorems = theorems_1
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ProbabilityTheory.IndepFun f g μ → ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.cartanSubalgebra'.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] (b : P.Base) [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  RootPairing.GeckConstruction.cartanSubalgebra' b =
    LieSubalgebra.comap (RootPairing.GeckConstruction.lieAlgebra b).incl
      (RootPairing.GeckConstruction.cartanSubalgebra b)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.IsRegularOfDegree.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : G.LocallyFinite] (d : ℕ), G.IsRegularOfDegree d = ∀ (v : V), G.degree v = d
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
exteriorPower.inner_ιMulti_ιMulti : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  (x y : Fin n → E),
  inner ℝ ((exteriorPower.ιMulti ℝ n) x) ((exteriorPower.ιMulti ℝ n) y) = (Matrix.of fun i j => inner ℝ (x j) (y i)).det
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.top_covering : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X}, S ∈ ⊤ X
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
Std.IterM.takeWhile.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] (P : β → Bool) (it : Std.IterM m β),
  Std.IterM.takeWhile P it = Std.IterM.takeWhileWithPostcondition (pure ∘ ULift.up ∘ P) it
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.isProtected : Lean.Elab.Modifiers → Bool
-- Init.Data.List.Basic
/-- Pairs each element of a list with its index, optionally starting from an index other than `0`.

`O(|l|)`.

Examples:
* `[a, b, c].zipIdx = [(a, 0), (b, 1), (c, 2)]`
* `[a, b, c].zipIdx 5 = [(a, 5), (b, 6), (c, 7)]`
 -/
List.zipIdx : {α : Type u} → List α → optParam ℕ 0 → List (α × ℕ)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.mulOneClass : {R : Type u} →
  {M : Type v} →
    [inst : Monoid R] →
      [inst_1 : AddMonoid M] → [DistribMulAction R M] → [DistribMulAction Rᵐᵒᵖ M] → MulOneClass (TrivSqZeroExt R M)
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In an additive unital magma with multiplication, squares are sums of squares
(see Mathlib.Algebra.Group.Even).
 -/
IsSquare.isSumSq : ∀ {R : Type u_1} [inst : AddZeroClass R] [inst_1 : Mul R] {x : R}, IsSquare x → IsSumSq x
-- Lean.Environment
/-- Compacted regions for all imported modules. Objects in compacted memory regions do no require any memory management.  -/
Lean.EnvironmentHeader.regions : Lean.EnvironmentHeader → Array Lean.CompactedRegion
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β},
  f₁ ≤ᶠ[l] f₂ → g₁ ≤ᶠ[l] g₂ → f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.mk.sizeOf_spec : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M] [inst_3 : SizeOf A]
  [inst_4 : SizeOf M] (toRelations : Module.Relations A) (toSolution : toRelations.Solution M)
  (toIsPresentation : toSolution.IsPresentation),
  sizeOf { toRelations := toRelations, toSolution := toSolution, toIsPresentation := toIsPresentation } =
    1 + sizeOf toRelations + sizeOf toSolution + sizeOf toIsPresentation
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_add_zpow_mem_Ioc : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G},
  1 < a → ∀ (b c : G), ∃! m, b * a ^ m ∈ Set.Ioc c (c * a)
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.fullSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      (Z : CategoryTheory.ObjectProperty C) → CategoryTheory.Preadditive Z.FullSubcategory
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.ofSubsingleton_val : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : Subsingleton S]
  (x : PUnit.{u_2 + 1}), (Algebra.SubmersivePresentation.ofSubsingleton R S).val x = 1
-- Mathlib.Algebra.Group.Hom.End
/-- See also `AddMonoid.End.natCast_def`.  -/
AddMonoid.End.natCast_apply : ∀ {M : Type uM} [inst : AddCommMonoid M] (n : ℕ) (m : M), ↑n m = n • m
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addSimproc : Lean.Name → Bool → Lean.Elab.Tactic.ElabSimpArgResult
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_inf : ∀ {M : Type u_2} [inst : Add M] (S₁ S₂ : AddSubsemigroup M), (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend_single_d : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {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] [inst_3 : DecidableEq ι] (e : c.Embedding c') (X : C) (i : ι)
  (j' k' : ι'), (((HomologicalComplex.single C c i).obj X).extend e).d j' k' = 0
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.flatMapAfterM.eq_1 : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [inst_2 : Std.Iterator α Id β]
  [inst_3 : Std.Iterator α₂ m γ] (f : β → m (Std.IterM m γ)) (it₁ : Std.Iter β) (it₂ : Option (Std.IterM m γ)),
  Std.Iter.flatMapAfterM f it₁ it₂ = Std.IterM.flatMapAfterM f (Std.Iter.mapWithPostcondition pure it₁) it₂
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lsum_apply : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid N] [inst_6 : Module R₂ N] {σ : R →+* R₂} [inst_7 : Module S N] [inst_8 : SMulCommClass R₂ S N]
  (f : α → M →ₛₗ[σ] N) (l : α →₀ M), ((Finsupp.lsum S) f) l = l.sum fun b => ⇑(f b)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.preconnected_induce_iff : ∀ {V : Type u} {G : SimpleGraph V} {s : Set V}, (SimpleGraph.induce s G).Preconnected ↔ (⊤.induce s).Preconnected
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.instIsKProjectiveCochainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (R : CategoryTheory.ProjectiveResolution X), R.cochainComplex.IsKProjective
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_empty : ∀ (α : Type u_2), Matroid.freeOn ∅ = Matroid.emptyOn α
-- Mathlib.Algebra.Order.Monovary
monovaryOn_inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < g i) → (MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.const.instIsZeroOrMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μβ : MeasureTheory.Measure β}
  [hμβ : MeasureTheory.IsZeroOrProbabilityMeasure μβ],
  ProbabilityTheory.IsZeroOrMarkovKernel (ProbabilityTheory.Kernel.const α μβ)
-- Std.Do.WP.Monad
Std.Do.Reader.instWPMonad : {ρ : Type u_1} → Std.Do.WPMonad (ReaderM ρ) (Std.Do.PostShape.arg ρ Std.Do.PostShape.pure)
-- Mathlib.Computability.Partrec
_private.Mathlib.Computability.Partrec.0.Nat.wf_lbp : ∀ (p : ℕ →. Bool), (∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom) → WellFounded (Nat.lbp✝ p)
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- The set of points smooth over a base, as a `Scheme.Opens`.  -/
AlgebraicGeometry.Scheme.Hom.smoothLocus : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [AlgebraicGeometry.LocallyOfFinitePresentation f] → X.Opens
-- Lean.Meta.Tactic.Grind.Types
/-- If `anchorRefs? := some anchorRefs`, then only local instances and case-splits in `anchorRefs`
are considered.
 -/
Lean.Meta.Grind.Context.anchorRefs? : Lean.Meta.Grind.Context → Option (Array Lean.Meta.Grind.AnchorRef)
-- Mathlib.Data.Finset.Dedup
Multiset.Nodup.toFinset_inj : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : Multiset α}, l.Nodup → l'.Nodup → l.toFinset = l'.toFinset → l = l'
-- Init.Data.List.Nat.Erase
List.set_getElem_succ_eraseIdx_succ : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : i + 1 < l.length), (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i
-- Lean.Widget.InteractiveDiagnostic
/-- Transform a Lean Message concerning the given text into an LSP Diagnostic.  -/
Lean.Widget.msgToInteractiveDiagnostic : Lean.FileMap → Lean.Message → Bool → BaseIO Lean.Widget.InteractiveDiagnostic
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `b₂` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.b₂ : {R : Type u} → [CommRing R] → WeierstrassCurve R → R
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the forward direction of `SimpleGraph.Walk.isTrail_rotate`. -/
SimpleGraph.Walk.IsTrail.of_rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v} (hu : u ∈ c.support),
  (c.rotate u hu).IsTrail → c.IsTrail
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.inv_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommGroup Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedAddMonoid Γ]
  [inst_3 : Field R] (a : Γ) (r : R), ((HahnSeries.single a) r)⁻¹ = (HahnSeries.single (-a)) r⁻¹
-- Init.Internal.Order.Basic
Lean.Order.implication_order_monotone_or : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] (f₁ f₂ : α → Lean.Order.ImplicationOrder),
  Lean.Order.monotone f₁ → Lean.Order.monotone f₂ → Lean.Order.monotone fun x => f₁ x ∨ f₂ x
-- Init.WFComputable
Acc.rec_eq_recC : @Acc.rec = @Acc.recC
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.eqToHom_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (h : C₁ = C₂) (n : ι), (CategoryTheory.eqToHom h).f n = CategoryTheory.eqToHom ⋯