mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.node.inj : ∀ {α : Type u} {a : α} {child sibling : Batteries.BinomialHeap.Imp.HeapNode α} {a_1 : α}
  {child_1 sibling_1 : Batteries.BinomialHeap.Imp.HeapNode α},
  Batteries.BinomialHeap.Imp.HeapNode.node a child sibling =
      Batteries.BinomialHeap.Imp.HeapNode.node a_1 child_1 sibling_1 →
    a = a_1 ∧ child = child_1 ∧ sibling = sibling_1
-- Init.Data.Repr
ReprAtom.mk : {α : Type u} → ReprAtom α
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasAbsLeftKanExtension.commute : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [self : CategoryTheory.Bicategory.HasAbsLeftKanExtension f g] {x : B} (h : c ⟶ x),
  CategoryTheory.Bicategory.Lan.CommuteWith f g h
-- Mathlib.RingTheory.Kaehler.TensorProduct
/-- (Implementation). `A`-module structure on `S ⊗[R] Ω[A⁄R]`.  -/
KaehlerDifferential.moduleBaseChange : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] → [inst_3 : CommRing A] → [inst_4 : Algebra R A] → Module A (TensorProduct R S Ω[A⁄R])
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_subtype_max : ∀ {X : Type u_1} {P₁ P₂ : X → Prop} {κ : Cardinal.{u_2}},
  Cardinal.aleph0 ≤ κ →
    HasCardinalLT (Subtype P₁) κ → HasCardinalLT (Subtype P₂) κ → HasCardinalLT (Subtype (P₁ ⊔ P₂)) κ
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_add_le : ∀ {r p : ℝ}, (r + p).toNNReal ≤ r.toNNReal + p.toNNReal
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.compl : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, BaireMeasurableSet s → BaireMeasurableSet sᶜ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.eq_of_toPoly_nc_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (a b : Lean.Grind.CommRing.Expr),
  (a.toPoly_nc == b.toPoly_nc) = true → Lean.Grind.CommRing.Expr.denote ctx a = Lean.Grind.CommRing.Expr.denote ctx b
-- Mathlib.Algebra.Group.Finsupp
/-- Composition with a fixed zero-preserving homomorphism is itself a zero-preserving homomorphism
on functions.  -/
Finsupp.mapRange.zeroHom : {ι : Type u_1} →
  {M : Type u_3} → {N : Type u_4} → [inst : Zero M] → [inst_1 : Zero N] → ZeroHom M N → ZeroHom (ι →₀ M) (ι →₀ N)
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCoreAux_balanced : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E}, 0 ∈ balancedCoreAux 𝕜 s → Balanced 𝕜 (balancedCoreAux 𝕜 s)
-- Mathlib.Order.Defs.Unbundled
IsLinearOrder.mk : ∀ {α : Sort u_1} {r : α → α → Prop} [toIsPartialOrder : IsPartialOrder α r] [toTotal : Std.Total r], IsLinearOrder α r
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- The canonical `R`-algebra isomorphism between `WithVal v` and `S`, when `v : Valuation S Γ₀`.  -/
WithVal.algEquiv : (R : Type u_1) →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      {S : Type u_3} →
        [inst_1 : CommSemiring R] →
          [inst_2 : Ring S] → [inst_3 : Algebra R S] → (v : Valuation S Γ₀) → WithVal v ≃ₐ[R] S
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instAddMonObjTensorObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N],
  CategoryTheory.AddMon.instAddMonObjTensorObj =
    {
      zero :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero CategoryTheory.AddMonObj.zero),
      add :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.tensorμ { X := M, addMon := inst_3 }.X { X := N, addMon := inst_4 }.X
            { X := M, addMon := inst_3 }.X { X := N, addMon := inst_4 }.X)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add),
      zero_add := ⋯, add_zero := ⋯, add_assoc := ⋯ }
