mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] (I : Ideal R)
  [Submodule.IsPrincipal I], IsLocalRing.maximalIdeal R ∈ I.minimalPrimes → (IsLocalRing.maximalIdeal R).height ≤ 1
-- Mathlib.Algebra.Polynomial.Bivariate
/-- Given valuations `x` and `y` of the variables in an `R`-algebra `A`, the bijection induced by
the unique `R`-algebra homomorphism from `R[X][Y]` to `A` sending `X` to `x` and `Y` to `y`.  -/
Polynomial.aevalAevalEquiv : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → A × A ≃ (Polynomial (Polynomial R) →ₐ[R] A)
-- Mathlib.Data.Fintype.Order
Finite.le_ciSup_of_le : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] [inst : ConditionallyCompleteLattice α] {a : α} {f : ι → α} (c : ι),
  a ≤ f c → a ≤ iSup f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, l.contains k = false → k ∈ m.insertManyIfNewUnit l → k ∈ m
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.addMonoid : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddMonoid α] → AddMonoid (Matrix m n α)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
uniqueMDiffWithinAt_univ : ∀ {𝕜 : 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] {x : M}, UniqueMDiffAt[Set.univ] x
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_lt_re`. -/
Complex.frontier_setOf_lt_re : ∀ (a : ℝ), frontier {z | a < z.re} = {z | z.re = a}
-- Mathlib.Topology.Order.T5
Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X},
  Disjoint s (closure t) → a ∈ s → (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ nhdsWithin a (Set.Iic a)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.pairwiseDisjoint_smul_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] [IsLeftCancelSMul α β] {s : Set α} {t : Set β},
  (s.PairwiseDisjoint fun x => x • t) ↔ Set.InjOn (fun p => p.1 • p.2) (s ×ˢ t)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
/-- Compose an edge-labeling with a graph embedding.  -/
SimpleGraph.EdgeLabeling.pullback : {V : Type u_1} →
  {V' : Type u_2} →
    {G : SimpleGraph V} → {G' : SimpleGraph V'} → {K : Type u_3} → G.EdgeLabeling K → G' →g G → G'.EdgeLabeling K
-- Mathlib.GroupTheory.CoprodI
Monoid.instInhabitedCoprodI : {ι : Type u_1} → (M : ι → Type u_2) → [inst : (i : ι) → Monoid (M i)] → Inhabited (Monoid.CoprodI M)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
/-- Deligne's archimedean Gamma factor for a complex infinite place.

See "Valeurs de fonctions L et périodes d'intégrales" § 5.3. (Some authors omit the factor of 2).
Note that this is not the same as `Complex.Gamma`.  -/
Complex.Gammaℂ : ℂ → ℂ
-- Mathlib.Algebra.Notation
/-- A notation class for the *positive part* function (multiplicative version): `a⁺ᵐ`.  -/
OneLePart : Type u_1 → Type u_1
-- Std.Time.DateTime
/-- Subtract `Week.Offset` from a `DateTime`.
 -/
Std.Time.DateTime.subWeeks : Std.Time.DateTime → Std.Time.Week.Offset → Std.Time.DateTime
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The affine open sets of an open subscheme
corresponds to the affine open sets containing in the subset.  -/
AlgebraicGeometry.affineOpensRestrict : {X : AlgebraicGeometry.Scheme} → (U : X.Opens) → ↑(↑U).affineOpens ≃ { V // ↑V ≤ U }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOfCoconeRightOp_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F.rightOp),
  (CategoryTheory.Limits.coneOfCoconeRightOp c).pt = Opposite.unop c.pt
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.classifyWeekdayText : ℕ → Option Std.Time.Text
-- Lean.Util.PtrSet
Lean.Ptr.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (value : α), sizeOf { value := value } = 1 + sizeOf value
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
MonomialOrder.degLex_le_iff : ∀ {σ : Type u_2} [inst : LinearOrder σ] [inst_1 : WellFoundedGT σ] {a b : σ →₀ ℕ},
  MonomialOrder.degLex.toSyn a ≤ MonomialOrder.degLex.toSyn b ↔ toDegLex a ≤ toDegLex b
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.isOpenMap_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsOpenMap)
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_mono : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], Monotone Rat.cast
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
SimpleGraph.triangleRemovalBound_nonpos : ∀ {ε : ℝ}, ε ≤ 0 → SimpleGraph.triangleRemovalBound ε ≤ 0
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.List.length_filter_strict_mono : ∀ {α : Type u} {l : List α} {P Q : α → Bool} {a : α},
  (∀ (a : α), P a = true → Q a = true) →
    a ∈ l → ¬P a = true → Q a = true → (List.filter P l).length < (List.filter Q l).length
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measure_add_right_null : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant] (y : G),
  μ ((fun x => x + y) ⁻¹' s) = 0 ↔ μ s = 0
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.default.sizeOf_spec : ∀ (gen : Bool), sizeOf (Lean.Meta.Grind.EMatchTheoremKind.default gen) = 1 + sizeOf gen
-- Mathlib.Tactic.NormNum.Result
/-- Extract from a `Result` the integer value (as both a term and an expression),
and the proof that the original expression is equal to this integer.
 -/
Mathlib.Meta.NormNum.Result.toInt : {u : Lean.Level} →
  {α : Q(Type u)} →
    {e : Q(«$α»)} →
      (_i : autoParam Q(Ring «$α») Mathlib.Meta.NormNum.Result.toInt._auto_1) →
        Mathlib.Meta.NormNum.Result e → Option (ℤ × (lit : Q(ℤ)) × Q(Mathlib.Meta.NormNum.IsInt «$e» «$lit»))
-- Init.Data.List.MapIdx
List.mapIdx_eq_zipIdx_map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β},
  List.mapIdx f l =
    List.map
      (fun x =>
        match x with
        | (a, i) => f i a)
      l.zipIdx
-- Mathlib.Order.ModularLattice
inf_covBy_of_covBy_sup_left : ∀ {α : Type u_1} [inst : Lattice α] [IsLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → a ⊓ b ⋖ b
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.instTransForallIsTheta : {α : Type u_1} →
  {E : Type u_3} →
    {G : Type u_5} →
      {F' : Type u_7} →
        [inst : Norm E] →
          [inst_1 : Norm G] →
            [inst_2 : SeminormedAddCommGroup F'] →
              {l : Filter α} → Trans (Asymptotics.IsTheta l) (Asymptotics.IsTheta l) (Asymptotics.IsTheta l)
-- Lean.Server.References
/-- Checks whether any of the ranges in `self.definition?` or `self.usages` contains `pos`.  -/
Lean.Lsp.RefInfo.contains : Lean.Lsp.RefInfo → Lean.Lsp.Position → optParam Bool false → Bool
-- Lean.Elab.ConfigEval.Basic
/-- Calls `EvalConfigItem.setConfigs'` from within `runConfigElab`.
 -/
