mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.CopyDiscardCategory.Basic
/-- Discard on the unit object.  -/
CategoryTheory.CopyDiscardCategory.discard_unit : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.CopyDiscardCategory C],
  CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.snd_apply : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (self : A × B), (NonUnitalStarAlgHom.snd R A B) self = self.2
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.trivial_mon_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
/-- The functor `AddGrpCat ⥤ GrpCat` by sending `X ↦ Multiplicative X` and `f ↦ f`.
 -/
AddGrpCat.toGrp : CategoryTheory.Functor AddGrpCat GrpCat
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.isSplitEpi_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [F.Full] [F.Faithful],
  CategoryTheory.IsSplitEpi (F.map f) ↔ CategoryTheory.IsSplitEpi f
-- Mathlib.Analysis.Calculus.BumpFunction.Convolution
/-- `(φ i ⋆ g i) (k i)` tends to `z₀` as `i` tends to some filter `l` if
* `φ` is a sequence of normed bump functions
  such that `(φ i).rOut` tends to `0` as `i` tends to `l`;
* `g i` is `μ`-a.e. strongly measurable as `i` tends to `l`;
* `g i x` tends to `z₀` as `(i, x)` tends to `l ×ˢ 𝓝 x₀`;
* `k i` tends to `x₀`.  -/
ContDiffBump.convolution_tendsto_right : ∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace ℝ G]
  [CompleteSpace E'] [BorelSpace G] [inst_7 : FiniteDimensional ℝ G] [μ.IsAddHaarMeasure] {ι : Type u_1}
  {φ : ι → ContDiffBump 0} {g : ι → G → E'} {k : ι → G} {x₀ : G} {z₀ : E'} {l : Filter ι},
  Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0) →
    (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (g i) μ) →
      Filter.Tendsto (Function.uncurry g) (l ×ˢ nhds x₀) (nhds z₀) →
        Filter.Tendsto k l (nhds x₀) →
          Filter.Tendsto
            (fun i => MeasureTheory.convolution ((φ i).normed μ) (g i) (ContinuousLinearMap.lsmul ℝ ℝ) μ (k i)) l
            (nhds z₀)
-- Mathlib.Data.Set.Prod
Set.pi_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  (∀ i ∈ s, t₁ i ⊆ t₂ i) → s.pi t₁ ⊆ s.pi t₂
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.inv_symm : ∀ (G : Type v) [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G], (IsometryEquiv.inv G).symm = IsometryEquiv.inv G
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.of_denote_eq_cancelAux : ∀ (ctx : Nat.Internal.Linear.Context) (fuel : ℕ) (m₁ m₂ r₁ r₂ : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote_eq ctx (Nat.Internal.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂) →
    Nat.Internal.Linear.Poly.denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_addSubgroupOf_closure_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G),
  ((AddSubgroup.closure s).addSubgroupOf (AddSubgroup.normalizer s)).Normal
-- Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
SSet.RelativeMorphism.botEquiv_apply : ∀ {X Y : SSet} (f : SSet.RelativeMorphism ⊥ ⊥ (SSet.Subcomplex.isInitialBot.to ⊥.toSSet)),
  SSet.RelativeMorphism.botEquiv f = f.map
-- Mathlib.Data.Num.ZNum
ZNum.zero_add : ∀ (n : ZNum), 0 + n = n
-- Lean.Elab.Tactic.Basic
/-- Analogue of `liftMetaTactic` for tactics that do not return any goals.  -/
Lean.Elab.Tactic.liftMetaFinishingTactic : (Lean.MVarId → Lean.MetaM Unit) → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.Order.OrderClosed
Filter.tendsto_nhds_min_left : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f : β → α}
  {l : Filter β} {a : α},
  Filter.Tendsto f l (nhdsWithin a (Set.Iio a)) → Filter.Tendsto (fun i => min (f i) a) l (nhdsWithin a (Set.Iio a))
-- Std.Http.Data.Chunk
/-- Merges two trailers, accumulating values for duplicate keys from both.
 -/
