mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal],
  F.mapAddGrp =
    { obj := fun A => { X := F.obj A.X, addGrp := CategoryTheory.Functor.addGrpObjObj },
      map := fun {X Y} f => CategoryTheory.AddGrp.homMk' (F.mapAddMon.map f.hom), map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Analysis.Normed.Operator.Extend
LinearMap.compLeftInverse.eq_1 : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : DivisionRing 𝕜]
  [inst_1 : DivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : AddCommGroup E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : SeminormedAddCommGroup Eₗ] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ F] [inst_7 : Module 𝕜 Eₗ]
  (f : E →ₛₗ[σ₁₂] F) (g : E →ₗ[𝕜] Eₗ),
  f.compLeftInverse g =
    if h : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖ then
      (g.ker.liftQ f ⋯ ∘ₛₗ ↑g.quotKerEquivRange.symm).mkContinuousOfExistsBound ⋯
    else 0
-- Std.Sat.CNF.Literal
Std.Sat.Literal.negate.eq_1 : ∀ {α : Type u_1} (l : Std.Sat.Literal α), l.negate = (l.1, !l.2)
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- If two additive homomorphisms from `R[M]` are equal on each `single r m`,
then they are equal.  -/
MonoidAlgebra.addMonoidHom_ext : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddZeroClass N]
  ⦃f g : MonoidAlgebra R M →+ N⦄,
  (∀ (m : M) (r : R), f (MonoidAlgebra.single m r) = g (MonoidAlgebra.single m r)) → f = g
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_append : ∀ {α : Type u_1} (xs ys : List α), FreeAddMonoid.ofList (xs ++ ys) = FreeAddMonoid.ofList xs + FreeAddMonoid.ofList ys
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.surjective_map_ofLE : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G'),
  Function.Surjective (SimpleGraph.ConnectedComponent.map (SimpleGraph.Hom.ofLE h))
