mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.Reedy.Basic
/-- the degree of an object  -/
HomotopicalAlgebra.ReedyStructure.deg : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      [inst_1 : W₁.IsMultiplicative] →
        [inst_2 : W₂.IsMultiplicative] →
          {α : Type u_2} →
            [inst_3 : LinearOrder α] →
              [inst_4 : OrderBot α] →
                [inst_5 : SuccOrder α] → [inst_6 : WellFoundedLT α] → HomotopicalAlgebra.ReedyStructure W₁ W₂ α → C → α
-- Lean.Parser.Syntax
Lean.Parser.Command.macroTail.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of the forward direction of `continuousOn_inv_iff`. -/
ContinuousOn.of_inv : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G]
  [inst_3 : TopologicalSpace α] {f : α → G} {s : Set α}, ContinuousOn f⁻¹ s → ContinuousOn f s
-- Mathlib.SetTheory.Cardinal.EventuallyConst
Cardinal.eventuallyConst_of_antitone : ∀ {β : Type v} [inst : PartialOrder β] {f : Cardinal.{v} → β} [Small.{v, v} β],
  Antitone f → Filter.EventuallyConst f Filter.atTop
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.topologicalClosure.eq_1 : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [inst_2 : SeparatelyContinuousMul M]
  (s : Subsemigroup M), s.topologicalClosure = { carrier := closure ↑s, mul_mem' := ⋯ }
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_iff : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α},
  MeasurableSet s ↔ ∀ (t : Set α), m t = m (t ∩ s) + m (t \ s)
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.eqToEquivalenceFunctorIso_hom : ∀ {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (f : J → I)
  {i' j' : J} (h : i' = j'), (CategoryTheory.Pi.eqToEquivalenceFunctorIso C f h).hom = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.analyticAt_weierstrassPExcept : ∀ (L : PeriodPair) (l₀ : ℂ), AnalyticAt ℂ (L.weierstrassPExcept l₀) l₀
-- Init.Data.Int.Lemmas
Int.ofNat_add_ofNat : ∀ (m n : ℕ), ↑m + ↑n = ↑(m + n)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_negPart : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν], (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart = ν - μ
-- Mathlib.Algebra.Ring.Action.Basic
/-- `RingHom.applyMulSemiringAction` is faithful.  -/
RingHom.applyFaithfulSMul : ∀ (R : Type v) [inst : Semiring R], FaithfulSMul (R →+* R) R
-- Std.Http.Data.Headers.Basic
/-- Optional port.
 -/
Std.Http.Header.Host.port : Std.Http.Header.Host → Std.Http.URI.Port
-- Mathlib.Algebra.GCDMonoid.Nat
Int.nonneg_of_normalize_eq_self : ∀ {z : ℤ}, normalize z = z → 0 ≤ z
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The integral of an almost-everywhere strongly measurable function over `AddCircle T` is equal
to the integral over an interval $(t, t + T]$ in `ℝ` of its lift to `ℝ`.  -/
AddCircle.integral_preimage : ∀ (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (t : ℝ)
  (f : AddCircle T → E), ∫ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.LE.eq : {n : ℤ} → Std.Time.Internal.Bounded.LE n n
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSpace_const : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] (f : MeasureTheory.Filtration ι m) (i : ι),
  ⋯.measurableSpace = ↑f i
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.mk.inj : ∀ {ι : 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} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂} {inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂}
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {toHom : P.Hom Q}
  {bijective_weightMap : Function.Bijective ⇑toHom.weightMap}
  {bijective_coweightMap : Function.Bijective ⇑toHom.coweightMap} {toHom_1 : P.Hom Q}
  {bijective_weightMap_1 : Function.Bijective ⇑toHom_1.weightMap}
  {bijective_coweightMap_1 : Function.Bijective ⇑toHom_1.coweightMap},
  { toHom := toHom, bijective_weightMap := bijective_weightMap, bijective_coweightMap := bijective_coweightMap } =
      { toHom := toHom_1, bijective_weightMap := bijective_weightMap_1,
        bijective_coweightMap := bijective_coweightMap_1 } →
    toHom = toHom_1
