mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyGE_of_ge : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (p q : ℤ), p ≤ q → ∀ [K.IsStrictlyGE q], K.IsStrictlyGE p
-- Lean.Meta.Tactic.Induction
/-- Auxiliary method for implementing `induction`-like tactics.
It creates the prefix of a recursor application up-to `motive`.
The motive is computed by abstracting `major` and `indices` at `mvarId.getType`.
It retrieves indices from `majorType` using `recursorInfo`.
Remark: `mvarId` and `tacticName` are used to generate error messages.
 -/
Lean.Meta.mkRecursorAppPrefix : Lean.MVarId → Lean.Name → Lean.FVarId → Lean.Meta.RecursorInfo → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Balanced.brecOn : ∀ {α : Type u_1} {motive : (a : RBTree.RBNode α) → (a_1 : RBTree.RBColor) → (a_2 : ℕ) → a.Balanced a_1 a_2 → Prop}
  {a : RBTree.RBNode α} {a_1 : RBTree.RBColor} {a_2 : ℕ} (t : a.Balanced a_1 a_2),
  (∀ (a : RBTree.RBNode α) (a_3 : RBTree.RBColor) (a_4 : ℕ) (t : a.Balanced a_3 a_4),
      RBTree.RBNode.Balanced.below t → motive a a_3 a_4 t) →
    motive a a_1 a_2 t
