mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.WellFoundedSet
/-- Given a bad sequence `f`, this constructs a bad sequence that agrees with `f` on the first `n`
terms and is minimal at `n`.
 -/
Set.PartiallyWellOrderedOn.minBadSeqOfBadSeq : {α : Type u_2} →
  (r : α → α → Prop) →
    (rk : α → ℕ) →
      (s : Set α) →
        (n : ℕ) →
          (f : ℕ → α) →
            Set.PartiallyWellOrderedOn.IsBadSeq r s f →
              { g //
                (∀ m < n, f m = g m) ∧
                  Set.PartiallyWellOrderedOn.IsBadSeq r s g ∧ Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n g }
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprTZifV1 : Repr Std.Time.TimeZone.TZif.TZifV1
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLE.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.eq = Ordering.gt → motive Ordering.gt)
  (h_2 : Ordering.eq = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.eq = Ordering.lt → motive Ordering.lt),
  (match hkky : Ordering.eq with
    | Ordering.gt => h_1 hkky
    | Ordering.eq => h_2 hkky
    | Ordering.lt => h_3 hkky) =
    h_2 ⋯
-- Mathlib.Data.Seq.Basic
Stream'.Seq.take_succ_cons : ∀ {α : Type u} {n : ℕ} {x : α} {s : Stream'.Seq α},
  Stream'.Seq.take (n + 1) (Stream'.Seq.cons x s) = x :: Stream'.Seq.take n s
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.mk.inj : ∀ {inner inner_1 : Int16}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.mem_homologicalKernel_trW_iff : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ] {X Y : C} (f : X ⟶ Y),
  F.homologicalKernel.trW f ↔ ∀ (n : ℤ), CategoryTheory.IsIso ((F.shift n).map f)
