mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.MetavarContext
/-- Given `toRevert` an array of free variables s.t. `lctx` contains their declarations,
return a new array of free variables that contains `toRevert` and all variables
in `lctx` that may depend on `toRevert`.

When `generalizeNondepLet := true` (the default), then the values of nondependent lets are not considered
when computing forward dependencies.

Remark: the result is sorted by `LocalDecl` indices.

Remark: We used to throw an `Exception.revertFailure` exception when an auxiliary declaration
had to be reversed. Recall that auxiliary declarations are created when compiling (mutually)
recursive definitions. The `revertFailure` due to auxiliary declaration dependency was originally
introduced in Lean3 to address issue <https://github.com/leanprover/lean/issues/1258>.

In Lean4, this solution is not satisfactory because all definitions/theorems are potentially
recursive. So, even a simple (incomplete) definition such as
```
variables {α : Type} in
def f (a : α) : List α :=
_
```
would trigger the `Exception.revertFailure` exception. In the definition above,
the elaborator creates the auxiliary definition `f : {α : Type} → List α`.
The `_` is elaborated as a new fresh variable `?m` that contains `α : Type`, `a : α`, and `f : α → List α` in its context,
When we try to create the lambda `fun {α : Type} (a : α) => ?m`, we first need to create
an auxiliary `?n` which does not contain `α` and `a` in its context. That is,
we create the metavariable `?n : {α : Type} → (a : α) → (f : α → List α) → List α`,
add the delayed assignment `?n #[l, a, f] := ?m`, and create the lambda
`fun {α : Type} (a : α) => ?n α a f`.

See `elimMVarDeps` for more information.

If we kept using the Lean3 approach, we would get the `Exception.revertFailure` exception because we are
reverting the auxiliary definition `f`.

Note that <https://github.com/leanprover/lean/issues/1258> is not an issue in Lean4 because
we have changed how we compile recursive definitions.
 -/
Lean.MetavarContext.MkBinding.collectForwardDeps : Lean.LocalContext → Array Lean.Expr → optParam Bool true → Lean.MetavarContext.MkBinding.M (Array Lean.Expr)
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.instIsRegularEpiEStrongEpiMonoFactorisation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsRegularEpi (CategoryTheory.Regular.strongEpiMonoFactorisation f).e
-- Mathlib.Topology.Separation.Hausdorff
SeparatedNhds.of_finite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {s t : Set X},
  s.Finite → t.Finite → Disjoint s t → SeparatedNhds s t
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.nil.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Batteries.BinomialHeap.Imp.Heap.nil = 1
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_apply_above : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {i j : Fin (n + 1)} (h : i < j) (x : α i) (p : (k : Fin n) → α (i.succAbove k)),
  i.insertNth x p j = ⋯ ▸ p (j.pred ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.bypass.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} (v_3 : V) (ha : G.Adj u v_3) (p : G.Walk v_3 v),
  (SimpleGraph.Walk.cons ha p).bypass =
    if hs : u ∈ p.bypass.support then p.bypass.dropUntil u hs else SimpleGraph.Walk.cons ha p.bypass
