mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Constructions
/-- ZPowers of analytic functions (into a normed division algebra over `𝕜`) are analytic if the
exponent is nonnegative.  -/
AnalyticOn.zpow_nonneg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E} {n : ℤ}, AnalyticOn 𝕜 f s → 0 ≤ n → AnalyticOn 𝕜 (f ^ n) s
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasurableEmbedding.setIntegral_map_vectorMeasure : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {β : Type u_7} [inst_6 : MeasurableSpace β] {φ : X → β} {f : β → E},
  MeasurableEmbedding φ →
    ∀ {s : Set β}, MeasurableSet s → ∫ᵛ (y : β) in s, f y ∂[B; μ.map φ] = ∫ᵛ (x : X) in φ ⁻¹' s, f (φ x) ∂[B; μ]
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_lt_log : ∀ {x y : ℝ}, 0 < x → x < y → Real.log x < Real.log y
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Formula for `hurwitzZetaEven` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version without absolute values, assuming `a ∈ Icc 0 1`)  -/
HurwitzZeta.hasSum_nat_hurwitzZetaEven_of_mem_Icc : ∀ {a : ℝ},
  a ∈ Set.Icc 0 1 →
    ∀ {s : ℂ},
      1 < s.re → HasSum (fun n => (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2) (HurwitzZeta.hurwitzZetaEven (↑a) s)
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv.eq_def : ∀ {α : Type u_1} [inst : DecidableEq α] (x : RegularExpression α) (x_1 : α),
  x.deriv x_1 =
    match x, x_1 with
    | RegularExpression.zero, x => 0
    | RegularExpression.epsilon, x => 0
    | RegularExpression.char a₁, a₂ => if a₁ = a₂ then 1 else 0
    | P.plus Q, a => P.deriv a + Q.deriv a
    | P.comp Q, a => if P.matchEpsilon = true then P.deriv a * Q + Q.deriv a else P.deriv a * Q
    | P.star, a => P.deriv a * P.star
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- Given an additive submonoid `s` of `M`, we say that `s` is **saturated** if it satisfies
`x + y ∈ s → x ∈ s ∧ y ∈ s`.

It is called `AddSaturated` here to be distinguished from `Submonoid.PowSaturated` or
`AddSubmonoid.NSMulSaturated`, which is also called "saturated" in the literature.  -/
AddSubmonoid.AddSaturated : {M : Type u_1} → [inst : AddZeroClass M] → AddSubmonoid M → Prop
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
FundamentalGroup.mapOfEq_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)) {x : X} {y : Y}
  (h : f x = y) (p : FundamentalGroup X x),
  (FundamentalGroup.mapOfEq f h) p = (Path.Homotopic.Quotient.map p f).cast ⋯ ⋯
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.isIntegral_root' : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R}, g.Monic → IsIntegral R (AdjoinRoot.root g)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.smul_mem : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A) {x : A},
  x ∈ S → ∀ (r : R), r • x ∈ S
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_neg_same : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable (fun x => Real.exp (f x)) μ → (μ.tilted f).tilted (-f) = μ
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
/-- Being an isomorphism satisfies fpqc descent.  -/
AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact : (CategoryTheory.MorphismProperty.isomorphisms AlgebraicGeometry.Scheme).DescendsAlong
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_radical : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), I.radical.support = I.support
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The action by a subalgebra is the action by the underlying algebra.  -/
Subalgebra.instSMulSubtypeMem : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → {α : Type u_1} → [SMul A α] → (S : Subalgebra R A) → SMul (↥S) α
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.merge.eq_def : ∀ {α : Type u_1} (xs ys : List α) (le : α → α → Bool),
  xs.merge ys le =
    match xs, ys with
    | [], ys => ys
    | xs, [] => xs
    | x :: xs, y :: ys => if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le
