mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Given such a diagram, then there is a natural morphism `W ⨿ₛ X ⟶ Y ⨿ₜ Z`.

```
  W ⟶ Y
 ↗   ↗
S ⟶ T
 ↘   ↘
  X ⟶ Z
```
 -/
CategoryTheory.Limits.pushout.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z S T : C} →
      (f₁ : S ⟶ W) →
        (f₂ : S ⟶ X) →
          [inst_1 : CategoryTheory.Limits.HasPushout f₁ f₂] →
            (g₁ : T ⟶ Y) →
              (g₂ : T ⟶ Z) →
                [inst_2 : CategoryTheory.Limits.HasPushout g₁ g₂] →
                  (i₁ : W ⟶ Y) →
                    (i₂ : X ⟶ Z) →
                      (i₃ : S ⟶ T) →
                        CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁ →
                          CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂ →
                            (CategoryTheory.Limits.pushout f₁ f₂ ⟶ CategoryTheory.Limits.pushout g₁ g₂)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedSignature.default : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Signature pu
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} (remaining : ℕ) (inner : Std.IterM m β) (remaining_1 : ℕ)
  (inner_1 : Std.IterM m β),
  ({ remaining := remaining, inner := inner } = { remaining := remaining_1, inner := inner_1 }) =
    (remaining = remaining_1 ∧ inner = inner_1)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instSub : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Sub β] → Sub (MeasureTheory.SimpleFunc α β)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_natCast_eq_lift : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.beth ↑n = Cardinal.lift.{v, u} c ↔ Cardinal.beth ↑n = c
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.equivalenceOfReindexing_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  (CategoryTheory.Limits.Cone.equivalenceOfReindexing e α).counitIso =
    (((CategoryTheory.Limits.Cone.postcompose α.inv).comp
              ((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
                (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom))).associator
          (CategoryTheory.Limits.Cone.whiskering e.functor) (CategoryTheory.Limits.Cone.postcompose α.hom)).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight
          ((CategoryTheory.Limits.Cone.postcompose α.inv).associator
            ((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
              (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom))
            (CategoryTheory.Limits.Cone.whiskering e.functor))
          (CategoryTheory.Limits.Cone.postcompose α.hom) ≪≫
        CategoryTheory.Functor.isoWhiskerRight
            ((CategoryTheory.Limits.Cone.postcompose α.inv).isoWhiskerLeft
              (CategoryTheory.NatIso.ofComponents
                (fun s => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯))
            (CategoryTheory.Limits.Cone.postcompose α.hom) ≪≫
          CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Limits.Cone.postcompose α.inv).rightUnitor
              (CategoryTheory.Limits.Cone.postcompose α.hom) ≪≫
            CategoryTheory.NatIso.ofComponents
              (fun s => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯
-- Mathlib.Control.Basic
CommApplicative.commutative_map : ∀ {m : Type u → Type v} [h : Applicative m] [CommApplicative m] {α β γ : Type u} (a : m α) (b : m β) {f : α → β → γ},
  f <$> a <*> b = flip f <$> b <*> a
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.op_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (a : Mᵃᵒᵖ),
  (AddMonoidHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.succ_lt : ∀ {α : Type u_1} {a b : α} [inst : PartialOrder α] [inst_1 : SuccOrder α],
  Order.IsSuccLimit b → a < b → Order.succ a < b
-- Mathlib.Data.Nat.GCD.BigOperators
Nat.coprime_fintype_prod_left_iff : ∀ {ι : Type u_1} [inst : Fintype ι] {s : ι → ℕ} {x : ℕ}, (∏ i, s i).Coprime x ↔ ∀ (i : ι), (s i).Coprime x
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.instIsCancelMulZero : ∀ {𝕜 : Type u_1} [inst : NonUnitalSeminormedRing 𝕜] [IsCancelMulZero 𝕜], IsCancelMulZero ↑(Metric.ball 0 1)
-- Mathlib.Data.Int.ModEq
Int.modEq_sub : ∀ (a b : ℤ), a ≡ b [ZMOD a - b]
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.map_comp_inr : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N'),
  (Monoid.Coprod.map f g).comp Monoid.Coprod.inr = Monoid.Coprod.inr.comp g
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalarsSum_of_subsingleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) [Subsingleton E] {x : E}, FormalMultilinearSeries.ofScalarsSum c x = 0
-- Mathlib.Topology.MetricSpace.Lipschitz
lipschitzWith_min : LipschitzWith 1 fun p => min p.1 p.2
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.decidableLT.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α}
  [inst_3 : DecidableLT α] (a b : Localization s),
  a.decidableLT b = a.recOnSubsingleton₂ b fun x x_1 x_2 x_3 => decidable_of_iff' (↑x_3 * x < ↑x_2 * x_1) ⋯
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_neg : ∀ {R : Type u} {M : Type v} [inst : Neg R] [inst_1 : Neg M] (x : TrivSqZeroExt R M), (-x).fst = -x.fst
-- Mathlib.MeasureTheory.Integral.IntervalAverage
/-- If `f : ℝ → ℝ` is continuous on `uIcc a b`, the interval has finite and nonzero `μ`-measure,
then `∃ c ∈ Ι a b, f c = ⨍ x in Ι a b, f x ∂μ`.  -/
exists_eq_interval_average_of_measure : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  ContinuousOn f (Set.uIcc a b) →
    μ (Set.uIoc a b) ≠ ⊤ → μ (Set.uIoc a b) ≠ 0 → ∃ c ∈ Set.uIoc a b, f c = ⨍ (x : ℝ) in Set.uIoc a b, f x ∂μ
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivialization.prod_apply' : ∀ (𝕜 : Type u_1) {B : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : TopologicalSpace B] {F₁ : Type u_3}
  [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_4}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_5} [inst_5 : NormedAddCommGroup F₂]
  [inst_6 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_8 : (x : B) → AddCommMonoid (E₁ x)] [inst_9 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_10 : (x : B) → AddCommMonoid (E₂ x)] [inst_11 : (x : B) → Module 𝕜 (E₂ x)]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : FiberBundle F₂ E₂] [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₂] {x : B} (hx₁ : x ∈ e₁.baseSet) (hx₂ : x ∈ e₂.baseSet) (v₁ : E₁ x)
  (v₂ : E₂ x),
  ↑(e₁.prod e₂) ⟨x, (v₁, v₂)⟩ =
    (x, (Bundle.Trivialization.continuousLinearEquivAt 𝕜 e₁ x hx₁) v₁,
      (Bundle.Trivialization.continuousLinearEquivAt 𝕜 e₂ x hx₂) v₂)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.instSliceableImplUnitRioSlice : {α : Type u} →
  [inst : Ord α] →
    Std.Rio.Sliceable (Std.DTreeMap.Internal.Impl α fun x => Unit) α (Std.DTreeMap.Internal.Unit.RioSlice α)