-- Mathlib.RingTheory.Flat.Equalizer
/-- The canonical map `M ⊗[R] ker f →ₗ[R] ker (𝟙 ⊗ f)`.  -/
LinearMap.tensorKer : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    {N : Type u_4} →
                      {P : Type u_5} →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : AddCommGroup P] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module R P] →
                                (f : N →ₗ[R] P) →
                                  TensorProduct R M ↥f.ker →ₗ[S]
                                    ↥((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.comp_one : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : One M] [inst_1 : One N] [inst_2 : One P] (f : OneHom N P),
  f.comp 1 = 1
-- Mathlib.Order.Hom.Basic
OrderIso.self_trans_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), e.trans e.symm = OrderIso.refl α
-- Lean.Meta.Tactic.Cases
Lean.Meta.CasesSubgoal : Type
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.continuous_of_continuous_comp : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [inst : AddCommGroup E]
  [inst_1 : NormedField 𝕝] [inst_2 : Module 𝕝 E] [inst_3 : AddCommGroup F] [inst_4 : NormedField 𝕝₂]
  [inst_5 : Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_6 : RingHomIsometric τ₁₂] {q : SeminormFamily 𝕝₂ F ι'}
  [inst_7 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_9 : TopologicalSpace F],
  WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), (∀ (i : ι'), Continuous ⇑((q i).comp f)) → Continuous ⇑f
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.m_add_one_div_m_le_one_add : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {ε : ℝ} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ε ≤ 1 →
        ((↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1) /
              ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card)) ^
            2 ≤
          1 + ε ^ 5 / 49
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.hasSum_lt : ∀ {α : Type u_1} {f g : α → NNReal} {sf sg : NNReal} {i : α},
  (∀ (a : α), f a ≤ g a) → f i < g i → HasSum f sf → HasSum g sg → sf < sg
-- Mathlib.CategoryTheory.SingleObj
/-- Construct a natural transformation between functors `SingleObj M ⥤ C` by
giving a compatible morphism `SingleObj.star M`.  -/
CategoryTheory.SingleObj.natTrans : {M : Type u} →
  [inst : Monoid M] →
    {C : Type v} →
      [inst_1 : CategoryTheory.Category.{w, v} C] →
        {F G : CategoryTheory.Functor (CategoryTheory.SingleObj M) C} →
          (u : F.obj (CategoryTheory.SingleObj.star M) ⟶ G.obj (CategoryTheory.SingleObj.star M)) →
            (∀ (a : M),
                CategoryTheory.CategoryStruct.comp (F.map a) u = CategoryTheory.CategoryStruct.comp u (G.map a)) →
              (F ⟶ G)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.neg_fst : ∀ {q : ℕ} (x : LucasLehmer.X q), (-x).1 = -x.1
-- Mathlib.Data.List.SplitLengths
/-- Split a list to chunks of given lengths.
 -/
List.splitLengths : {α : Type u_1} → List ℕ → List α → List (List α)
-- Lean.Parser.Term
Lean.Parser.Term.throwNamedErrorAtMacro.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.quotient_map : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S] (p : Ideal R), Algebra.EssFiniteType (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
-- Mathlib.Topology.EMetricSpace.Weak
/-- If `α` has a topology induced by a linear order and is a weak extended metric space,
so is `WithTop α`  -/
instWeakEMetricSpaceWithTop : {α : Type u} →
  [t : TopologicalSpace α] →
    [inst : LinearOrder α] → [inst_1 : OrderTopology α] → [m : WeakEMetricSpace α] → WeakEMetricSpace (WithTop α)
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffOn_extChartAt_symm : ∀ {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] (x : M),
  ContMDiffOn (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (extChartAt I x).target
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.introsClean.loop : Lean.MVarId → CongrMetaM (List Lean.MVarId)
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenRatio_ne_zero : Real.goldenRatio ≠ 0
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.instEmptyCollection : {α : Type u_1} → [inst : BEq α] → EmptyCollection (Aesop.UnorderedArraySet α)
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The `n`-cocycles `Zⁿ(G, A)` of a `k`-linear `G`-representation `A`, i.e. the kernel of the
`n`th differential in the complex of homogeneous cochains.  -/
ContinuousCohomology.cocycles : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → TopRep k G → ℕ → TopModuleCat k
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.rightAdjointObjIsDefined_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (Y : D),
  F.rightAdjointObjIsDefined Y ↔ (F.op.comp (CategoryTheory.yoneda.obj Y)).IsRepresentable
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.dropLastTR.eq_1 : ∀ {α : Type u_1} (l : List α), l.dropLastTR = l.toArray.pop.toList
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.Mon C} {x y : M.Hom N}, x = y ↔ x.hom = y.hom
-- Mathlib.RingTheory.RootsOfUnity.Basic
ker_zpowGroupHom_eq_rootsOfUnity : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℤ}, (zpowGroupHom k).ker = rootsOfUnity k.natAbs M
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.addFreshJP : Array (Lean.Elab.Term.Do.Var × Bool) →
  Lean.Elab.Term.Do.Code → StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Name
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.measurable_preCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} {r : ℚ},
  Measurable (ProbabilityTheory.preCDF ρ r)
-- Plausible.Random
Plausible.Random.mk : {m : Type u → Type u_1} → {α : Type u} → ({g : Type} → [RandomGen g] → Plausible.RandGT g m α) → Plausible.Random m α
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.clm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {G : Type u_2} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  {c : 𝕜 → F →L[𝕜] G} {c' : F →L[𝕜] G} {u : 𝕜 → F} {u' : F},
  HasStrictDerivAt c c' x → HasStrictDerivAt u u' x → HasStrictDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instSemilatticeInf : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Min α] →
      [inst_1 : Top α] → [inst_2 : SemilatticeInf β] → [inst_3 : OrderTop β] → SemilatticeInf (InfTopHom α β)
-- Aesop.RulePattern
_private.Aesop.RulePattern.0.Aesop.RulePattern.elab.abstractMVars' : Lean.Expr → Lean.MetaM (Lean.Meta.AbstractMVarsResult × Std.HashMap Lean.MVarId ℕ × Std.HashMap Lean.LMVarId ℕ)
-- Mathlib.Algebra.AddConstMap.Basic
/-- A map of `AddConstMapClass` class semiconjugates shift by `a` to the shift by `b`:
`∀ x, f (x + a) = f x + b`.  -/
AddConstMapClass.map_add_const : ∀ {F : Type u_1} {G : outParam (Type u_2)} {H : outParam (Type u_3)} {inst : Add G} {inst_1 : Add H} {a : outParam G}
  {b : outParam H} {inst_2 : FunLike F G H} [self : AddConstMapClass F G H a b] (f : F) (x : G), f (x + a) = f x + b
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_cons : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (p : ℤ × M) (l : Mathlib.Tactic.FieldSimp.NF M),
  (p ::ᵣ l).eval = l.eval * Mathlib.Tactic.FieldSimp.zpow' p.2 p.1
