mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The underlying object associated to an algebra.  -/
CategoryTheory.Monad.Algebra.A : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {T : CategoryTheory.Monad C} → T.Algebra → C
-- Lean.Language.Basic
Lean.Language.DynamicSnapshot.mk : Dynamic → Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree → Lean.Language.DynamicSnapshot
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `rgStart` is the `Position` where the deprecated declaration starts.  -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo.rgStart : Mathlib.Tactic.DeprecationInfo✝ → Lean.Position
-- Std.Do.PostCond
Std.Do.ExceptConds.and.eq_2 : ∀ (σ : Type u) (ps_2 : Std.Do.PostShape) (x_2 y_2 : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps_2)),
  (x_2 ∧ₑ y_2) = (x_2 ∧ₑ y_2)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ⊤)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp U.toSpecΓ
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.homOfLE ⋯).op))
        h) =
    CategoryTheory.CategoryStruct.comp U.ι (CategoryTheory.CategoryStruct.comp X.toSpecΓ h)
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.LocalTimeType.mk.injEq : ∀ (gmtOffset : ℤ) (isDst : Bool) (abbreviationIndex : UInt8) (gmtOffset_1 : ℤ) (isDst_1 : Bool)
  (abbreviationIndex_1 : UInt8),
  ({ gmtOffset := gmtOffset, isDst := isDst, abbreviationIndex := abbreviationIndex } =
      { gmtOffset := gmtOffset_1, isDst := isDst_1, abbreviationIndex := abbreviationIndex_1 }) =
    (gmtOffset = gmtOffset_1 ∧ isDst = isDst_1 ∧ abbreviationIndex = abbreviationIndex_1)
-- Mathlib.Data.Nat.Bits
Nat.bitCasesOn_bit1 : ∀ {motive : ℕ → Sort u} (H : (b : Bool) → (n : ℕ) → motive (Nat.bit b n)) (n : ℕ),
  Nat.bitCasesOn (2 * n + 1) H = H true n
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateIsSharedImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Init.Data.List.Lemmas
List.filter_eq_nil_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = [] ↔ ∀ a ∈ l, ¬p a = true
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle**: if `f : E → F` is complex differentiable in a neighborhood of `c`
and the norm `‖f z‖` has a local maximum at `c`, then `f` is locally constant in a neighborhood
of `c`.  -/
Complex.eventually_eq_of_isLocalMax_norm : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [StrictConvexSpace ℝ F] {f : E → F} {c : E},
  (∀ᶠ (z : E) in nhds c, DifferentiableAt ℂ f z) → IsLocalMax (norm ∘ f) c → ∀ᶠ (y : E) in nhds c, f y = f c
-- Mathlib.Topology.EMetricSpace.Defs
EMetricSpace.eq_of_edist_eq_zero : ∀ {α : Type u} [self : EMetricSpace α] {x y : α}, edist x y = 0 → x = y
-- Init.Prelude
/-- The length of a list.

This is a tail-recursive version of `List.length`, used to implement `List.length` without running
out of stack space.

Examples:
 * `([] : List String).lengthTR = 0`
 * `["green", "brown"].lengthTR = 2`
 -/