-- Mathlib.CategoryTheory.Sites.InducedTopology
CategoryTheory.Functor.induced_induced_le : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  (G : CategoryTheory.Functor D E) (J : CategoryTheory.GrothendieckTopology E),
  F.inducedTopology (G.inducedTopology J) ≤ (F.comp G).inducedTopology J
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (xs : List ((a : α) × β a)),
  Std.Internal.List.minKey? xs = Option.map Sigma.fst (Std.Internal.List.minEntry? xs)
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.girth_top : ∀ {α : Type u_1}, 3 ≤ ENat.card α → ⊤.girth = 3
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMax'_dual : ∀ {α : Type u_1} (t : Ordnode α) (x : α), Ordnode.findMax' x t.dual = t.findMin' x
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.description : Lean.Elab.Do.ControlStack → Unit → Lean.MessageData
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- Analogue of `congr_fun h x`,
when `h : f = g` is an equality between morphisms in a concrete category.
 -/
CategoryTheory.congr_fun : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} {f g : X ⟶ Y},
  f = g →
    ∀ (x : CategoryTheory.ToType X),
      (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.adjoint_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E], LinearMap.adjoint LinearMap.id = LinearMap.id
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.eventually_left_inverse : ∀ {𝕜 : 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] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  ∀ᶠ (x : E) in nhds a, HasStrictFDerivAt.localInverse f f' a hf (f x) = x
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_right' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto (fun x => ↑⌈x⌉) (nhdsWithin (↑n) (Set.Ioi ↑n)) (nhds (↑n + 1))
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.evaluationPreservesLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (D : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Sheaf J RingCat) [Small.{v, u₂} D] (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesLimitsOfShape D (SheafOfModules.evaluation R X)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Adding a point in the affine span of a set does not change whether that set is coplanar.  -/
coplanar_insert_iff_of_mem_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p : P}, p ∈ affineSpan k s → (Coplanar k (insert p s) ↔ Coplanar k s)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- Notation for the identity functor on a based category.  -/
CategoryTheory.BasedFunctor.«term𝟭» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Definition of the positive part of the logarithm, formulated as a theorem.  -/
Real.posLog_def : Real.posLog = 0 ⊔ fun x => Real.log x
-- Mathlib.Topology.ShrinkingLemma
/-- Auxiliary definition for the proof of the shrinking lemma. A partial refinement of a covering
`⋃ i, u i` of a set `s` is a map `v : ι → Set X` and a set `carrier : Set ι` such that

* `s ⊆ ⋃ i, v i`;
* all `v i` are open;
* if `i ∈ carrier v`, then `closure (v i) ⊆ u i`;
* if `i ∉ carrier`, then `v i = u i`.