Lean.Elab.ConfigEval.EvalConfigItem.setConfigs' : {α : Type} →
  Lean.Elab.ConfigEval.EvalConfigItem α →
    α →
      Array Lean.Syntax →
        (optParam (α → Lean.Syntax → Lean.Elab.TermElabM α) fun cfg cfgItem =>
            Lean.Elab.ConfigEval.EvalConfigItem.defaultOnErr cfg cfgItem) →
          optParam Bool false → Lean.CoreM α
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- an auxiliary type  -/
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.I₁₂ : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} →
      {J : Type u_10} → {r : I₁ × I₂ × I₃ → J} → CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r → Type u_11
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {h' : k' ∈ t.insertManyIfNewUnit l},
          k ∉ t →
            List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKey k' h' = k
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_nsmul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : AddMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] (i : ℕ),
  ContMDiff I I n fun a => i • a
-- Lean.DocString.Markdown
/-- A renderer for custom inline elements of type `α`. It receives a renderer for inline content, the
custom element, and the element's fallback content.
 -/
Lean.Doc.InlineMdRendererOf : Type → Type
-- Mathlib.GroupTheory.Finiteness
/-- A group is finitely generated if it is finitely generated as a subgroup of itself.  -/
Group.FG : (G : Type u_3) → [Group G] → Prop
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.mkQ_hom_toFun : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] (A : Rep.{u_1, u, v} k G) (W : Submodule k ↑A)
  (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) (a : ↑A),
  (Rep.Hom.hom (A.mkQ W le_comap)) a = Submodule.Quotient.mk a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.insertMany_ind : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)]
  {motive : Std.DHashMap α β → Prop} (m : Std.DHashMap α β) (l : ρ),
  motive m → (∀ (m : Std.DHashMap α β) (a : α) (b : β a), motive m → motive (m.insert a b)) → motive (m.insertMany l)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.range_mk : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  Set.range MulArchimedeanClass.mk = Set.univ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, m.WF → (Std.HashMap.Raw.map f m).contains k = m.contains k