-- Mathlib.Data.Vector.Defs
/-- If `a : α` and `l : Vector α n`, then `cons a l`, is the vector of length `n + 1`
whose first element is a and with l as the rest of the list.  -/
List.Vector.cons : {α : Type u_1} → {n : ℕ} → α → List.Vector α n → List.Vector α n.succ
-- Mathlib.Tactic.Have
/-- Uses `checkColGt` to prevent

```lean
have h
exact Nat
```

From being interpreted as
```lean
have h
  exact Nat
```
 -/
Mathlib.Tactic.haveIdLhs' : Lean.Parser.Parser
-- Mathlib.Logic.Equiv.List
/-- A finite type is encodable. Because the encoding is not unique, we wrap it in `Trunc` to
preserve computability.  -/
Fintype.truncEncodable : (α : Type u_2) → [DecidableEq α] → [Fintype α] → Trunc (Encodable α)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
IsIntegral.isAlmostIntegral_of_isLocalization : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {s : S},
  IsIntegral R s → ∀ M ≤ nonZeroDivisors R, ∀ [IsLocalization M S], IsAlmostIntegral R s
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
/-- An arrow in the groupoid defines, by conjugation, an isomorphism of groups between
its endpoints.
 -/
CategoryTheory.Groupoid.vertexGroupIsomOfMap : {C : Type u} → [inst : CategoryTheory.Groupoid C] → {c d : C} → (c ⟶ d) → (c ⟶ c) ≃* (d ⟶ d)
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Peek a value from the stack and place the result in local store.  -/
Turing.PartrecToTM2.peek' : Turing.PartrecToTM2.K' → Turing.PartrecToTM2.Stmt' → Turing.PartrecToTM2.Stmt'
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.nextn_zero : ∀ {s : String.Slice} {p : s.Pos}, p.nextn 0 = p
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_c_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 0 → P.toPoly.degree ≤ 0
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.isLocalHom_localRingHom : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [hJ : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J),
  IsLocalHom (Localization.localRingHom I J f hIJ)