-- Mathlib.Data.Nat.PrimeFin
/-- **Alias** of `Nat.infinite_setOfPred_prime`.

---

A version of `Nat.exists_infinite_primes` using the `Set.Infinite` predicate.  -/
Nat.infinite_setOf_prime : {p | Nat.Prime p}.Infinite
-- Mathlib.Topology.Baire.Lemmas
/-- If a countable family of closed sets cover a dense `Gδ` set, then the union of their interiors
is dense. Formulated here with `⋃₀`.  -/
IsGδ.dense_sUnion_interior_of_closed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {T : Set (Set X)} {s : Set X},
  IsGδ s → Dense s → T.Countable → (∀ t ∈ T, IsClosed t) → s ⊆ ⋃₀ T → Dense (⋃ t ∈ T, interior t)
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.monoModSerre_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
  P.monoModSerre f
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.mk.sizeOf_spec : ∀ {G : Type u_6} [inst : Group G] [inst_1 : SizeOf G] (toFun : G → ℝ) (map_one' : toFun 1 = 0)
  (mul_le' : ∀ (x y : G), toFun (x * y) ≤ toFun x + toFun y) (inv' : ∀ (x : G), toFun x⁻¹ = toFun x),
  sizeOf { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' } = 1 + sizeOf map_one'
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.not_mem_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → k ∉ m₁ ∩ m₂
-- Mathlib.Topology.Order.Monotone
/-- In a second countable space, the set of points where an antitone function is not continuous
within a set is at most countable.  -/
AntitoneOn.countable_not_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β]
  {s : Set α}, AntitoneOn f s → {x | x ∈ s ∧ ¬ContinuousWithinAt f s x}.Countable
-- Lean.ToExpr
Lean.instToExprUnit : Lean.ToExpr Unit
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {f : α → β → Bool}
  {k k' : α} {fallback : β},
  t.WF →
    t.getKey? k = some k' →
      (Std.TreeMap.Raw.filter f t).getD k fallback = (Option.filter (fun x => f k' x) t[k]?).getD fallback
-- Mathlib.Topology.WithTopology
WithTopology.ofTopology_bijective : ∀ {X : Type u_1} (t : TopologicalSpace X), Function.Bijective WithTopology.ofTopology
-- Mathlib.CategoryTheory.CopyDiscardCategory.Basic
/-- Category where objects have compatible copy and discard operations.  -/
CategoryTheory.CopyDiscardCategory : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_inj : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α}, ↑U = ↑V ↔ U = V
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.num_eq_zero : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K), IsFractionRing.num A x = 0 ↔ x = 0
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instCategoryWithCofibrationsOpposite : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithFibrations C] → HomotopicalAlgebra.CategoryWithCofibrations Cᵒᵖ
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiff.norm_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {n : WithTop ℕ∞}, ContDiff ℝ n f → ContDiff ℝ n fun x => ‖f x‖ ^ 2
-- Std.Internal.Do.WP.Basic
/-- Weakest precondition interpretation of a program type `Prog` whose results have type `Value`,
as a monotone predicate transformer over assertion language `Pred` with exception postconditions
`EPred`.  -/
Std.Internal.Do.WP : Type u →
  outParam (Type v) →
    (Pred : outParam (Type w)) →
      (EPred : outParam (Type w')) →
        [Std.Internal.Do.Assertion Pred] → [Std.Internal.Do.Assertion EPred] → Type (max (max (max u v) w) w')
-- Mathlib.RingTheory.Nakayama
Submodule.eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {N N' : Submodule R M}, N.FG → I ≤ ⊥.jacobson → Submodule.map (I • N).mkQ N = Submodule.map (I • N).mkQ N' → N = N'
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_neg_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Neg.neg '' Set.Ioc a b = Set.Ico (-b) (-a)
-- Mathlib.Data.List.Basic
List.length_pos_iff_ne_nil : ∀ {α : Type u} {l : List α}, 0 < l.length ↔ l ≠ []
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- Linear disjointness is preserved by injective algebra homomorphisms.  -/
Submodule.LinearDisjoint.map : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ {T : Type w} [inst_3 : Semiring T] [inst_4 : Algebra R T] (f : S →ₐ[R] T),
      Function.Injective ⇑f → (Submodule.map (↑f) M).LinearDisjoint (Submodule.map (↑f) N)
-- Mathlib.Topology.Bases
Topology.IsQuotientMap.separableSpace : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [inst : TopologicalSpace β]
  {f : α → β}, Topology.IsQuotientMap f → TopologicalSpace.SeparableSpace β
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.of_subsingleton : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [Subsingleton α] [MeasureTheory.IsFiniteMeasure μ] {f : α → β}, MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.instInhabitedSheafBotGrothendieckTopologyType : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → Inhabited (CategoryTheory.Sheaf ⊥ (Type w))
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.addLeftStrictMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddMonoid (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddLeftStrictMono (α i)],
  AddLeftStrictMono (Colex (Π₀ (i : ι), α i))
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conj_pow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.End X) (n : ℕ),
  α.conj (f ^ n) = α.conj f ^ n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_multiplicative_iff : ∀ {α : Type u_1} [inst : SubNegMonoid α], IsCyclic (Multiplicative α) ↔ IsAddCyclic α
-- Mathlib.Data.List.Lookmap
_private.Mathlib.Data.List.Lookmap.0.List.lookmap.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (b : α) (h_1 : (b : α) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.instCoeSortType.eq_1 : Semigrp.instCoeSortType = { coe := Semigrp.carrier }
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Convert a term syntax to a grindParam syntax (wrapping in grindLemma).
If the term is a simple identifier (like `pi_pos`), wrap it in an explicit application
`(id pi_pos)` so grind treats it as a term rather than an e-matching theorem.  -/
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.termToGrindParam : Lean.Syntax → Lean.Syntax
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.emptyAt.injEq : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.endPos) (pos_1 : s.Pos) (h_1 : pos_1 ≠ s.endPos),
  (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h =
      String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos_1 h_1) =
    (pos = pos_1)
-- Mathlib.Algebra.Group.Action.Faithful
/-- `AddMonoid.toAddAction` is faithful on additive cancellative monoids.  -/
AddRightCancelMonoid.faithfulVAdd : ∀ {α : Type u_3} [inst : AddRightCancelMonoid α], FaithfulVAdd α α
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- A linear equivalence which maps a submodule of one module onto another, restricts to a linear
equivalence of the two submodules.  -/
LinearEquiv.ofSubmodules : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {module_M : Module R M} →
                  {module_M₂ : Module R₂ M₂} →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                          {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                            (e : M ≃ₛₗ[σ₁₂] M₂) →
                              (p : Submodule R M) → (q : Submodule R₂ M₂) → Submodule.map (↑e) p = q → ↥p ≃ₛₗ[σ₁₂] ↥q
-- Mathlib.Order.Lattice.Congruence
LatticeCon.mk.inj : ∀ {α : Type u_2} {inst : Lattice α} {toSetoid : Setoid α}
  {inf : ∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊓ y) (x ⊓ z)}
  {sup : ∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊔ y) (x ⊔ z)} {toSetoid_1 : Setoid α}
  {inf_1 : ∀ {w x y z : α}, toSetoid_1 w x → toSetoid_1 y z → toSetoid_1 (w ⊓ y) (x ⊓ z)}
  {sup_1 : ∀ {w x y z : α}, toSetoid_1 w x → toSetoid_1 y z → toSetoid_1 (w ⊔ y) (x ⊔ z)},
  { toSetoid := toSetoid, inf := inf, sup := sup } = { toSetoid := toSetoid_1, inf := inf_1, sup := sup_1 } →
    toSetoid = toSetoid_1
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y) (x : ↑Y.toTopCat),
  IsLocalHom
    (CommRingCat.Hom.hom
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap
        (CategoryTheory.Limits.coequalizer.π (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
            (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).hom
        x))
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion, it is a submersion at each point.  -/
Manifold.IsSubmersionOfComplement.isSubmersionAt : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsSubmersionOfComplement F I J n f → ∀ (x : M), Manifold.IsSubmersionAtOfComplement F I J n f x
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1),
  stereographic hv = stereographic hv
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element that is greater than the given element,
panicking if no such element exists.
 -/
Std.TreeSet.Raw.getGT! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet.Raw α cmp → α → α
-- Mathlib.Analysis.Convex.Between
wbtw_iff_left_eq_or_right_mem_image_Ici : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z ↔ x = y ∨ z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ici 1
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
/-- Whisker a `V`-enriched natural transformation on the left.  -/
CategoryTheory.EnrichedCat.whiskerLeft : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₁} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              {E : Type u₂} →
                [inst_4 : CategoryTheory.EnrichedCategory V E] →
                  (F : CategoryTheory.EnrichedFunctor V C D) →
                    {G H : CategoryTheory.EnrichedFunctor V D E} →
                      (G ⟶ H) → (CategoryTheory.EnrichedFunctor.comp V F G ⟶ CategoryTheory.EnrichedFunctor.comp V F H)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_zpow_left₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀} [MulPosMono G₀]
  {n : ℤ}, 0 < n → 0 ≤ a → a < b → a ^ n < b ^ n