-- Mathlib.CategoryTheory.Skeletal
/-- The functor from the skeleton of `C` to `C`.  -/
CategoryTheory.fromSkeleton : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor (CategoryTheory.Skeleton C) C
-- Mathlib.Tactic.Translate.ToAdditive
/-- The global `do_translate`/`dont_translate` attributes specify whether operations on
a given type should be translated. `dont_translate` can be used for types that are translated,
such as `MonoidAlgebra` -> `AddMonoidAlgebra`, or for fixed types, such as `Fin n`/`ZMod n`.
`do_translate` is for types without arguments, like `Unit` and `Empty`, where the structure on it
can be translated.

Note: The name generation is not aware of `dont_translate`, so if some part of a lemma is not
  translated thanks to this, you generally have to specify the translated name manually.
 -/
Mathlib.Tactic.ToAdditive.doTranslateAttr : Lean.NameMapExtension Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_congr : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α}
  (hab : (a == b) = true) {h : Std.Internal.List.containsKey a l = true},
  Std.Internal.List.getValue a l h = Std.Internal.List.getValue b l ⋯
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.of_isIso_fac_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z}
  [CategoryTheory.IsIso f] [hh : CategoryTheory.IsIso h],
  CategoryTheory.CategoryStruct.comp f g = h → CategoryTheory.IsIso g
-- Mathlib.Order.SuccPred.Basic
Order.le_iff_eq_or_succ_le : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α}, a ≤ b ↔ a = b ∨ Order.succ a ≤ b
-- Init.Data.List.Range
List.range'_subset_right_1 : ∀ {s m n : ℕ}, List.range' s m ⊆ List.range' s n ↔ m ≤ n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α}, k ∉ m₁ → Std.DHashMap.Const.get! (m₁.inter m₂) k = default
-- Mathlib.RingTheory.Algebraic.Basic
Polynomial.algEquivOfTranscendental_symm_aeval : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (s : S)
  (h : Transcendental R s) (f : Polynomial R),
  (Polynomial.algEquivOfTranscendental R s h).symm ((Polynomial.aeval ⟨s, ⋯⟩) f) = f
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Given a type `ι`, this is the shape of multicoequalizer diagrams corresponding
to situations where we want to coequalize two families of maps `V ⟨i, j⟩ ⟶ U i`
and `V ⟨i, j⟩ ⟶ U j` with `i : ι` and `j : ι`.  -/
CategoryTheory.Limits.MultispanShape.prod : Type w → CategoryTheory.Limits.MultispanShape
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.map_measureReal_apply_of_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β]
  {f : α → β},
  AEMeasurable f μ → ∀ {s : Set β}, MeasurableSet s → (MeasureTheory.Measure.map f μ).real s = μ.real (f ⁻¹' s)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.map.congr_simp : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f f_1 : S.LocalizationMap N),
  f = f_1 →
    ∀ {g g_1 : M →* P} (e_g : g = g_1) {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4}
      [inst_3 : CommMonoid Q] (k k_1 : T.LocalizationMap Q), k = k_1 → f.map hy k = f_1.map ⋯ k_1
-- Mathlib.Dynamics.Ergodic.Extreme
Ergodic.iff_mem_extremePoints_measure_univ_eq : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsFiniteMeasure μ],
  Ergodic f μ ↔ μ ∈ Set.extremePoints ENNReal {ν | MeasureTheory.MeasurePreserving f ν ν ∧ ν Set.univ = μ Set.univ}
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- There is a unique morphism from the zero object to any object `X`.  -/
CategoryTheory.Limits.HasZeroObject.uniqueTo : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → (X : C) → Unique (0 ⟶ X)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_indicatorConstLp : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E),
  (MeasureTheory.L1.setToL1 hT) (MeasureTheory.indicatorConstLp 1 hs hμs x) = (T s) x