-- Mathlib.Data.Set.Prod
Set.EqOn.eq_1 : ∀ {α : Type u} {β : Type v} (f₁ f₂ : α → β) (s : Set α), Set.EqOn f₁ f₂ s = ∀ ⦃x : α⦄, x ∈ s → f₁ x = f₂ x
-- Init.Data.String.Lemmas.Order
String.Pos.sliceTo_lt_sliceTo_iff : ∀ {s : String} {p₀ q r : s.Pos} {h₁ : q ≤ p₀} {h₂ : r ≤ p₀}, p₀.sliceTo q h₁ < p₀.sliceTo r h₂ ↔ q < r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryGE!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryGE! t₁ k = Std.DTreeMap.Raw.Const.getEntryGE! t₂ k
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.mul_log_le_toReal_klDiv : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      μ.real Set.univ * Real.log (μ.real Set.univ / ν.real Set.univ) + ν.real Set.univ - μ.real Set.univ ≤
        (InformationTheory.klDiv μ ν).toReal
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opMap_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.opMap φ).τ₃ = φ.τ₁.op
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : K.X k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv
      (CategoryTheory.CategoryStruct.comp (K.fromOpcycles j k) h) =
    CategoryTheory.CategoryStruct.comp (K.sc' i j k).fromOpcycles h
-- Lean.IdentifierSuggestion
/-- Given a \(presumably existing\) identifier, find all the `suggest_for` annotations that were given
for that identifier.
 -/
Lean.getStoredSuggestions : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Lean.NameSet
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.trans_isBigOWith : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Norm E] [inst_1 : Norm F] [inst_2 : Norm G]
  {c : ℝ} {f : α → E} {g : α → F} {k : α → G} {l : Filter α},
  f =o[l] g → Asymptotics.IsBigOWith c l g k → 0 < c → f =o[l] k
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonArray : {α : Type u_1} → [Lean.FromJson α] → Lean.FromJson (Array α)
-- Mathlib.Order.Category.LinOrd
LinOrd.id_apply : ∀ (X : LinOrd) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Algebra.Group.Action.Pi
Pi.mulAction'.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {m : (i : ι) → Monoid (α i)}
  [inst : (i : ι) → MulAction (α i) (β i)], Pi.mulAction' = { toSMul := Pi.smul', mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.inf : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : SemilatticeInf M] {f g : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → Function.HasFiniteSupport fun a => f a ⊓ g a
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.le_prod_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {s : Subsemigroup M} {t : Subsemigroup N}
  {u : Subsemigroup (M × N)},
  u ≤ s.prod t ↔ Subsemigroup.map (MulHom.fst M N) u ≤ s ∧ Subsemigroup.map (MulHom.snd M N) u ≤ t
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- If a limit already exists in `C`, then the limit of the image of the diagram under the Yoneda
embedding is an ind-object.  -/
CategoryTheory.Limits.isIndObject_limit_comp_yoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit (F.comp CategoryTheory.yoneda))
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instRxcHasSize : {α : Type u} →
  [inst : LE α] →
    [inst_1 : LT α] →
      {β : Type v} →
        [inst_2 : LE β] →
          [inst_3 : LT β] →
            [inst_4 : Std.PRange.UpwardEnumerable β] →
              [inst_5 : Std.PRange.LawfulUpwardEnumerable β] →
                [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] →
                  [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] →
                    [m : HasModel✝ α β] → [Std.Rxc.HasSize β] → Std.Rxc.HasSize α
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.map'_injective_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α →* β},
  Function.Injective ⇑(WithZero.map' f) ↔ Function.Injective ⇑f
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.coordChange_comp : ∀ {ι : Type u_5} {B : Type u_6} [inst : TopologicalSpace B] {F : Type u_7} [inst_1 : TopologicalSpace F]
  (self : FiberBundleCore ι B F) (i j k : ι),
  ∀ x ∈ self.baseSet i ∩ self.baseSet j ∩ self.baseSet k,
    ∀ (v : F), self.coordChange j k x (self.coordChange i j x v) = self.coordChange i k x v
-- Std.Async.System
Std.Async.System.instReprCPUTimes : Repr Std.Async.System.CPUTimes
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyGTD : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → α → α
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map_π_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b)
  (b : β) {Z : C} (h : g b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (CategoryTheory.CategoryStruct.comp (p b) h)
-- Init.Data.Queue
/-- `O(1)`. The empty queue.  -/
Std.Queue.empty : {α : Type u} → Std.Queue α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyπ_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {Z : C}
  (h : S₂.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.homologyπ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.homologyπ h)
-- Aesop.Tree.Data
Aesop.GoalState.isProven : Aesop.GoalState → Bool
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} {φ φ' : D₁ ⟶ D₂},
  φ = φ' ↔ ∀ (i : ι), φ.hom i = φ'.hom i
-- Mathlib.Topology.Neighborhoods
tendsto_pure_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} (f : α → X) (a : α), Filter.Tendsto f (pure a) (nhds (f a))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.core_certC.eq_1 : ∀ (lhs rhs : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Stepwise.core_certC lhs rhs p c = ((lhs.sub rhs).toPolyC c).beq' p
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When the first map `S.f` is zero, this is the right homology data on `S` given
by any limit kernel fork of `S.g`  -/
CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        S.f = 0 → (c : CategoryTheory.Limits.KernelFork S.g) → CategoryTheory.Limits.IsLimit c → S.RightHomologyData
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.prodEquiv_apply_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] (X₁ X₂ : C)
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)]
  (x : CategoryTheory.ToType (X₁ ⨯ X₂)),
  ((CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂) x).2 =
    (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) x
-- Std.Data.DHashMap.Raw
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.DHashMap.Raw.modify : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → [Hashable α] → Std.DHashMap.Raw α β → (a : α) → (β a → β a) → Std.DHashMap.Raw α β
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.cast_apply : ∀ {R : Type uR} [inst : CommSemiring R] {ι : Type u_1} {A : ι → Type u_2} [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {i j : ι} (h : i = j) (a : A i), (AlgEquiv.cast h) a = cast ⋯ a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {a b : α}, cmp a b = Ordering.eq → t[a]! = t[b]!
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.notFollowedBy.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to a `UInt64`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toUInt64 : Float.Model → UInt64
-- Aesop.Rule.Forward
Aesop.ForwardRulePriority.unsafe.sizeOf_spec : ∀ (p : Aesop.Percent), sizeOf (Aesop.ForwardRulePriority.unsafe p) = 1 + sizeOf p
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
TopCat.Presheaf.Γgerm.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) (x : ↑X), F.Γgerm x = F.germ ⊤ x True.intro
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.codeSupp'.match_1.eq_2 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.zero' → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.succ → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.tail → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (c f fs : Turing.ToPartrec.Code) → c = f.cons fs → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (c f g : Turing.ToPartrec.Code) → c = f.comp g → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (c f g : Turing.ToPartrec.Code) → c = f.case g → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (c f : Turing.ToPartrec.Code) → c = f.fix → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match Turing.ToPartrec.Code.succ, k with
    | c@h:Turing.ToPartrec.Code.zero', k => h_1 c h k
    | c@h:Turing.ToPartrec.Code.succ, k => h_2 c h k
    | c@h:Turing.ToPartrec.Code.tail, k => h_3 c h k
    | c@h:(f.cons fs), k => h_4 c f fs h k
    | c@h:(f.comp g), k => h_5 c f g h k
    | c@h:(f.case g), k => h_6 c f g h k
    | c@h:f.fix, k => h_7 c f h k) =
    h_2 Turing.ToPartrec.Code.succ ⋯ k
