mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.neg_ofSubmodule : ∀ {R : Type u_5} {E : Type u_6} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] (S : Submodule R E), -↑S = ↑(-S)
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.match_1.splitter : (s : String) →
  (motive : Char → Option (s.Pos × ℕ) → Sort u_1) →
    (ch : Char) →
      (x : Option (s.Pos × ℕ)) →
        ((q : s.Pos) → (v : ℕ) → x = some (q, v) → motive 'U' (some (q, v))) →
          ((x_1 : Char) →
              (x_2 : Option (s.Pos × ℕ)) →
                (∀ (q : s.Pos) (v : ℕ), x_1 = 'U' → x_2 = some (q, v) → False) → x = x_2 → motive x_1 x_2) →
            motive ch x
-- Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
/-- `X □ Y` lifts against `Z` if and only if `X` lifts against `Y ⋔ Z`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_iff' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] {X Y Z : CategoryTheory.Arrow C},
  CategoryTheory.HasLiftingProperty (X □ Y).hom Z.hom ↔ CategoryTheory.HasLiftingProperty X.hom (Opposite.op Y ⋔ Z).hom
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Specialized destructor on `WPath`  -/
MvPFunctor.wPathDestRight : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      {a : P.A} →
        {f : P.last.B a → P.last.W} →
          TypeVec.Arrow (P.WPath (WType.mk a f)) α → (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α
-- Init.Grind.Order
Lean.Grind.Order.eq_trans_true : ∀ {p q : Prop}, p = q → q = True → p = True
-- Std.Data.DHashMap.Raw
/-- Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
 -/
Std.DHashMap.Raw.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.antipode_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.HopfObj.antipode CategoryTheory.ComonObj.counit =
    CategoryTheory.ComonObj.counit
-- Mathlib.RingTheory.Smooth.Kaehler
/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with kernel `I`,
there is a one-to-one correspondence between `P`-linear retractions of `I/I² →ₗ[P] S ⊗[P] Ω[P/R]`
and algebra homomorphism sections of `f‾ : P/I² → S`.
 -/
retractionKerCotangentToTensorEquivSection : {R : Type u_1} →
  {P : Type u_2} →
    {S : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing P] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R P] →
              [inst_4 : Algebra P S] →
                [inst_5 : Algebra R S] →
                  [inst_6 : IsScalarTower R P S] →
                    Function.Surjective ⇑(algebraMap P S) →
                      { l // l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P S = LinearMap.id } ≃
                        { g // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S }
-- Mathlib.Analysis.MeanInequalitiesPow
_private.Mathlib.Analysis.MeanInequalitiesPow.0.NNReal.add_rpow_le_one_of_add_le_one : ∀ {p : ℝ} (a b : NNReal), a + b ≤ 1 → 1 ≤ p → a ^ p + b ^ p ≤ 1
-- Lean.Elab.Coinductive
Lean.Elab.Command.addFunctorPostfix : Lean.Name → Lean.Name
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
linearIndependent_span : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v → LinearIndependent R fun i => ⟨v i, ⋯⟩
-- Lean.Meta.Tactic.Grind.EMatch
/-- Choice point for the backtracking search.
The state of the procedure contains a stack of choices.
 -/
Lean.Meta.Grind.EMatch.Choice : Type
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isEverywherePos : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : μ'.IsAddHaarMeasure] {s : Set G},
  MeasurableSet s → μ.IsEverywherePos s → μ' s = μ'.addHaarScalarFactor μ • μ s
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toAffineEquiv : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P ≃ᵃⁱ[𝕜] P₂) → P ≃ᵃ[𝕜] P₂
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.length_le_card_edgeFinset : ∀ {V : Type u} {G : SimpleGraph V} [inst : Fintype ↑G.edgeSet] {u v : V} {w : G.Walk u v},
  w.IsTrail → w.length ≤ G.edgeFinset.card
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_throw_ExceptT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ (ε → Pred) EPred} (err : ε),
  Lean.Order.PartialOrder.rel (epost.head err) (Std.Internal.Do.wp (MonadExceptOf.throw err) post epost)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.ε_succ : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [inst_1 : c.TensorSigns] {p q : I},
  c.Rel p q → c.ε q = -c.ε p
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.cardinalMk_adjoin_le : ∀ (F : Type u) [inst : Field F] {E : Type u} [inst_1 : Field E] [inst_2 : Algebra F E] (s : Set E),
  Cardinal.mk ↥(IntermediateField.adjoin F s) ≤ max (max (Cardinal.mk F) (Cardinal.mk ↑s)) Cardinal.aleph0
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.pow : ∀ {𝕜 : 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_21} [inst_6 : NormedRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'}, MDiff p → ∀ (n : ℕ), MDiff (p ^ n)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
TensorialAt.mkHom.congr_simp : ∀ {𝕜 : 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 I_1 : ModelWithCorners 𝕜 E H}
  (e_I : I = I_1) {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_9 : (x : M) → AddCommGroup (V x)]
  [inst_10 : (x : M) → Module 𝕜 (V x)] [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V]
  {A : Type u_9} [inst_13 : AddCommGroup A] [inst_14 : Module 𝕜 A] [inst_15 : VectorBundle 𝕜 F V]
  [inst_16 : CompleteSpace 𝕜] [inst_17 : FiniteDimensional 𝕜 F] [inst_18 : ContMDiffVectorBundle 1 F V I]
  [inst_19 : TopologicalSpace A] [inst_20 : IsTopologicalAddGroup A] [inst_21 : ContinuousSMul 𝕜 A]
  (Φ Φ_1 : ((x : M) → V x) → A) (e_Φ : Φ = Φ_1) (x : M) (hΦ : TensorialAt I F Φ x),
  TensorialAt.mkHom Φ x hΦ = TensorialAt.mkHom Φ_1 x ⋯
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.eq_lift_inv_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj B] (f g h : A ⟶ B),
  f =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift g
          (CategoryTheory.CategoryStruct.comp h CategoryTheory.GrpObj.inv))
        CategoryTheory.MonObj.mul ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f h) CategoryTheory.MonObj.mul = g