-- Mathlib.CategoryTheory.Pi.Basic
/-- Assemble an `I`-indexed family of equivalences of categories
into a single equivalence.  -/
CategoryTheory.Equivalence.pi : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : I → Type u₂} →
        [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
          ((i : I) → C i ≌ D i) → (((i : I) → C i) ≌ (i : I) → D i)
-- Mathlib.Algebra.Order.CauSeq.BigOperators
IsCauSeq.of_abv_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β} {a : ℕ → α} (n : ℕ),
  (∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m) →
    (IsCauSeq abs fun n => ∑ i ∈ Finset.range n, a i) → IsCauSeq abv fun n => ∑ i ∈ Finset.range n, f i
-- Mathlib.Order.OrderDual
OrderDual.toDual_lt_toDual : ∀ {α : Type u_1} [inst : LT α] {a b : α}, OrderDual.toDual a < OrderDual.toDual b ↔ b < a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_map : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [LawfulBEq α] {f : α → β → γ} {k : α} {fallback : γ},
  (↑m).WF →
    Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.map f m) k fallback =
      (Option.map (f k) (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback
-- Mathlib.Order.CompleteLattice.Basic
sInf_upperBounds_eq_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), sInf (upperBounds s) = sSup s
-- Mathlib.Topology.Order
map_nhds_induced_eq : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} (a : α),
  Filter.map f (nhds a) = nhdsWithin (f a) (Set.range f)
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.Paths.morphismProperty_eq_top_of_isMultiplicative : ∀ (V : Type u₁) [inst : Quiver V] (P : CategoryTheory.MorphismProperty (CategoryTheory.Paths V)) [P.IsMultiplicative],
  (∀ {u v : V} (p : u ⟶ v), P ((CategoryTheory.Paths.of V).map p)) → P = ⊤
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : AddZeroClass α] [inst_4 : AddZeroClass β] [inst_5 : AddZeroClass γ] {g₁ g₂ : β →+o γ} {f : α →+o β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Data.List.Forall2
List.forall₂_and_left : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {p : α → Prop} (l : List α) (u : List β),
  List.Forall₂ (fun a b => p a ∧ R a b) l u ↔ (∀ a ∈ l, p a) ∧ List.Forall₂ R l u
-- Init.Prelude
/-- Throws an exception of type `ε` to the nearest enclosing handler.
 -/
EStateM.throw : {ε σ α : Type u} → ε → EStateM ε σ α
-- Mathlib.Data.ZMod.Basic
ZMod.val_eq_one : ∀ {n : ℕ}, 1 < n → ∀ (a : ZMod n), a.val = 1 ↔ a = 1
-- Mathlib.RingTheory.Localization.AtPrime.Basic
_private.Mathlib.RingTheory.Localization.AtPrime.Basic.0.IsLocalization.AtPrime.termPSₚ : Lean.ParserDescr
-- Mathlib.Order.Filter.Pointwise
Filter.neg_atTop : ∀ {G : Type u_7} [inst : AddCommGroup G] [inst_1 : Preorder G] [IsOrderedAddMonoid G], -Filter.atTop = Filter.atBot
-- Init.Data.SInt.Lemmas
Int32.sub_eq_add_neg : ∀ (a b : Int32), a - b = a + -b
-- Init.Data.Array.Attach
List.pmap_toArray : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {P : α → Prop} {f : (a : α) → P a → β} {H : ∀ a ∈ l.toArray, P a},
  Array.pmap f l.toArray H = (List.pmap f l ⋯).toArray
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.mem_resolventSet_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : A},
  r ∈ resolventSet R a ↔ IsUnit ((algebraMap R A) r - a)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.lt_invVeblen₂_iff : ∀ {a x : Ordinal.{u}}, a < x.invVeblen₂ ↔ Ordinal.veblen x.invVeblen₁ a < Ordinal.omega0 ^ x
