mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f f_1 : X ⟶ Y} (e_f : f = f_1) {a a_1 : R ⟶ X}
  (e_a : a = a_1) {b b_1 : R ⟶ X} (e_b : b = b_1) {S : C} (k : CategoryTheory.IsKernelPair f a b) (p p_1 : S ⟶ X)
  (e_p : p = p_1) (q q_1 : S ⟶ X) (e_q : q = q_1)
  (w : CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f), k.lift p q w = ⋯.lift p_1 q_1 ⋯
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.congr : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f g : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l : Filter α},
  MeasureTheory.IntegrableAtFilter f l μ → f =ᵐ[μ] g → MeasureTheory.IntegrableAtFilter g l μ
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
_private.Mathlib.RingTheory.DedekindDomain.Ideal.Basic.0.IsDedekindDomainInv.isNoetherianRing : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A], IsDedekindDomainInv✝ A → IsNoetherianRing A
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- If `I` is a nonzero fractional ideal, then `I` is equal to the product `∏_v v^(count K v I)`.  -/
FractionalIdeal.finprod_heightOneSpectrum_factorization' : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 → ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ FractionalIdeal.count K v I = I
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_C : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).divX = 0
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.ofReal_average : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ →
    0 ≤ᵐ[μ] f → ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ Set.univ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.trim_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m n : MeasurableSpace α}
  (v : MeasureTheory.VectorMeasure α M) (hle : m ≤ n) (i : Set α),
  (v.trim hle).measureOf' i = if MeasurableSet i then v i else 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.of_sub_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α}, (s - t).Nonempty → t.Nonempty