-- Mathlib.Probability.Moments.Covariance
/-- The covariance of the real-valued random variables `X` and `Y`
according to the volume measure.  -/
ProbabilityTheory.«termCov[_,_]» : Lean.ParserDescr
-- Mathlib.Data.ZMod.Basic
ZMod.ringEquivCongr_refl : ∀ (a : ℕ), ZMod.ringEquivCongr ⋯ = RingEquiv.refl (ZMod a)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_eq : ∀ {z : ℂ},
  (((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), ↑z.im * Complex.I ≠ (2 * ↑l + 1) * ↑Real.pi / 2) ∨
      (∃ k, ↑z.re = (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∃ l, ↑z.im * Complex.I = (2 * ↑l + 1) * ↑Real.pi / 2) →
    Complex.tan z =
      (Complex.tan ↑z.re + Complex.tanh ↑z.im * Complex.I) / (1 - Complex.tan ↑z.re * Complex.tanh ↑z.im * Complex.I)
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply' : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [inst_2 : NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial (ZMod p)}
  (hQ : Q ∈ RingOfIntegers.monicFactorsMod θ p),
  (↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩)).ramificationIdx ℤ =
    multiplicity Q (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.irreducible : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  Irreducible v.asIdeal
-- Mathlib.LinearAlgebra.AffineSpace.Basis
finsuppAffineCoords.eq_1 : ∀ (ι : Type u_1) (k : Type u_2) [inst : Ring k],
  finsuppAffineCoords ι k = AffineSubspace.comap (Finsupp.linearCombination k 1).toAffineMap (affineSpan k {1})
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.support_seq : ∀ {α : Type u_1} {β : Type u_2} (q : PMF (α → β)) (p : PMF α), (q.seq p).support = ⋃ f ∈ q.support, f '' p.support
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffAt_const : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {x : M} {n : WithTop ℕ∞}
  {c : M'}, ContMDiffAt I I' n (fun x => c) x
-- Std.Time.Time.Unit.Second
/-- Creates an `Second.Offset` from an integer.
 -/
Std.Time.Second.Offset.ofInt : ℤ → Std.Time.Second.Offset
-- Mathlib.Order.Filter.AtTopBot.Archimedean
tendsto_PNat_val_atTop_atTop : Filter.Tendsto PNat.val Filter.atTop Filter.atTop
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.kextract.match_3.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List (Sigma β) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (s : Sigma β) → (l : List (Sigma β)) → motive (s :: l)),
  (match [] with
    | [] => h_1 ()
    | s :: l => h_2 s l) =
    h_1 ()
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `goalsTargetedBy t` are the `MVarId`s before the `TacticInfo` `t` that "disappear" after it.
They should correspond to the goals in which the tactic `t` performs some action.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Lean.Elab.TacticInfo.goalsTargetedBy : Lean.Elab.TacticInfo → List Lean.MVarId
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.setOfPred_subset_eq_empty_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (S : (L.withConstants α).Theory),
  {p | S ⊆ ↑p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varsToConstants.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    {γ : Type u_4} →
      (motive : L.Term (γ ⊕ α) → Sort u_5) →
        (x : L.Term (γ ⊕ α)) →
          ((a : α) → motive (FirstOrder.Language.var (Sum.inr a))) →
            ((c : γ) → motive (FirstOrder.Language.var (Sum.inl c))) →
              ((l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term (γ ⊕ α)) → motive (FirstOrder.Language.func f ts)) →
                motive x
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.main : Lean.Expr → Lean.CollectLevelMVars.Visitor
-- Mathlib.Algebra.Order.Ring.Finset
Nat.cast_finsetSup' : ∀ {ι : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {s : Finset ι}
  (f : ι → ℕ) (hs : s.Nonempty), ↑(s.sup' hs f) = s.sup' hs fun i => ↑(f i)
-- Mathlib.Algebra.Order.SuccPred.TypeTags
Order.succ_ofAdd : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : SuccOrder X] (x : X),
  Order.succ (Multiplicative.ofAdd x) = Multiplicative.ofAdd (Order.succ x)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map'_comp_map' : ∀ {β : Type w} {α : Type w₂} {γ : Type w₃} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C}
  {g : β → C} {h : γ → C} [inst_1 : CategoryTheory.Limits.HasCoproduct f]
  [inst_2 : CategoryTheory.Limits.HasCoproduct g] [inst_3 : CategoryTheory.Limits.HasCoproduct h] (p : α → β)
  (p' : β → γ) (q : (a : α) → f a ⟶ g (p a)) (q' : (b : β) → g b ⟶ h (p' b)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map' p q) (CategoryTheory.Limits.Sigma.map' p' q') =
    CategoryTheory.Limits.Sigma.map' (p' ∘ p) fun a => CategoryTheory.CategoryStruct.comp (q a) (q' (p a))
-- Mathlib.Algebra.CharP.Lemmas
add_pow_eq_mul_pow_add_pow_div_expChar_of_commute : ∀ {R : Type u_1} [inst : Semiring R] {x y : R} (p n : ℕ) [hR : ExpChar R p],
  Commute x y → (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_ne_one : ∀ {x : ℝ}, ↑x ≠ 1 ↔ x ≠ 1
-- Mathlib.Topology.MetricSpace.MetricSeparated
/-- **Alias** of the reverse direction of `Metric.AreSeparated.finite_iUnion_left_iff`. -/
Metric.AreSeparated.finite_iUnion_left : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ι : Type u_3} {I : Set ι},
  I.Finite →
    ∀ {s : ι → Set X} {t : Set X}, (∀ i ∈ I, Metric.AreSeparated (s i) t) → Metric.AreSeparated (⋃ i ∈ I, s i) t
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_le_mul_of_nonpos_left : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b c : R}, a ≤ b → c ≤ 0 → c * b ≤ c * a
-- Lean.Elab.Exception
Lean.Elab.throwAbortCommand : {α : Type u_1} → {m : Type u_1 → Type u_2} → [MonadExcept Lean.Exception m] → m α
-- Mathlib.RingTheory.Bialgebra.Basic
/-- The comultiplication on a bialgebra preserves multiplication. This is written in
a rather obscure way: it says that two bilinear maps `A →ₗ[R] A →ₗ[R] (A ⊗[R] A)`
are equal. The corresponding equal linear maps `A ⊗[R] A →ₗ[R] A ⊗[R] A`
are firstly multiplication followed by `comul`, and secondly `comul ⊗ comul` followed
by multiplication on `A ⊗[R] A`.

See `Bialgebra.mk'` for a constructor for bialgebras which uses the more familiar
but mathematically equivalent `comul (a * b) = comul a * comul b`.  -/
Bialgebra.mul_compr₂_comul : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : Bialgebra R A],
  (LinearMap.mul R A).compr₂ CoalgebraStruct.comul =
    (LinearMap.mul R (TensorProduct R A A)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul
-- Mathlib.CategoryTheory.Sites.Continuous
/-- The image of a 1-pre-hypercover by a functor.  -/
CategoryTheory.PreOneHypercover.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : C} →
          CategoryTheory.PreOneHypercover X →
            (F : CategoryTheory.Functor C D) → CategoryTheory.PreOneHypercover (F.obj X)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.CompatibleRing.toStructure : {R : Type u_2} →
  {inst : Add R} →
    {inst_1 : Mul R} →
      {inst_2 : Neg R} →
        {inst_3 : One R} →
          {inst_4 : Zero R} → [self : FirstOrder.Ring.CompatibleRing R] → FirstOrder.Language.ring.Structure R
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The canonical map from the unit group of `A` to the units of the residue field of `A`.  -/
ValuationSubring.unitGroupToResidueFieldUnits : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → ↥A.unitGroup →* (IsLocalRing.ResidueField ↥A)ˣ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.le_maxKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k km : α} (hc : t.contains k = true), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Lean.Data.PersistentArray
Lean.PersistentArray.pop : {α : Type u} → Lean.PersistentArray α → Lean.PersistentArray α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_of_contains_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, (m.erase k).contains a = true → m.contains a = true
-- Mathlib.Data.Int.Init
Int.neg_succ : ∀ (a : ℤ), -a.succ = (-a).pred
-- Init.Data.Option.Lemmas
Option.isNone_bind : ∀ {α : Type u_1} {β : Type u_2} (x : Option α) (f : α → Option β),
  (x.bind f).isNone = Option.all (fun x => (f x).isNone) x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core.inj : ∀ {a b : Lean.Expr} {p₁ p₂ : Int.Internal.Linear.Poly} {a_1 b_1 : Lean.Expr} {p₁_1 p₂_1 : Int.Internal.Linear.Poly},
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core a b p₁ p₂ =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core a_1 b_1 p₁_1 p₂_1 →
    a = a_1 ∧ b = b_1 ∧ p₁ = p₁_1 ∧ p₂ = p₂_1
-- Init.Grind.Lemmas
Lean.Grind.intro_with_eq : (p p' : Prop) → (q : Sort u) → p = p' → (p' → q) → p → q
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.p_comm_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (f : P.Hom Q) {Z : C} (h : Q.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f.f h) =
    CategoryTheory.CategoryStruct.comp f.f (CategoryTheory.CategoryStruct.comp Q.p h)
-- Lean.Environment
_private.Lean.Environment.0.Lean.instTypeNameAsyncConsts : TypeName Lean.AsyncConsts✝
-- Mathlib.Tactic.Widget.SelectInsertParamsClass
/-- Structures providing parameters for a Select and insert widget.  -/
SelectInsertParamsClass : Type → Type
-- Mathlib.Logic.Nontrivial.Defs
NeZero.nontrivial : ∀ {α : Type u_3} [inst : Zero α] (a : α) [NeZero a], Nontrivial α
-- Mathlib.Topology.Constructions.SumProd
closure_prod_eq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
  closure (s ×ˢ t) = closure s ×ˢ closure t
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.union_eq_sdiff_union_sdiff_union_inter`. -/
Set.union_eq_diff_union_diff_union_inter : ∀ {α : Type u_1} (s t : Set α), s ∪ t = s \ t ∪ t \ s ∪ s ∩ t
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_iUnion_le`. -/
EMetric.hausdorffEdist_iUnion_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ι : Sort u_2} {s t : ι → Set α},
  Metric.hausdorffEDist (⋃ i, s i) (⋃ i, t i) ≤ ⨆ i, Metric.hausdorffEDist (s i) (t i)
-- Lean.Environment
Lean.PersistentEnvExtension.addEntryFn : {α β σ : Type} → Lean.PersistentEnvExtension α β σ → σ → β → σ
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiff.neg_section : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s : (x : M) → V x},
  (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, s x⟩) →
    ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, (-s) x⟩
-- Std.Data.ExtDHashMap.Lemmas
_private.Std.Data.ExtDHashMap.Lemmas.0.Std.ExtDHashMap.insertMany_list_mk : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m : Std.DHashMap α β} {l : List ((a : α) × β a)},
  (Std.ExtDHashMap.mk m).insertMany l = Std.ExtDHashMap.mk (m.insertMany l)
