mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.algebraMap_equiv : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (A' : Type u_4)
  [inst_6 : CommRing A'] [inst_7 : Algebra A' B] [inst_8 : IsIntegralClosure A' R B] [inst_9 : Algebra R A]
  [inst_10 : Algebra R A'] [inst_11 : IsScalarTower R A B] [inst_12 : IsScalarTower R A' B] (x : A),
  (algebraMap A' B) ((IsIntegralClosure.equiv R A B A') x) = (algebraMap A B) x
-- Lean.Meta.Tactic.FunIndInfo
/-- `true` means that the corresponding level parameter of the function is also a level param
of the induction principle.
 -/
Lean.Meta.FunIndInfo.levelMask : Lean.Meta.FunIndInfo → Array Bool
-- Mathlib.Analysis.Complex.HalfPlane
/-- An open right half-plane (with boundary real part given by an `EReal`) is an open set
in the complex plane.  -/
Complex.isOpen_re_gt_EReal : ∀ (x : EReal), IsOpen {z | x < ↑z.re}
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MorApplication.none.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.MorApplication.none = 1
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_iff_isPredLimit : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [NoMaxOrder α], Order.IsPredPrelimit a ↔ Order.IsPredLimit a
-- Mathlib.Computability.ContextFreeGrammar
Language.isContextFree_reverse : ∀ {T : Type u_1} {L : Language T}, L.reverse.IsContextFree ↔ L.IsContextFree
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_swapEquiv_symm_apply : ∀ {R : Type u_3} (c₁ c₃ : R) [inst : CommRing R] (t : QuaternionAlgebra R c₃ 0 c₁),
  ((QuaternionAlgebra.swapEquiv c₁ c₃).symm t).imI = t.imJ
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.memLp_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : NormedAddCommGroup γ] [BorelSpace γ] {p : ENNReal},
  ProbabilityTheory.IdentDistrib f g μ ν → MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g p ν
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioi_pred_eq_Ici_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : PredOrder α] {a : α},
  ¬IsMin a → Finset.Ioi (Order.pred a) = Finset.Ici a
-- Mathlib.Topology.EMetricSpace.Lipschitz
continuous_prod_of_dense_continuous_lipschitzWith' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) {t : Set β},
  Dense t → (∀ (a : α), LipschitzWith K fun y => f (a, y)) → (∀ b ∈ t, Continuous fun x => f (x, b)) → Continuous f
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.FixedPointFree.coe_eq_inv_of_sq_eq_one : ∀ {F : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : FunLike F G G] [MonoidHomClass F G G] {φ : F} [Finite G],
  MonoidHom.FixedPointFree ⇑φ → (⇑φ)^[2] = id → ⇑φ = fun x => x⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.map_baseChange : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W'.baseChange A).map ↑f = W'.baseChange B
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.iUnion₂ : ∀ {R : Type u_1} {X : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] {x : X} {s : (i : ι) → κ i → Set X},
  (∀ (i : ι) (j : κ i), Convexity.IsStarConvexSet R x (s i j)) → Convexity.IsStarConvexSet R x (⋃ i, ⋃ j, s i j)
-- Init.Data.String.Lemmas.Iterate
String.Pos.Splits.mem_toList_right_iff : ∀ {s : String} {pos : s.Pos} {t u : String} {c : Char},
  pos.Splits t u → (c ∈ u.toList ↔ ∃ pos', ∃ (_ : pos ≤ pos') (h : pos' ≠ s.endPos), pos'.get h = c)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.rfl : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {l : Filter α} {f : α → E}, f =O[𝕜; l] f
-- Mathlib.Algebra.Group.Subgroup.Map
AddMonoidHom.addSubgroupComap_apply_coe : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G') (H' : AddSubgroup G')
  (x : ↥(AddSubmonoid.comap f H'.toAddSubmonoid)), ↑((f.addSubgroupComap H') x) = f ↑x
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- Isomorphic `PresheafedSpace`s have naturally isomorphic presheaves.  -/
AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : AlgebraicGeometry.PresheafedSpace C} →
      (H : X ≅ Y) → Y.presheaf ≅ (TopCat.Presheaf.pushforward C H.hom.base).obj X.presheaf
-- Init.Control.StateCps
StateCpsT.runK_bind_modify : ∀ {σ : Type u} {m : Type u → Type v} {β γ : Type u} (f : σ → σ) (g : PUnit.{u + 1} → StateCpsT σ m β) (s : σ)
  (k : β → σ → m γ), (modify f >>= g).runK s k = (g PUnit.unit).runK (f s) k