-- Init.Data.Order.Ord
Std.ReflOrd.isLE_rfl : ∀ {α : Type u_1} [inst : Ord α] [Std.ReflOrd α] {a : α}, (compare a a).isLE = true
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.isPresentation_iff : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M),
  solution.IsPresentation ↔
    Submodule.span A (Set.range solution.var) = ⊤ ∧ solution.π.ker = Submodule.span A (Set.range relations.relation)
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- the name of the recursive function  -/
Lean.Elab.Structural.RecArgInfo.fnName : Lean.Elab.Structural.RecArgInfo → Lean.Name
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size
-- Mathlib.Algebra.Group.Equiv.Opposite
MonoidHom.op_symm_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : Mᵐᵒᵖ →* Nᵐᵒᵖ) (a : M),
  (MonoidHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the functor on the left component  -/
CategoryTheory.Limits.CatCospanTransform.left : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A' : Type u₄} →
                  {B' : Type u₅} →
                    {C' : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                CategoryTheory.Limits.CatCospanTransform F G F' G' → CategoryTheory.Functor A A'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_none : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∉ t → t[a]? = none
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctorMapMapIso_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} {Y₁ Y₂ : CategoryTheory.GradedObject J C₂}
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
  [inst_4 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] (e : X₁ ≅ X₂) (e' : Y₁ ≅ Y₂)
  (i : K),
  (CategoryTheory.GradedObject.mapBifunctorMapMapIso F p e e').hom i =
    CategoryTheory.GradedObject.mapBifunctorMapMap F p e.hom e'.hom i
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_pos_iff'`. -/
EMetric.diam_pos_iff' : ∀ {X : Type u_2} {s : Set X} [inst : EMetricSpace X], 0 < Metric.ediam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_sInf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S : Set (StarSubalgebra R A)} {x : A},
  x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.GroupTheory.QuotientGroup.Finite
/-- If `F` and `H` are finite such that `ker(G →+ H) = im(F →+ G)`, then `G` is finite.  -/
AddGroup.fintypeOfKerEqRange : {F : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : AddGroup F] →
        [inst_1 : AddGroup G] →
          [inst_2 : AddGroup H] → [Fintype F] → [Fintype H] → (f : F →+ G) → (g : G →+ H) → g.ker = f.range → Fintype G
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.nat_gcd_helper_1' : ∀ (x y a b : ℕ), y * b = x * a + 1 → x.gcd y = 1
-- Init.Grind.Ring.Basic
/-- Negation is the left inverse of addition.  -/
Lean.Grind.Ring.neg_add_cancel : ∀ {α : Type u} [self : Lean.Grind.Ring α] (a : α), -a + a = 0
-- Mathlib.Data.Set.Basic
Set.inter_union_distrib_left : ∀ {α : Type u} (s t u : Set α), s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
/-- The *spectral mapping theorem* for polynomials.  Note: the assumption `degree p > 0`
is necessary in case `σ a = ∅`, for then the left-hand side is `∅` and the right-hand side,
assuming `[Nontrivial A]`, is `{k}` where `p = Polynomial.C k`.  -/
spectrum.map_polynomial_aeval_of_degree_pos : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A)
  (p : Polynomial 𝕜),
  0 < p.degree → spectrum 𝕜 ((Polynomial.aeval a) p) = (fun x => Polynomial.eval x p) '' spectrum 𝕜 a
-- Mathlib.Algebra.Order.Field.Basic
/-- **Alias** of the reverse direction of `mul_sub_mul_div_mul_nonpos_iff`. -/
mul_sub_mul_div_mul_nonpos : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b c d : α},
  c ≠ 0 → d ≠ 0 → a / c ≤ b / d → (a * d - b * c) / (c * d) ≤ 0
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.aedisjoint_compl_left : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.AEDisjoint μ sᶜ s
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mulPosMono_iff : ∀ (α : Type u_1) [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  MulPosMono α ↔ ∀ ⦃c : α⦄, 0 ≤ c → ∀ ⦃a b : α⦄, a ≤ b → a * c ≤ b * c
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
instSMulWeakSpaceOfModule : {𝕜 : Type u_3} →
  {𝕝 : Type u_1} →
    {E : Type u_2} →
      [inst : CommSemiring 𝕜] →
        [inst_1 : TopologicalSpace 𝕜] →
          [inst_2 : ContinuousAdd 𝕜] →
            [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
              [inst_4 : AddCommMonoid E] →
                [inst_5 : Module 𝕜 E] →
                  [inst_6 : TopologicalSpace E] → [inst_7 : CommSemiring 𝕝] → [Module 𝕝 E] → SMul 𝕝 (WeakSpace 𝕜 E)
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearMap.codRestrictOfInjective_comp_apply : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M₁ →ₗ[R] M₂) (i : M₃ →ₗ[R] M₂) (hi : Function.Injective ⇑i)
  (hf : ∀ (x : M₁), f x ∈ i.range) (x : M₁), i ((f.codRestrictOfInjective i hi hf) x) = f x
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_uIcc_castLE : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.uIcc (Fin.castLE h i) (Fin.castLE h j) = Set.uIcc i j
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableMul₂.measurable_mul : ∀ {M : Type u_2} {inst : MeasurableSpace M} {inst_1 : Mul M} [self : MeasurableMul₂ M], Measurable fun p => p.1 * p.2
-- Mathlib.RingTheory.Localization.Defs
/-- Every element in the localization can be expressed as a quotient of an element in the
range of `algebraMap` by the image of an element of the submonoid.  -/
IsLocalization.surj : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (z : S), ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Eta rule for structured arrows. Prefer `StructuredArrow.eta` for rewriting, since equality of
objects tends to cause problems.  -/
CategoryTheory.StructuredArrow.eq_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T),
  f = CategoryTheory.StructuredArrow.mk f.hom
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.isoMk_hom_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map r.hom))
      CategoryTheory.MorphismProperty.Comma.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Comma.isoMk l r h).hom.right = r.hom
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.mk.inj : ∀ {G : Type u_1} {inst : Group G} {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  {toReducedWord : HNNExtension.NormalWord.ReducedWord G A B}
  {mem_set : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord.toList → g ∈ d.set u}
  {toReducedWord_1 : HNNExtension.NormalWord.ReducedWord G A B}
  {mem_set_1 : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord_1.toList → g ∈ d.set u},
  { toReducedWord := toReducedWord, mem_set := mem_set } = { toReducedWord := toReducedWord_1, mem_set := mem_set_1 } →
    toReducedWord = toReducedWord_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ne_empty_of_erase_ne_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.erase k ≠ ∅ → t ≠ ∅
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_symm_trans : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12}
  [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₂] [inst_9 : SeminormedAddCommGroup V₃]
  [inst_10 : NormedSpace 𝕜 V₃] [inst_11 : PseudoMetricSpace P₃] [inst_12 : NormedAddTorsor V₃ P₃] (e₁ : P ≃ᵃⁱ[𝕜] P₂)
  (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃), ⇑(e₁.trans e₂).symm = ⇑e₁.symm ∘ ⇑e₂.symm
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
/-- When `E` is a topological module over a topological ring `R`, the class `SeparatingDual R E`
registers that continuous linear forms on `E` separate points of `E`.  -/
SeparatingDual : (R : Type u_1) →
  (V : Type u_2) →
    [inst : Ring R] → [inst_1 : AddCommGroup V] → [TopologicalSpace V] → [TopologicalSpace R] → [Module R V] → Prop
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- Constructs intermediate states of an iterator created with the combinator
`IterM.dropWhileWithPostcondition`.
When `it.dropWhileWithPostcondition P` has stopped dropping elements, its new state cannot be
created directly with `IterM.dropWhileWithPostcondition` but only with
`Intermediate.dropWhileWithPostcondition`.