-- Mathlib.Analysis.RCLike.Basic
RCLike.div_re_ofReal : ∀ {K : Type u_1} [inst : RCLike K] {z : K} {r : ℝ}, RCLike.re (z / ↑r) = RCLike.re z / r
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.functorFunctor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (f : C ≌ D), (CategoryTheory.Equivalence.functorFunctor C D).obj f = f.functor
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mem_maxGenEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R) (m : M), m ∈ f.maxGenEigenspace μ ↔ ∃ k, ((f - μ • 1) ^ k) m = 0
-- Mathlib.Data.List.AList
/-- Recursion on an `AList`, using `insert`. Use as `induction l`.  -/
AList.insertRec : {α : Type u} →
  {β : α → Type v} →
    [inst : DecidableEq α] →
      {C : AList β → Sort u_1} →
        C ∅ → ((a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)) → (l : AList β) → C l
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Std.Do.PredTrans.pushExcept.match_1.splitter : {α ε : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderIdent.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Rat.Lemmas
Rat.normalize_add_normalize : ∀ (n₁ n₂ : ℤ) {d₁ d₂ : ℕ} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0),
  Rat.normalize n₁ d₁ z₁ + Rat.normalize n₂ d₂ z₂ = Rat.normalize (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂) ⋯
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for exponents larger than `k`.  -/
Module.End.hasGenEigenvalue_of_hasGenEigenvalue_of_le : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k m : ℕ}, k ≤ m → f.HasGenEigenvalue μ k → f.HasGenEigenvalue μ m
-- Mathlib.Topology.Algebra.Group.Basic
/-- A compact set is covered by finitely many left multiplicative translates of a set
with non-empty interior.  -/
compact_covered_by_mul_left_translates : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {K V : Set G},
  IsCompact K → (interior V).Nonempty → ∃ t, K ⊆ ⋃ g ∈ t, (fun x => g * x) ⁻¹' V
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.instFullMonFunctorOppositeMonCatYonedaAddMon : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddMon.Full
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand_map_frobenius_le : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p : ℕ) [inst_2 : ExpChar R p] (f : Polynomial R),
  Multiset.map (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots ≤ p • f.roots
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_eq_some_get : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  (h : a ∈ m), m.get? a = some (m.get a h)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorRightTensor.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategory.tensorRightTensor X Y =
    CategoryTheory.NatIso.ofComponents (fun Z => (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).symm) ⋯
-- Mathlib.AlgebraicGeometry.Scheme
/-- An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.  -/
AlgebraicGeometry.Scheme.homeoOfIso : {X Y : AlgebraicGeometry.Scheme} → (X ≅ Y) → ↥X ≃ₜ ↥Y
-- Std.Time.Format.Modifier
Std.Time.DayPeriod.am.sizeOf_spec : sizeOf Std.Time.DayPeriod.am = 1
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t` is in the upper shadow of `𝒜` iff `t` is exactly one element less than something from `𝒜`.

See also `Finset.mem_upShadow_iff_exists_sdiff`.  -/
Finset.mem_upShadow_iff_exists_mem_card_add_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α},
  t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ t.card = s.card + 1
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddLeftCancelSemigroup : {α : Type u_1} → [AddLeftCancelSemigroup α] → AddLeftCancelSemigroup αᵐᵒᵖ
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_add : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (f g : M → N) (x y : M),
  QuadraticMap.polar (f + g) x y = QuadraticMap.polar f x y + QuadraticMap.polar g x y
-- Mathlib.Analysis.Real.Cardinality
/-- `cantorFunction c` is strictly increasing with if `0 < c < 1/2`, if we endow `ℕ → Bool` with a
lexicographic order. The lexicographic order doesn't exist for these infinitary products, so we
explicitly write out what it means.  -/
Cardinal.increasing_cantorFunction : ∀ {c : ℝ},
  0 < c →
    c < 1 / 2 →
      ∀ {n : ℕ} {f g : ℕ → Bool},
        (∀ k < n, f k = g k) → f n = false → g n = true → Cardinal.cantorFunction c f < Cardinal.cantorFunction c g
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
/-- Variant of the 5-lemma for complexes of any size  -/
CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {n k : ℕ}
  (h : k + 4 ≤ n) {R₁ R₂ : CategoryTheory.ComposableArrows C n},
  R₁.Exact →
    R₂.Exact →
      ∀ (φ : R₁ ⟶ R₂) (k₀ k₁ k₂ k₃ k₄ : ℕ) (hk₀ : k₀ = k) (hk₁ : k₁ = k + 1) (hk₂ : k₂ = k + 2) (hk₃ : k₃ = k + 3)
        (hk₄ : k₄ = k + 4),
        CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ k₀ ⋯) →
          CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ k₁ ⋯) →
            CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ k₃ ⋯) →
              CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ k₄ ⋯) →
                CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ k₂ ⋯)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.privateNames : Lean.Option Bool
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
coe_nonZeroDivisorsRight_eq : ∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀],
  ↑(nonZeroDivisorsRight M₀) = {x | x ≠ 0}
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flippingEquiv_apply_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) (j : C),
  ((CategoryTheory.Functor.flippingEquiv F).obj k).obj j = (F.obj j).obj k
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_b₄ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).b₄ = ↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_ringHom_trans : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S'), ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- **Alias** of `PowerSeries.trunc_derivative`. -/
PowerSeries.trunc_derivativeFun : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (n : ℕ),
  (PowerSeries.trunc n) ((PowerSeries.derivative R) f) = Polynomial.derivative ((PowerSeries.trunc (n + 1)) f)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.getThenInsertIfNew? k v).2 = t.insertIfNew k v
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
isLittleO_exp_mul_rpow_of_lt : ∀ (k : ℝ) {a b : ℝ}, a < b → (fun t => Real.exp (a * t) * t ^ k) =o[Filter.atTop] fun t => Real.exp (b * t)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_functor_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).functor.map f).left = f.left
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_def : ∀ {R : Type u_1} [inst : Semiring R] (φ : Polynomial R), ↑φ = PowerSeries.mk φ.coeff
-- Mathlib.Topology.Category.CompHaus.Basic
CompHaus.instInhabited : Inhabited CompHaus
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.add_one_le_natCast_iff`. -/
ENat.add_one_le_coe_iff : ∀ {m : ℕ∞} {n : ℕ}, m + 1 ≤ ↑n ↔ m < ↑n
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.bijective : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [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₂] (e : P ≃ᵃⁱ[𝕜] P₂), Function.Bijective ⇑e
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restrictionMap_comp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') {L : HomologicalComplex C c'} (M : HomologicalComplex C c') (φ : K ⟶ L) (φ' : L ⟶ M)
  (e : c.Embedding c') [inst_2 : e.IsRelIff],
  HomologicalComplex.restrictionMap (CategoryTheory.CategoryStruct.comp φ φ') e =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap φ e) (HomologicalComplex.restrictionMap φ' e)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.csinh : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ},
  AEMeasurable f μ → AEMeasurable (fun x => Complex.sinh (f x)) μ
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- The linear equivalence between `ContinuousMultilinearMap 𝕜 E F` and `(⨂[𝕜] i, Eᵢ) →L[𝕜] F`
induced by `PiTensorProduct.lift`, for every normed space `F`.
 -/