This type is equipped with the following partial order: `v ≤ v'` if `v.carrier ⊆ v'.carrier`
and `v i = v' i` for `i ∈ v.carrier`. We will use Zorn's lemma to prove that this type has
a maximal element, then show that the maximal element must have `carrier = univ`.  -/
ShrinkingLemma.PartialRefinement : {ι : Type u_1} → {X : Type u_2} → [TopologicalSpace X] → (ι → Set X) → Set X → (Set X → Prop) → Type (max u_1 u_2)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.insert : ℤ → Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instVAddAssocClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M N] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddAssocClass M N α], VAddAssocClass Mᵒᵈ N α
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.iSup_pow : ∀ {ι : Sort u_1} [Nonempty ι] (f : ι → NNReal) (n : ℕ), (⨆ i, f i) ^ n = ⨆ i, f i ^ n
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_natCast_atTop_cobounded : ∀ {α : Type u_1} [inst : NormedRing α] [NormSMulClass ℤ α] [Nontrivial α],
  Filter.Tendsto Nat.cast Filter.atTop (Bornology.cobounded α)
-- Mathlib.CategoryTheory.Yoneda
/-- Taking the `unop` of morphisms is a natural isomorphism.  -/
CategoryTheory.Coyoneda.opIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.yoneda.comp ((CategoryTheory.Functor.whiskeringLeft C Cᵒᵖᵒᵖ (Type v₁)).obj (CategoryTheory.opOp C)) ≅
      CategoryTheory.coyoneda
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.toRegular_coe : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a : Heyting.Regular α), Heyting.Regular.toRegular ↑a = a
-- Mathlib.Data.Set.Basic
Set.Nonempty.of_subtype : ∀ {α : Type u} {s : Set α} [Nonempty ↑s], s.Nonempty
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprLinarithConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Grind.LinarithConfig
-- Mathlib.Condensed.Equivalence
/-- The equivalence from coherent sheaves on `Profinite` to coherent sheaves on `CompHaus`
(i.e. condensed sets).  -/
Condensed.ProfiniteCompHaus.equivalence : (A : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [∀ (X : CompHausᵒᵖ),
          CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X profiniteToCompHaus.op) A] →
      CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) A ≌ Condensed A
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.prop_arbitrary : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : P.Nonempty], P P.arbitrary
-- Mathlib.CategoryTheory.EssentialImage
/-- Isomorphic functors have equal essential images.  -/
CategoryTheory.Functor.essImage_eq_of_natIso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (h : F ≅ F'), F.essImage = F'.essImage
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.getBuilder : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Aesop.Frontend.RuleConfig → m Aesop.Frontend.DBuilderName
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_mono₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₃ = 0 ↔ CategoryTheory.Mono T.mor₁
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.isNormal' : ∀ {G : Type u_1} [inst : AddGroup G] (self : FiniteIndexNormalAddSubgroup G), self.Normal
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalContradiction : Lean.Elab.Tactic.Tactic
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P},
  Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0
-- Mathlib.Algebra.Group.Defs
/-- In a class equipped with instances of both `AddMonoid` and `Neg`, this definition records what
the default definition for `Sub` would be: `a + -b`.  This is later provided as the default value
for the `Sub` instance in `SubNegMonoid`.

We keep it as a separate definition rather than inlining it in `SubNegMonoid` so that the `Sub`
field of individual `SubNegMonoid`s constructed using that default value will not be unfolded at
`.instance` transparency.  -/
SubNegMonoid.sub' : {G : Type u} → [AddMonoid G] → [Neg G] → G → G → G
-- Mathlib.Analysis.Convex.StoneSeparation
/-- **Stone's Separation Theorem**  -/
exists_convex_convex_compl_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s t : Set E},
  Convex 𝕜 s → Convex 𝕜 t → Disjoint s t → ∃ C, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestRevMatchAt_of_get_eq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.startPos},
  (pos.prev h).get ⋯ = c → String.Slice.Pattern.Model.IsLongestRevMatchAt c (pos.prev h) pos
-- Mathlib.Topology.Order
preimage_nhds_coinduced : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {π : α → β} {s : Set β} {a : α},
  s ∈ nhds (π a) → π ⁻¹' s ∈ nhds a
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.isBase_of_maximal : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J) → M.IsBase I
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_mul_of_pos : ∀ {a : ℤ} (b c : ℤ), 0 < a → (a * b).fdiv (a * c) = b.fdiv c
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_lt_self : ∀ {o : Ordinal.{u_1}} (i : o.ToType), (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.coe_comp_rangeRestrict : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N),
  Subtype.val ∘ ⇑f.rangeRestrict = ⇑f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {k : α} {v : β}, (t.insert k v)[k]! = v
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Multiplication of monomials.  -/
Tactic.ComputeAsymptotics.Monomial.mul : Tactic.ComputeAsymptotics.Monomial → Tactic.ComputeAsymptotics.Monomial → Tactic.ComputeAsymptotics.Monomial
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- If `x` is an element of a subgroup `s` of a seminormed group `E`,
its norm in `s` is equal to its norm in `E`.  -/
AddSubgroup.coe_norm : ∀ {E : Type u_1} [inst : SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s), ‖x‖ = ‖↑x‖
-- Init.Data.List.Basic
List.filter_eq_filterTR : @List.filter = @List.filterTR
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_iUnion_fintype : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [inst_2 : Fintype ι] {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      (∀ (i : ι), MeasureTheory.IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i, s i, f x ∂μ = ∑ i, ∫ (x : X) in s i, f x ∂μ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.eqToIso_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} (h : n = n),
  X.eqToIso h = CategoryTheory.Iso.refl (X.obj { len := n })
-- Init.WFExtrinsicFix
_private.Init.WFExtrinsicFix.0.WellFounded.partialExtrinsicFix₂.eq_1 : ∀ {α : Sort u_1} {β : α → Sort u_2} {C₂ : (a : α) → β a → Sort u_3} [inst : ∀ (a : α) (b : β a), Nonempty (C₂ a b)]
  (R : (a : α) ×' β a → (a : α) ×' β a → Prop)
  (F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b) (a : α) (b : β a),
  WellFounded.partialExtrinsicFix₂ R F a b =
    WellFounded.extrinsicFix₂ (fun p q => R ⟨p.fst, ↑p.snd⟩ ⟨q.fst, ↑q.snd⟩)
      (fun a_1 b_1 recur => F a_1 ↑b_1 fun a' b' hR => recur a' ⟨b', ⋯⟩ hR) a ⟨b, ⋯⟩
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.one_sub_mem : ∀ {β : Type u_2} [inst : Ring β] [inst_1 : PartialOrder β] [IsOrderedRing β] {t : β},
  t ∈ Set.Ioo 0 1 → 1 - t ∈ Set.Ioo 0 1
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- **Alias** of the forward direction of `LinearMap.hasNoetherianRange_iff_quotient_ker`. -/
LinearMap.HasNoetherianRange.quotient_ker : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.HasNoetherianRange → IsNoetherian K (V ⧸ f.ker)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_word_prod_nontrivial_of_head_eq_last : ∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G) {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
  (∀ (i : ι), (X i).Nonempty) →
    Pairwise (Function.onFun Disjoint X) →
      (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
        ∀ [Nontrivial ι] {i : ι} (w : Monoid.CoprodI.NeWord H i i), (Monoid.CoprodI.lift f) w.prod ≠ 1
-- Std.Data.TreeSet.Basic
/-- Inserts multiple elements into the tree set by iterating over the given collection and calling
`insert`. If the same element (with respect to `cmp`) appears multiple times, the first occurrence
takes precedence.

Note: this precedence behavior is true for `TreeSet` and `TreeSet.Raw`. The `insertMany` function on
`TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw` behaves differently: it will prefer the last
appearance.
 -/
Std.TreeSet.insertMany : {α : Type u} → {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ α] → Std.TreeSet α cmp → ρ → Std.TreeSet α cmp
-- Batteries.Data.String.Lemmas
String.Legacy.length_map : ∀ (s : String) (f : Char → Char), (String.Legacy.map f s).length = s.length
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_snd : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B),
  (CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso.inv.app X).2 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Sum.swapCompInr A' A).inv X)
      ((CategoryTheory.Sum.inr_ A' A).associator (CategoryTheory.Sum.swap A' A) X).hom
-- Mathlib.RingTheory.LocalRing.Etale
/-- If `R → S` is étale and `R[β] = S`, then `f'(β)` is a unit in `S`,
where `f = minpoly R β`. The proof reduces to separability of the
residue field extension via `minpoly_map_residue`.  -/
IsLocalRing.isUnit_aeval_derivative_minpoly_of_adjoin_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsLocalRing S]
  [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S] {β : S},
  R[β] = ⊤ → IsUnit ((Polynomial.aeval β) (Polynomial.derivative (minpoly R β)))
-- Batteries.Data.Nat.Basic
/-- Diagonal recursor for `Nat`
 -/
Nat.recDiag : {motive : ℕ → ℕ → Sort u_1} →
  motive 0 0 →
    ((n : ℕ) → motive 0 n → motive 0 (n + 1)) →
      ((m : ℕ) → motive m 0 → motive (m + 1) 0) →
        ((m n : ℕ) → motive m n → motive (m + 1) (n + 1)) → (m n : ℕ) → motive m n