List.lengthTR : {α : Type u_1} → List α → ℕ
-- Mathlib.Topology.MetricSpace.Gluing
Metric.glueDist.eq_2 : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x_2 y : Y), Metric.glueDist Φ Ψ ε (Sum.inr x_2) (Sum.inr y) = dist x_2 y
-- Init.Data.Vector.Find
Vector.find?_flatMap : ∀ {α : Type u_1} {n : ℕ} {β : Type} {m : ℕ} {xs : Vector α n} {f : α → Vector β m} {p : β → Bool},
  Vector.find? p (xs.flatMap f) = Vector.findSome? (fun x => Vector.find? p (f x)) xs
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, k ∉ m₂ → (m₁ \ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.MeasureTheory.Integral.MeanInequalities
_private.Mathlib.MeasureTheory.Integral.MeanInequalities.0.ENNReal.lintegral_Lp_add_le_aux : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → ENNReal},
      AEMeasurable f μ →
        AEMeasurable g μ →
          ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0 →
            ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤ →
              (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
                (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.reuse.sizeOf_spec : ∀ (x : Lean.IR.VarId) (i : Lean.IR.CtorInfo) (updtHeader : Bool) (ys : Array Lean.IR.Arg),
  sizeOf (Lean.IR.Expr.reuse x i updtHeader ys) = 1 + sizeOf x + sizeOf i + sizeOf updtHeader + sizeOf ys
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mapRange.linearEquiv_trans : ∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β : ι → Type u_7} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → AddCommMonoid (β₁ i)]
  [inst_3 : (i : ι) → AddCommMonoid (β₂ i)] [inst_4 : (i : ι) → Module R (β i)] [inst_5 : (i : ι) → Module R (β₁ i)]
  [inst_6 : (i : ι) → Module R (β₂ i)] (f : (i : ι) → β i ≃ₗ[R] β₁ i) (f₂ : (i : ι) → β₁ i ≃ₗ[R] β₂ i),
  (DFinsupp.mapRange.linearEquiv fun i => f i ≪≫ₗ f₂ i) =
    DFinsupp.mapRange.linearEquiv f ≪≫ₗ DFinsupp.mapRange.linearEquiv f₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.mul_star_le_algebraMap_norm_sq : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A},
  a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
-- Mathlib.CategoryTheory.Category.Bipointed
pointedToBipointedCompBipointedToPointedFst_hom_app_toFun : ∀ (X : Pointed) (a : ((pointedToBipointed.comp bipointedToPointedFst).obj X).X),
  (pointedToBipointedCompBipointedToPointedFst.hom.app X).toFun a = a
-- Mathlib.Algebra.Homology.ExactSequence
/-- `F : ComposableArrows C n` is a complex if all compositions of
two consecutive arrows are zero.  -/
CategoryTheory.ComposableArrows.IsComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → {n : ℕ} → CategoryTheory.ComposableArrows C n → Prop
-- Mathlib.Topology.Spectral.Prespectral
PrespectralSpace.isTopologicalBasis : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : PrespectralSpace X],
  TopologicalSpace.IsTopologicalBasis {U | IsOpen U ∧ IsCompact U}
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The codomain of a 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.AtomIso.tgt : Mathlib.Tactic.BicategoryLike.AtomIso → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.LinearAlgebra.Matrix.Block
/-- `M` is upper triangular: entries below the diagonal vanish.  -/
Matrix.IsUpperTriangular : {m : Type u_3} → {R : Type v} → [Zero R] → [LT m] → Matrix m m R → Prop
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- Equality of linear maps out of an adic completion can be checked on Cauchy sequences.  -/
AdicCompletion.map_ext' : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {T : Type u_5} [inst_3 : AddCommGroup T] [inst_4 : Module (AdicCompletion I R) T]
  {f g : AdicCompletion I M →ₗ[AdicCompletion I R] T},
  (∀ (a : AdicCompletion.AdicCauchySequence I M), f ((AdicCompletion.mk I M) a) = g ((AdicCompletion.mk I M) a)) → f = g
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.centerToMulOpposite.eq_1 : ∀ (G : Type u_1) [inst : Group G], Subgroup.centerToMulOpposite G = Submonoid.centerToMulOpposite
-- Lean.Meta.PPBinder
/-- Pretty-prints a free variable and its type as a binder,
using the appropriate brackets given its `BinderInfo`. Example output: `{α : Type}`.

Returns `none` for let decls.
 -/
Lean.FVarId.ppAsBinder : Lean.FVarId → Lean.MetaM (Option Lean.MessageData)
-- Mathlib.Topology.Algebra.UniformConvergence
/-- If `G` is a uniform additive group,
then `α →ᵤ G` is a uniform additive group as well.  -/
instIsUniformAddGroupUniformFun : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G],
  IsUniformAddGroup (UniformFun α G)