-- Mathlib.MeasureTheory.Order.Lattice
AEMeasurable.const_inf : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → M} [inst_1 : Min M] [MeasurableInf M], AEMeasurable f μ → ∀ (c : M), AEMeasurable (fun x => c ⊓ f x) μ
-- Mathlib.Data.Nat.Sqrt
Nat.not_exists_sq' : ∀ {m n : ℕ}, m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.Head.lambda : Mathlib.Tactic.Push.Head
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.numLitNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.mk.inj : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  {map : SSet.stdSimplex.obj { len := n + 1 } ⟶ X}
  {δ_castSucc_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map = g.map)
      SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam}
  {δ_succ_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map = fg.map)
      SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam}
  {δ_succ_succ_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map = f.map)
      SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam}
  {δ_map_of_lt :
    autoParam (∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam}
  {δ_map_of_gt :
    autoParam
      (∀ (j : Fin (n + 2)),
        i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam}
  {map_1 : SSet.stdSimplex.obj { len := n + 1 } ⟶ X}
  {δ_castSucc_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map_1 = g.map)
      SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam}
  {δ_succ_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map_1 = fg.map)
      SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam}
  {δ_succ_succ_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map_1 = f.map)
      SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam}
  {δ_map_of_lt_1 :
    autoParam (∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam}
  {δ_map_of_gt_1 :
    autoParam
      (∀ (j : Fin (n + 2)),
        i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam},
  { map := map, δ_castSucc_castSucc_map := δ_castSucc_castSucc_map, δ_succ_castSucc_map := δ_succ_castSucc_map,
        δ_succ_succ_map := δ_succ_succ_map, δ_map_of_lt := δ_map_of_lt, δ_map_of_gt := δ_map_of_gt } =
      { map := map_1, δ_castSucc_castSucc_map := δ_castSucc_castSucc_map_1,
        δ_succ_castSucc_map := δ_succ_castSucc_map_1, δ_succ_succ_map := δ_succ_succ_map_1,
        δ_map_of_lt := δ_map_of_lt_1, δ_map_of_gt := δ_map_of_gt_1 } →
    map = map_1
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer.normal.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (promise : IO.Promise (Option α)),
  sizeOf (Std.CloseableChannel.Consumer.normal✝ promise) = 1 + sizeOf promise
-- Mathlib.Data.Num.Basic
/-- `bit b n` appends the bit `b` to the end of `n`, where `bit tt x = x1` and `bit ff x = x0`.  -/
PosNum.bit : Bool → PosNum → PosNum
-- Init.Data.Bool
Bool.xor_self : ∀ (x : Bool), (x ^^ x) = false
-- Lean.Language.Basic
/-- Arbitrary value paired with a syntax that should be inspected when considering the value for reuse.
 -/
Lean.Language.SyntaxGuarded : Type → Type
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.ι_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ) {Z : CochainComplex C ℤ}
  (h : L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.ι✝ f n)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.π✝ f n) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Analysis.InnerProductSpace.NormPow
differentiable_norm_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {p : ℝ},
  1 < p → Differentiable ℝ fun x => ‖x‖ ^ p