-- Init.Data.Rat.Lemmas
Rat.div_mul_cancel : ∀ {a b : ℚ}, b ≠ 0 → a / b * b = a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_of_contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, (Std.TreeMap.map f t).contains k = true → t.contains k = true
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_val : ∀ (b : Bool) (n : ℕ), Nat.bit b n = 2 * n + b.toNat
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.FixedPointFree.coe_eq_inv_of_involutive : ∀ {F : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : FunLike F G G] [MonoidHomClass F G G] {φ : F} [Finite G],
  MonoidHom.FixedPointFree ⇑φ → Function.Involutive ⇑φ → ⇑φ = fun x => x⁻¹
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.sub_apply : ∀ {M : Type u_8} {N : Type u_9} [inst : Zero M] [inst_1 : SubtractionMonoid N] (f g : ZeroHom M N) (x : M),
  (f - g) x = f x - g x
-- Mathlib.Order.PFilter
Order.PFilter.mk.injEq : ∀ {P : Type u_1} [inst : Preorder P] (dual dual_1 : Order.Ideal Pᵒᵈ),
  ({ dual := dual } = { dual := dual_1 }) = (dual = dual_1)
-- Mathlib.Analysis.Normed.Operator.Basic
SemilinearMapClass.ebound_of_continuous : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} {𝓕 : Type u_8} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : FunLike 𝓕 E F]
  [RingHomIsometric σ₁₂] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕),
  Continuous ⇑f → ∃ C, 0 < C ∧ ∀ (x : E), ‖f x‖ₑ ≤ ↑C * ‖x‖ₑ