-- Mathlib.CategoryTheory.Presentable.Type
HasCardinalLT.Set.functor_obj : ∀ (X : Type u) (κ : Cardinal.{u}) (X_1 : HasCardinalLT.Set X κ), (HasCardinalLT.Set.functor X κ).obj X_1 = ↑↑X_1
-- Mathlib.Analysis.Complex.Liouville
_private.Mathlib.Analysis.Complex.Liouville.0.Complex.norm_deriv_le_aux : ∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F},
  0 < R → DiffContOnCl ℂ f (Metric.ball c R) → (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) → ‖deriv f c‖ ≤ C / R
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.List.applyId_zip_eq : ∀ {α : Type u} [inst : DecidableEq α] {xs ys : List α},
  xs.Nodup →
    xs.length = ys.length →
      ∀ (x y : α) (i : ℕ),
        xs[i]? = some x → (Plausible.InjectiveFunction.List.applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
-- Mathlib.Topology.Order.Monotone
/-- An antitone map has a limit to the left of any point `x`, equal to `sInf (f '' (Iio x))`.  -/
Antitone.tendsto_nhdsLT : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f → ∀ (x : α), Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sInf (f '' Set.Iio x)))
-- Mathlib.CategoryTheory.Localization.FiniteProducts
/-- When `C` has finite products and `W : MorphismProperty C` contains
identities and is stable under finite products,
then any localization functor for `W` preserves finite products.  -/
CategoryTheory.Localization.preservesFiniteProducts : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.ContainsIdentities]
  [CategoryTheory.Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts],
  CategoryTheory.Limits.PreservesFiniteProducts L
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Multiplication by a nonzero element `a` on the left
as a `DilationEquiv` of a normed division ring.  -/
DilationEquiv.mulLeft : {α : Type u_1} → [inst : NormedDivisionRing α] → (a : α) → a ≠ 0 → α ≃ᵈ α
-- Mathlib.Data.Set.Basic
Set.mem_ite_empty_right : ∀ {α : Type u} (p : Prop) [inst : Decidable p] (t : Set α) (x : α), (x ∈ if p then t else ∅) ↔ p ∧ x ∈ t
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.mk_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsFiniteMeasure μ)
  (s : Set Ω), ⟨μ, hμ⟩ s = (μ s).toNNReal
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNorm_zero : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι], ‖0‖ = 0
-- Mathlib.Analysis.Convex.NNReal
NNReal.segment_eq_uIcc : ∀ {x y : NNReal}, segment NNReal x y = Set.uIcc x y
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The composition of a partial map and a morphism on the right.  -/
AlgebraicGeometry.Scheme.PartialMap.compHom : {X Y Z : AlgebraicGeometry.Scheme} → X.PartialMap Y → (Y ⟶ Z) → X.PartialMap Z
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.up_sInf : ∀ {α : Type u_1} [inst : InfSet α] (s : Set α), { down := sInf s } = sInf (ULift.down ⁻¹' s)
-- Mathlib.GroupTheory.ClassEquation
/-- Conjugacy classes form a partition of G, stated in terms of cardinality.  -/
Group.sum_card_conj_classes_eq_card : ∀ (G : Type u_1) [inst : Group G] [Finite G], ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
/-- A continuous function `f` on an unbounded linear order with compact intervals has bounded range if
and only if it is `O(1)` at both `atTop` and `atBot`.
 -/
Continuous.isBounded_range_iff_isBigO_atTop_atBot : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : LinearOrder β]
  [OrderClosedTopology β] [CompactIccSpace β] [NoMaxOrder β] [NoMinOrder β] {f : β → E},
  Continuous f → (Bornology.IsBounded (Set.range f) ↔ f =O[Filter.atTop] 1 ∧ f =O[Filter.atBot] 1)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.isOpen_B_with_param : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [LocallyCompactSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {α : Type u_4} [inst_6 : TopologicalSpace α] {f : α → E → F} {r s t : ℝ},
  Continuous (Function.uncurry f) → ∀ (K : Set (E →L[𝕜] F)), IsOpen {p | p.2 ∈ FDerivMeasurableAux.B (f p.1) K r s t}
-- Init.Data.Int.Linear
Int.Internal.Linear.le_combine_coeff_cert.eq_1 : ∀ (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.le_combine_coeff_cert p₁ p₂ p₃ k =
    (Int.blt' 0 k).and'
      ((Int.Internal.Linear.Poly.divCoeffs k
            (Int.Internal.Linear.Poly.combine_mul_k (↑p₂.leadCoeff.natAbs) (↑p₁.leadCoeff.natAbs) p₁ p₂)).and'
        (p₃.beq'
          (Int.Internal.Linear.Poly.div k
            (Int.Internal.Linear.Poly.combine_mul_k (↑p₂.leadCoeff.natAbs) (↑p₁.leadCoeff.natAbs) p₁ p₂))))
-- Mathlib.Dynamics.Flow
Flow.mem_orbit_self : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) (x : α), x ∈ ϕ.orbit x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k}, t.isEmpty = true → (t.insert k v).minKey! = k
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minEntry?_insertEntry.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → (Unit → motive none) → ((w : (a : α) × β a) → motive (some w)) → motive x
-- Mathlib.Algebra.FreeAlgebra.Cardinality
FreeAlgebra.cardinalMk_eq_max_lift : ∀ (R : Type u) [inst : CommSemiring R] (X : Type v) [Nonempty X] [Nontrivial R],
  Cardinal.mk (FreeAlgebra R X) =
    max (max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk X))) Cardinal.aleph0
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1 : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L₁ L₂ : IntermediateField k K) [Algebra.IsSeparable k ↥L₂], Algebra.IsSeparable k ↥(L₁ ⊓ L₂)
-- Mathlib.Topology.UniformSpace.Cauchy
IsClosed.isComplete : ∀ {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α}, IsClosed s → IsComplete s
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instCommRing : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] → [IsOrderedCancelAddMonoid Γ] → [inst : CommRing R] → CommRing (HahnSeries Γ R)
-- Mathlib.Topology.Basic
Filter.limUnder.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_3} [inst_1 : Nonempty X] (f f_1 : Filter α),
  f = f_1 → ∀ (g g_1 : α → X), g = g_1 → f.limUnder g = f_1.limUnder g_1