-- Batteries.Data.UnionFind.Basic
/-- Check whether two union-find nodes are equivalent, updating structure using path compression.  -/
Batteries.UnionFind.checkEquiv : (self : Batteries.UnionFind) → Fin self.size → Fin self.size → Batteries.UnionFind × Bool
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
/-- `alternatizeUncurryFin` of `fderivCompContinuousLinearMap f g`
composed with a symmetric bilinear map is zero.  -/
ContinuousAlternatingMap.alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (f : F [⋀^Fin n]→L[𝕜] G) (g : E →L[𝕜] F)
  {h : E →L[𝕜] E →L[𝕜] F},
  (∀ (x y : E), (h x) y = (h y) x) →
    ContinuousAlternatingMap.alternatizeUncurryFin (f.fderivCompContinuousLinearMap g ∘SL h) = 0
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instZeroHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        [inst_2 : CategoryTheory.Preadditive C] →
          [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] → Zero (T₁ ⟶ T₂)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₁_inv_comp_iCocycles : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).inv (groupCohomology.iCocycles A 1) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.i
      (groupCohomology.cochainsIso₁ A).inv
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.coe_id : ∀ (X : ProfiniteGrp.{u_1}), ⇑(ProfiniteGrp.Hom.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toArray_toList : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toList.toArray = r.toArray
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
dreduceIte : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} (lift : (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I)
  (lift_fac :
    autoParam
      (∀ (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (lift F') F'.m = F.m)
      CategoryTheory.Limits.IsImage.lift_fac._autoParam)
  (lift_1 : (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I)
  (lift_fac_1 :
    autoParam
      (∀ (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (lift_1 F') F'.m = F.m)
      CategoryTheory.Limits.IsImage.lift_fac._autoParam),
  ({ lift := lift, lift_fac := lift_fac } = { lift := lift_1, lift_fac := lift_fac_1 }) = (lift = lift_1)
-- Init.Data.Array.Lemmas
Array.size_eq_of_beq : ∀ {α : Type u_1} [inst : BEq α] {xs ys : Array α}, (xs == ys) = true → xs.size = ys.size
-- Lean.Level
_private.Lean.Level.0.Lean.Level.geq.go.match_1.eq_1 : ∀ (motive : Lean.Level → Lean.Level → Sort u_1) (x : Lean.Level) (h_1 : (x : Lean.Level) → motive x Lean.Level.zero)
  (h_2 : (u v₁ v₂ : Lean.Level) → motive u (v₁.max v₂)) (h_3 : (u₁ u₂ v : Lean.Level) → motive (u₁.max u₂) v)
  (h_4 : (a u₂ v : Lean.Level) → motive (a.imax u₂) v) (h_5 : (u v : Lean.Level) → motive u.succ v.succ)
  (h_6 : (x x_1 : Lean.Level) → motive x x_1),
  (match x, Lean.Level.zero with
    | x, Lean.Level.zero => h_1 x
    | u, v₁.max v₂ => h_2 u v₁ v₂
    | u₁.max u₂, v => h_3 u₁ u₂ v
    | a.imax u₂, v => h_4 a u₂ v
    | u.succ, v.succ => h_5 u v
    | x, x_1 => h_6 x x_1) =
    h_1 x
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.eq_of_norm_eq_of_divCoeffs : ∀ {ctx : Int.Internal.Linear.Context} {p₁ p₂ : Int.Internal.Linear.Poly} {k : ℤ},
  k > 0 →
    Int.Internal.Linear.Poly.divCoeffs k p₁ = true →
      p₂ = Int.Internal.Linear.Poly.div k p₁ →
        (Int.Internal.Linear.Poly.denote ctx p₁ ≤ 0 ↔ Int.Internal.Linear.Poly.denote ctx p₂ ≤ 0)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_mul_le : ∀ {u v : ℕ → ENNReal},
  ExpGrowth.expGrowthSup u ≠ ⊥ ∨ ExpGrowth.expGrowthSup v ≠ ⊤ →
    ExpGrowth.expGrowthSup u ≠ ⊤ ∨ ExpGrowth.expGrowthSup v ≠ ⊥ →
      ExpGrowth.expGrowthSup (u * v) ≤ ExpGrowth.expGrowthSup u + ExpGrowth.expGrowthSup v
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonRenameParams : Lean.ToJson Lean.Lsp.RenameParams
-- Mathlib.Analysis.Complex.LocallyUniformLimit
Complex.norm_cderiv_sub_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {z : ℂ} {M r : ℝ} {f g : ℂ → E},
  0 < r →
    (∀ w ∈ Metric.sphere z r, ‖f w - g w‖ < M) →
      ContinuousOn f (Metric.sphere z r) →
        ContinuousOn g (Metric.sphere z r) → ‖Complex.cderiv r f z - Complex.cderiv r g z‖ < M / r
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instFinitenessRelation : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LT α] →
      [inst_2 : DecidableLT α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.Rxo.IsAlwaysFinite α] → Std.Iterators.FinitenessRelation (Std.Rxo.Iterator α) Id
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.self_add_star' : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R],
  a + star a = ↑(2 * a.re + c₂ * a.imI)
-- Init.Data.AC
Lean.Data.AC.Context.mk.inj : ∀ {α : Sort u} {op : α → α → α} {assoc : Std.Associative op} {comm : Option (PLift (Std.Commutative op))}
  {idem : Option (PLift (Std.IdempotentOp op))} {vars : List (Lean.Data.AC.Variable op)} {arbitrary : α}
  {op_1 : α → α → α} {assoc_1 : Std.Associative op_1} {comm_1 : Option (PLift (Std.Commutative op_1))}
  {idem_1 : Option (PLift (Std.IdempotentOp op_1))} {vars_1 : List (Lean.Data.AC.Variable op_1)} {arbitrary_1 : α},
  { op := op, assoc := assoc, comm := comm, idem := idem, vars := vars, arbitrary := arbitrary } =
      { op := op_1, assoc := assoc_1, comm := comm_1, idem := idem_1, vars := vars_1, arbitrary := arbitrary_1 } →
    op = op_1 ∧ comm ≍ comm_1 ∧ idem ≍ idem_1 ∧ vars ≍ vars_1 ∧ arbitrary = arbitrary_1
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₂_obj_X_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
  {X Y : SimplexCategoryᵒᵖ} (θ : X ⟶ Y),
  (AlgebraicTopology.DoldKan.Γ₂.obj P).X.map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map P.X θ
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.hom_inv_rightUnitor : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R},
  ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv = ↑(TensorProduct.rid R ↑M).symm
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fstHom_apply : ∀ (R : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (a : Unitization R A),
  (Unitization.fstHom R A) a = a.toProd.1
-- Mathlib.Order.Heyting.Basic
sup_sdiff_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊔ b \ a = a ⊔ b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Given a point in an affine subspace, a result of subtracting that point on the right is in the
direction if and only if the other point is in the subspace.  -/
AffineSubspace.vsub_right_mem_direction_iff_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ∀ (p₂ : P), p₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.nonCommSemiring.injEq : ∀ (id id_1 : ℕ),
  (Lean.Meta.Sym.Arith.ClassifyResult.nonCommSemiring id = Lean.Meta.Sym.Arith.ClassifyResult.nonCommSemiring id_1) =
    (id = id_1)
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_natCast : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : DecidableEq m] (a : ℕ), (↑a).num = ↑a
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- An endomorphism of a module is skew-adjoint with respect to a bilinear map if its negation
serves as an adjoint.  -/
LinearMap.IsSkewAdjoint : {R : Type u_1} →
  {M : Type u_5} →
    {M₂ : Type u_7} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup M₂] → [inst_4 : Module R M₂] → (M →ₗ[R] M →ₗ[R] M₂) → (M → M) → Prop
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.comp_toShHom : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z),
  AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
      (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)
-- Mathlib.Algebra.Field.GeomSum
Commute.geom_sum₂ : ∀ {K : Type u_2} [inst : DivisionRing K] {x y : K},
  Commute x y → x ≠ y → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderProcessedState.mk.inj : ∀ {cmdState : Lean.Elab.Command.State}
  {firstCmdSnap : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot}
  {cmdState_1 : Lean.Elab.Command.State}
  {firstCmdSnap_1 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot},
  { cmdState := cmdState, firstCmdSnap := firstCmdSnap } = { cmdState := cmdState_1, firstCmdSnap := firstCmdSnap_1 } →
    cmdState = cmdState_1 ∧ firstCmdSnap = firstCmdSnap_1
-- Mathlib.Data.Num.Bitwise
/-- An induction principle for `SNum` which avoids relying on `NzsNum`.  -/
SNum.rec' : {α : Sort u_1} → (Bool → α) → (Bool → SNum → α → α) → SNum → α
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.sup_mem : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : α}, a ∈ L → b ∈ L → a ⊔ b ∈ L
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushoutComparison_map_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  {W : C} {h : Y ⟶ W} {k : Z ⟶ W} (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g)
      (G.map (CategoryTheory.Limits.pushout.desc h k w)) =
    CategoryTheory.Limits.pushout.desc (G.map h) (G.map k) ⋯
-- Lean.Language.Lean.Types
/-- Snapshot for incremental reporting and reuse during elaboration, type dependent on specific
elaborator.
  -/
Lean.Language.Lean.CommandElaboratingSnapshot.elabSnap : Lean.Language.Lean.CommandElaboratingSnapshot → Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot
-- Batteries.Data.Fin.Lemmas
Fin.findSomeRev?.eq_1 : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → Option α), Fin.findSomeRev? f = Fin.findSome? fun x => f x.rev
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLEMap_id : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C],
  HomologicalComplex.truncLEMap (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.truncLE e)
