mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_top_objs : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (c : C), c ∈ ⊤.objs
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableMul` if `(c * ·)` and `(· * c)` are measurable functions.
For a typeclass assuming measurability of `uncurry (*)` see `MeasurableMul₂`.  -/
MeasurableMul : (M : Type u_2) → [MeasurableSpace M] → [Mul M] → Prop
-- Aesop.Rule
Aesop.UnfoldRule.instHashable : Hashable Aesop.UnfoldRule
-- Mathlib.LinearAlgebra.Span.Basic
/-- If `s` generates the whole module and linear maps `f`, `g` are equal on `s`, then they are
equal.  -/
LinearMap.ext_on : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {s : Set M} {f g : M →ₛₗ[σ₁₂] M₂}, Submodule.span R s = ⊤ → Set.EqOn (⇑f) (⇑g) s → f = g
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_pos_iff_support_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ f → MeasureTheory.Integrable f μ → (0 < ∫ (x : α), f x ∂μ ↔ 0 < μ (Function.support f))
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_uIoc_castLE : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.uIoc (Fin.castLE h i) (Fin.castLE h j) = Set.uIoc i j
-- Aesop.Tree.Data
Aesop.RappData.successProbability : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Aesop.Percent
-- Mathlib.Data.Holor
Holor.instAddMonoid : {α : Type} → {ds : List ℕ} → [AddMonoid α] → AddMonoid (Holor α ds)
-- Mathlib.Algebra.BigOperators.Finprod
MulEquiv.map_finprod_mem : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] (g : M ≃* N) (f : α → M)
  {s : Set α}, s.Finite → g (∏ᶠ (i : α) (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set `B f K r s ε` is the set of points `x` around which there exists a continuous linear map
`L` belonging to `K` (a given set of continuous linear maps) that approximates well the
function `f` (up to an error `ε`), simultaneously at scales `r` and `s`.  -/
FDerivMeasurableAux.B : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → (E → F) → Set (E →L[𝕜] F) → ℝ → ℝ → ℝ → Set E
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.map_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (g : β →o γ), (c.map f).map g = c.map (g.comp f)
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- A morphism `f : X ⟶ Y` satisfies the valuative criterion if
every valuative commutative square over `f` has a unique lift.  -/
AlgebraicGeometry.ValuativeCriterion : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Lean.Environment
Lean.AsyncConstantInfo.mk : Lean.Name → Lean.ConstantKind → Task Lean.ConstantVal → Task Lean.ConstantInfo → Lean.AsyncConstantInfo
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedGroup.mem_closure_iff : ∀ {E : Type u_4} [inst : SeminormedGroup E] {s : Set E} {a : E},
  a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a⁻¹ * b‖ < ε
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).isEmpty = false →
        ((t.alter k f).minKey! = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Mathlib.Algebra.Order.IsBotOne
one_lt_iff_ne_one : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α], 1 < a ↔ a ≠ 1
-- Mathlib.Topology.Category.DeltaGenerated
/-- The faithful (but not full) functor taking each topological space to its delta-generated
coreflection.  -/
TopCat.toDeltaGenerated : CategoryTheory.Functor TopCat DeltaGenerated
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.le_total : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (f g : CauSeq α abs),
  f ≤ g ∨ g ≤ f
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- See also `MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm` which work for general
Lp-convergence for all `p ≠ 0`.  -/
MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top : ∀ {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5}
  [inst : SeminormedAddCommGroup E] {f : ι → α → E} {g : α → E} {l : Filter ι},
  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) ⊤ μ) l (nhds 0) → MeasureTheory.TendstoInMeasure μ f l g
-- Mathlib.Data.Nat.Fib.Zeckendorf
List.IsZeckendorfRep.sum_fib_lt : ∀ {n : ℕ} {l : List ℕ}, l.IsZeckendorfRep → (∀ a ∈ (l ++ [0]).head?, a < n) → (List.map Nat.fib l).sum < Nat.fib n
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below.pair : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop} {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f)
  (hh : Nat.RecursiveIn O h),
  Nat.RecursiveIn.below hf → motive f hf → Nat.RecursiveIn.below hh → motive h hh → Nat.RecursiveIn.below ⋯
-- Init.Meta.Defs
/-- Creates an identifier referring to a constant `c`. The identifier's position is copied from the
syntax returned by `getRef`.

This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally be captured.
 -/
Lean.mkCIdentFromRef : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → Lean.Name → optParam Bool false → m Lean.Syntax
-- Mathlib.Order.Hom.CompleteLattice
supsSupHom_apply : ∀ {α : Type u_2} [inst : CompleteLattice α] (x : α × α), supsSupHom x = x.1 ⊔ x.2
-- Mathlib.Tactic.FunProp.FunctionData
/-- The function can be decomposed in a non-trivial way.  -/
Mathlib.Meta.FunProp.DecompositionResult.comp : Lean.Expr → Lean.Expr → Mathlib.Meta.FunProp.DecompositionResult
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The center of a semiring acts commutatively on that semiring.  -/
Subsemiring.center.smulCommClass_right : ∀ {R' : Type u_1} [inst : Semiring R'], SMulCommClass R' (↥(Subsemiring.center R')) R'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasStrictDerivAt.sinh : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Real.sinh (f x)) (Real.cosh (f x) * f') x
-- Mathlib.Analysis.Normed.Group.Bounded
IsCompact.exists_bound_of_continuousOn' : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {s : Set α},
  IsCompact s → ∀ {f : α → E}, ContinuousOn f s → ∃ C, ∀ x ∈ s, ‖f x‖ ≤ C
-- Mathlib.Order.Interval.Lex
NonemptyInterval.instPartialOrderLex : {α : Type u_1} → [inst : PartialOrder α] → PartialOrder (Lex (NonemptyInterval α))
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.comp_natTransLift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F G H : CategoryTheory.Functor (CategoryTheory.Quotient r) D}
  (τ : (CategoryTheory.Quotient.functor r).comp F ⟶ (CategoryTheory.Quotient.functor r).comp G)
  (τ' : (CategoryTheory.Quotient.functor r).comp G ⟶ (CategoryTheory.Quotient.functor r).comp H),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Quotient.natTransLift r τ)
      (CategoryTheory.Quotient.natTransLift r τ') =
    CategoryTheory.Quotient.natTransLift r (CategoryTheory.CategoryStruct.comp τ τ')
-- Mathlib.RingTheory.Localization.Away.Lemmas
Ideal.le_of_map_algebraMap_le : ∀ {R : Type u_2} (S : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [IsLocalization.Away x S] {I J : Ideal R},
  Ideal.map (algebraMap R S) I ≤ Ideal.map (algebraMap R S) J → (∀ (y : R), x * y ∈ J → y ∈ J) → I ≤ J
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.h1Cotangentι_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (self : ↥P.cotangentComplex.ker), Algebra.Extension.h1Cotangentι self = ↑self
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_re_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] (r : ℝ), RCLike.re ((algebraMap ℝ K) r) = r
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_comp : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) {Z : SSet} (g : Y ⟶ Z),
  A.image (CategoryTheory.CategoryStruct.comp f g) = (A.image f).image g
-- Init.Data.UInt.Bitwise
USize.xor_assoc : ∀ (a b c : USize), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Aesop.Stats.Basic
Aesop.GoalKind.preNorm : Aesop.GoalKind
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.floor_add_nsmul_self : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] {x : ι → ℕ}
  {i : ↑(IsProperLinearSet.basisSet✝ hs)} {n : ℕ},
  IsProperLinearSet.floor✝ hs (x + n • ↑i) i = IsProperLinearSet.floor✝ hs x i + ↑n
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertPlainTime : Std.Time.PlainTime → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instBEqConfig.beq : Mathlib.Tactic.RingNF.Config → Mathlib.Tactic.RingNF.Config → Bool
-- Mathlib.Topology.Order.Bornology
Prod.instIsOrderBornology : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α] {β : Type u_2} [inst_3 : Preorder β]
  [inst_4 : Bornology β] [IsOrderBornology β], IsOrderBornology (α × β)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function preserves 1  -/
MulSemiringActionHom.map_one' : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (self : R →ₑ+*[φ] S), self.toFun 1 = 1
-- Mathlib.Topology.Compactness.Compact
IsCompact.exists_mapClusterPt_of_frequently : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set X} {l : Filter ι} {f : ι → X},
  IsCompact s → (∃ᶠ (x : ι) in l, f x ∈ s) → ∃ a ∈ s, MapClusterPt a l f
-- Mathlib.Analysis.Convolution
HasCompactSupport.convolutionExists_left_of_continuous_right : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [inst_9 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G],
  HasCompactSupport f → MeasureTheory.LocallyIntegrable f μ → Continuous g → MeasureTheory.ConvolutionExists f g L μ
-- Lean.Meta.Sym.AlphaShareBuilder
/-- Helper monad for constructing maximally shared terms.
The `Bool` flag indicates whether it is debug-mode or not.
 -/
Lean.Meta.Sym.Internal.AlphaShareBuilderM : Type → Type
-- Mathlib.Analysis.Normed.Algebra.Spectrum
WeakDual.CharacterSpace.equivAlgHom_symm_coe : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : CompleteSpace A]
  [inst_3 : NormedAlgebra 𝕜 A] (f : A →ₐ[𝕜] 𝕜), ⇑(WeakDual.CharacterSpace.equivAlgHom.symm f) = ⇑f
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.erase.injEq : ∀ (a : Lean.Name) (a_1 : Lean.Syntax) (a_2 : Lean.Name) (a_3 : Lean.Syntax),
  (Simps.ProjectionRule.erase a a_1 = Simps.ProjectionRule.erase a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X)
      (CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) h) =
    h
-- Mathlib.Algebra.Group.Commute.Defs
/-- If `a` commutes with `b`, then `b` commutes with `a`.  -/
Commute.symm : ∀ {S : Type u_3} [inst : Mul S] {a b : S}, Commute a b → Commute b a
-- Mathlib.Topology.GDelta.Basic
/-- A set is residual iff it includes a countable intersection of dense open sets.  -/
mem_residual_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  s ∈ residual X ↔ ∃ S, (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s
-- Mathlib.Algebra.Star.Rat
star_nnratCast : ∀ {R : Type u_1} [inst : DivisionSemiring R] [inst_1 : StarRing R] (q : ℚ≥0), star ↑q = ↑q
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_coe_toMonoidHom : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M), Submonoid.map (↑f) S = Submonoid.map f S
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app : ∀ {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 D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.LaxMonoidal.ε e.inverse))
      (e.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) =
    CategoryTheory.Functor.OplaxMonoidal.η e.functor
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuous_biSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {p : ι → Prop} {f : (i : ι) → p i → α → δ},
  (∀ (i : ι) (hi : p i), LowerSemicontinuous (f i hi)) → LowerSemicontinuous fun x' => ⨆ i, ⨆ (hi : p i), f i hi x'
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.dist_ofSnowflaking_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X]
  (x y : Metric.Snowflaking X α hα₀ hα₁),
  dist (Metric.Snowflaking.ofSnowflaking x) (Metric.Snowflaking.ofSnowflaking y) = dist x y ^ α⁻¹
-- Lean.Declaration
Lean.instBEqDeclaration.beq : Lean.Declaration → Lean.Declaration → Bool
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnriched_id_comp_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₁] {Z : CategoryTheory.Functor J V}
  (h : CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedId V F₁)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₁ F₂)
          h)) =
    h
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.allM.eq_1 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type v} (p : α → m Bool), List.allM p [] = pure true
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.const_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {d : 𝕜 → 𝔸} {d' : 𝔸} (c : 𝔸),
  HasDerivAt d d' x → HasDerivAt (fun y => c * d y) (c * d') x
-- Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
CategoryTheory.projective_iff_llp_epimorphisms_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Z : C}
  (i : Z ⟶ P),
  CategoryTheory.Limits.IsZero Z →
    (CategoryTheory.Projective P ↔ (CategoryTheory.MorphismProperty.epimorphisms C).llp i)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.ext_iff : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f g : NormedAddGroupHom V₁ V₂}, f = g ↔ ∀ (x : V₁), f x = g x
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
CovariantDerivative.derivMetricTensor_apply_eq_extend : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] (cov : CovariantDerivative I F V)
  [inst_11 : VectorBundle ℝ F V] [inst_12 : IsContMDiffRiemannianBundle I 1 F V] {x : M}
  [inst_13 : ContMDiffVectorBundle 1 F V I] [inst_14 : FiniteDimensional ℝ F] (X₀ : TangentSpace I x) (σ₀ τ₀ : V x),
  (((cov.derivMetricTensor x) σ₀) τ₀) X₀ =
    ((d% fun x_1 => inner ℝ (FiberBundle.extend F σ₀ x_1) (FiberBundle.extend F τ₀ x_1)) x) X₀ -
        inner ℝ ((↑cov (FiberBundle.extend F σ₀) x) X₀) τ₀ -
      inner ℝ σ₀ ((↑cov (FiberBundle.extend F τ₀) x) X₀)
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instSubSubtypeMem : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → (I : TwoSidedIdeal R) → Sub ↥I
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.productEquiv_functor_map : ∀ {J : Type u_1} {K : Type u_2} {X Y : CategoryTheory.Discrete (J × K)} (f : X ⟶ Y),
  CategoryTheory.Discrete.productEquiv.functor.map f = ULift.rec (fun down => CategoryTheory.eqToHom ⋯) f
-- Init.Data.UInt.Lemmas
USize.lt_or_le : ∀ (a b : USize), a < b ∨ b ≤ a
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.id_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.CategoryStruct.id A).hom₃ = CategoryTheory.CategoryStruct.id A.obj₃
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_inv_iff_mul_le_one_left : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b : α}, a ≤ b⁻¹ ↔ b * a ≤ 1
-- Init.Grind.AC
Lean.Grind.AC.Seq.endsWithVar_k : Lean.Grind.AC.Seq → Lean.Grind.AC.Var → Bool
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D],
  (CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).counitIso =
    CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg_X : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R), W'.neg P 0 = P 0
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.neg_mem_iff : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x : G}, -x ∈ H ↔ x ∈ H
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_comp_of_zero : ∀ {α : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] {s : Set α} {f : α → M} {g : M → N},
  g 0 = 0 → s.indicator (g ∘ f) = g ∘ s.indicator f
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.eq_1 : ∀ (m : Tactic.ComputeAsymptotics.UnitMonomial),
  m.FirstNonzeroIsPos = (m.sign = Tactic.ComputeAsymptotics.UnitMonomial.Sign.pos)
-- Mathlib.Tactic.ModCases
/-- The successor case decomposes `∃ m, b ≤ m < n ∧ a ≡ m (mod n)` into
`a ≡ b (mod n) ∨ ∃ m, b+1 ≤ m < n ∧ a ≡ m (mod n)`,
and the `a ≡ b (mod n) → p` case becomes a subgoal.
 -/
Mathlib.Tactic.ModCases.NatMod.onModCases_succ : {p : Sort u_1} →
  {n a : ℕ} →
    (b : ℕ) →
      (a ≡ b [MOD n] → p) →
        Mathlib.Tactic.ModCases.NatMod.OnModCases n a (b.add 1) p → Mathlib.Tactic.ModCases.NatMod.OnModCases n a b p
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.centralizer_eq_top_iff_subset : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M}, Submonoid.centralizer s = ⊤ ↔ s ⊆ ↑(Submonoid.center M)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ μ : MeasureTheory.Measure (α × β)}, ρ ≤ μ → ρ.snd ≤ μ.snd
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instGeometricallyIrreducibleOverSchemeInferInstanceOverClass : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.GeometricallyIrreducible (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
/-- An upper bound on the degree of a number field `K` with `|discr K| ≤ N`,
see `rank_le_rankOfDiscrBdd`.  -/
NumberField.hermiteTheorem.rankOfDiscrBdd : ℕ → ℕ
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
RingSubgroupsBasis.mk : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] {B : ι → AddSubgroup A},
  (∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j) →
    (∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)) →
      (∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(B i)) →
        (∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)) → RingSubgroupsBasis B
-- Mathlib.Geometry.Manifold.MFDeriv.Tangent
/-- To write a linear map between tangent spaces in coordinates amounts to precomposing and
postcomposing it with derivatives of extended charts.
Concrete version of `inTangentCoordinates_eq`.  -/
inTangentCoordinates_eq_mfderiv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M'] [inst_11 : ChartedSpace H' M']
  [inst_12 : IsManifold I' 1 M'] {N : Type u_8} {f : N → M} {g : N → M'}
  {ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)} {x₀ x : N},
  f x ∈ (chartAt H (f x₀)).source →
    g x ∈ (chartAt H' (g x₀)).source →
      inTangentCoordinates I I' f g ϕ x₀ x =
        mfderiv% ↑(extChartAt I' (g x₀)) (g x) ∘SL
          ϕ x ∘SL mfderiv[Set.range ↑I] ↑(extChartAt I (f x₀)).symm (↑(extChartAt I (f x₀)) (f x))
-- Mathlib.RingTheory.Nilpotent.Lemmas
nilradical_eq_bot_iff : ∀ {R : Type u_3} [inst : CommSemiring R], nilradical R = ⊥ ↔ IsReduced R
-- Mathlib.CategoryTheory.Category.ULift
/-- The obvious function `C → ULiftHom C`.  -/
CategoryTheory.ULiftHom.objUp : {C : Type u_1} → C → CategoryTheory.ULiftHom C