Std.Http.Trailer.merge : Std.Http.Trailer → Std.Http.Trailer → Std.Http.Trailer
-- Mathlib.Order.Interval.Multiset
Multiset.mem_Iic : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {b x : α}, x ∈ Multiset.Iic b ↔ x ≤ b
-- Init.Data.Int.Gcd
Int.lcm_mul_left_left : ∀ (a b : ℤ), (a * b).lcm b = a.natAbs * b.natAbs
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.instHasSmallObjectArgumentGeneratingMonomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C],
  (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G).HasSmallObjectArgument
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getEntry? a (Std.Internal.List.eraseKey k l) =
      if (k == a) = true then none else Std.Internal.List.getEntry? a l
-- Init.Data.Array.Count
Array.replicate_count_eq_of_count_eq_size : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α},
  Array.count a xs = xs.size → Array.replicate (Array.count a xs) a = xs
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.le_jacobson : ∀ {R : Type u} [inst : Ring R] {I : Ideal R}, I ≤ I.jacobson
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.range_vadd_range : ∀ {α : Type u_2} {β : Type u_3} {ι : Type u_5} {κ : Type u_6} [inst : VAdd α β] (b : ι → α) (c : κ → β),
  Set.range b +ᵥ Set.range c = Set.range fun p => b p.1 +ᵥ c p.2
-- Mathlib.Order.UpperLower.Basic
isLowerSet_sUnion : ∀ {α : Type u_1} [inst : LE α] {S : Set (Set α)}, (∀ s ∈ S, IsLowerSet s) → IsLowerSet (⋃₀ S)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_vadd_right_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P} {v : V}, v ∈ s.direction → (s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y)
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.node.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α),
  sizeOf (Ordnode.node size l x r) = 1 + sizeOf size + sizeOf l + sizeOf x + sizeOf r
-- Mathlib.Combinatorics.Quiver.Covering
/-- The `Quiver.Star` at a vertex is the collection of arrows whose source is the vertex.
The type `Quiver.Star u` is defined to be `Σ (v : U), (u ⟶ v)`.  -/
Quiver.Star : {U : Type u_1} → [Quiver U] → U → Type (max u_1 u)
-- Mathlib.Order.CountableSupClosed
supClosed_countableSupClosure : ∀ {α : Type u_2} {s : Set α} [inst : SemilatticeSup α], SupClosed (countableSupClosure s)
-- Mathlib.Algebra.GCDMonoid.Basic
isUnit_gcd_of_eq_mul_gcd : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {x y x' y' : α},
  x = gcd x y * x' → y = gcd x y * y' → gcd x y ≠ 0 → IsUnit (gcd x' y')
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.add_iff_right : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M N : Matrix m m R} {b : m → α} [inst : LT α] [inst_1 : AddGroup R],
  M.BlockTriangular b → ((M + N).BlockTriangular b ↔ N.BlockTriangular b)
-- Lean.Elab.Command
Lean.Elab.Command.Context.mk : String →
  Lean.FileMap →
    ℕ →
      String.Pos.Raw →
        Lean.Elab.MacroStack →
          Option Lean.Name →
            Lean.MacroScope →
              Lean.Syntax →
                Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot) →
                  Option IO.CancelToken → Bool → Lean.Elab.Command.Context
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.le_centralizer_centralizer : ∀ (M : Type u_1) [inst : AddMonoid M] {s : AddSubmonoid M}, s ≤ AddSubmonoid.centralizer ↑(AddSubmonoid.centralizer ↑s)
-- Mathlib.Order.WithBot
WithBot.instBoundedOrder : {α : Type u_1} → [inst : LE α] → [OrderTop α] → BoundedOrder (WithBot α)
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A surjective embedding is a homeomorphism.  -/
Topology.IsEmbedding.toHomeomorphOfSurjective : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f : X → Y} → Topology.IsEmbedding f → Function.Surjective f → X ≃ₜ Y
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `Left.one_lt_inv_iff`.