-- Mathlib.Data.List.Shortlex
/-- **Alias** of the forward direction of `List.shortlex_cons_iff`. -/
List.Shortlex.of_cons : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] {a : α} {s t : List α},
  List.Shortlex r (a :: s) (a :: t) → List.Shortlex r s t
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.mvarId.sizeOf_spec : ∀ (mvarId : Lean.MVarId), sizeOf (Aesop.EqualUpToIds.MVarValue.mvarId mvarId) = 1 + sizeOf mvarId
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.zoom_ins : ∀ {α : Type u_1} {v : α} {path : RBTree.RBNode.Path α} {t' : RBTree.RBNode α} {path' : RBTree.RBNode.Path α}
  {t : RBTree.RBNode α} {cmp : α → α → Ordering},
  RBTree.RBNode.zoom (cmp v) t path = (t', path') →
    path.ins (RBTree.RBNode.ins cmp v t) = path'.ins (RBTree.RBNode.setRoot v t')
-- Init.Data.Bool
Bool.true_eq_false : (true = false) = False
-- Mathlib.Algebra.GroupWithZero.Nat
Nat.instCommMonoidWithZero : CommMonoidWithZero ℕ
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'_eq_foldlM.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.yield b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_1 b
-- Init.Data.List.Nat.Count
List.IsPrefix.le_count : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α},
  l₁ <+: l₂ → ∀ (a : α), List.count a l₂ - (l₂.length - l₁.length) ≤ List.count a l₁