-- Init.Data.LawfulHashable
LawfulHashable.mk : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α], (∀ (a b : α), (a == b) = true → hash a = hash b) → LawfulHashable α
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  {F G : CategoryTheory.Functor (A ⊕ A') B}
  (η₁ : (CategoryTheory.Sum.inl_ A A').comp F ≅ (CategoryTheory.Sum.inl_ A A').comp G)
  (η₂ : (CategoryTheory.Sum.inr_ A A').comp F ≅ (CategoryTheory.Sum.inr_ A A').comp G),
  (CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr η₁ η₂).hom =
    CategoryTheory.Sum.natTransOfWhiskerLeftInlInr η₁.hom η₂.hom
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Alias** of `MeasureTheory.integral_inter_add_sdiff`. -/
MeasureTheory.integral_inter_add_diff : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet t →
    MeasureTheory.IntegrableOn f s μ → ∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `G : C → D` is a faithful functor which sends t to a limit cone,
then it suffices to check that the induced maps for the image of t
can be lifted to maps of `C`.  -/
CategoryTheory.Limits.IsLimit.ofFaithful : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            {D : Type u₄} →
              [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
                (G : CategoryTheory.Functor C D) →
                  [G.Faithful] →
                    (ht : CategoryTheory.Limits.IsLimit (G.mapCone t)) →
                      (lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt) →
                        (∀ (s : CategoryTheory.Limits.Cone F), G.map (lift s) = ht.lift (G.mapCone s)) →
                          CategoryTheory.Limits.IsLimit t
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α}, ∅.isEmpty = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ordCompare_maxKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap α (fun x => β) compare} {k : α}
  {f : β → β} {fallback : α},
  compare ((Std.DTreeMap.Const.modify t k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_Ioo : ∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : Preorder α] [CompactIccSpace α] (a b : α),
  Bornology.IsBounded (Set.Ioo a b)
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.LetRecClosure.mk.injEq : ∀ (ref : Lean.Syntax) (localDecls : Array Lean.LocalDecl) (closed : Lean.Expr) (toLift : Lean.Elab.Term.LetRecToLift)
  (ref_1 : Lean.Syntax) (localDecls_1 : Array Lean.LocalDecl) (closed_1 : Lean.Expr)
  (toLift_1 : Lean.Elab.Term.LetRecToLift),
  ({ ref := ref, localDecls := localDecls, closed := closed, toLift := toLift } =
      { ref := ref_1, localDecls := localDecls_1, closed := closed_1, toLift := toLift_1 }) =
    (ref = ref_1 ∧ localDecls = localDecls_1 ∧ closed = closed_1 ∧ toLift = toLift_1)
-- Init.Data.UInt.Lemmas
UInt64.toUSize_le : ∀ {a b : UInt64}, a.toUSize ≤ b.toUSize ↔ a % UInt64.ofNat USize.size ≤ b % UInt64.ofNat USize.size
-- Mathlib.Algebra.Module.Submodule.LinearMap
SMulMemClass.subtype_injective : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : SetLike A M] [inst_4 : AddSubmonoidClass A M] [inst_5 : SMulMemClass A R M] (S' : A),
  Function.Injective ⇑(SMulMemClass.subtype S')
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findSomeM?.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)),
  List.findSomeM? f [] = pure none
-- Std.Sat.AIG.Basic
Std.Sat.AIG.BinaryInput.mk : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.Ref → aig.Ref → aig.BinaryInput
-- Mathlib.Topology.Algebra.Star.LinearMap
/-- The intrinsic star operation on continuous linear maps defined by
`(star f) x = star (f (star x))`.  -/
ContinuousLinearMap.intrinsicStar : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : InvolutiveStar R] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : StarAddMonoid E] →
                [StarModule R E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module R F] →
                      [inst_8 : StarAddMonoid F] →
                        [StarModule R F] →
                          [inst_10 : TopologicalSpace E] →
                            [inst_11 : TopologicalSpace F] →
                              [ContinuousStar E] → [ContinuousStar F] → Star (WithConv (E →L[R] F))
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.le_iff : ∀ {α : 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✝ α β]
  {x y : α},
  Std.PRange.UpwardEnumerable.LE x y ↔ Std.PRange.UpwardEnumerable.LE (HasModel.encode✝ x) (HasModel.encode✝ y)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.lowerBound?_mem : ∀ {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α}, RBTree.RBNode.lowerBound? cut t = some x → x ∈ t
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.mk.inj : ∀ {knowsType knowsLevel inBottomUp parentIsApp : Bool} {subExpr : Lean.SubExpr}
  {knowsType_1 knowsLevel_1 inBottomUp_1 parentIsApp_1 : Bool} {subExpr_1 : Lean.SubExpr},
  { knowsType := knowsType, knowsLevel := knowsLevel, inBottomUp := inBottomUp, parentIsApp := parentIsApp,
        subExpr := subExpr } =
      { knowsType := knowsType_1, knowsLevel := knowsLevel_1, inBottomUp := inBottomUp_1, parentIsApp := parentIsApp_1,
        subExpr := subExpr_1 } →
    knowsType = knowsType_1 ∧
      knowsLevel = knowsLevel_1 ∧ inBottomUp = inBottomUp_1 ∧ parentIsApp = parentIsApp_1 ∧ subExpr = subExpr_1
-- Lean.DocString.Parser
Lean.Doc.Parser.InlineCtxt.mk.inj : ∀ {allowNewlines : Bool} {minIndent : ℕ} {boldDepth emphDepth : Option ℕ} {inLink allowNewlines_1 : Bool}
  {minIndent_1 : ℕ} {boldDepth_1 emphDepth_1 : Option ℕ} {inLink_1 : Bool},
  { allowNewlines := allowNewlines, minIndent := minIndent, boldDepth := boldDepth, emphDepth := emphDepth,
        inLink := inLink } =
      { allowNewlines := allowNewlines_1, minIndent := minIndent_1, boldDepth := boldDepth_1, emphDepth := emphDepth_1,
        inLink := inLink_1 } →
    allowNewlines = allowNewlines_1 ∧
      minIndent = minIndent_1 ∧ boldDepth = boldDepth_1 ∧ emphDepth = emphDepth_1 ∧ inLink = inLink_1
-- Mathlib.Data.ZMod.ValMinAbs
/-- Returns the integer in the same equivalence class as `x` that is closest to `0`.