---

Uses `left` co(ntra)variant.  -/
one_lt_inv_of_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a : α}, a < 1 → 1 < a⁻¹
-- Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
HomotopyCategory.spectralObjectMappingCone_δ'_app : ∀ (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.Limits.HasBinaryBiproducts C]
  (D : CategoryTheory.ComposableArrows (CochainComplex C ℤ) 2),
  (HomotopyCategory.spectralObjectMappingCone C).δ'.app D =
    ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj
        (CochainComplex.mappingConeCompTriangle
          (D.map' 0 1 HomotopyCategory.composableArrowsFunctor._proof_1
            HomotopyCategory.spectralObjectMappingCone._proof_2)
          (D.map' 1 2 HomotopyCategory.spectralObjectMappingCone._proof_2
            HomotopyCategory.spectralObjectMappingCone._proof_3))).mor₃
-- Mathlib.Algebra.Module.Submodule.Lattice
/-- Version of `AddSubgroup.disjoint_iff_add_eq_zero` for submodules.  -/
Submodule.disjoint_iff_add_eq_zero : ∀ {M : Type u_4} {R : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N₁ N₂ : Submodule R M},
  Disjoint N₁ N₂ ↔ ∀ {x y : M}, x ∈ N₁ → y ∈ N₂ → x + y = 0 → x = 0 ∧ y = 0
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.State.perfect : Aesop.Script.DynStructureM.State → Bool
-- Mathlib.Tactic.Linarith.Datatypes
/-- A `CertificateOracle` provides a function
`produceCertificate : List Comp → Nat → MetaM (HashMap Nat Nat)`.

The default `CertificateOracle` used by `linarith` is
`Linarith.CertificateOracle.simplexAlgorithmSparse`.
`Linarith.CertificateOracle.simplexAlgorithmDense` and `Linarith.CertificateOracle.fourierMotzkin`
are also available (though the Fourier-Motzkin oracle has some bugs).
 -/
Mathlib.Tactic.Linarith.CertificateOracle : Type
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} {fallback : γ} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl k fallback =
    ((Std.DTreeMap.Internal.Impl.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k : α} [inst_1 : Inhabited β] {f : β → β},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.modify t k f) k =
    (Option.map f (Std.ExtDTreeMap.Const.get? t k)).get!
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.coe_id : ∀ (α : Type u_2) [inst : CompleteLattice α], ⇑(FrameHom.id α) = id
-- Mathlib.Data.Sum.Order
/-- The lexicographical top of a sum is the top of the right component.  -/
Sum.Lex.orderTop : {α : Type u_1} → {β : Type u_2} → [inst : LE α] → [inst_1 : LE β] → [OrderTop β] → OrderTop (α ⊕ₗ β)
-- Mathlib.RingTheory.Localization.Defs
/-- The localization of a `Fintype` is a `Fintype`. Cannot be an instance.  -/
IsLocalization.fintype' : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) →
        [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → [Fintype R] → Fintype S
-- Mathlib.Algebra.Homology.SpectralObject.Page
_private.Mathlib.Algebra.Homology.SpectralObject.Page.0.CategoryTheory.ComposableArrows.Precomp.obj.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin (n + 1 + 1) → Sort u_1) (isLt : 0 < n + 1 + 1) (h_1 : (isLt : 0 < n + 1 + 1) → motive ⟨0, isLt⟩)
  (h_2 : (i : ℕ) → (hi : i + 1 < n + 1 + 1) → motive ⟨i.succ, hi⟩),
  (match ⟨0, isLt⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨i.succ, hi⟩ => h_2 i hi) =
    h_1 isLt
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.minKey? = some km → t.contains km = true
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
/-- If elements of a list additively commute with each other, then their sum does not
depend on the order of elements.  -/
List.Perm.sum_eq' : ∀ {M : Type u_4} [inst : AddMonoid M] {l₁ l₂ : List M}, l₁.Perm l₂ → List.Pairwise AddCommute l₁ → l₁.sum = l₂.sum
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.smul_bot : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (m : M),
  m • ⊥ = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_fst_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : Inhabited β] {a : α},
  Std.DTreeMap.Raw.Const.get! ∅ a = default
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp.sizeOf_spec : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift)
  (f g h i : Mathlib.Tactic.BicategoryLike.Mor₁) (α : Mathlib.Tactic.BicategoryLike.CoherenceHom)
  (η θ : Mathlib.Tactic.BicategoryLike.Mor₂),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp e isoLift? f g h i α η θ) =
    1 + sizeOf e + sizeOf isoLift? + sizeOf f + sizeOf g + sizeOf h + sizeOf i + sizeOf α + sizeOf η + sizeOf θ
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Jacobi symbol takes only the values `0`, `1` and `-1`.  -/
jacobiSym.trichotomy : ∀ (a : ℤ) (b : ℕ), jacobiSym a b = 0 ∨ jacobiSym a b = 1 ∨ jacobiSym a b = -1
-- Init.Data.ByteArray.Basic
ByteArray.ext_iff : ∀ {x y : ByteArray}, x = y ↔ x.data = y.data
-- Mathlib.FieldTheory.KrullTopology
krullTopology_mem_nhds_one_iff_of_normal : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Normal K L]
  (s : Set Gal(L/K)), s ∈ nhds 1 ↔ ∃ E, FiniteDimensional K ↥E ∧ Normal K ↥E ∧ ↑E.fixingSubgroup ⊆ s
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_inv_fst : ∀ (X Y : TopCat),
  CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv CategoryTheory.Limits.prod.fst = TopCat.prodFst
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.topCat_hasColimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasColimitsOfSize.{w, v, u, u + 1} TopCat
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_eq_empty_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ε : ℝ} {s : Set α}, Metric.thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_hom_left_snd_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom T.hom) S.hom))
        (CategoryTheory.Limits.pullback.fst S.hom T.hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom)
      (CategoryTheory.Limits.pullback.snd R.hom S.hom)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmopFunctor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (self : Cᴹᵒᵖ),
  (CategoryTheory.unmopFunctor C).obj self = self.unmop