PiTensorProduct.liftEquiv : {ι : Type u_1} →
  [inst : Fintype ι] →
    (𝕜 : Type u_2) →
      (E : ι → Type u_3) →
        [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] →
              (F : Type u_4) →
                [inst_4 : SeminormedAddCommGroup F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    ContinuousMultilinearMap 𝕜 E F ≃ₗ[𝕜] (PiTensorProduct 𝕜 fun i => E i) →L[𝕜] F
-- Mathlib.Data.Rat.BigOperators
Rat.cast_multiset_sum : ∀ {α : Type u_2} [inst : DivisionRing α] [CharZero α] (s : Multiset ℚ), ↑s.sum = (Multiset.map Rat.cast s).sum
-- Mathlib.RingTheory.Localization.Basic
/-- If the square below commutes, the bottom map is uniquely specified:
```
R  →  S
↓     ↓
Rₘ → Sₘ
```
 -/
IsLocalization.algebraMap_apply_eq_map_map_submonoid : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [inst_3 : CommSemiring Rₘ] [inst_4 : CommSemiring Sₘ]
  [inst_5 : Algebra R Rₘ] [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ]
  [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ]
  [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] (x : Rₘ),
  (algebraMap Rₘ Sₘ) x = (IsLocalization.map Sₘ (algebraMap R S) ⋯) x
-- Mathlib.Algebra.GroupWithZero.Units.Basic
one_div_mul_cancel : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → 1 / a * a = 1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableOn.hasFDerivAt : ∀ {𝕜 : 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} {s : Set E},
  DifferentiableOn 𝕜 f s → s ∈ nhds x → HasFDerivAt f (fderiv 𝕜 f x) x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.zero_eq_coe : ∀ {α : Type u} [inst : Zero α] {a : α}, 0 = ↑a ↔ a = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.PreservesLimit₂.nonempty_isLimit_mapCone₂ : ∀ {J₁ : Type u_1} {J₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} J₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} J₂} {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C₁} {inst_3 : CategoryTheory.Category.{v_4, u_4} C₂}
  {inst_4 : CategoryTheory.Category.{v_5, u_5} C} {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)}
  [self : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cone K₁}
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) {c₂ : CategoryTheory.Limits.Cone K₂}
  (hc₂ : CategoryTheory.Limits.IsLimit c₂), Nonempty (CategoryTheory.Limits.IsLimit (G.mapCone₂ c₁ c₂))