`Intermediate.dropWhileWithPostcondition` is meant to be used only for internally or for
verification purposes.
 -/
Std.IterM.Intermediate.dropWhileWithPostcondition : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → (P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)) → Bool → Std.IterM m β → Std.IterM m β
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.default.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {code code_1 : Lean.Compiler.LCNF.Code pu},
  Lean.Compiler.LCNF.Alt.default code = Lean.Compiler.LCNF.Alt.default code_1 → code = code_1
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.IsSplitCoequalizer.asCofork_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {h : Y ⟶ Z}
  (t : CategoryTheory.IsSplitCoequalizer f g h), t.asCofork.π = h
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- An alternative constructor for `Hom`,
taking a morphism without a `[IsModHom]` instance, as well as the relevant
equality to put such an instance.  -/
CategoryTheory.Mod.Hom.mk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] →
                {M N : CategoryTheory.Mod D A} →
                  (f : M.X ⟶ N.X) →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
                            CategoryTheory.ModObj.smul)
                        CategoryTheory.Mod.Hom.mk'._auto_1 →
                      M.Hom N
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- If a monotone function has a derivative, then this derivative is nonnegative.  -/
HasDerivAt.nonneg_of_monotone : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜}, HasDerivAt g g' x → Monotone g → 0 ≤ g'
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Two group homomorphisms `G →* G'` are equal if and only if they agree on a generator of `G`.  -/
MonoidHom.eq_iff_eq_on_generator : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g : G},
  (∀ (x : G), x ∈ Subgroup.zpowers g) → ∀ (f₁ f₂ : G →* G'), f₁ = f₂ ↔ f₁ g = f₂ g
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.instInhabitedPrincipal : {α : Type u_1} → (s : Set α) → Inhabited (Filter.principal s).Realizer
-- Mathlib.Tactic.Simproc.FinsetInterval
/-- Simproc to compute `Finset.Ico 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.Ico_ofNat_ofNat : Lean.Meta.Simp.Simproc
-- Mathlib.Order.CompleteLattice.Basic
Prod.snd_sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst_1 : InfSet β] (s : Set (α × β)),
  (sInf s).2 = sInf (Prod.snd '' s)
-- Mathlib.RingTheory.FiniteType
/-- A monoid `M` is finitely generated if and only if `R[M]` is of finite type.  -/
MonoidAlgebra.finiteType_iff_fg : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid M] [inst_1 : CommRing R] [Nontrivial R],
  Algebra.FiniteType R (MonoidAlgebra R M) ↔ Monoid.FG M
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Data exhibiting that a given factorisation through a mono is initial.  -/
CategoryTheory.Limits.IsImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Limits.MonoFactorisation f → Type (max u v)
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesColimit.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [toReflectsColimit : CategoryTheory.Limits.ReflectsColimit K F] →
                  ((c : CategoryTheory.Limits.Cocone (K.comp F)) →
                      CategoryTheory.Limits.IsColimit c → CategoryTheory.LiftableCocone K F c) →
                    CategoryTheory.CreatesColimit K F
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Return `true` if `s` and `t` are equal up to changing the `MVarId`s.  -/
Mathlib.Tactic.LibraryRewrite.isMVarSwap : Lean.Expr → Lean.Expr → Bool
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Algebra.IsIntegral.of_finite : ∀ (R : Type u_1) (B : Type u_3) [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] [Module.Finite R B],
  Algebra.IsIntegral R B
-- Lean.Meta.Match.Match
Lean.Meta.Match.State.counterExamples : Lean.Meta.Match.State → Array (List Lean.Meta.Match.Example)
-- Mathlib.CategoryTheory.Limits.Elements
/-- (implementation) The constructed limit cone.  -/
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor C (Type w)} →
      {I : Type u₁} →
        [inst_1 : CategoryTheory.Category.{v₁, u₁} I] →
          [Small.{w, u₁} I] →
            (F : CategoryTheory.Functor I A.Elements) →
              [CategoryTheory.Limits.HasLimitsOfShape I C] →
                [CategoryTheory.Limits.PreservesLimitsOfShape I A] → CategoryTheory.Limits.Cone F
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given
```
Y₃ - i₃ -> X₃
|          |
g₂         f₂
∨          ∨
Y₂ - i₂ -> X₂
|          |
g₁         f₁
∨          ∨
Y₁ - i₁ -> X₁
```
The big square is a pullback if both the small squares are.
 -/
CategoryTheory.Limits.pasteVertIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₂ ⟶ X₁} →
        {f₂ : X₃ ⟶ X₂} →
          {i₁ : Y₁ ⟶ X₁} →
            {t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁} →
              {i₂ : t₁.pt ⟶ X₂} →
                {t₂ : CategoryTheory.Limits.PullbackCone i₂ f₂} →
                  (hi₂ : i₂ = t₁.snd) →
                    CategoryTheory.Limits.IsLimit t₁ →
                      CategoryTheory.Limits.IsLimit t₂ → CategoryTheory.Limits.IsLimit (t₁.pasteVert t₂ hi₂)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearEquiv.coe_toLinearMap_flip : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M),
  ↑e.flip = (↑e).flip
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The Lévy-Prokhorov distance between finite measures:
`d(μ,ν) = inf {r ≥ 0 | ∀ B, μ B ≤ ν Bᵣ + r ∧ ν B ≤ μ Bᵣ + r}`.  -/
MeasureTheory.levyProkhorovDist : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] → [PseudoEMetricSpace Ω] → MeasureTheory.Measure Ω → MeasureTheory.Measure Ω → ℝ
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.continuousWithinAt_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {b : β} {s : Set β},
  ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, edist (f x) (f b) < ε
-- Mathlib.CategoryTheory.Opposites
/-- The isomorphism between `F.unop.op` and `F`.  -/
CategoryTheory.Functor.unopOpIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) → F.unop.op ≅ F
-- Mathlib.Order.Filter.Pointwise
Filter.inv_atTop : ∀ {G : Type u_7} [inst : CommGroup G] [inst_1 : Preorder G] [IsOrderedMonoid G], Filter.atTop⁻¹ = Filter.atBot