mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.AddMon C),
  ((CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso C).inv.app X).hom =
    CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Nat.Ioc_eq_of_Icc_succ_eq : ∀ {m n : ℕ} {s : Finset ℕ}, Finset.Icc (m + 1) n = s → Finset.Ioc m n = s
-- Mathlib.Algebra.Module.Presentation.DirectSum
/-- The direct sum admits a presentation by generators and relations.  -/
Module.Relations.Solution.IsPresentation.directSum.isRepresentationCore : {A : Type u} →
  [inst : Ring A] →
    {ι : Type w} →
      [inst_1 : DecidableEq ι] →
        {relations : ι → Module.Relations A} →
          {M : ι → Type v} →
            [inst_2 : (i : ι) → AddCommGroup (M i)] →
              [inst_3 : (i : ι) → Module A (M i)] →
                {solution : (i : ι) → (relations i).Solution (M i)} →
                  (∀ (i : ι), (solution i).IsPresentation) →
                    (Module.Relations.Solution.directSum solution).IsPresentationCore
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The line derivative commutes with scalar multiplication, `∂_{r • v} x = r • ∂_{v} x` for all
`r : R` and `v : V`.
 -/
LineDerivLeftSMul : (R : Type u_11) →
  (V : Type u) → (E : Type v) → (F : outParam (Type w)) → [SMul R V] → [SMul R F] → [LineDeriv V E F] → Prop
-- Mathlib.Data.Finset.Image
Finset.mem_map_mk : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {a : α} {s : Finset α} (hf : Function.Injective f),
  f a ∈ Finset.map { toFun := f, inj' := hf } s ↔ a ∈ s
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- A property of objects in a category `C` is a predicate `C → Prop`.  -/
CategoryTheory.ObjectProperty : (C : Type u) → [CategoryTheory.CategoryStruct.{v, u} C] → Type u
-- Mathlib.Order.Basic
update_le_update_iff' : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x : (i : ι) → π i}
  {i : ι} {a b : π i}, Function.update x i a ≤ Function.update x i b ↔ a ≤ b
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.mkAuxMVarType.abstractRangeAux : Array Lean.Expr → ℕ → Lean.Expr → Lean.MetavarContext.MkBinding.M Lean.Expr
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableNeg.mk : ∀ {G : Type u_2} [inst : Neg G] [inst_1 : MeasurableSpace G], Measurable Neg.neg → MeasurableNeg G
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mem_nonZeroDivisors_iff' : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {r : M₀},
  r ∈ nonZeroDivisors M₀ ↔ r ∈ nonZeroDivisorsLeft M₀ ∧ r ∈ nonZeroDivisorsRight M₀
-- Mathlib.Algebra.BigOperators.Group.Finset.Interval
Finset.sum_Icc_succ_eq_add_endpoints : ∀ {R : Type u_1} [inst : AddCommGroup R] (f : ℤ → R) {N : ℕ},
  ∑ m ∈ Finset.Icc (-(↑N + 1)) (↑N + 1), f m = f (↑N + 1) + f (-(↑N + 1)) + ∑ m ∈ Finset.Icc (-↑N) ↑N, f m
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- If there is a pointwise left Kan extension of `F` along `L`, and if `G` preserves them,
then `G` preserves left Kan extensions of `F` along `L`.  -/
CategoryTheory.Functor.preservesPointwiseLKEOfHasPointwiseAndPreservesPointwise : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [L.HasPointwiseLeftKanExtension F] [G.PreservesPointwiseLeftKanExtension F L],
  G.PreservesLeftKanExtension F L
-- Mathlib.Algebra.Module.ULift
ULift.smulLeft : {R : Type u} → {M : Type v} → [SMul R M] → SMul (ULift.{u_1, u} R) M
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.map.eq_1 : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] (f : M →ₗ[R'] N),
  TrivSqZeroExt.map f = TrivSqZeroExt.liftEquivOfComm ⟨TrivSqZeroExt.inrHom R' N ∘ₗ f, ⋯⟩
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mk.injEq : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (toAddSubmonoid : AddSubmonoid M)
  (smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier)
  (toAddSubmonoid_1 : AddSubmonoid M)
  (smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier),
  ({ toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' } =
      { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 }) =
    (toAddSubmonoid = toAddSubmonoid_1)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.forget_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Center C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Center.forget C) X Y =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Center.forget C).obj X)
        ((CategoryTheory.Center.forget C).obj Y))