-- Mathlib.Algebra.Group.Conj
ConjClasses.mk_surjective : ∀ {α : Type u} [inst : Monoid α], Function.Surjective ConjClasses.mk
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.IsFundamentalGroup.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] {G : Type u_1} [inst_2 : Group G]
  [inst_3 : (X : C) → MulAction G (F.obj X).obj] [inst_4 : TopologicalSpace G] [inst_5 : IsTopologicalGroup G]
  [inst_6 : CompactSpace G] [toIsNaturalSMul : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G],
  (∀ (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G (F.obj X).obj) →
    (∀ (X : C), ContinuousSMul G (F.obj X).obj) →
      (∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1) →
        CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
Semigrp.Hom.Simps.hom : (X Y : Semigrp) → X.Hom Y → ↑X →ₙ* ↑Y
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instTransOrdOrdinal : Std.TransOrd Std.Time.Nanosecond.Ordinal
-- Mathlib.Topology.Spectral.Hom
SpectralMapClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : FunLike F α β], (∀ (f : F), IsSpectralMap ⇑f) → SpectralMapClass F α β
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_diff_le_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ \ t₂).size ≤ t₁.size
-- Mathlib.Algebra.Group.TransferInstance
Equiv.zero.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Zero β], e.zero = { zero := e.invFun 0 }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.writes.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Fintype Γ] (a : Γ → σ → σ) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.writes (Turing.TM1.Stmt.load a q) = Turing.TM1to1.writes q
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Entry.mk.injEq : ∀ (type : Lean.MessageData) (line : Option ℕ) (depth : ℕ) (status : Mathlib.Explode.Status) (thm : Lean.MessageData)
  (deps : List (Option ℕ)) (useAsDep : Bool) (type_1 : Lean.MessageData) (line_1 : Option ℕ) (depth_1 : ℕ)
  (status_1 : Mathlib.Explode.Status) (thm_1 : Lean.MessageData) (deps_1 : List (Option ℕ)) (useAsDep_1 : Bool),
  ({ type := type, line := line, depth := depth, status := status, thm := thm, deps := deps, useAsDep := useAsDep } =
      { type := type_1, line := line_1, depth := depth_1, status := status_1, thm := thm_1, deps := deps_1,
        useAsDep := useAsDep_1 }) =
    (type = type_1 ∧
      line = line_1 ∧ depth = depth_1 ∧ status = status_1 ∧ thm = thm_1 ∧ deps = deps_1 ∧ useAsDep = useAsDep_1)
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_finVal : ∀ (n : Fin UInt32.size), UInt32.ofNatLT ↑n ⋯ = UInt32.ofFin n
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  {hf₁ : F.relativelyRepresentable f₁} {f₂ : F.obj A₂ ⟶ X} {f₃ : F.obj A₃ ⟶ X}
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [F.Faithful] {Z : C}
  {φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃},
  CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃) =
      CategoryTheory.CategoryStruct.comp φ' (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃) →
    CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃) =
        CategoryTheory.CategoryStruct.comp φ' (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃) →
      CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃) =
          CategoryTheory.CategoryStruct.comp φ'
            (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃) →
        φ = φ'
-- Mathlib.Algebra.Group.Equiv.Basic
Equiv.inv_apply : ∀ (G : Type u_14) [inst : InvolutiveInv G], ⇑(Equiv.inv G) = Inv.inv
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.extend_map : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [inst_2 : UniformSpace γ] [CompleteSpace γ] [T0Space γ]
  {f : β → γ} {g : α → β},
  UniformContinuous f → UniformContinuous g → pkg'.extend f ∘ pkg.map pkg' g = pkg.extend (f ∘ g)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_comm : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] {s : Finset β} {t : Finset γ} (hs : s.Nonempty)
  (ht : t.Nonempty) (f : β → γ → α), (s.inf' hs fun b => t.inf' ht (f b)) = t.inf' ht fun c => s.inf' hs fun b => f b c
-- Init.Data.Array.Lemmas
/-- Variant of `any_eq_false` in terms of membership rather than an array index.  -/
Array.any_eq_false' : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.any p = false ↔ ∀ x ∈ as, ¬p x = true
-- Std.Http.Internal.Char
Std.Http.Internal.Char.quotedStringChar.eq_1 : ∀ (c : Char),
  Std.Http.Internal.Char.quotedStringChar c =
    (Std.Http.Internal.Char.qdtext c || Std.Http.Internal.Char.quotedPairChar c)
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_one_eq_const : SimplexCategory.Truncated.δ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
    SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3 =
  SimplexCategory.Truncated.Hom.tr ({ len := 0 }.const { len := 0 + 1 } 0)
    SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3