-- Mathlib.CategoryTheory.Monoidal.Rigid.Braided
/-- If a braided category is right-rigid, then it is left-rigid.
Not registered as an instance as this is not canonical enough.  -/
CategoryTheory.BraidedCategory.leftRigidCategoryOfRightRigidCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → [CategoryTheory.RightRigidCategory C] → CategoryTheory.LeftRigidCategory C
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIdempotentElemEquivClopens_mul : ∀ {R : Type u} [inst : CommRing R] (e₁ e₂ : ↑{e | IsIdempotentElem e}),
  PrimeSpectrum.isIdempotentElemEquivClopens ⟨↑e₁ * ↑e₂, ⋯⟩ =
    PrimeSpectrum.isIdempotentElemEquivClopens e₁ ⊓ PrimeSpectrum.isIdempotentElemEquivClopens e₂
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ},
  m.getKey? k = some k' → (Std.ExtHashMap.map f m).getD k fallback = (Option.map (f k') m[k]?).getD fallback
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- Refine a term of `Meq P T` with respect to a refinement `S ⟶ T` of covers.  -/
CategoryTheory.Meq.refine : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {FD : D → D → Type u_1} →
            {CD : D → Type t} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [inst_3 : CategoryTheory.ConcreteCategory D FD] →
                  {X : C} →
                    {P : CategoryTheory.Functor Cᵒᵖ D} →
                      {S T : J.Cover X} → CategoryTheory.Meq P T → (S ⟶ T) → CategoryTheory.Meq P S
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_eq_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) {F G : CategoryTheory.Functor C D} (e : F ≅ G), P.map F = P.map G
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.holder_add_left : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G)
  (f₁ f₂ : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp F q μ)),
  ContinuousLinearMap.holder r B (f₁ + f₂) g = ContinuousLinearMap.holder r B f₁ g + ContinuousLinearMap.holder r B f₂ g
-- Mathlib.Analysis.MeanInequalities
/-- **Young's inequality**, a version for arbitrary real numbers.  -/
Real.young_inequality : ∀ (a b : ℝ) {p q : ℝ}, p.HolderConjugate q → a * b ≤ |a| ^ p / p + |b| ^ q / q
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.getKeyD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a fallback : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.getKeyD ⟨{ size := size, buckets := buckets }, hm⟩ a fallback =
    Std.DHashMap.Internal.AssocList.getKeyD a fallback buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Mathlib.NumberTheory.SmoothNumbers
/-- The non-zero non-`N`-smooth numbers are `≥ N`.  -/
Nat.smoothNumbers_compl : ∀ (N : ℕ), N.smoothNumbersᶜ \ {0} ⊆ {n | N ≤ n}
-- Mathlib.RingTheory.Localization.Defs
/-- Localizing at a submonoid with 0 inside it leads to the trivial ring.  -/
IsLocalization.uniqueOfZeroMem : {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] → 0 ∈ M → Unique S
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is monotone on a left neighborhood of `a` and
the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is continuous at
`a` from the left.  -/
continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α},
  MonotoneOn f s →
    s ∈ nhdsWithin a (Set.Iic a) → f '' s ∈ nhdsWithin (f a) (Set.Iic (f a)) → ContinuousWithinAt f (Set.Iic a) a
-- Mathlib.Order.RelIso.Basic
/-- Any equivalence lifts to a relation isomorphism between `s` and its preimage.  -/
RelIso.preimage : {α : Type u_1} → {β : Type u_2} → (f : α ≃ β) → (s : β → β → Prop) → ⇑f ⁻¹'o s ≃r s
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_Except : ∀ {ε α : Type} {post : α → Prop} {epost : EPost⟨ε → Prop⟩} (err : ε),
  ⦃ epost.head err ⦄ MonadExceptOf.throw err ⦃ post; epost ⦄
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.of_lt : ∀ {b o : Ordinal.{u_1}}, o ≠ 0 → o < b → Ordinal.CNF b o = [(0, o)]
-- Mathlib.CategoryTheory.Action.Continuous
CategoryTheory.Functor.mapContActionCongr_inv : ∀ {V : Type u_5} {W : Type u_6} [inst : CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7}
  {CV : V → Type u_8} [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
  [inst_2 : CategoryTheory.ConcreteCategory V FV] [inst_3 : CategoryTheory.HasForget₂ V TopCat]
  [inst_4 : CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10}
  [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [inst_6 : CategoryTheory.ConcreteCategory W FW]
  [inst_7 : CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [inst_8 : Monoid G] [inst_9 : TopologicalSpace G]
  {F F' : CategoryTheory.Functor V W} (e : F ≅ F')
  (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
  (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous),
  (CategoryTheory.Functor.mapContActionCongr G e H H').inv =
    { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (e.app X.obj.V) ⋯).inv, naturality := ⋯ }
-- Mathlib.RingTheory.Ideal.Maps
Ideal.coe_comap : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S] (I : Ideal S), ↑(Ideal.comap f I) = ⇑f ⁻¹' ↑I
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instCoeTC : {α : Type u} → CoeTC α (WithZero α)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasColimit_iff_of_iso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  CategoryTheory.Limits.HasColimit F ↔ CategoryTheory.Limits.HasColimit G
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.splitAtPred.eq_1 : ∀ {α : Type u_1} (p : α → Bool), Turing.PartrecToTM2.splitAtPred p [] = ([], none, [])
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : EquivBEq α] {f : (a : α) → β a → Option (γ a)}
  {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l)
  {h :
    Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      true},
  Std.Internal.List.getKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) h =
    Std.Internal.List.getKey k l ⋯
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- If a function is `C^k` on open sets `s i`, it is `C^k` on their union  -/
ContDiffOn.iUnion_of_isOpen : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {ι : Type u_5} {s : ι → Set E},
  (∀ (i : ι), ContDiffOn 𝕜 n f (s i)) → (∀ (i : ι), IsOpen (s i)) → ContDiffOn 𝕜 n f (⋃ i, s i)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.equiv_iff_toList_perm : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_coprod : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁] [inst_9 : AddCommMonoid M₂]
  [inst_10 : Module R M₂] (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M), ↑(f₁.coprod f₂) = (↑f₁).coprod ↑f₂
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.rightHomologyMap'_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.rightHomologyMap' (φ + φ') h₁ h₂ =
    CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂ + CategoryTheory.ShortComplex.rightHomologyMap' φ' h₁ h₂
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence_inverse : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) {G : CategoryTheory.Functor B A}
  (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence hF hG).inverse = G