-- Mathlib.RingTheory.Algebraic.Integral
Polynomial.exists_dvd_map_of_isAlgebraic : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] {f : Polynomial S},
  f ≠ 0 → ∃ g, g ≠ 0 ∧ f ∣ Polynomial.map (algebraMap R S) g
-- Mathlib.CategoryTheory.Action.Basic
Action.instFaithfulForget : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G],
  (Action.forget V G).Faithful
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.hasWeakLimit_iff_of_iso : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  CategoryTheory.Limits.HasWeakLimit F ↔ CategoryTheory.Limits.HasWeakLimit G
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k k' fallback : α},
  cmp k k' = Ordering.eq → t.getD k fallback = t.getD k' fallback
-- Init.Data.List.Basic
List.decidableBAll : {α : Type u} → (p : α → Prop) → [DecidablePred p] → (l : List α) → Decidable (∀ x ∈ l, p x)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_mono : ∀ {α : Type u_1} (M : Matroid α), Monotone M.eRk
-- Init.Data.Array.Lemmas
Array.foldlM_pure : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] [LawfulMonad m] {f : β → α → β} {b : β}
  {xs : Array α} {start stop : ℕ},
  Array.foldlM (fun x1 x2 => pure (f x1 x2)) b xs start stop = pure (Array.foldl f b xs start stop)
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.exact_of_δlast : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} (S : CategoryTheory.ComposableArrows C (n + 2)),
  S.δlast.Exact →
    (CategoryTheory.ComposableArrows.mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact → S.Exact
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {x y : Cᴹᵒᵖ} {f g : x ⟶ y}, f.unmop = g.unmop → f = g
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_id : ∀ {M : Type u_1} [inst : AddCommGroup M] {R : Type u_3} [inst_1 : Ring R] [inst_2 : Module R M] [StrongRankCondition R],
  LinearMap.id.index = 0
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsPivotedBy.mk : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] [inst_1 : LT m] [inst_2 : LT n] {A : Matrix m n R}
  {l : m → WithTop n},
  A.IsRowEchelon → (∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0) → A.IsPivotedBy l
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.objEquiv_symm_δ_mem_horn_iff : ∀ {n : ℕ} (i j : Fin (n + 2)),
  SSet.stdSimplex.objEquiv.symm (SimplexCategory.δ i) ∈ (SSet.horn (n + 1) j).obj (Opposite.op { len := n }) ↔ i ≠ j