-- Mathlib.Data.List.Dedup
List.dedup_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.dedup ⊆ l
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.nnnorm_nnrpow : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A)
  {r : NNReal}, 0 < r → autoParam (0 ≤ a) CFC.nnnorm_nnrpow._auto_1 → ‖a ^ r‖₊ = ‖a‖₊ ^ ↑r
-- Init.Data.Array.Subarray
/-- Checks whether any of the elements in a subarray satisfy a monadic Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that satisfies the predicate is found.

Example:
```lean example
#eval #["red", "green", "blue", "orange"].toSubarray.popFront.anyM fun x => do
  IO.println x
  pure (x == "blue")
```
```output
green
blue
```
```output
true
```
 -/
Subarray.anyM : {α : Type u} → {m : Type → Type w} → [Monad m] → (α → m Bool) → Subarray α → m Bool
-- Init.Data.UInt.Bitwise
USize.toNat_not : ∀ (a : USize), (~~~a).toNat = USize.size - 1 - a.toNat
-- Mathlib.Data.Matrix.Block
/-- `Matrix.blockDiagonal'` as a `RingHom`.  -/
Matrix.blockDiagonal'RingHom : {o : Type u_4} →
  (m' : o → Type u_7) →
    (α : Type u_12) →
      [inst : DecidableEq o] →
        [inst_1 : (i : o) → DecidableEq (m' i)] →
          [inst_2 : Fintype o] →
            [inst_3 : (i : o) → Fintype (m' i)] →
              [inst_4 : NonAssocSemiring α] →
                ((i : o) → Matrix (m' i) (m' i) α) →+* Matrix ((i : o) × m' i) ((i : o) × m' i) α
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.eq_symm_apply : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B) {x : B} {y : A},
  y = e.symm x ↔ e y = x
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropyInfEntourage_closure : ∀ {X : Type u_1} {T : X → X} {V : SetRel X X} [inst : UniformSpace X],
  Continuous T →
    ∀ (F : Set X) (U : SetRel X X),
      V ∈ uniformity X →
        Dynamics.coverEntropyInfEntourage T (closure F) (V.comp U) ≤ Dynamics.coverEntropyInfEntourage T F U
-- Mathlib.Algebra.Homology.Bifunctor
/-- The first differential on `mapBifunctor K₁ K₂ F c`  -/
HomologicalComplex.mapBifunctor.D₁ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            (K₁ : HomologicalComplex C₁ c₁) →
                              (K₂ : HomologicalComplex C₂ c₂) →
                                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  [inst_6 : F.PreservesZeroMorphisms] →
                                    [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      (c : ComplexShape J) →
                                        [inst_8 : TotalComplexShape c₁ c₂ c] →
                                          [inst_9 : K₁.HasMapBifunctor K₂ F c] →
                                            [inst_10 : DecidableEq J] →
                                              (j j' : J) → (K₁.mapBifunctor K₂ F c).X j ⟶ (K₁.mapBifunctor K₂ F c).X j'
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommGroupOfAddMonoidHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddCommGroup (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instAddCommGroupOfAddMonoidHomClass = { toAddGroup := DirectLimit.instAddGroup, add_comm := ⋯ }
-- Mathlib.Order.Filter.Map
Function.Surjective.filter_map_top : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → Filter.map f ⊤ = ⊤
-- Mathlib.Algebra.DualQuaternion
Quaternion.fst_imI_dualNumberEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (d : DualNumber (Quaternion R)),
  TrivSqZeroExt.fst (Quaternion.dualNumberEquiv.symm d).imI = (TrivSqZeroExt.fst d).imI
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanIso.bijOn : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β}, IsMulFreimanIso n A B f → Set.BijOn f A B
-- Mathlib.Algebra.Group.Defs
NPow.ofPow : {M : Type u_2} → [Pow M ℕ] → NPow M
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.units_ofUnits_eq : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ), S.ofUnits.units = S
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.equivRing_symm_X : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S), P.equivRing.symm P.X = P.x
-- Init.Data.Array.Basic
/-- Inserts an element into an array at the specified index. If the index is greater than the size of
the array, then the array is returned unmodified.

In other words, the new element is inserted into the array `as` after the first `i` elements of
`as`.

This function takes worst case `O(n)` time because it has to swap the inserted element into place.

Examples:
 * `#["tues", "thur", "sat"].insertIdx 1 "wed" = #["tues", "wed", "thur", "sat"]`
 * `#["tues", "thur", "sat"].insertIdx 2 "wed" = #["tues", "thur", "wed", "sat"]`
 * `#["tues", "thur", "sat"].insertIdx 3 "wed" = #["tues", "thur", "sat", "wed"]`
 -/
Array.insertIdx : {α : Type u} → (as : Array α) → (i : ℕ) → α → autoParam (i ≤ as.size) Array.insertIdx._auto_1 → Array α
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
/-- The underlying endofunctor `r : C ⥤ C` of a preradical `Φ`.  -/
CategoryTheory.Abelian.Preradical.r : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Abelian.Preradical C → CategoryTheory.Functor C C
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_eball_le`. -/
EMetric.diam_ball : ∀ {X : Type u_2} {x : X} [inst : PseudoEMetricSpace X] {r : ENNReal}, Metric.ediam (Metric.eball x r) ≤ 2 * r
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- `lTensorHom M` is the natural linear map that sends a linear map `f : N →ₗ P` to `M ⊗ f`.

See also `Module.End.lTensorAlgHom`.  -/
LinearMap.lTensorHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      {N : Type u_8} →
        {P : Type u_9} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] → (N →ₗ[R] P) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M P
-- Init.Data.Int.DivMod.Bootstrap
_private.Init.Data.Int.DivMod.Bootstrap.0.Int.emod_add_mul_ediv.aux : ∀ (m n : ℕ), ↑n - (↑m % ↑n + 1) - (↑n * (↑m / ↑n) + ↑n) = Int.negSucc m
-- Init.Data.List.Nat.Modify
List.modifyTailIdx_modifyTailIdx : ∀ {α : Type u_1} {f g : List α → List α} (i j : ℕ) (l : List α),
  (l.modifyTailIdx j f).modifyTailIdx (i + j) g = l.modifyTailIdx j fun l => (f l).modifyTailIdx i g
-- Mathlib.Data.Set.Sups
Set.sep_infs_le : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t : Set α) (a : α),
  {b | b ∈ s ⊼ t ∧ a ≤ b} = {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}
-- Init.Data.Nat.Lemmas
Nat.dvd_mul_of_div_dvd : ∀ {a b c : ℕ}, b ∣ a → a / b ∣ c → a ∣ b * c
-- Init.Data.SInt.Lemmas
USize.toISize_neg : ∀ (a : USize), (-a).toISize = -a.toISize
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopicalAlgebra.weakEquivalences (CochainComplex.Plus C)).IsStableUnderRetracts
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posDef_intCast_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] [NoZeroDivisors R] [Nonempty n] [Nontrivial R] {d : ℤ}, (↑d).PosDef ↔ 0 < d
-- Init.WFExtrinsicFix
WellFounded.extrinsicFix_invImage : ∀ {α : Sort u_3} {C : α → Sort u_2} {α' : Sort u_1} [inst : ∀ (a : α), Nonempty (C a)] (R : α → α → Prop) (f : α' → α)
  (F : (a : α) → ((a' : α) → R a' a → C a') → C a) (F' : (a : α') → ((a' : α') → R (f a') (f a) → C (f a')) → C (f a)),
  (∀ (a : α') (r : (a' : α) → R a' (f a) → C a'), F (f a) r = F' a fun a' hR => r (f a') hR) →
    ∀ (a : α'), WellFounded R → WellFounded.extrinsicFix (InvImage R f) F' a = WellFounded.extrinsicFix R F (f a)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis'.isBasis_closure_right : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis' I X → M.IsBasis I (M.closure X)
-- Aesop.Script.Step
Aesop.Script.Step.mk.sizeOf_spec : ∀ (preState : Lean.Meta.SavedState) (preGoal : Lean.MVarId) (tactic : Aesop.Script.Tactic)
  (postState : Lean.Meta.SavedState) (postGoals : Array Aesop.GoalWithMVars),
  sizeOf
      { preState := preState, preGoal := preGoal, tactic := tactic, postState := postState, postGoals := postGoals } =
    1 + sizeOf preState + sizeOf preGoal + sizeOf tactic + sizeOf postState + sizeOf postGoals
-- Mathlib.Topology.ClusterPt
isClosed_iff_accPt : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s ↔ ∀ (a : X), AccPt a (Filter.principal s) → a ∈ s
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.const_apply : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] (y : Y) (x : X),
  (Convexity.ConvexSpace.AffineMap.const y) x = y
-- Mathlib.Algebra.Order.Sub.Basic
tsub_add_min : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, a - b + min a b = a
-- Mathlib.Order.Filter.NAry
Filter.map₂_mk_eq_prod : ∀ {α : Type u_1} {β : Type u_3} (f : Filter α) (g : Filter β), Filter.map₂ Prod.mk f g = f ×ˢ g
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.IsOver.trans : ∀ {X Y Z S : AlgebraicGeometry.Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S} {f : X.PartialIso Y} {g : Y.PartialIso Z},
  AlgebraicGeometry.Scheme.PartialIso.IsOver sX sY f →
    AlgebraicGeometry.Scheme.PartialIso.IsOver sY sZ g → AlgebraicGeometry.Scheme.PartialIso.IsOver sX sZ (f.trans g)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_le_two_mul_radius : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam ≤ 2 * G.radius
-- Std.Sync.Semaphore
/-- Tries to acquire a permit without blocking. Returns `true` on success.
 -/
Std.Semaphore.tryAcquire : Std.Semaphore → BaseIO Bool
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atBot_atTop_iff_of_antitone : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {f : α → β}
  [inst_2 : Preorder β], Antitone f → (Filter.Tendsto f Filter.atBot Filter.atTop ↔ ∀ (b : β), ∃ a, b ≤ f a)
-- Mathlib.Algebra.AddConstMap.Equiv
/-- An equivalence between `G` and `H` conjugating `(· + a)` to `(· + b)`,
denoted as `G ≃+c[a, b] H`.  -/
AddConstEquiv : (G : Type u_1) → (H : Type u_2) → [Add G] → [Add H] → G → H → Type (max u_1 u_2)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.ext_fourfold : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P : Type u_9} {Q : Type u_10} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid P] [inst_5 : AddCommMonoid Q] [inst_6 : AddCommMonoid P₂] [inst_7 : Module R M]
  [inst_8 : Module R N] [inst_9 : Module R₂ P₂] [inst_10 : Module R P] [inst_11 : Module R Q]
  {g h : TensorProduct R (TensorProduct R (TensorProduct R M N) P) Q →ₛₗ[σ₁₂] P₂},
  (∀ (w : M) (x : N) (y : P) (z : Q), g (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) = h (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)) → g = h
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instEpiFactorThruImage : ∀ (Δ Δ' : SimplexCategory) (θ : Δ ⟶ Δ'), CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage θ)
-- Mathlib.Algebra.CharZero.Defs
Nat.cast_inj : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] {m n : ℕ}, ↑m = ↑n ↔ m = n
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelπ_desc : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0),
  CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) (SemiNormedGrp.explicitCokernelDesc w) = g
-- Mathlib.MeasureTheory.Integral.IntervalAverage
/-- **Alias** of `exists_eq_interval_average_of_nullSingletonClass`.

---

If `f : ℝ → ℝ` is continuous on `uIcc a b`, the interval has finite and nonzero `μ`-measure,
and `μ` has value zero on singletons, then `∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ`.  -/
exists_eq_interval_average_of_noAtoms : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  ContinuousOn f (Set.uIcc a b) →
    μ (Set.uIoc a b) ≠ ⊤ → μ (Set.uIoc a b) ≠ 0 → ∃ c ∈ Set.uIoo a b, f c = ⨍ (x : ℝ) in Set.uIoc a b, f x ∂μ
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.toPartialEquiv_coe : ∀ {𝕜 : 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),
  ↑I.toPartialEquiv = ↑I
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.coverPreserving : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D)
  [CategoryTheory.Functor.IsDenseSubsite J K G], CategoryTheory.CoverPreserving J K G
-- Init.Data.List.Lemmas
List.replicate_inj : ∀ {n : ℕ} {α : Type u_1} {a : α} {m : ℕ} {b : α}, List.replicate n a = List.replicate m b ↔ n = m ∧ (n = 0 ∨ a = b)
-- Init.Data.SInt.Bitwise
Int32.zero_xor : ∀ {a : Int32}, 0 ^^^ a = a
-- Init.Internal.Order.Basic
Lean.Order.Option.admissible_eq_some : ∀ {α : Type u_1} (P : Prop) (y : α), Lean.Order.admissible fun x => x = some y → P
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Methods.mk.injEq : ∀ (propagateUp propagateDown : Lean.Meta.Grind.Propagator) (evalTactic : Lean.Meta.Grind.EvalTactic)
  (propagateUp_1 propagateDown_1 : Lean.Meta.Grind.Propagator) (evalTactic_1 : Lean.Meta.Grind.EvalTactic),
  ({ propagateUp := propagateUp, propagateDown := propagateDown, evalTactic := evalTactic } =
      { propagateUp := propagateUp_1, propagateDown := propagateDown_1, evalTactic := evalTactic_1 }) =
    (propagateUp = propagateUp_1 ∧ propagateDown = propagateDown_1 ∧ evalTactic = evalTactic_1)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinite_finite : ∀ {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E),
  (IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).matroid.Finite
-- Init.Data.Bool
Bool.eq_false_iff : ∀ {b : Bool}, b = false ↔ b ≠ true
-- Mathlib.Order.Filter.Basic
Set.EqOn.eventuallyEq_of_mem : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {l : Filter α} {f g : α → β}, Set.EqOn f g s → s ∈ l → f =ᶠ[l] g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → Std.DTreeMap.Const.get? t a = none
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestTacticSeq : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extend_none : ∀ {n : ℕ} (c : OrderedFinpartition n), c.extend none = c.extendLeft
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval.eq_def : ∀ (x : Nat.Partrec.Code),
  x.eval =
    match x with
    | Nat.Partrec.Code.zero => pure 0
    | Nat.Partrec.Code.succ => ↑Nat.succ
    | Nat.Partrec.Code.left => ↑fun n => (Nat.unpair n).1
    | Nat.Partrec.Code.right => ↑fun n => (Nat.unpair n).2
    | cf.pair cg => fun n => Nat.pair <$> cf.eval n <*> cg.eval n
    | cf.comp cg => fun n => cg.eval n >>= cf.eval
    | cf.prec cg =>
      Nat.unpaired fun a n =>
        Nat.rec (cf.eval a)
          (fun y IH => do
            let i ← IH
            cg.eval (Nat.pair a (Nat.pair y i)))
          n
    | cf.rfind' =>
      Nat.unpaired fun a m =>
        Part.map (fun x => x + m) (Nat.rfind fun n => (fun m => decide (m = 0)) <$> cf.eval (Nat.pair a (n + m)))
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.MonadCommRing : (Type → Type) → Type
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.outer_Ioc : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R]
  [CompactIccSpace R] [DenselyOrdered R] (a b : R), f.outer (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)