-- Mathlib.Analysis.ODE.Gronwall
gronwallBound_K0 : ∀ (δ ε : ℝ), gronwallBound δ 0 ε = fun x => δ + ε * x
-- Init.Data.Int.LemmasAux
Int.sub_max_sub_right : ∀ (a b c : ℤ), max (a - c) (b - c) = max a b - c
-- Mathlib.Order.Interval.Set.Image
Set.preimage_subtype_val_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a b : { x // p x }), Subtype.val ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b
-- Mathlib.LinearAlgebra.LinearPMap
/-- Restrict codomain of a `LinearPMap`  -/
LinearPMap.codRestrict : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module S F] →
                      (f : E →ₛₗ.[σ] F) → (p : Submodule S F) → (∀ (x : ↥f.domain), ↑f x ∈ p) → E →ₛₗ.[σ] ↥p
-- Mathlib.Analysis.RCLike.Basic
RCLike.reCLM_coe : ∀ {K : Type u_1} [inst : RCLike K], ↑RCLike.reCLM = RCLike.reLm
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_comm : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ∧ Q ⊣⊢ₛ Q ∧ P
-- Mathlib.Algebra.Exact.Basic
/-- If two maps `f : M → N` and `g : N → P` are exact, then the induced maps
`Set.range f → N → Set.range g` are exact.

Note that if you already have an instance `[One (Set.range g)]` (which is unlikely) this lemma
may not apply if the one of `Set.range g` is not definitionally equal to `⟨1, hg⟩`.  -/
Function.MulExact.rangeFactorization : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : One P],
  Function.MulExact f g → ∀ (hg : 1 ∈ Set.range g), Function.MulExact Subtype.val (Set.rangeFactorization g)
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForDiagnosticsParams.version : Lean.Lsp.WaitForDiagnosticsParams → ℕ
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseExtendedDayPeriodFrom : Vector String 6 → Std.Internal.Parsec.String.Parser Std.Time.ExtendedDayPeriod
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The identification `X ⊗ - = mop (- ⊗ unmop X)` as a natural isomorphism.  -/
CategoryTheory.MonoidalOpposite.tensorLeftIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : Cᴹᵒᵖ) →
        CategoryTheory.MonoidalCategory.tensorLeft X ≅
          (CategoryTheory.unmopFunctor C).comp
            ((CategoryTheory.MonoidalCategory.tensorRight X.unmop).comp (CategoryTheory.mopFunctor C))
