mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_edist_eq_add : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : EDist α] [inst_1 : EDist β],
  0 < p.toReal →
    ∀ (f g : WithLp p (α × β)),
      edist f g = (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`w, z : N` and `y ∈ S`, we have `z = w * (f y)⁻¹ ↔ z * f y = w`.  -/
Submonoid.LocalizationMap.mul_inv_right : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
  (h : ∀ (y : ↥S), IsUnit (f ↑y)) (y : ↥S) (w z : N),
  z = w * ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ ↔ z * f ↑y = w
-- Init.Data.String.OrderInstances
String.Slice.Pos.toInt_eq : ∀ {s : String.Slice} {p : s.Pos}, ↑p = ↑p.offset.byteIdx
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.monoFactorisationZero_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X Y : C), (CategoryTheory.Limits.monoFactorisationZero X Y).e = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = (t.isEmpty || t.size == 1 && t.contains k)
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.TreeMap.minEntryD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α × β → α × β
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- A finsupp `∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A` satisfies the 2-cycle condition if
`∑ (gᵢ⁻¹ • aᵢ)·hᵢ + aᵢ·gᵢ = ∑ aᵢ·gᵢhᵢ`.  -/
groupHomology.IsCycle₂ : {G : Type u_1} → {A : Type u_2} → [Mul G] → [Inv G] → [inst : AddCommGroup A] → [SMul G A] → (G × G →₀ A) → Prop
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_apply_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), toIocMod hp a (a + p) = a + p
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.Context.setTransparency : Lean.Meta.Context → Lean.Meta.TransparencyMode → Lean.Meta.Context
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_sub_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a‖ ≤ ‖a - b‖ + ‖b‖
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is non-strictly above the
segment `[(a, f a), (b, f b)]` if and only if `slope f c b ≤ slope f a c`.  -/
lineMap_le_map_iff_slope_le_slope : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  a < b →
    0 < r →
      r < 1 →
        ((AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔
          slope f ((AffineMap.lineMap a b) r) b ≤ slope f a ((AffineMap.lineMap a b) r))
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_iSup_of_mem : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} {S : ι → AddSubmonoid M} (i : ι) {x : M}, x ∈ S i → x ∈ iSup S
-- Init.Data.Fin.Lemmas
Fin.mul_comm : ∀ {n : ℕ} (a b : Fin n), a * b = b * a
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (X : C) {Z : C}
  (h : (t.eTruncGE.obj i).obj ((t.eTruncGE.obj i).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X)) h =
    CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)) h