-- Mathlib.Topology.Bornology.Basic
Bornology.ext_iff_isBounded : ∀ {α : Type u_2} {t t' : Bornology α}, t = t' ↔ ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.krullDimLE_zero_and_isLocalRing_tfae : ∀ (R : Type u_1) [inst : CommSemiring R],
  [Ring.KrullDimLE 0 R ∧ IsLocalRing R, ∃! I, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x,
      (nilradical R).IsMaximal].TFAE
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_mapFinIdx : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β}
  {g : (i : ℕ) → β → i < n → γ}, (xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx fun i a h => g i (f i a h) h
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A countably compact set has a finite subcover for any countable open cover indexed by a
subset.  -/
IsCountablyCompact.elim_finite_subcover_image : ∀ {ι : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] {A : Set E},
  IsCountablyCompact A →
    ∀ {b : Set ι},
      b.Countable → ∀ {U : ι → Set E}, (∀ i ∈ b, IsOpen (U i)) → A ⊆ ⋃ i ∈ b, U i → ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` is absolutely continuous on `uIcc a b`, then `f` is bounded on `uIcc a b`.  -/
AbsolutelyContinuousOnInterval.exists_bound : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F},
  AbsolutelyContinuousOnInterval f a b → ∃ C, ∀ x ∈ Set.uIcc a b, ‖f x‖ ≤ C
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_done_iff_toBitVec : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.done ↔
    BitVec.extractLsb' 7 1 b.toBitVec = 0#1
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (curr : ℕ)
  (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs rhs : aig.RefVec len)
  (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α f]
  (idx : ℕ) (hidx : idx < curr)
  (hfoo : aig.decls.size ≤ (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).aig.decls.size),
  (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).vec.get idx ⋯ = (s.get idx hidx).cast hfoo
-- Mathlib.Algebra.Ring.Pointwise.Set
Set.add_mul_subset : ∀ {α : Type u_1} [inst : Distrib α] (s t u : Set α), (s + t) * u ⊆ s * u + t * u
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.parseFirstByte.eq_1 : ∀ (b : UInt8),
  ByteArray.utf8DecodeChar?.parseFirstByte b =
    if (b &&& 128 == 0) = true then ByteArray.utf8DecodeChar?.FirstByte.done
    else
      if (b &&& 224 == 192) = true then ByteArray.utf8DecodeChar?.FirstByte.oneMore
      else
        if (b &&& 240 == 224) = true then ByteArray.utf8DecodeChar?.FirstByte.twoMore
        else
          if (b &&& 248 == 240) = true then ByteArray.utf8DecodeChar?.FirstByte.threeMore
          else ByteArray.utf8DecodeChar?.FirstByte.invalid
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.mk'_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : HomotopicalAlgebra.IsFibrant X] [inst_3 : HomotopicalAlgebra.IsFibrant Y]
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))),
  (HomotopicalAlgebra.FibrantBrownFactorization.mk' f h).r =
    CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.snd
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.ofProd.eq_1 : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (Q₁ : QuadraticForm R M₁)
  (Q₂ : QuadraticForm R M₂),
  CliffordAlgebra.ofProd Q₁ Q₂ =
    (CliffordAlgebra.lift (QuadraticMap.prod Q₁ Q₂))
      ⟨((GradedTensorProduct.includeLeft (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂)).toLinearMap ∘ₗ
              (CliffordAlgebra.evenOdd Q₁ 1).subtype ∘ₗ
                LinearMap.codRestrict (CliffordAlgebra.evenOdd Q₁ 1) (CliffordAlgebra.ι Q₁) ⋯).coprod
          ((GradedTensorProduct.includeRight (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂)).toLinearMap ∘ₗ
            (CliffordAlgebra.evenOdd Q₂ 1).subtype ∘ₗ
              LinearMap.codRestrict (CliffordAlgebra.evenOdd Q₂ 1) (CliffordAlgebra.ι Q₂) ⋯),
        ⋯⟩
-- Mathlib.NumberTheory.FunctionField
FunctionField.ringOfIntegers.instIsFractionRingSubtypeMemSubalgebraPolynomial : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] [FunctionField F K],
  IsFractionRing (↥(FunctionField.ringOfIntegers F K)) K
-- Mathlib.MeasureTheory.Group.Arithmetic
Multiset.aemeasurable_sum : ∀ {M : Type u_2} {α : Type u_4} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (l : Multiset (α → M)),
  (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.sum μ
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1Fin.congr_simp : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s s_1 : Set α} (e_s : s = s_1) [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0)
  [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x x_1 : G),
  x = x_1 → MeasureTheory.condExpIndL1Fin hm hs hμs x = MeasureTheory.condExpIndL1Fin hm ⋯ ⋯ x_1
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_eq_of_col_eq : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {p q : n}, p ≠ q → A.col p = A.col q → ∀ (s : optParam ℤˣ 1) (t : optParam ℤˣ (-1)), Matrix.detp s A = Matrix.detp t A
-- Mathlib.MeasureTheory.Measure.PreVariation
/-- Additivity of `preVariationFun` for disjoint measurable sets.  -/
MeasureTheory.preVariation.iUnion : ∀ {X : Type u_1} [inst : MeasurableSpace X] {f : Set X → ENNReal},
  MeasureTheory.IsSigmaSubadditiveSetFun f →
    f ∅ = 0 →
      ∀ (s : ℕ → Set X),
        (∀ (i : ℕ), MeasurableSet (s i)) →
          Pairwise (Function.onFun Disjoint s) →
            HasSum (fun i => MeasureTheory.preVariationFun f (s i)) (MeasureTheory.preVariationFun f (⋃ i, s i))