-- Mathlib.Data.Vector3
Vector3.append_add : ∀ {α : Type u_1} {m : ℕ} (v : Vector3 α m) {n : ℕ} (w : Vector3 α n) (i : Fin2 n), v.append w (i.add m) = w i
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
/-- If g(t)=t^c for all roots of unity, then c=χ(g).  -/
modularCyclotomicCharacter.toFun_unique : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (g : L ≃+* L)
  (c : ZMod (Nat.card ↥(rootsOfUnity n L))),
  (∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)) → c = modularCyclotomicCharacter.toFun n g
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_iff_succ_lt : ∀ {α : Type u_1} {b : α} [inst : PartialOrder α] [inst_1 : SuccOrder α],
  Order.IsSuccPrelimit b ↔ ∀ a < b, Order.succ a < b
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] {p : Polynomial R} {n : ℕ}, p.IsMonicOfDegree n → p ≠ 0
-- Mathlib.RingTheory.Unramified.LocalStructure
HasStandardEtaleSurjectionOn.isStandardEtale : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f : S},
  HasStandardEtaleSurjectionOn R f →
    ∀ [Algebra.Etale R (Localization.Away f)], Algebra.IsStandardEtale R (Localization.Away f)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.snd_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S : CategoryTheory.Over X},
  CategoryTheory.Over.Hom.left (CategoryTheory.SemiCartesianMonoidalCategory.snd R S) =
    CategoryTheory.Limits.pullback.snd R.hom S.hom
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.toList_cons : ∀ {α : Type u} (a : α) (s : Stream'.WSeq α), (Stream'.WSeq.cons a s).toList = (List.cons a <$> s.toList).think
-- Batteries.Data.Float.Lemmas
Float32.isNaN_eq_decide_eq_nan : ∀ {f : Float32}, f.isNaN = decide (f = Float32.nan)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_nonneg_iff : ∀ {x : ℝ}, 0 ≤ Real.sinh x ↔ 0 ≤ x
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.maxSteps : Lean.PrettyPrinter.Delaborator.OmissionReason
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.eqToHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] [inst_2 : CategoryTheory.Limits.HasImage f'] (h : f = f'),
  CategoryTheory.Limits.image.eqToHom h =
    CategoryTheory.Limits.image.lift
      { I := CategoryTheory.Limits.image f', m := CategoryTheory.Limits.image.ι f', m_mono := ⋯,
        e := CategoryTheory.Limits.factorThruImage f', fac := ⋯ }
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.apply_lt_nfp : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ {a b : Ordinal.{u}}, f b < Ordinal.nfp f a ↔ b < Ordinal.nfp f a
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.IsCyclicallyReduced.eq_1 : ∀ {α : Type u} (L : List (α × Bool)),
  FreeGroup.IsCyclicallyReduced L = (FreeGroup.IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2)
-- Mathlib.Analysis.MeanInequalities
/-- For `1 ≤ p`, the `p`-th power of the sum of `f i` is bounded above by a constant times the
sum of the `p`-th powers of `f i`. Version for sums over finite sets, with `ℝ≥0`-valued functions.
 -/
NNReal.rpow_sum_le_const_mul_sum_rpow : ∀ {ι : Type u} (s : Finset ι) (f : ι → NNReal) {p : ℝ},
  1 ≤ p → (∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Submonoid.smul_mem_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : GroupWithZero G₀] [inst_2 : MulDistribMulAction G₀ M]
  {a : G₀}, a ≠ 0 → ∀ (S : Submonoid M) (x : M), a • x ∈ a • S ↔ x ∈ S
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.mk : ∀ {pat s : String.Slice} {needlePos stackPos : String.Pos.Raw},
  pat.isEmpty = false →
    String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat.copy.toByteArray s.copy.toByteArray
        needlePos.byteIdx stackPos.byteIdx →
      (needlePos = 0 → String.Pos.Raw.IsValidForSlice s stackPos) →
        String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos
-- Mathlib.Data.Set.Subsingleton
Set.strictMonoOn_singleton : ∀ {α : Type u} {β : Type v} {a : α} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β), StrictMonoOn f {a}
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.neg_eq_neg_one_mul : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (a : α), -a = -1 * a
-- Init.Data.SInt.Lemmas
Int32.mul_assoc : ∀ (a b c : Int32), a * b * c = a * (b * c)
-- Mathlib.Algebra.Homology.Opposite
/-- The natural isomorphism `K.op.homology i ≅ op (K.homology i)`.  -/
HomologicalComplex.homologyOpNatIso : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          [inst_2 : CategoryTheory.CategoryWithHomology V] →
            (i : ι) →
              (HomologicalComplex.opFunctor V c).comp (HomologicalComplex.homologyFunctor Vᵒᵖ c.symm i) ≅
                (HomologicalComplex.homologyFunctor V c i).op
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.toEnd.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.toEnd = { s := s, i := s.rawEndPos }
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E], μ.withDensityᵥ 0 = 0
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.Decomposition.isInternal : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [DirectSum.Decomposition ℳ], DirectSum.IsInternal ℳ
-- Mathlib.Order.Antichain
IsAntichain.image_compl : ∀ {α : Type u_1} {s : Set α} [inst : BooleanAlgebra α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → IsAntichain (fun x1 x2 => x1 ≤ x2) (compl '' s)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.foldM_filterWithPostcondition : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o]
  [LawfulMonad m] [LawfulMonad n] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad o Pred EPred] [inst_10 : Std.IteratorLoop α m n] [inst_11 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o] [inst_14 : MonadLiftT m n] [inst_15 : MonadLiftT n o]
  [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)}
  {g : δ → β → o δ} {init : δ} {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let __do_lift ← liftM (f b).run
          if __do_lift.down = true then g d b else pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.IterM.filterWithPostcondition f it) ⦃ Q; eQ ⦄