-- Mathlib.Order.RelSeries
RelSeries.cons_self_tail : ∀ {α : Type u_1} {r : SetRel α α} {p : RelSeries r} (hp : p.length ≠ 0), (p.tail hp).cons p.head ⋯ = p
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.ApplyRulesConfig.toBacktrackConfig : Lean.Meta.SolveByElim.ApplyRulesConfig → Lean.Meta.Tactic.Backtrack.BacktrackConfig
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.fold_filter : ∀ {α β δ : Type w} {m : Type w → Type w'} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.Do.WPMonad m ps] [inst_5 : Std.IteratorLoop α m m]
  [Std.LawfulIteratorLoop α m m] {f : β → Bool} {g : δ → β → δ} {init : δ} {it : Std.IterM m β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄ Std.IterM.fold (fun d b => if f b = true then g d b else d) init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.IterM.filter f it) ⦃Q⦄
-- Mathlib.Data.Finset.Density
Finset.dens_sdiff_comm : ∀ {α : Type u_2} [inst : Fintype α] {s t : Finset α} [inst_1 : DecidableEq α],
  s.card = t.card → (s \ t).dens = (t \ s).dens
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(I⁻ⁿ) = -val_v(Iⁿ)` for every `n ∈ ℤ`.  -/
FractionalIdeal.count_neg_zpow : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ)
  (I : FractionalIdeal (nonZeroDivisors R) K), FractionalIdeal.count K v (I ^ (-n)) = -FractionalIdeal.count K v (I ^ n)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toIsometryEquiv_inj : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {f g : E ≃ₛₗᵢ[σ₁₂] E₂}, f.toIsometryEquiv = g.toIsometryEquiv ↔ f = g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filter!_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! f t).isEmpty = false ↔
      ∃ k, ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), f k (t.get k h) = true)
-- Init.Data.String.Search
String.Internal.containsImpl : String → Char → Bool
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_union_convexHull : ∀ (R : Type u_1) {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] (s t : Set X),
  (Convexity.convexHull R) (s ∪ (Convexity.convexHull R) t) = (Convexity.convexHull R) (s ∪ t)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.forget_map : ∀ {ι : Type u_1} (V : Type u) [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) {X Y : HomologicalComplex V c} (f : X ⟶ Y)
  (i : ι), (HomologicalComplex.forget V c).map f i = f.f i
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_of_hasLimit_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [CategoryTheory.Limits.HasLimit F.rightOp], CategoryTheory.Limits.HasColimit F
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.of_iSup_eq_top : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine Y]
  {ι : Type u_1} (U : ι → ↑X.affineOpens),
  ⨆ i, ↑(U i) = ⊤ → (∀ (i : ι), Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))) → P f
-- Init.Data.Int.Order
Int.lt_add_of_pos_right : ∀ (a : ℤ) {b : ℤ}, 0 < b → a < a + b
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.brecOn.go : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {motive_1 : Lean.PrefixTreeNode α β cmp → Sort u_1} →
        {motive_2 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
          {motive_3 : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
            {motive_4 : (Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) → Sort u_1} →
              (t : Lean.PrefixTreeNode α β cmp) →
                ((t : Lean.PrefixTreeNode α β cmp) → t.below → motive_1 t) →
                  ((t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) →
                      Lean.PrefixTreeNode.below_1 t → motive_2 t) →
                    ((t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) →
                        Lean.PrefixTreeNode.below_2 t → motive_3 t) →
                      ((t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
                          Lean.PrefixTreeNode.below_3 t → motive_4 t) →
                        motive_1 t ×' t.below
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
SlashInvariantForm.exists_one_half_le_im_and_norm_le : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ}
  [SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k],
  k ≤ 0 → ∀ (f : F) (τ : UpperHalfPlane), ∃ ξ, 1 / 2 ≤ ξ.im ∧ ‖f τ‖ ≤ ‖f ξ‖
-- Mathlib.Data.Finset.Basic
Finset.filter_or : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : DecidableEq α]
  (s : Finset α), {a ∈ s | p a ∨ q a} = Finset.filter p s ∪ Finset.filter q s
-- Mathlib.CategoryTheory.Limits.Comma
/-- (Implementation). An auxiliary cone which is useful in order to construct limits
in the comma category.  -/
CategoryTheory.Comma.limitAuxiliaryCone : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {B : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
            {T : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} T] →
                {L : CategoryTheory.Functor A T} →
                  {R : CategoryTheory.Functor B T} →
                    (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) →
                      CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R)) →
                        CategoryTheory.Limits.Cone ((F.comp (CategoryTheory.Comma.snd L R)).comp R)
-- Mathlib.Topology.UnitInterval
unitInterval.lt_symm_comm : ∀ {i j : ↑unitInterval}, i < unitInterval.symm j ↔ j < unitInterval.symm i
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.alterAux : {α : Type u_1} →
  {β : Type u_2} →
    [BEq α] →
      [Hashable α] →
        (Option β → Option β) → Lean.PersistentHashMap.Node α β → USize → USize → α → Lean.PersistentHashMap.Node α β
-- Init.Data.SInt.Bitwise
Int32.toInt8_or : ∀ (a b : Int32), (a ||| b).toInt8 = a.toInt8 ||| b.toInt8
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.coe_toHom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f : L.Embedding M N}, ⇑f.toHom = ⇑f
-- Init.Data.AC
Lean.Data.AC.mergeIdem.loop.eq_1 : ∀ (a next : ℕ) (rest : List ℕ),
  Lean.Data.AC.mergeIdem.loop a (next :: rest) =
    if a = next then Lean.Data.AC.mergeIdem.loop a rest else a :: Lean.Data.AC.mergeIdem.loop next rest
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.braiding'_eq_braiding : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {P Q : C},
  CategoryTheory.Limits.biprod.braiding' P Q = CategoryTheory.Limits.biprod.braiding P Q
-- Std.Data.ByteSlice
ByteSlice.instGetElemNatUInt8LtSize : GetElem ByteSlice ℕ UInt8 fun xs i => i < xs.size
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Note that this provides `IsScalarTower F K K` which is needed by `smul_mul_assoc`.  -/
IntermediateField.instIsScalarTowerSubtypeMem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {X : Type u_4} {Y : Type u_5}
  [inst_3 : SMul X Y] [inst_4 : SMul L X] [inst_5 : SMul L Y] [IsScalarTower L X Y] (F : IntermediateField K L),
  IsScalarTower (↥F) X Y
-- Mathlib.LinearAlgebra.Span.TensorProduct
Submodule.tensorToSpan.congr_simp : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (p : Submodule R M), Submodule.tensorToSpan A p = Submodule.tensorToSpan A p
-- Mathlib.Order.CompleteBooleanAlgebra
iSup₂_inf_eq : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : Order.Frame α] {f : (i : ι) → κ i → α} (a : α),
  (⨆ i, ⨆ j, f i j) ⊓ a = ⨆ i, ⨆ j, f i j ⊓ a
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.integral_condExpL2_eq_of_fin_meas_real : ∀ {α : Type u_1} {𝕜 : Type u_7} [inst : RCLike 𝕜] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  {hm : m ≤ m0} (f : ↥(MeasureTheory.Lp 𝕜 2 μ)),
  MeasurableSet s → μ s ≠ ⊤ → ∫ (x : α) in s, ↑↑↑((MeasureTheory.condExpL2 𝕜 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
-- Init.SizeOf
Lean.TSyntax.mk.sizeOf_spec : ∀ {ks : Lean.SyntaxNodeKinds} (raw : Lean.Syntax), sizeOf { raw := raw } = 1 + sizeOf raw
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.ofReal_variance : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ → ENNReal.ofReal (ProbabilityTheory.variance X μ) = ProbabilityTheory.evariance X μ
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The forgetful functor from bimonoid objects to comonoid objects.  -/
CategoryTheory.Bimon.toComon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.Bimon C) (CategoryTheory.Comon C)
-- Mathlib.Analysis.Convex.Basic
/-- The image of a convex set under an affine map is convex.  -/
Convex.affine_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {s : Set E} (f : E →ᵃ[𝕜] F),
  Convex 𝕜 s → Convex 𝕜 (⇑f '' s)
-- Mathlib.Probability.Independence.Basic
/-- Given random variables `X : Ω → 𝓧` and `Y : Ω' → 𝓨`, they are independent when viewed as random
variables defined on the product space `Ω × Ω'`.  -/
ProbabilityTheory.indepFun_prod : ∀ {Ω : Type u_10} {Ω' : Type u_11} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω}
  {ν : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  {𝓧 : Type u_12} {𝓨 : Type u_13} [inst : MeasurableSpace 𝓧] [inst_1 : MeasurableSpace 𝓨] {X : Ω → 𝓧} {Y : Ω' → 𝓨},
  Measurable X → Measurable Y → ProbabilityTheory.IndepFun (fun ω => X ω.1) (fun ω => Y ω.2) (μ.prod ν)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inl_pushoutAssoc_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inl g₁
        (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
      (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂)
      (CategoryTheory.Limits.pushout.inl
        (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
-- Mathlib.Analysis.Convex.Function
ConcaveOn.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : DistribMulAction 𝕜 β] {s : Set E} {f g : E → β}, ConcaveOn 𝕜 s f → ConcaveOn 𝕜 s g → ConcaveOn 𝕜 s (f + g)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPSafeShadowing : Lean.Options → Bool
-- Mathlib.Order.Filter.Pointwise
Filter.smul_neBot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β}, (f • g).NeBot ↔ f.NeBot ∧ g.NeBot
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the inverse direction of the isomorphism
`PreservesColimit₂.isoObjCoconePointsOfIsColimit` w.r.t. the canonical maps to the colimit.  -/
CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoObjConePointsOfIsColimit_inv : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cocone K₁}
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone K₂}
  (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  {c₃ :
    CategoryTheory.Limits.Cocone
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
  (hc₃ : CategoryTheory.Limits.IsColimit c₃) (j : J₁ × J₂),
  CategoryTheory.CategoryStruct.comp (c₃.ι.app j)
      (CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv =
    CategoryTheory.CategoryStruct.comp ((G.map (c₁.ι.app j.1)).app (K₂.obj j.2)) ((G.obj c₁.pt).map (c₂.ι.app j.2))
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.hasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasZeroObject C
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.sdiff_mem_iff : ∀ {α : Type u} {s t : Set α} (f : Ultrafilter α), s \ t ∈ f ↔ s ∈ f ∧ t ∉ f
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.continueT : Lean.Elab.Do.MonadInfo → Lean.Elab.Do.ControlStack → Lean.Elab.Do.ControlStack
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.instMonadShareCommonSymM : Lean.Meta.Sym.Internal.MonadShareCommon Lean.Meta.Sym.SymM
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.mulRight_mul_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] (u v : ↥(unitary A)) (x : A),
  (Unitary.mulRight R (u * v)) x = (Unitary.mulRight R v) ((Unitary.mulRight R u) x)
-- Mathlib.Order.Sublattice
Sublattice.comap_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {f : LatticeHom α β},
  Monotone (Sublattice.comap f)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.isImage_source_target_of_disjoint : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : OpenPartialHomeomorph X Y),
  Disjoint e.source e'.source → Disjoint e.target e'.target → e.IsImage e'.source e'.target
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.map : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S]
      [F.PreservesRightHomologyOf S] [CategoryTheory.Mono (F.map S.f)] [CategoryTheory.Epi (F.map S.g)],
      (S.map F).ShortExact
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The internal hom object from the unit to any object is isomorphic to that object.
The typeclass argument is explicit: any instance can be used.  -/
CategoryTheory.MonoidalClosed.unitIsoSelf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) →
        [inst_2 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] →
          CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟹ X ≅ X
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.toRingHom_mapRingEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S), (MonoidAlgebra.mapRingEquiv M e).toRingHom = MonoidAlgebra.mapRingHom M ↑e
-- Init.Data.UInt.Lemmas
UInt8.toNat_mod : ∀ (a b : UInt8), (a % b).toNat = a.toNat % b.toNat
-- Mathlib.Data.Set.Insert
Set.default_coe_singleton : ∀ {α : Type u_1} (x : α), default = ⟨x, ⋯⟩
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] [inst_2 : SizeOf C]
  (L₀ L₁ L₂ L₃ : CategoryTheory.ShortComplex C) (v₀₁ : L₀ ⟶ L₁) (v₁₂ : L₁ ⟶ L₂) (v₂₃ : L₂ ⟶ L₃)
  (w₀₂ :
    autoParam (CategoryTheory.CategoryStruct.comp v₀₁ v₁₂ = 0) CategoryTheory.ShortComplex.SnakeInput.w₀₂._autoParam)
  (w₁₃ :
    autoParam (CategoryTheory.CategoryStruct.comp v₁₂ v₂₃ = 0) CategoryTheory.ShortComplex.SnakeInput.w₁₃._autoParam)
  (h₀ : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι v₀₁ w₀₂))
  (h₃ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ v₂₃ w₁₃)) (L₁_exact : L₁.Exact)
  (epi_L₁_g : CategoryTheory.Epi L₁.g) (L₂_exact : L₂.Exact) (mono_L₂_f : CategoryTheory.Mono L₂.f),
  sizeOf
      { L₀ := L₀, L₁ := L₁, L₂ := L₂, L₃ := L₃, v₀₁ := v₀₁, v₁₂ := v₁₂, v₂₃ := v₂₃, w₀₂ := w₀₂, w₁₃ := w₁₃, h₀ := h₀,
        h₃ := h₃, L₁_exact := L₁_exact, epi_L₁_g := epi_L₁_g, L₂_exact := L₂_exact, mono_L₂_f := mono_L₂_f } =
    1 + sizeOf L₀ + sizeOf L₁ + sizeOf L₂ + sizeOf L₃ + sizeOf v₀₁ + sizeOf v₁₂ + sizeOf v₂₃ + sizeOf w₀₂ + sizeOf w₁₃ +
                sizeOf h₀ +
              sizeOf h₃ +
            sizeOf L₁_exact +
          sizeOf epi_L₁_g +
        sizeOf L₂_exact +
      sizeOf mono_L₂_f
-- Mathlib.Algebra.Torsor.Basic
Set.singleton_sdiv_self : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p : P), {p} /ₛ {p} = {1}
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.opHomeomorph_apply : ∀ {M : Type u_1} [inst : TopologicalSpace M] (a : M), AddOpposite.opHomeomorph a = AddOpposite.op a
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.mul_rpow : ∀ {x y : NNReal} {z : ℝ}, (x * y) ^ z = x ^ z * y ^ z
-- Mathlib.RingTheory.Jacobson.Radical
Module.jacobson_quotient_jacobson : ∀ (R : Type u_1) (M : Type u_3) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.jacobson R (M ⧸ Module.jacobson R M) = ⊥