-- Mathlib.Algebra.CharZero.Defs
CharZero.mk : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], Function.Injective Nat.cast → CharZero R
-- Mathlib.Topology.UniformSpace.Basic
Uniform.continuousWithinAt_iff'_right : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {b : β} {s : Set β},
  ContinuousWithinAt f s b ↔ Filter.Tendsto (fun x => (f b, f x)) (nhdsWithin b s) (uniformity α)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_toList_roc : ∀ {m n : ℕ}, (m<...=n).toList.toArray = (m<...=n).toArray
-- Init.Data.SInt.Lemmas
ISize.ofInt_int16ToInt : ∀ (x : Int16), ISize.ofInt x.toInt = x.toISize
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddMonoidWithOne : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [AddMonoidWithOne M] → AddMonoidWithOne (l.Germ M)
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- **Noether's second isomorphism theorem**: given two subgroups `H` and `N` of a group `G`,
where `N` is normal, defines an isomorphism between `H/(H ∩ N)` and `(HN)/N`.  -/
QuotientGroup.quotientInfEquivProdNormalQuotient : {G : Type u} →
  [inst : Group G] → (H N : Subgroup G) → [hN : N.Normal] → ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.of_keys_unit_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α fun x => Unit}, m₁.keys.Perm m₂.keys → m₁.Equiv m₂
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0.inj : ∀ {a zero a_1 zero_1 : Lean.Expr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0 a zero = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0 a_1 zero_1 →
    a = a_1 ∧ zero = zero_1
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_inv_of_invertible : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [Invertible A], A * A⁻¹ = 1
-- Mathlib.Analysis.Calculus.Conformal.InnerProduct
/-- A real differentiable map `f` is conformal at point `x` if and only if its
differential `f'` at that point scales every inner product by a positive scalar.  -/
conformalAt_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f : E → F} {x : E} {f' : E →L[ℝ] F},
  HasFDerivAt f f' x → (ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), inner ℝ (f' u) (f' v) = c * inner ℝ u v)
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ],
  ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0),
    ∀ (x : α),
      μ (Metric.closedBall x (2 * ε)) ≤ ↑(IsUnifLocDoublingMeasure.doublingConstant μ) * μ (Metric.closedBall x ε)
-- Mathlib.Data.FunLike.Basic
DFunLike.ext : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] (f g : F), (∀ (x : α), f x = g x) → f = g
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.smul_apply : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {R : Type u_4}
  [inst_1 : Monoid R] [inst_2 : DistribMulAction R M] (c : R) (f : BoxIntegral.BoxAdditiveMap ι M I₀)
  (J : BoxIntegral.Box ι), (c • f) J = c • f J
-- Mathlib.Order.Filter.Pointwise
Filter.Tendsto.div_div : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β},
  Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) g₁ g₂ → Filter.Tendsto (⇑m) (f₁ / g₁) (f₂ / g₂)