-- Mathlib.RingTheory.RingHomProperties
RingHom.IsStableUnderBaseChange.mk : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.RespectsIso P →
    (∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
        [inst_4 : Algebra R T], P (algebraMap R T) → P (algebraMap S (TensorProduct R S T))) →
      RingHom.IsStableUnderBaseChange P
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Monoidal functors commute with left tensoring up to isomorphism  -/
CategoryTheory.Functor.Monoidal.commTensorLeft : {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] →
            (F : CategoryTheory.Functor C D) →
              [F.Monoidal] →
                (X : C) →
                  F.comp (CategoryTheory.MonoidalCategory.tensorLeft (F.obj X)) ≅
                    (CategoryTheory.MonoidalCategory.tensorLeft X).comp F
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.pullback_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f : X ⟶ Y), (CategoryTheory.Subobject.pullback f).obj ⊤ = ⊤
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.symm_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.symm.target = e.source
-- Mathlib.Algebra.Ring.Prod
RingEquiv.prodProdProdComm_toAddEquiv : ∀ (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [inst : NonAssocSemiring R]
  [inst_1 : NonAssocSemiring S] [inst_2 : NonAssocSemiring R'] [inst_3 : NonAssocSemiring S'],
  ↑(RingEquiv.prodProdProdComm R R' S S') = AddEquiv.prodProdProdComm R R' S S'
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedNatTrans.mk.inj : ∀ {V : Type v} {inst : CategoryTheory.Category.{w, v} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u₁}
  {inst_2 : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst_3 : CategoryTheory.EnrichedCategory V D}
  {F G : CategoryTheory.EnrichedFunctor V C D} {out out_1 : F.forget ⟶ G.forget},
  { out := out } = { out := out_1 } → out = out_1
-- Mathlib.Data.Set.Defs
/-- `Set.insert a s` is the set `{a} ∪ s`.

Note that you should **not** use this definition directly, but instead write `insert a s` (which is
mediated by the `Insert` typeclass).  -/
Set.insert : {α : Type u} → α → Set α → Set α
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map_coe : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), WithOne.map f ↑a = ↑(f a)
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.below : {motive : {n : ℕ} → (a : List.Vector ℕ n →. ℕ) → Nat.Partrec' a → Prop} →
  {n : ℕ} → {a : List.Vector ℕ n →. ℕ} → Nat.Partrec' a → Prop
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_π_app : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D}
  [inst_3 : CategoryTheory.IsConnected J] {B : D} {F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow K B)}
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.CostructuredArrow.proj K B))) (j : J),
  (CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone c).π.app j =
    CategoryTheory.CostructuredArrow.homMk (c.π.app j) ⋯
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.fst_smul : ∀ {ι : Type u_1} {α : Type u_3} {A : ι → Type u_2} [inst : (i : ι) → SMul α (A i)] (a : α) (x : GradedMonoid A),
  (a • x).fst = x.fst
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vaddCommClass_finset : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddCommClass α β γ], VAddCommClass α β (Finset γ)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_right_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∪ t ∪ u = s ∪ u ∪ t
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_x : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  ¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.x✝ S
-- Mathlib.Data.List.Pi
List.Pi.cons.congr_simp : ∀ {ι : Type u_1} {inst : DecidableEq ι} [inst_1 : DecidableEq ι] {α : ι → Sort u_2} (i : ι) (l : List ι) (a a_1 : α i),
  a = a_1 →
    ∀ (f f_1 : (j : ι) → j ∈ l → α j),
      f = f_1 → ∀ (j : ι) (a_2 : j ∈ i :: l), List.Pi.cons i l a f j a_2 = List.Pi.cons i l a_1 f_1 j a_2
-- Mathlib.Topology.Category.TopCat.OpenNhds
IsOpenMap.functorNhds_obj_coe : ∀ {X Y : TopCat} {f : X ⟶ Y} (h : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X)
  (U : TopologicalSpace.OpenNhds x), ↑((h.functorNhds x).obj U) = h.functor.obj ↑U
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_add_measure : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s : Set α} {μ ν : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε],
  MeasureTheory.IntegrableOn f s (μ + ν) ↔ MeasureTheory.IntegrableOn f s μ ∧ MeasureTheory.IntegrableOn f s ν
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.instHtmlEvalMetaMHtml : ProofWidgets.HtmlEval (Lean.MetaM ProofWidgets.Html)
-- Std.Time.Time.Unit.Basic
/-- Converts an `Hour.Offset` to a `Second.Offset`.
 -/
Std.Time.Hour.Offset.toSeconds : Std.Time.Hour.Offset → Std.Time.Second.Offset
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ S f → x ∈ interior S → HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Set.Iio x) x
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type t}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] {D : CategoryTheory.Limits.Cocone F}
  (hD : CategoryTheory.Limits.IsColimit D),
  have ff := fun a => (CategoryTheory.ConcreteCategory.hom (D.ι.app a.fst)) a.snd;
  Function.Surjective ff
-- Init.Prelude
/-- A product type in which both `α` and `β` are in the same universe.

It is called `MProd` is because it is the *universe-monomorphic* product type.
 -/