-- Init.Data.Int.Order
Int.neg_lt_zero_iff : ∀ {a : ℤ}, -a < 0 ↔ 0 < a
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommMagmaOfMulHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → CommMagma (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] → CommMagma (DirectLimit G f)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sInter_sub_subset : ∀ {α : Type u_2} [inst : Sub α] (S : Set (Set α)) (t : Set α), ⋂₀ S - t ⊆ ⋂ s ∈ S, s - t
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ofEq_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂),
  (CategoryTheory.ShortComplex.Homotopy.ofEq h).h₃ = 0
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.symm_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A), P.symm.p₁ = P.p₀
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A category `HasFiniteBiproducts` if it has a biproduct for every finite family of objects in `C`
indexed by a finite type.  -/
CategoryTheory.Limits.HasFiniteBiproducts : (C : Type uC) → [inst : CategoryTheory.Category.{uC', uC} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go.eq_1 : ∀ (coeff : ℤ), Lean.Grind.Linarith.Expr.toPoly'.go coeff Lean.Grind.Linarith.Expr.zero = id
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (yx, x⁻¹)` is measure-preserving.
This is the function `S⁻¹RSR` in [Halmos, §59],
where `S` is the map `(x, y) ↦ (x, xy)` and `R` is `Prod.swap`.  -/
MeasureTheory.measurePreserving_mul_prod_inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Order.CompleteLattice.Basic
iInf_dite : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (p : ι → Prop) [inst_1 : DecidablePred p]
  (f : (i : ι) → p i → α) (g : (i : ι) → ¬p i → α),
  (⨅ i, if h : p i then f i h else g i h) = (⨅ i, ⨅ (h : p i), f i h) ⊓ ⨅ i, ⨅ (h : ¬p i), g i h
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.add_X_none : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C}
  (f : T ⟶ S), (E.add f).X none = T
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_smul_left : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X] (c : M) (x y : X),
  edist (c • x) (c • y) = edist x y
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertMany_list_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k : α}
  {v : β}, ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m [(k, v)]) = m.insert k v
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isNonarchimedean_norm : ∀ {R : Type u_4} [inst : SeminormedAddCommGroup R] [IsUltrametricDist R], IsNonarchimedean fun x => ‖x‖
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Definition of the divisor  -/
MeromorphicOn.divisor_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (U : Set 𝕜),
  (MeromorphicOn.divisor f U) z = if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Constant to use for terminfo. This is added to the `HandlerTrie`.  -/
Lean.Elab.ConfigEval.EvalConfigItemHandler.projFn? : Lean.Elab.ConfigEval.EvalConfigItemHandler → Option Lean.Name
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.flipHom_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P}
  (f : M →+ N →+ P), AddMonoidHom.flipHom f = f.flip
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.subtypeDomain_sum : ∀ {γ : Type w} {ι : Type u_1} {β : ι → Type v} [inst : (i : ι) → AddCommMonoid (β i)] {s : Finset γ}
  {h : γ → Π₀ (i : ι), β i} {p : ι → Prop} [inst_1 : DecidablePred p],
  DFinsupp.subtypeDomain p (∑ c ∈ s, h c) = ∑ c ∈ s, DFinsupp.subtypeDomain p (h c)
-- Mathlib.LinearAlgebra.Projection
/-- A linear endomorphism of a module `E` is a projection onto a submodule `p` if it sends every element
of `E` to `p` and fixes every element of `p`.
The definition allow more generally any `FunLike` type and not just linear maps, so that it can be
used for example with `ContinuousLinearMap` or `Matrix`.
 -/
LinearMap.IsProj : {S : Type u_5} →
  [inst : Semiring S] →
    {M : Type u_6} →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module S M] → Submodule S M → {F : Type u_7} → [FunLike F M M] → F → Prop
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
LinearMap.minpoly_toMatrix' : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (f : (n → R) →ₗ[R] n → R),
  minpoly R (LinearMap.toMatrix' f) = minpoly R f
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.ne_zero_of_mem_integerSet : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)), ↑a ≠ 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.takeWhile_takeWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, (s.takeWhile pat).takeWhile pat = s.takeWhile pat
-- Mathlib.CategoryTheory.Abelian.Ext
/-- Given a chain complex `X` and an object `Y`, this is the cochain complex
which in degree `i` consists of the module of morphisms `X.X i ⟶ Y`.  -/
ChainComplex.linearYonedaObj : {C : Type u_2} →
  [inst : CategoryTheory.Category.{v_1, u_2} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {α : Type u_3} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] →
            ChainComplex C α →
              (A : Type u_4) → [inst_4 : Ring A] → [CategoryTheory.Linear A C] → C → CochainComplex (ModuleCat A) α
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.loop.wf.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] {inst_2 : DecidableLT α} [inst_3 : DecidableLT α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w}
  [inst_6 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxo.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (upperBound : α)
  (acc acc_1 : γ),
  acc = acc_1 →
    ∀ (next next_1 : α) (e_next : next = next_1) (h : LargeEnough next)
      (f f_1 : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n { s // Pl out c s }),
      f = f_1 →
        Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f =
          Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl ⋯ LargeEnough hl upperBound acc_1 next_1 ⋯ f_1
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_equiv_eq_zero_iff_ne : ∀ {α β : Type u}, Cardinal.mk (α ≃ β) = 0 ↔ Cardinal.mk α ≠ Cardinal.mk β
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- In a complete normed algebra, the operation of inversion is `C^n`, for all `n`, at each
invertible element, as it is analytic.  -/
contDiffAt_ringInverse : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {R : Type u_3} [inst_1 : NormedRing R]
  [inst_2 : NormedAlgebra 𝕜 R] [HasSummableGeomSeries R] (x : Rˣ), ContDiffAt 𝕜 n Ring.inverse ↑x
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.fg_iff_mul_fg : ∀ {M : Type u_3} [inst : AddMonoid M] (P : AddSubmonoid M), P.FG ↔ (AddSubmonoid.toSubmonoid P).FG
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- The map `v ↦ v +ᵥ p` as an affine isometric equivalence between `V` and `P`.  -/
AffineIsometryEquiv.vaddConst : (𝕜 : Type u_1) →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] → [inst_3 : PseudoMetricSpace P] → [inst_4 : NormedAddTorsor V P] → P → V ≃ᵃⁱ[𝕜] P
-- Init.Data.Int.DivMod.Lemmas
Int.lt_mul_fdiv_self_add : ∀ {x k : ℤ}, 0 < k → x < k * x.fdiv k + k
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  {f : α → β → Option γ} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.toList (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl =
    List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsEulerian.even_degree_iff : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] {x u v : V} {p : G.Walk u v},
  p.IsEulerian → ∀ [inst : Fintype V] [inst_1 : DecidableRel G.Adj], Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctor_map_inclLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G)
  {c c' : C} (f : c ⟶ c'),
  (CategoryTheory.Join.mkFunctor F G α).map ((CategoryTheory.Join.inclLeft C D).map f) = F.map f
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupUnits_performRupCheck : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array ℕ),
  (f.performRupCheck rupHints).1.rupUnits = f.rupUnits
-- Std.Sat.AIG.RelabelNat
/-- The key property provided by `Inv2`, if we have `Inv2` at a certain index, then all atoms below
that index have been inserted into the `HashMap`.
 -/
Std.Sat.AIG.RelabelNat.State.Inv2.property : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (decls : Array (Std.Sat.AIG.Decl α)) (idx upper : ℕ)
  (map : Std.HashMap α ℕ) (hidx : idx < upper) (a : α) (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls upper map),
  decls[idx] = Std.Sat.AIG.Decl.atom a → ∃ n, map[a]? = some n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, l.contains k = false → (Std.ExtTreeMap.unitOfList l cmp).getKey? k = none
-- Mathlib.Data.Finset.Filter
Finset.filter_subset : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α), Finset.filter p s ⊆ s
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- Left multiplying by an invertible matrix does not change the rank  -/
Matrix.rank_mul_eq_right_of_isUnit_det : ∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] (A : Matrix m m R) (B : Matrix m n R), IsUnit A.det → (A * B).rank = B.rank
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of the forward direction of `ProbabilityTheory.iIndepFun_iff_finset`. -/
ProbabilityTheory.iIndepFun.restrict : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ → ∀ (s : Finset ι), ProbabilityTheory.iIndepFun (s.restrict f) μ
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.comap_mabs_atTop : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G],
  Filter.comap mabs Filter.atTop = Filter.atBot ⊔ Filter.atTop
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.algEquiv_symm_apply : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : CommSemiring R]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] (v : AbsoluteValue T S) (x : T),
  (WithAbs.algEquiv R v).symm x = WithAbs.toAbs v x
-- Mathlib.Data.Matrix.Block
/-- Let `p` pick out certain rows and `q` pick out certain columns of a matrix `M`. Then
`toBlock M p q` is the corresponding block matrix.  -/
Matrix.toBlock : {m : Type u_2} →
  {n : Type u_3} → {α : Type u_12} → Matrix m n α → (p : m → Prop) → (q : n → Prop) → Matrix { a // p a } { a // q a } α
-- Mathlib.Util.CountHeartbeats
/-- Run a command, optionally restoring the original state, and report just the number of heartbeats.
 -/
Mathlib.CountHeartbeats.elabForHeartbeats : Lean.TSyntax `command → optParam Bool true → Lean.Elab.Command.CommandElabM ℕ
-- Init.Data.List.MapIdx
List.mem_mapIdx : ∀ {β : Type u_1} {α : Type u_2} {f : ℕ → α → β} {b : β} {l : List α},
  b ∈ List.mapIdx f l ↔ ∃ i, ∃ (h : i < l.length), f i l[i] = b
-- Mathlib.Algebra.Category.Ring.Under.Property
/-- If `Q` is stable under finite products, the inclusion from the subcategory of `Under R` defined
by `Q` creates finite products.  -/
RingHom.HasFiniteProducts.createsFiniteProductsForget : {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} →
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) →
      (R : CommRingCat) →
        CategoryTheory.Limits.CreatesFiniteProducts
          (CategoryTheory.MorphismProperty.Under.forget
            (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q) ⊤ R)