-- Mathlib.Tactic.TacticAnalysis
/-- `accept` means to run the test on the sequence of `.continue`s up to this `.accept`.  -/
Mathlib.TacticAnalysis.TriggerCondition.accept : {ctx : Type u_1} → ctx → Mathlib.TacticAnalysis.TriggerCondition ctx
-- Mathlib.Data.List.Intervals
List.Ico.mem : ∀ {n m l : ℕ}, l ∈ List.Ico n m ↔ n ≤ l ∧ l < m
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.eraseIndices : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.rootSpan.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [inst_5 : CharZero K]
  [inst_6 : LieAlgebra.IsKilling K L] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L),
  I.rootSpan = Submodule.span K (⇑(LieAlgebra.IsKilling.rootSystem H).root '' I.rootSet)
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.sum_finsupport_smul_eq_finsum : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) {x₀ : X} {M : Type u_2}
  [inst_1 : AddCommMonoid M] [inst_2 : Module ℝ M] (φ : ι → X → M),
  ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ • φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ • φ i x₀
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_const_div_atTop_nhds_zero_nat : ∀ {𝕜 : Type u_4} [inst : DivisionSemiring 𝕜] [inst_1 : CharZero 𝕜] [inst_2 : TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜]
  [ContinuousMul 𝕜] (C : 𝕜), Filter.Tendsto (fun n => C / ↑n) Filter.atTop (nhds 0)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.linear_eq_zero_iff_exists_const : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2), f.linear = 0 ↔ ∃ q, f = AffineMap.const k P1 q
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.hom_forget₂_map : ∀ {X Y : CommMonCat} (f : X ⟶ Y),
  MonCat.Hom.hom ((CategoryTheory.forget₂ CommMonCat MonCat).map f) = CommMonCat.Hom.hom f
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedDep.mk.injEq : ∀ (name : Lean.Name) (ident : Lean.TSyntax `ident) (binderType : Lean.TSyntax `term) (isClass : Bool)
  (name_1 : Lean.Name) (ident_1 : Lean.TSyntax `ident) (binderType_1 : Lean.TSyntax `term) (isClass_1 : Bool),
  ({ name := name, ident := ident, binderType := binderType, isClass := isClass } =
      { name := name_1, ident := ident_1, binderType := binderType_1, isClass := isClass_1 }) =
    (name = name_1 ∧ ident = ident_1 ∧ binderType = binderType_1 ∧ isClass = isClass_1)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_add_sub : ∀ {α : Type u} [inst : SubtractionMonoid α] {b : α} (a : α), IsAddUnit b → a + b + (0 - b) = a
-- Init.Data.UInt.Lemmas
UInt64.ofFin_mul : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a * b) = UInt64.ofFin a * UInt64.ofFin b
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.fold_filterM : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Std.Do.WPMonad n ps] [inst_9 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] [inst_11 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (ULift.{w, 0} Bool)}
  {g : δ → β → δ} {init : δ} {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let __do_lift ← f b
          pure (if __do_lift.down = true then g d b else d))
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.IterM.filterM f it) ⦃Q⦄
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.mk.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app app_1 : (a : B) → η.app a ⟶ θ.app a) (e_app : app = app_1)
  (naturality :
    ∀ {a b : B} (f : a ⟶ b),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
          (θ.naturality f).hom =
        CategoryTheory.CategoryStruct.comp (η.naturality f).hom
          (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f))),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Init.Data.List.Basic
List.all_nil : ∀ {α : Type u_1} {f : α → Bool}, [].all f = true
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_twoMore_iff : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.twoMore ↔ b &&& 240 = 224
-- Mathlib.Analysis.ODE.ExistUnique
/-- Local uniqueness of ODE solutions.  -/
ODE_solution_unique_of_eventually : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {t₀ : ℝ},
  (∀ᶠ (t : ℝ) in nhds t₀, LipschitzOnWith K (v t) (s t)) →
    (∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) →
      (∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) → f t₀ = g t₀ → f =ᶠ[nhds t₀] g
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- **Alias** of `LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero`. -/
LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero : ∀ {G₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀},
  g ≠ 0 → (({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ)))
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Grind.Config
-- Mathlib.Algebra.Group.Units.Equiv
/-- Left addition of an additive unit is a permutation of the underlying type.  -/
AddUnits.addLeft : {M : Type u_3} → [inst : AddMonoid M] → AddUnits M → Equiv.Perm M
-- Mathlib.Algebra.Group.Units.Equiv
AddEquiv.neg.eq_1 : ∀ (G : Type u_6) [inst : SubtractionCommMonoid G],
  AddEquiv.neg G = { toFun := Neg.neg, invFun := Neg.neg, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Enriched.HomCongr
CategoryTheory.Iso.eHomCongr_refl : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X Y : C),
  CategoryTheory.Iso.eHomCongr V (CategoryTheory.Iso.refl X) (CategoryTheory.Iso.refl Y) =
    CategoryTheory.Iso.refl (X ⟶[V] Y)
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condIndep_iSup_directed_limsup : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [inst : StandardBorelSpace Ω] (hm : m ≤ m0)
  [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) → ProbabilityTheory.CondIndep m (⨆ a, ⨆ n ∈ ns a, s n) (Filter.limsup s f) hm μ
-- Batteries.Data.UInt
USize.ext : ∀ {x y : USize}, x.toNat = y.toNat → x = y
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.coe_asOrderHom_objEquiv_symm : ∀ {n m : ℕ} (α : { len := n } ⟶ { len := m }),
  ⇑(SSet.stdSimplex.asOrderHom (SSet.stdSimplex.objEquiv.symm α)) = ⇑(CategoryTheory.ConcreteCategory.hom α)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.id_mapAddMon_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      CategoryTheory.AddMonObj.zero
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.ofHom_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : HopfAlgebra R X] [inst_3 : CommRing Y]
  [inst_4 : HopfAlgebra R Y] (f : X →ₐc[R] Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.ofHom f)) x = f x
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mkArrowIso_inv_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (f : CategoryTheory.MonoOver X),
  f.mkArrowIso.inv.hom.left = CategoryTheory.CategoryStruct.id f.obj.left
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (K : NNReal) (f : α → β),
  AntilipschitzWith K f = ∀ (x y : α), edist x y ≤ ↑K * edist (f x) (f y)
-- Mathlib.Computability.RegularExpressions
RegularExpression.plus_def : ∀ {α : Type u_1} (P Q : RegularExpression α), P.plus Q = P + Q
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instHasLimit : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}),
  CategoryTheory.Limits.HasLimit F
-- Init.Data.SInt.Lemmas
Int32.sub_right_inj : ∀ {a b : Int32} (c : Int32), c - a = c - b ↔ a = b
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural projection `AddMonoid.Coprod M N →+ M × N`.  -/
AddMonoid.Coprod.toProd : {M : Type u_1} → {N : Type u_2} → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → AddMonoid.Coprod M N →+ M × N
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- The **complete equipartite graph** in `r` parts each of *equal* size `t` such that two
vertices are adjacent if and only if they are in different parts, often denoted $K_r(t)$.

This is isomorphic to a corresponding `completeMultipartiteGraph` and `turanGraph`. The difference
is that the former vertices are a product type.

See `completeEquipartiteGraph.completeMultipartiteGraph`, `completeEquipartiteGraph.turanGraph`.  -/
SimpleGraph.completeEquipartiteGraph : (r t : ℕ) → SimpleGraph (Fin r × Fin t)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.aestronglyMeasurable_condExpIndSMul : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G),
  MeasureTheory.AEStronglyMeasurable (↑↑(MeasureTheory.condExpIndSMul hm hs hμs x)) μ
-- Mathlib.Topology.Algebra.Ring.Real
Real.uniformContinuous_neg : UniformContinuous Neg.neg
-- Mathlib.Algebra.Order.Field.Basic
one_div_pow_anti : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  1 ≤ a → Antitone fun n => 1 / a ^ n
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from semirings to additive commutative monoids preserves all limits.
 -/
SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (CategoryTheory.forget₂ SemiRingCat AddCommMonCat)
-- Mathlib.Analysis.Convex.Segment
mem_openSegment_sub_add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [Invertible 2] (x y : E), x ∈ openSegment 𝕜 (x - y) (x + y)
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Equivalence.isCardinalAccessibleCategory : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (e : C ≌ D) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] [CategoryTheory.IsCardinalAccessibleCategory C κ],
  CategoryTheory.IsCardinalAccessibleCategory D κ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_add_iff_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (a : α) {b c : α},
  a + b < a + c ↔ b < c
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `CommGroup` across an `Equiv`  -/
Equiv.commGroup : {α : Type u_2} → {β : Type u_3} → α ≃ β → [CommGroup β] → CommGroup α
-- Mathlib.Data.Ordmap.Ordset
/-- The validity predicate for an `Ordnode` subtree. This asserts that the `size` fields are
correct, the tree is balanced, and the elements of the tree are organized according to the
ordering. This version of `Valid` also puts all elements in the tree in the interval `(lo, hi)`.  -/
Ordnode.Valid' : {α : Type u_1} → [Preorder α] → WithBot α → Ordnode α → WithTop α → Prop
-- Mathlib.CategoryTheory.GradedObject.Braiding
CategoryTheory.GradedObject.symmetricCategory : {I : Type u_1} →
  [inst : AddCommMonoid I] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : ∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] →
            [inst_4 : ∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] →
              [inst_5 : ∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] →
                [inst_6 : DecidableEq I] →
                  [inst_7 : CategoryTheory.Limits.HasInitial C] →
                    [inst_8 :
                        ∀ (X₁ : C),
                          CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                            ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] →
                      [inst_9 :
                          ∀ (X₂ : C),
                            CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                              ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] →
                        [inst_10 : ∀ (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] →
                          [CategoryTheory.SymmetricCategory C] →
                            CategoryTheory.SymmetricCategory (CategoryTheory.GradedObject I C)
-- Mathlib.Algebra.Module.Torsion.Basic
_private.Mathlib.Algebra.Module.Torsion.Basic.0.Submodule.sup_torsionBySet_ideal_eq_torsionBySet_inf.match_1_1.eq_2 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (toFunctor : CategoryTheory.Functor C C)
  (ε : toFunctor ⟶ CategoryTheory.Functor.id C) (δ : toFunctor ⟶ toFunctor.comp toFunctor)
  (coassoc :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ.app X) (toFunctor.map (δ.app X)) =
          CategoryTheory.CategoryStruct.comp (δ.app X) (δ.app (toFunctor.obj X)))
      CategoryTheory.Comonad.coassoc._autoParam)
  (left_counit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ.app X) (ε.app (toFunctor.obj X)) =
          CategoryTheory.CategoryStruct.id (toFunctor.obj X))
      CategoryTheory.Comonad.left_counit._autoParam)
  (right_counit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ.app X) (toFunctor.map (ε.app X)) =
          CategoryTheory.CategoryStruct.id (toFunctor.obj X))
      CategoryTheory.Comonad.right_counit._autoParam)
  (toFunctor_1 : CategoryTheory.Functor C C) (ε_1 : toFunctor_1 ⟶ CategoryTheory.Functor.id C)
  (δ_1 : toFunctor_1 ⟶ toFunctor_1.comp toFunctor_1)
  (coassoc_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ_1.app X) (toFunctor_1.map (δ_1.app X)) =
          CategoryTheory.CategoryStruct.comp (δ_1.app X) (δ_1.app (toFunctor_1.obj X)))
      CategoryTheory.Comonad.coassoc._autoParam)
  (left_counit_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ_1.app X) (ε_1.app (toFunctor_1.obj X)) =
          CategoryTheory.CategoryStruct.id (toFunctor_1.obj X))
      CategoryTheory.Comonad.left_counit._autoParam)
  (right_counit_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ_1.app X) (toFunctor_1.map (ε_1.app X)) =
          CategoryTheory.CategoryStruct.id (toFunctor_1.obj X))
      CategoryTheory.Comonad.right_counit._autoParam),
  ({ toFunctor := toFunctor, ε := ε, δ := δ, coassoc := coassoc, left_counit := left_counit,
        right_counit := right_counit } =
      { toFunctor := toFunctor_1, ε := ε_1, δ := δ_1, coassoc := coassoc_1, left_counit := left_counit_1,
        right_counit := right_counit_1 }) =
    (toFunctor = toFunctor_1 ∧ ε ≍ ε_1 ∧ δ ≍ δ_1)
-- Mathlib.Order.Interval.Finset.Defs
instLocallyFiniteOrderTopSubtypeLtOfDecidableLTOfLocallyFiniteOrder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {y : α} [inst_1 : DecidableLT α] [inst_2 : LocallyFiniteOrder α],
  instLocallyFiniteOrderTopSubtypeLtOfDecidableLTOfLocallyFiniteOrder =
    { finsetIoi := fun a => Finset.subtype (fun x => x < y) (Finset.Ioo (↑a) y),
      finsetIci := fun a => Finset.subtype (fun x => x < y) (Finset.Ico (↑a) y), finset_mem_Ici := ⋯,
      finset_mem_Ioi := ⋯ }
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.map' : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {pa qa : Set α → Prop},
  μ.InnerRegularWRT pa qa →
    ∀ (f : α ≃ᵐ β) {pb qb : Set β → Prop},
      (∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)) →
        (∀ (K : Set α), pa K → pb (⇑f '' K)) → (MeasureTheory.Measure.map (⇑f) μ).InnerRegularWRT pb qb
-- Lean.Linter.UnusedVariables
/-- Collect into a heterogeneous collection of objects with external storage. This uses
pointer identity and does not store the objects, so it is important not to store the last
pointer to an object in the map, or it can be freed and reused, resulting in incorrect behavior.

Returns `true` if the object was not already in the set.  -/
Lean.Linter.UnusedVariables.insertObj : {α : Type} → IO.Ref (Std.HashSet USize) → α → IO Bool
-- Mathlib.Order.CompleteLattice.Basic
iSup_split_single : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (i₀ : β),
  ⨆ i, f i = f i₀ ⊔ ⨆ i, ⨆ (_ : i ≠ i₀), f i
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.ennreal_ofReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => ENNReal.ofReal (f x)) μ