The result will be in the interval `(-n/2, n/2]`.  -/
ZMod.valMinAbs : {n : ℕ} → ZMod n → ℤ
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendSingleIso_hom_f_assoc : ∀ {ι : 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)
  [inst_4 : DecidableEq ι'] (i : ι) (i' : ι') (h : e.f i = i') {Z : C}
  (h_1 : ((HomologicalComplex.single C c' i').obj X).X i' ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HomologicalComplex.extendSingleIso e X i i' h).hom.f i') h_1 =
    CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c i).obj X).extendXIso e h).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c i X).hom
        (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c' i' X).inv h_1))
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_isEmpty : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] [IsEmpty n]
  {A : Matrix n n R}, A.charpoly = 1
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.isOpen_sphere : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ}, r ≠ 0 → IsOpen (Metric.sphere x r)
-- Mathlib.GroupTheory.OrderOfElement
isPeriodicPt_mul_iff_pow_eq_one : ∀ {G : Type u_1} [inst : Monoid G] {n : ℕ} (x : G), Function.IsPeriodicPt (fun x_1 => x * x_1) n 1 ↔ x ^ n = 1
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- A dually finitely generated cone is the dual of a finitely generated cone.  -/
PointedCone.DualFG.exists_fg_dual : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R N},
  PointedCone.DualFG p C → ∃ D, Submodule.FG D ∧ PointedCone.dual p ↑D = C
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- The identity as a positive linear map.  -/
PositiveLinearMap.id : (R : Type u_1) →
  (E₁ : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid E₁] → [inst_2 : PartialOrder E₁] → [inst_3 : Module R E₁] → E₁ →ₚ[R] E₁
-- Mathlib.Computability.Primrec.List
Primrec.vector_ofFn : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : Fin n → α → σ},
  (∀ (i : Fin n), Primrec (f i)) → Primrec fun a => List.Vector.ofFn fun i => f i a
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.invOn : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.InvOn (↑e.symm) (↑e) e.source e.target
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
hasMFDerivWithinAt_inter : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  t ∈ nhds x → (HasMFDerivAt[s ∩ t] f x f' ↔ HasMFDerivAt[s] f x f')
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.splitFromSteps.match_1.eq_3 : ∀ {s : String.Slice} (motive : List (String.Slice.Pattern.SearchStep s) → Sort u_1) (p q : s.Pos)
  (l : List (String.Slice.Pattern.SearchStep s)) (h_1 : Unit → motive [])
  (h_2 :
    (startPos endPos : s.Pos) →
      (l : List (String.Slice.Pattern.SearchStep s)) →
        motive (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l))
  (h_3 :
    (p q : s.Pos) →
      (l : List (String.Slice.Pattern.SearchStep s)) → motive (String.Slice.Pattern.SearchStep.matched p q :: l)),
  (match String.Slice.Pattern.SearchStep.matched p q :: l with
    | [] => h_1 ()
    | String.Slice.Pattern.SearchStep.rejected startPos endPos :: l => h_2 startPos endPos l
    | String.Slice.Pattern.SearchStep.matched p q :: l => h_3 p q l) =
    h_3 p q l
-- Init.Data.List.Sublist
List.isSublist.eq_2 : ∀ {α : Type u} [inst : BEq α] (x : List α), (x = [] → False) → x.isSublist [] = false
-- Mathlib.Algebra.Group.Action.Defs
neg_vadd_eq_iff : ∀ {G : Type u_3} {α : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a b : α}, -g +ᵥ a = b ↔ a = g +ᵥ b
-- Mathlib.CategoryTheory.Elements
/-- The reverse direction of the equivalence `F.Elements ≅ (*, F)`.  -/
CategoryTheory.CategoryOfElements.fromStructuredArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) →
      CategoryTheory.Functor (CategoryTheory.StructuredArrow PUnit.{w + 1} F) F.Elements
-- Mathlib.Topology.Separation.Basic
/-- In a weakly locally compact R₁ space,
every point has an open neighborhood with compact closure.  -/
exists_isOpen_mem_isCompact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X),
  ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instMulValueGroup : (A : Type u) →
  [inst : CommRing A] → (K : Type v) → [inst_1 : Field K] → [inst_2 : Algebra A K] → Mul (ValuationRing.ValueGroup A K)
-- Mathlib.Order.Disjoint
Codisjoint.eq_top_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b → a ≤ b → b = ⊤
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.erase : {α : Type u} →
  {β : α → Type v} → [BEq α] → α → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β
-- Mathlib.Algebra.Group.Even
even_subset_image_even : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] {f : F}, Function.Surjective ⇑f → {b | Even b} ⊆ ⇑f '' {a | Even a}
-- Mathlib.RingTheory.Multiplicity
multiplicity.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] (a b : α), multiplicity a b = WithTop.untopD 1 (emultiplicity a b)
-- Mathlib.Order.Preorder.Finsupp
Finsupp.semilatticeInf : {ι : Type u_1} → {M : Type u_2} → [inst : Zero M] → [SemilatticeInf M] → SemilatticeInf (ι →₀ M)