-- Lean.Meta.Tactic.Grind.Anchor
_private.Lean.Meta.Tactic.Grind.Anchor.0.Lean.Meta.Grind.getNumDigitsForAnchors.go.eq_def : ∀ {α : Type u_1} [inst : Lean.Meta.Grind.HasAnchor α] (es : Array α) (numDigits : ℕ),
  Lean.Meta.Grind.getNumDigitsForAnchors.go✝ es numDigits =
    (if 4 * numDigits < 64 then
        have shift := 64 - 4 * numDigits;
        have found := ∅;
        do
        let __s ←
          forIn es (none, found) fun e __s =>
              have found := __s.2;
              have a := Lean.Meta.Grind.HasAnchor.getAnchor e;
              have a' := a >>> shift.toUInt64;
              match found[a']? with
              | some b =>
                if (b != a) = true then do
                  let __do_lift ← Lean.Meta.Grind.getNumDigitsForAnchors.go✝ es (numDigits + 1)
                  pure (ForInStep.done (some __do_lift, found))
                else pure (ForInStep.yield (none, found))
              | x =>
                have found := found.insert a' a;
                pure (ForInStep.yield (none, found))
        have __r : Option ℕ := __s.1
        match __r with
          | some r => pure r
          | none => pure numDigits
      else pure numDigits).run
-- Batteries.Lean.Meta.InstantiateMVars
/-- Instantiate metavariables in the local context of the given metavariable, update
the metavariable's declaration and return the new local context.
 -/
Lean.MVarId.instantiateMVarsInLocalContext : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → [Lean.MonadError m] → Lean.MVarId → m Lean.LocalContext
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLE_iff_isChain`. -/
List.SortedLE.isChain : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLE → List.IsChain (fun x1 x2 => x1 ≤ x2) l
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ext_get?_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtTreeSet α cmp},
  t₁ = t₂ ↔ ∀ (k : α), t₁.get? k = t₂.get? k