-- Init.Data.Iterators.Consumers.Monadic.Total
Std.IterM.Total.mk : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.IterM m β → Std.IterM.Total m β
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) {a b c : B'}
  (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).mapComp f g).inv.iso.hom = (F.mapComp f g).inv
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.add_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} [inst_3 : CategoryTheory.Preadditive C] {a b c : M}
  (α₁ α₂ : CategoryTheory.ShiftedHom X Y a) (β : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c),
  (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
-- Std.Data.TreeSet.AdditionalOperations
/-- Given a proof that such an element exists, retrieves the largest element that is
less than or equal to the given element.
 -/
Std.TreeSet.getLE : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] → (t : Std.TreeSet α cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.restrict_coe_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q) (x : ↥p),
  ↑((f.restrict hf) x) = f ↑x
-- Mathlib.Algebra.Tropical.Basic
Tropical.instLETropical : {R : Type u} → [LE R] → LE (Tropical R)
-- Std.Time.Time.Unit.Hour
/-- Creates an `Ordinal` from a `Fin` value.
 -/
Std.Time.Hour.Ordinal.ofFin : Fin 24 → Std.Time.Hour.Ordinal
-- Mathlib.Algebra.Order.Nonneg.Module
Nonneg.instIsScalarTower : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R]
  [inst_3 : SMul R S] [inst_4 : SMul R M] [inst_5 : SMul S M] [IsScalarTower R S M], IsScalarTower { c // 0 ≤ c } S M
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k (List.filter (fun p => f p.fst p.snd) l) =
      (Std.Internal.List.getKey? k l).pfilter fun x h => f x (Std.Internal.List.getValueCast x l ⋯)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Continuous multilinear maps over the ring `R`, from `∀ i, M₁ i` to `M₂` where `M₁ i` and `M₂`
are modules over `R` with a topological structure. In applications, there will be compatibility
conditions between the algebraic and the topological structures, but this is not needed for the
definition.  -/
«term_[×_]→L[_]_» : Lean.TrailingParserDescr
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
/-- Let `it₁` and `it₂` be iterators and `f` a function mapping `it₁`'s outputs to iterators
of the same type as `it₂`. Then `it₁.flatMapAfter f it₂` first goes over `it₂` and then over
`it₁.flatMap f it₂`, emitting all their values.

The main purpose of this combinator is to represent the intermediate state of a `flatMap` iterator
that is currently iterating over one of the inner iterators.

**Marble diagram:**

```text
it₁                            --b      c    --d -⊥
it₂                      a1-a2⊥
f b                               b1-b2⊥
f c                                      c1-c2⊥
f d                                             ⊥
it.flatMapAfter  f it₂   a1-a2----b1-b2--c1-c2----⊥
```

**Termination properties:**

* `Finite` instance: only if `it₁`, `it₂` and the inner iterators are finite
* `Productive` instance: only if `it₁` is finite and `it₂` and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
iterator is productive and the inner
iterators are productive *and provably never empty*, then the resulting iterator is also productive.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal
iterator.

For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
 -/
Std.IterM.flatMapAfter : {α β α₂ γ : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [Std.Iterator α m β] →
        [Std.Iterator α₂ m γ] → (f : β → Std.IterM m γ) → Std.IterM m β → Option (Std.IterM m γ) → Std.IterM m γ
-- Batteries.Data.List.Lemmas
List.isChain_idxsOf : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α], List.IsChain (fun x1 x2 => x1 < x2) (List.idxsOf x xs s)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_eq_empty : ∀ {m n : ℕ}, n < m → (m...=n).toArray = #[]
-- Std.Net.Addr
Std.Net.SocketAddress.instToString : ToString Std.Net.SocketAddress
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.ext_iff : ∀ {M : Type u_4} [inst : MulOne M] {f g : Monoid.End M}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
/-- Every Yoneda-presheaf is a sheaf for the extensive topology.  -/
CategoryTheory.extensiveTopology.isSheaf_yoneda_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C] (W : C),
  CategoryTheory.Presieve.IsSheaf (CategoryTheory.extensiveTopology C) (CategoryTheory.yoneda.obj W)
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleδ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact), hS.singleδ = hS.singleδ
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.isFalseCond : Lean.Expr → Bool
-- Mathlib.Data.Finite.Prod
Set.Infinite.prod_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, t.Infinite → s.Nonempty → (s ×ˢ t).Infinite
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- A pushout cocone from `X` is a colimit if its corresponding binary cofan in `Under X` is a
colimit.  -/
CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanInverse : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {c : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)} →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.inverse.obj c)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_le_aleph : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.aleph o₁ ≤ Cardinal.aleph o₂ ↔ o₁ ≤ o₂