-- Mathlib.Algebra.Free
FreeSemigroup.instLawfulTraversable : LawfulTraversable FreeSemigroup
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_eq_singleton : ∀ {m n : ℤ}, n = m + 1 → (m...n).toList = [m]
-- Mathlib.Order.Cover
Prod.mk_wcovBy_mk_iff_left : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {a₁ a₂ : α} {b : β},
  (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂
-- Mathlib.Data.Set.Function
Set.eqOn_comp_right_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : α → β} {g₁ g₂ : β → γ},
  Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s ↔ Set.EqOn g₁ g₂ (f '' s)
-- Mathlib.Tactic.Simproc.FinsetInterval
/-- Simproc to compute `Finset.Ioo a b` where `a` and `b` are numerals.

**Warnings**:
* With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
* Make sure to exclude `Finset.insert_eq_of_mem` from your simp call when using this simproc. This
  avoids a quadratic time performance hit.  -/
Finset.Ioo_ofNat_ofNat : Lean.Meta.Simp.Simproc
-- Lean.Parser.Term
Lean.Parser.Termination.inductiveFixpoint.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' fallback : α} {f : Option β → Option β},
      (t.alter k f).getKeyD k' fallback =
        if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then k else fallback else t.getKeyD k' fallback
-- Mathlib.RingTheory.RootsOfUnity.Basic
restrictRootsOfUnity_coe_apply : ∀ {R : Type u_4} {S : Type u_5} {F : Type u_6} {k : ℕ} [inst : CommMonoid R] [inst_1 : CommMonoid S]
  [inst_2 : FunLike F R S] [inst_3 : MonoidHomClass F R S] (σ : F) (ζ : ↥(rootsOfUnity k R)),
  ↑↑((restrictRootsOfUnity σ k) ζ) = σ ↑↑ζ