-- Mathlib.Analysis.Calculus.Deriv.Slope
HasDerivAt.tendsto_slope_zero_left : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_3 : Preorder 𝕜],
  HasDerivAt f f' x → Filter.Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (nhdsWithin 0 (Set.Iio 0)) (nhds f')
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.rangeRestrict_surjective : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S),
  Function.Surjective ⇑f.rangeRestrict
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.algebra_section_section_basicOpen : {X : AlgebraicGeometry.Scheme} →
  {U : X.Opens} →
    (f : ↑(X.presheaf.obj (Opposite.op U))) →
      Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr' : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x₁ x₂ : ↥X} (e : x₁ = x₂),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x₁)
      (AlgebraicGeometry.Scheme.residueFieldCongr e).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom
      (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x₂)
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.page.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (self self_1 : CategoryTheory.SpectralSequence C c r₀),
  self = self_1 → ∀ (r : ℤ) (hr : r₀ ≤ r), self.page r hr = self_1.page r hr
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist.match_1.eq_2 : ∀ {X : Type u_1} {Y : Type u_2} (motive : X ⊕ Y → X ⊕ Y → Sort u_3) (x y : Y)
  (h_1 : (x y : X) → motive (Sum.inl x) (Sum.inl y)) (h_2 : (x y : Y) → motive (Sum.inr x) (Sum.inr y))
  (h_3 : (x : X) → (y : Y) → motive (Sum.inl x) (Sum.inr y)) (h_4 : (x : Y) → (y : X) → motive (Sum.inr x) (Sum.inl y)),
  (match Sum.inr x, Sum.inr y with
    | Sum.inl x, Sum.inl y => h_1 x y
    | Sum.inr x, Sum.inr y => h_2 x y
    | Sum.inl x, Sum.inr y => h_3 x y
    | Sum.inr x, Sum.inl y => h_4 x y) =
    h_2 x y
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A variant of `Sieve.toFunctor` with universe lifting.  -/
CategoryTheory.Sieve.toUliftFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (S : CategoryTheory.Sieve X) →
        {Y : C} → (f : Y ⟶ X) → S.arrows f → (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj Y ⟶ S.uliftFunctor)
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.of_commSq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S),
  CategoryTheory.CommSq (p.map φ) (CategoryTheory.eqToHom ha) (CategoryTheory.eqToHom hb) f → p.IsHomLift f φ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.le_inv_mul_iff : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a b : M}, a ≤ ↑u⁻¹ * b ↔ ↑u * a ≤ b
-- Mathlib.Order.RelSeries
/-- The longest relational series when a relation is finite dimensional  -/
RelSeries.longestOf : {α : Type u_1} → (r : SetRel α α) → [r.FiniteDimensional] → RelSeries r
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.instFunLikeSubtypeForallVMemSubmoduleCoboundaries₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → {A : Rep.{max u u_1, u, u} k G} → FunLike (↥(groupCohomology.coboundaries₁ A)) G ↑A
-- Init.Prelude
/-- The underlying Unicode scalar value as a `UInt32`.  -/
Char.val : Char → UInt32
-- Mathlib.Order.KrullDimension
Order.krullDim_nat : Order.krullDim ℕ = ⊤
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight_mono : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [inst_1 : I.IsPrime] [inst_2 : J.IsPrime],
  I ≤ J → Ideal.primeHeight✝ I ≤ Ideal.primeHeight✝ J
-- Mathlib.Data.Rat.Lemmas
Rat.mul_self_num : ∀ (q : ℚ), (q * q).num = q.num * q.num
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {X Y : CategoryTheory.Limits.Cocone F.unop} (f : X ⟶ Y),
  CategoryTheory.Limits.coconeUnopOfConeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }