mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatch_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch p pos ↔
    ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯)
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.fg : ∀ {R : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M] {S : Submodule R M},
  S.IsPrincipal → S.FG
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- A homeomorphism between two Borel spaces is a measurable equivalence.  -/
Homeomorph.toMeasurableEquiv : {γ : Type u_3} →
  {γ₂ : Type u_4} →
    [inst : TopologicalSpace γ] →
      [inst_1 : MeasurableSpace γ] →
        [BorelSpace γ] →
          [inst_3 : TopologicalSpace γ₂] → [inst_4 : MeasurableSpace γ₂] → [BorelSpace γ₂] → γ ≃ₜ γ₂ → γ ≃ᵐ γ₂
-- Mathlib.Algebra.Tropical.Basic
Tropical.instAddCommMonoidTropical : {R : Type u} → [inst : LinearOrder R] → [OrderTop R] → AddCommMonoid (Tropical R)
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- The `AddSubmonoid`s of an `AddMonoid` form a complete lattice.  -/
AddSubmonoid.instCompleteLattice : {M : Type u_1} → [inst : AddZeroClass M] → CompleteLattice (AddSubmonoid M)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false} {fallback : α},
      Std.Internal.List.getKeyD (Std.Internal.List.maxKey l he) l fallback = Std.Internal.List.maxKey l he
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.instReprHeap : {α : Type u_1} → [Repr α] → Repr (Batteries.PairingHeapImp.Heap α)
-- Aesop.Tree.Data
Aesop.instNonemptyTreeSpec : Nonempty Aesop.TreeSpec
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.getIntCastFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m Lean.Expr
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.State.cache : Lean.Elab.Tactic.Grind.State → Lean.Elab.Tactic.Grind.Cache
-- Mathlib.CategoryTheory.Abelian.Basic
/-- An abelian category has strong epi-mono factorisations.  -/
CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasStrongEpiMonoFactorisations C
-- Mathlib.Algebra.Group.Basic
sub_zero : ∀ {G : Type u_3} [inst : SubNegZeroMonoid G] (a : G), a - 0 = a
-- Mathlib.Analysis.SpecialFunctions.Arsinh
ContinuousOn.arsinh : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ} {s : Set X},
  ContinuousOn f s → ContinuousOn (fun x => Real.arsinh (f x)) s
-- Mathlib.GroupTheory.IsSubnormal
/-- A subnormal subgroup is either the whole group or it is contained in a proper normal subgroup.
 -/
Subgroup.IsSubnormal.lt_normal : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.IsSubnormal → H = ⊤ ∨ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
-- Mathlib.RingTheory.Ideal.Nonunits
Submonoid.mem_nonunits_iff_or : ∀ {α : Type u_2} {C : Type u_4} [inst : SetLike C α] [inst_1 : GroupWithZero α] [inst_2 : SubmonoidClass C α] {S : C}
  {a : ↥S}, a ∈ nonunits ↥S ↔ ↑a = 0 ∨ (↑a)⁻¹ ∉ S
-- Lean.Meta.AbstractMVars
Lean.Meta.openAbstractMVarsResult : Lean.Meta.AbstractMVarsResult → Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_le_ceil : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R), ⌊a⌋ ≤ ⌈a⌉
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.liminf_add_of_left_tendsto_zero : ∀ {ι : Type u_4} {u : Filter ι} {f : ι → ENNReal},
  Filter.Tendsto f u (nhds 0) → ∀ (g : ι → ENNReal), Filter.liminf (f + g) u = Filter.liminf g u
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified_iff_mult_le : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsUnramified k w ↔ w.mult ≤ (w.comap (algebraMap k K)).mult
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
/-- If `{x_i : A | i : ι}` is algebraically independent over `R`, and for each `i`,
`f_i : R[X]` is transcendental over `R`, then `{f_i(x_i) | i : ι}` is also
algebraically independent over `R`.  -/
AlgebraicIndependent.polynomial_aeval_of_transcendental : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x →
    ∀ {f : ι → Polynomial R},
      (∀ (i : ι), Transcendental R (f i)) → AlgebraicIndependent R fun i => (Polynomial.aeval (x i)) (f i)
-- Lean.Environment
Lean.instInhabitedModuleIdx : Inhabited Lean.ModuleIdx
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.injectiveDimension_eq_bot_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.injectiveDimension X = ⊥ ↔ CategoryTheory.Limits.IsZero X
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C} (X : C),
  J.Saturate X ⊤
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.mul_congr.wr : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Mul α] [Lean.Grind.ToInt.Mul α i],
  i.isFinite = true → ∀ {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = i.wrap b' → ↑(a * b) = i.wrap (a' * b')
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k a : α} {v : β},
      Std.DHashMap.Internal.Raw₀.Const.get? (m.insert k v) a =
        if (k == a) = true then some v else Std.DHashMap.Internal.Raw₀.Const.get? m a
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- A union of finitely many `IsRkFinite` sets is `IsRkFinite`.  -/
Matroid.IsRkFinite.iUnion : ∀ {α : Type u_1} {M : Matroid α} {ι : Type u_2} [Finite ι] {Xs : ι → Set α},
  (∀ (i : ι), M.IsRkFinite (Xs i)) → M.IsRkFinite (⋃ i, Xs i)
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `M` is flat, then for any submodule `N'` of `N`,
`M` and `N'` are also linearly disjoint.  -/
Submodule.LinearDisjoint.of_le_right_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → ∀ {N' : Submodule R S}, N' ≤ N → ∀ [Module.Flat R ↥M], M.LinearDisjoint N'
-- Mathlib.Algebra.Group.End
Equiv.addRight_add : ∀ {α : Type u_4} [inst : AddGroup α] (a b : α), Equiv.addRight (a + b) = Equiv.addRight b * Equiv.addRight a
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_natCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocDiv hp (a + ↑m * p) b = toIocDiv hp a b - ↑m
-- Init.Data.ByteArray.Lemmas
List.toByteArray_inj : ∀ {l l' : List UInt8}, l.toByteArray = l'.toByteArray ↔ l = l'
-- Mathlib.Analysis.Normed.Operator.Banach
/-- First step of the proof of the Banach open mapping theorem (using completeness of `F`):
by Baire's theorem, there exists a ball in `E` whose image closure has nonempty interior.
Rescaling everything, it follows that any `y ∈ F` is arbitrarily well approached by
images of elements of norm at most `C * ‖y‖`.
For further use, we will only need such an element whose image
is within distance `‖y‖/2` of `y`, to apply an iterative process.  -/
ContinuousLinearMap.exists_approx_preimage_norm_le : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ']
  [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F],
  Function.Surjective ⇑f → ∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
-- Mathlib.Data.Finset.Filter
Finset.filter.congr_simp : ∀ {α : Type u_1} (p p_1 : α → Prop),
  p = p_1 →
    ∀ {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (s s_1 : Finset α),
      s = s_1 → Finset.filter p s = Finset.filter p_1 s_1
-- Mathlib.LinearAlgebra.AffineSpace.Slope
sub_smul_slope_vadd : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE) (a b : k), (b - a) • slope f a b +ᵥ f a = f b
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.pos_or_neg_of_sum_smul_root_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [CharZero R] (f : ι → ℤ),
  ∑ j ∈ b.support, f j • P.root j ∈ Set.range ⇑P.root → Function.support f ⊆ ↑b.support → 0 < f ∨ f < 0
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invOneSubPow_inv_zero_eq_one : ∀ (S : Type u_1) [inst : CommRing S], (PowerSeries.invOneSubPow S 0).inv = 1
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.span_range_relation_eq_ker_comp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) [inst_5 : Algebra R T]
  [inst_6 : IsScalarTower R S T],
  Ideal.span (Set.range (Sum.elim (Q.compRelationAux P) fun rp => (MvPolynomial.rename Sum.inr) (P.relation rp))) =
    (Q.comp P.toGenerators).ker
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Icc_right_eq_Icc_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {a b : α},
  a ≤ Order.succ b → insert (Order.succ b) (Finset.Icc a b) = Finset.Icc a (Order.succ b)
-- Mathlib.RingTheory.DedekindDomain.SInteger
/-- If `S` is the whole set of places of `K`, then the `S`-integers are the whole of `K`.  -/
IsDedekindDomain.integer_univ : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K], Set.univ.integer K = ⊤
-- Mathlib.Algebra.Ring.BooleanRing
RingHom.asBoolAlg_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : BooleanRing α] [inst_1 : BooleanRing β] [inst_2 : BooleanRing γ]
  (g : β →+* γ) (f : α →+* β), (g.comp f).asBoolAlg = g.asBoolAlg.comp f.asBoolAlg
-- Lean.Data.Json.Basic
Lean.Json.brecOn_1.go : {motive_1 : Lean.Json → Sort u} →
  {motive_2 : Array Lean.Json → Sort u} →
    {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} →
      {motive_4 : List Lean.Json → Sort u} →
        {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u} →
          {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} →
            (t : Array Lean.Json) →
              ((t : Lean.Json) → t.below → motive_1 t) →
                ((t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t) →
                  ((t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t) →
                    ((t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t) →
                      ((t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t) →
                        ((t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) →
                            Lean.Json.below_5 t → motive_6 t) →
                          motive_2 t ×' Lean.Json.below_1 t
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.isBasis_insert_iff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e : α},
  M.Indep I → (M.IsBasis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.add_comm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Topology.Separation.CompletelyRegular
completelyRegularSpace_iff_isOpen : ∀ {X : Type u} [inst : TopologicalSpace X],
  CompletelyRegularSpace X ↔ ∀ (x : X) (K : Set X), IsOpen K → x ∈ K → ∃ f, Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 Kᶜ
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.nonempty : ∀ {X : Type u} [inst : PartialOrder X] (self : PartialOrder.NonemptyFiniteChains X), self.finset.Nonempty
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.smul_apply : ∀ {α : Type u_1} {R : Type u_6} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal]
  {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α) (s : Set α), (c • μ) s = c • μ s
-- Mathlib.Data.LawfulXor.Basic
xor_eq_iff_left_eq : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] (a b c : α), a ^^^ b = c ↔ a = c ^^^ b
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- The isomorphism `ε : L.obj (𝟙_ C) ≅ unit`,
as `(toMonoidalCategory L W ε).obj (𝟙_ C) ≅ unit`.  -/
CategoryTheory.Localization.Monoidal.ε' : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
                          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅
                        unit
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.generator_eq_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E = ⊥ → RatFunc.Luroth.generator E = 0
-- Lean.Parser.Command
Lean.Parser.Command.openRenaming.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
multipliable_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  ¬L.NeBot → ∀ (f : β → α), Multipliable f L
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.indicesPos : Lean.Meta.RecursorInfo → List ℕ
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
/-- Copy of a preordering with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
RingPreordering.copy : {R : Type u_1} → [inst : CommRing R] → (P : RingPreordering R) → (S : Set R) → S = ↑P → RingPreordering R
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableAt.continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F]
  [ContinuousSMul 𝕜 F], DifferentiableAt 𝕜 f x → ContinuousAt f x
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftLeft_and_distrib : ∀ {i a b : ℕ}, (a &&& b) <<< i = a <<< i &&& b <<< i
-- Init.Data.ByteArray.Basic
ByteArray.toList.loop : ByteArray → ℕ → List UInt8 → List UInt8
-- Mathlib.RingTheory.Valuation.AlgebraInstances
ValuationSubring.algebraMap_injective : ∀ {K : Type u_1} [inst : Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [inst_1 : Field L]
  [inst_2 : Algebra K L], Function.Injective ⇑(algebraMap (↥v.valuationSubring) L)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.nnnorm_lt_iff : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)) {M : NNReal}, 0 < M → (‖f‖₊ < M ↔ ∀ (x : α), ‖f x‖₊ < M)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ) [t.IsGE X a],
  t.IsGE ((t.truncLE b).obj X) a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.isIso_inr_iso_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y : C} {inl inr : X ⟶ P} {f : Y ⟶ X},
  CategoryTheory.IsPushout f f inl inr →
    autoParam (CategoryTheory.Epi f) CategoryTheory.IsPushout.isIso_inr_iso_of_epi._auto_1 → CategoryTheory.IsIso inr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} (hom hom_1 : M.X ⟶ N.X) (e_hom : hom = hom_1)
  [isMonHom_hom : CategoryTheory.IsMonHom hom],
  { hom := hom, isMonHom_hom := isMonHom_hom } = { hom := hom_1, isMonHom_hom := ⋯ }
-- Mathlib.Algebra.Category.Grp.Ulift
CommGrpCat.instCreatesLimitsOfSizeUliftFunctor.eq_1 : CommGrpCat.instCreatesLimitsOfSizeUliftFunctor =
  {
    CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, u} J] =>
      { CreatesLimit := fun {x} => CategoryTheory.createsLimitOfFullyFaithfulOfPreserves } }
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNeg.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Neg β],
  MeasureTheory.SimpleFunc.instNeg = { neg := fun f => MeasureTheory.SimpleFunc.map Neg.neg f }
-- Std.Time.Format.Modifier
Std.Time.Modifier.B.sizeOf_spec : ∀ (presentation : Std.Time.Text), sizeOf (Std.Time.Modifier.B presentation) = 1 + sizeOf presentation
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.directedSystem : ∀ {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) [inst_1 : (i : ι) → AddCommMonoid (G i)]
  (f : (i j : ι) → i ≤ j → G i →+ G j) [h : DirectedSystem G fun i j h => ⇑(f i j h)],
  DirectedSystem G fun i j hij => ⇑(f i j hij).toNatLinearMap
-- Mathlib.NumberTheory.Basic
dvd_sub_pow_of_dvd_sub : ∀ {R : Type u_1} [inst : CommRing R] {p : ℕ} {a b : R}, ↑p ∣ a - b → ∀ (k : ℕ), ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isConnected_eball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal},
  0 < r → IsConnected (Metric.eball x r)
-- Mathlib.Analysis.Normed.Operator.NNNorm
/-- For a continuous real linear map `f`, if one controls the norm of every `f x`, `‖x‖₊ = 1`, then
one controls the norm of `f`.  -/
ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  [NormedAlgebra ℝ 𝕜] {f : E →SL[σ₁₂] F} {C : NNReal}, (∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C) → ‖f‖₊ ≤ C
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instDist : {X : Type u_1} → {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [Dist X] → Dist (Metric.Snowflaking X α hα₀ hα₁)
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.mul_apply_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (m x2 : A), ((LinearMap.mul R A) m) x2 = m * x2
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_div : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∫ (x : ℝ) in a..b, f (x / c) = c • ∫ (x : ℝ) in a / c..b / c, f x
-- Mathlib.Data.PNat.Find
PNat.find_min' : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) {m : ℕ+}, p m → PNat.find h ≤ m
-- Mathlib.NumberTheory.PrimeCounting
Nat.tendsto_primeCounting : Filter.Tendsto Nat.primeCounting Filter.atTop Filter.atTop
-- Mathlib.Order.DirSupClosed
DirSupClosed.empty : ∀ {α : Type u_1} [inst : Preorder α], DirSupClosed ∅
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The bivariate polynomials `φₙ`.  -/
WeierstrassCurve.φ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → ℤ → Polynomial (Polynomial R)
-- Mathlib.Tactic.FunProp.Theorems
/-- Get morphism theorems applicable to `e`.

For example calling on `e` equal to `Continuous f` for `f : X→L[ℝ] Y` would return theorem
inferring continuity from the bundled morphism.  -/
Mathlib.Meta.FunProp.getMorphismTheorems : Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Array Mathlib.Meta.FunProp.GeneralTheorem)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.sat_def : ∀ {α : Type u_1} (a : α → Bool) (f : Std.Sat.CNF α), Std.Sat.CNF.Sat a f ↔ Std.Sat.CNF.eval a f = true
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalCommRing : {R : Type u_1} → {M : Type u_4} → [inst : CommRing R] → [AddCommSemigroup M] → NonUnitalCommRing (AddMonoidAlgebra R M)
-- Mathlib.Order.Filter.IndicatorFunction
Antitone.mulIndicator_eventuallyEq_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Preorder ι] [inst_1 : One β] (s : ι → Set α),
  Antitone s →
    ∀ (f : α → β) (a : α), (fun i => (s i).mulIndicator f a) =ᶠ[Filter.atTop] fun x => (⋂ i, s i).mulIndicator f a
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instModule : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → Module R (M →ₚₗ[R] N)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.modDocstringStateExt : Lean.EnvExtension (Option Lean.Doc.ModuleDocstringState✝)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_pow_orderOf_div : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, orderOf x ≠ 0 → n ∣ orderOf x → orderOf (x ^ (orderOf x / n)) = n
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.le_infDegree_add : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : Semiring R] [inst_1 : SemilatticeInf T] [inst_2 : OrderTop T]
  (D : A → T) (f g : AddMonoidAlgebra R A),
  AddMonoidAlgebra.infDegree D f ⊓ AddMonoidAlgebra.infDegree D g ≤ AddMonoidAlgebra.infDegree D (f + g)
-- Mathlib.Logic.Function.CompTypeclasses
/-- The maps form a commuting triangle  -/
CompTriple.comp_eq : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} {φ : M → N} {ψ : N → P} {χ : outParam (M → P)} [self : CompTriple φ ψ χ],
  ψ ∘ φ = χ
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.eventually : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f p s x → ∀ᶠ (r : ENNReal) in nhdsWithin 0 (Set.Ioi 0), HasFPowerSeriesWithinOnBall f p s x r