-- Mathlib.FieldTheory.Finite.Extension
Irreducible.natDegree_dvd_iff_dvd_X_pow_card_pow_sub_X : ∀ {k : Type u_1} [inst : Field k] [Finite k] {f : Polynomial k},
  Irreducible f → ∀ {n : ℕ}, f.natDegree ∣ n ↔ f ∣ Polynomial.X ^ Nat.card k ^ n - Polynomial.X
-- Mathlib.Algebra.Ring.Action.Field
/-- Note that `smul_inv'` refers to the group case, and `smul_inv` has an additional inverse
on `x`.  -/
smul_inv'' : ∀ {M : Type u_1} [inst : Monoid M] {F : Type u_2} [inst_1 : DivisionRing F] [inst_2 : MulSemiringAction M F] (x : M)
  (m : F), x • m⁻¹ = (x • m)⁻¹
-- Mathlib.Data.Quot
Quotient.exists : ∀ {α : Sort u_3} {s : Setoid α} {p : Quotient s → Prop}, (∃ a, p a) ↔ ∃ a, p ⟦a⟧
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGE_iff_pairwise`. -/
List.SortedGE.pairwise : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGE → List.Pairwise (fun x1 x2 => x1 ≥ x2) l
-- Mathlib.Topology.Connected.Basic
connectedComponent_nonempty : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, (connectedComponent x).Nonempty
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castSucc_Ico : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.castSucc (Finset.Ico i j) = Finset.Ico i.castSucc j.castSucc
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.natDegree_scaleRoots : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (s : R), (p.scaleRoots s).natDegree = p.natDegree
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.llift_apply : ∀ (M : Type u_2) (R : Type u_5) (S : Type u_8) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (X : Type u_9) [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] (f : X → M) (x : X →₀ R),
  ((Finsupp.llift M R S X) f) x = ((Finsupp.lift M R X) f) x
-- Init.Data.Ord.Basic
List.instOrd : {α : Type u_1} → [Ord α] → Ord (List α)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.ite.inj : ∀ {α : Type} {a a_1 a_2 a_3 a_4 a_5 : Std.Tactic.BVDecide.BoolExpr α},
  a.ite a_1 a_2 = a_3.ite a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.IterM.step_flatMapAfterM.match_3.eq_1 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m γ) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (it₂ : Std.IterM m γ) → motive (some it₂)),
  (match none with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_1 ()
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- `qrSign` is multiplicative in the first argument.  -/
qrSign.mul_left : ∀ (m₁ m₂ n : ℕ), qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n
-- Lean.Meta.Tactic.Grind.EMatch
/-- Helper function for marking parts of `match`-equation theorem as "do-not-simplify"
`initApp` is the match-expression used to instantiate the `match`-equation.
It also introduce `Grind.MatchCond` at equation conditions. See `MatchCond.lean`.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.annotateMatchEqnType : Lean.Expr → Lean.Expr → Lean.Meta.Grind.EMatch.M Lean.Expr
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.instInhabitedArgReorder.default : Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.LinearAlgebra.Matrix.WithConv
instAlgebraWithConvMatrix : {m : Type u_1} →
  {n : Type u_2} →
    {α : Type u_3} →
      {β : Type u_4} →
        [inst : CommSemiring β] → [inst_1 : Semiring α] → [Algebra β α] → Algebra β (WithConv (Matrix m n α))
-- Mathlib.Order.Interval.Basic
Interval.pure_ne_bot : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Interval.pure a ≠ ⊥
-- Mathlib.Data.Nat.ModEq
AddCommGroup.ModEq.natCast : ∀ {M : Type u_1} [inst : AddCommMonoidWithOne M] {a b n : ℕ}, a ≡ b [MOD n] → ↑a ≡ ↑b [PMOD ↑n]
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).hom
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.mk f).arrow h
-- Lean.PrettyPrinter.Formatter
/-- Execute `x` and concatenate generated Format objects.  -/
Lean.PrettyPrinter.Formatter.concat : Lean.PrettyPrinter.FormatterM Unit → Lean.PrettyPrinter.FormatterM Unit
-- Batteries.Data.String.Legacy
/-- Folds a function over a string from the left, accumulating a value starting with `init`. The
accumulated value is combined with each character in order, using `f`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.foldl`.

Examples:
 * `"coffee tea water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2`
 * `"coffee tea and water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3`
 * `"coffee tea water".foldl (·.push ·) "" = "coffee tea water"`
 -/
String.Legacy.foldl : {α : Type u} → (α → Char → α) → α → String → α