MProd : Type u → Type u → Type u
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- The morphism `Δ[c.dim + 1] ⟶ f.filtration (Order.succ j)` given
by `c : f.Cell j`, when `f` is a rank function for a proper pairing
of a subcomplex of a simplicial set.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          {f : P.RankFunction ι} →
            [P.IsProper] →
              {j : ι} →
                [inst_2 : SuccOrder ι] →
                  [NoMaxOrder ι] →
                    (c : f.Cell j) → SSet.stdSimplex.obj { len := c.dim + 1 } ⟶ (f.filtration (Order.succ j)).toSSet
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.inclLiftToTerminal_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (x : C),
  (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).hom.app x =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithTerminal.incl.obj x with
      | CategoryTheory.WithTerminal.of x => F.obj x
      | CategoryTheory.WithTerminal.star => Z)
-- Init.Data.Ord.Basic
List.compare_nil_cons : ∀ {α : Type u_1} [inst : Ord α] {x : α} {xs : List α}, compare [] (x :: xs) = Ordering.lt
-- Mathlib.GroupTheory.FinitelyPresentedGroup
Group.IsFinitelyPresented.exists_mulEquiv_presentedGroup : ∀ {G : Type u_1} [inst : Group G] [hg : Group.IsFinitelyPresented G], ∃ n s, s.Finite ∧ Nonempty (G ≃* PresentedGroup s)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff m₂ ⋯).get? k = none
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.one_lt_prod : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {f : ι → M}
  {s : Finset ι} [MulLeftStrictMono M], (∀ i ∈ s, 1 < f i) → s.Nonempty → 1 < ∏ i ∈ s, f i
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- Construct terminal object in the over category. This isn't an instance as it's not typically the
way we want to define terminal objects.
(For instance, this gives a terminal object which is different from the generic one given by
`over_product_of_widePullback` above.)
 -/
CategoryTheory.Over.over_hasTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C),
  CategoryTheory.Limits.HasTerminal (CategoryTheory.Over B)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.nextCoeff_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0
-- Mathlib.Control.Monad.Basic
/-- reduce the equivalence between two state monads to the equivalence between
their respective function spaces  -/
StateT.equiv : {σ₁ α₁ : Type u₀} →
  {σ₂ α₂ : Type u₁} →
    {m₁ : Type u₀ → Type v₀} →
      {m₂ : Type u₁ → Type v₁} → (σ₁ → m₁ (α₁ × σ₁)) ≃ (σ₂ → m₂ (α₂ × σ₂)) → StateT σ₁ m₁ α₁ ≃ StateT σ₂ m₂ α₂
-- Init.Data.List.Perm
List.Perm.count_eq : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α}, l₁.Perm l₂ → ∀ (a : α), List.count a l₁ = List.count a l₂
-- Init.Data.Fin.Fold
Fin.foldr_zero : ∀ {α : Sort u_1} (f : Fin 0 → α → α) (x : α), Fin.foldr 0 f x = x
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.instDecidableRelAdjReplaceVertex : {V : Type u_1} →
  (G : SimpleGraph V) →
    {s t : V} → [inst : DecidableEq V] → [DecidableRel G.Adj] → DecidableRel (G.replaceVertex s t).Adj
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_eq_zero_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.kahler x) y = 0 ↔ x = 0 ∨ y = 0
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- Smoothness exponent for infinitely differentiable functions.  -/
ContDiff.«term∞» : Lean.ParserDescr
-- Mathlib.Data.Finset.Sort
Finset.orderEmbOfFin_compl_singleton : ∀ {n : ℕ} {i : Fin (n + 1)} {k : ℕ} (h : {i}ᶜ.card = k),
  {i}ᶜ.orderEmbOfFin h = RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb
-- Mathlib.RingTheory.Ideal.Maps
RingHom.sub_mem_ker_iff : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Ring R] [inst_1 : Ring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F) {x y : R}, x - y ∈ RingHom.ker f ↔ f x = f y
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.mkD_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {g : C(α, β)}
  (hf : Continuous f), ContinuousMap.mkD f g = { toFun := f, continuous_toFun := hf }