mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- A choice of limit weighted cone.  -/
CategoryTheory.Functor.weightedLimCone : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (W : CategoryTheory.Functor J (Type w)) →
          (F : CategoryTheory.Functor J C) →
            [CategoryTheory.Limits.HasWeightedLimit W F] → CategoryTheory.Limits.WeightedCone W F
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.name : LeanSearchClient.SearchServer → String
-- Mathlib.Data.Sigma.Order
/-- The notation `Σₗ i, α i` refers to a sigma type equipped with the lexicographic order.  -/
Sigma.Lex.«termΣₗ_,_» : Lean.ParserDescr
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitial_succ : ∀ {o : Ordinal.{u_1}}, (Order.succ o).IsInitial ↔ o < Ordinal.omega0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.step.match_1.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (motive : Turing.TM1.Cfg Γ Λ σ → Sort u_4) (l : Λ)
  (v : σ) (T : Turing.Tape Γ)
  (h_1 : (var : σ) → (Tape : Turing.Tape Γ) → motive { l := none, var := var, Tape := Tape })
  (h_2 : (l : Λ) → (v : σ) → (T : Turing.Tape Γ) → motive { l := some l, var := v, Tape := T }),
  (match { l := some l, var := v, Tape := T } with
    | { l := none, var := var, Tape := Tape } => h_1 var Tape
    | { l := some l, var := v, Tape := T } => h_2 l v T) =
    h_2 l v T
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.drop_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X :
    CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C)
      (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))),
  CategoryTheory.CosimplicialObject.Augmented.drop.obj X = X.right
-- Mathlib.Condensed.Discrete.Colimit
Condensed.fintypeCatAsCofanIsColimit.congr_simp : ∀ (X : Profinite) [inst : Finite ↑X.toTop],
  Condensed.fintypeCatAsCofanIsColimit X = Condensed.fintypeCatAsCofanIsColimit X
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Matrix.IsHermitian.cfc_eq : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜}
  (hA : A.IsHermitian) (f : ℝ → ℝ), cfc f A = hA.cfc f
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- `arsinh` is the right inverse of `sinh`.  -/
Real.sinh_arsinh : ∀ (x : ℝ), Real.sinh (Real.arsinh x) = x
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_iInf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {ι : Sort u_5} {S : ι → StarSubalgebra R A}
  {x : A}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_natDegree_le_one : ∀ {R : Type u_1} [inst : DivisionSemiring R] {f : Polynomial R}, f.natDegree ≤ 1 → f.Splits
-- Std.Data.DTreeMap.Lemmas
_private.Std.Data.DTreeMap.Lemmas.0.Std.DTreeMap.equiv_iff_equiv : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ ↔ t₁.inner.Equiv t₂.inner
-- Init.Data.BitVec.Bitblast
/-- Recursive addition of the elements in a flattened bitvec.  -/
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRec : {l w : ℕ} → BitVec (l * w) → BitVec w
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_of_perm : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α},
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.getValue? a l = Std.Internal.List.getValue? a l'
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.toOrderHom.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β), f.toOrderHom = { toFun := (↑f.toMonoidHom).toFun, monotone' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.instSubsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D), Subsingleton F.Monoidal
-- Init.Data.Array.Range
Array.reverse_range' : ∀ {s n : ℕ}, (Array.range' s n).reverse = Array.map (fun x => s + n - 1 - x) (Array.range n)
-- Mathlib.Logic.Relation
Subrelation.antisymm : ∀ {α : Type u_1} {r r' : α → α → Prop}, r ≤ r' → r' ≤ r → r = r'
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryFinFinset_apply : ∀ {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k l : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : G [×n]→L[𝕜] G') (mk : Fin k → G) (ml : Fin l → G),
  (((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) mk) ml =
    f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.mk_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N)
  (hadd : ∀ (x y : M), (↑f).toFun (x + y) = (↑f).toFun x + (↑f).toFun y), { toZeroHom := ↑f, map_add' := hadd } = f
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsHaarMeasure.toIsOpenPosMeasure : ∀ {G : Type u_3} {inst : Group G} {inst_1 : TopologicalSpace G} {inst_2 : MeasurableSpace G}
  {μ : MeasureTheory.Measure G} [self : μ.IsHaarMeasure], μ.IsOpenPosMeasure
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumFinsuppEquivProdFinsupp_apply : ∀ {α : Type u_12} {β : Type u_13} {γ : Type u_14} [inst : Zero γ] (f : α ⊕ β →₀ γ),
  Finsupp.sumFinsuppEquivProdFinsupp f = (Finsupp.comapDomain Sum.inl f ⋯, Finsupp.comapDomain Sum.inr f ⋯)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSolvable L], LieAlgebra.IsSolvable ↥⊤
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.lift_algebraMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0)
  (a : R), (h.lift i x hx) ((algebraMap R S) a) = i a
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.mk_div_mk : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {x y : α} (hx : 0 ≤ x)
  (hy : 0 ≤ y), ⟨x, hx⟩ / ⟨y, hy⟩ = ⟨x / y, ⋯⟩
-- Lean.Parser.Command
Lean.Parser.Command.section.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.List.MinMaxOn
List.maxOn?_mem : ∀ {β : Type u_1} {α : Type u_2} {a : α} [inst : LE β] [inst_1 : DecidableLE β] {xs : List α} {f : α → β},
  List.maxOn? f xs = some a → a ∈ xs
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `upperHemicontinuous_singleton_iff`. -/
Continuous.upperHemicontinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → UpperHemicontinuous fun x => {f x}
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- If `C` has an object such that every morphism *from* it is an isomorphism, then `C`
has strict terminal objects.  -/
CategoryTheory.Limits.hasStrictTerminalObjects_of_terminal_is_strict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : C),
  (∀ (A : C) (f : I ⟶ A), CategoryTheory.IsIso f) → CategoryTheory.Limits.HasStrictTerminalObjects C
-- Mathlib.Topology.EMetricSpace.BoundedVariation
MonotoneOn.boundedVariationOn : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α} {C : ℝ},
  MonotoneOn f s → (∀ x ∈ s, |f x| ≤ C) → BoundedVariationOn f s
-- Batteries.Data.List.Interleave
List.interleave_append_append_of_length_eq_length_add_one : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.length = l₂.length + 1 →
    ∀ (l₃ l₄ : List α), (l₁ ++ l₃).interleave (l₂ ++ l₄) = l₁.interleave l₂ ++ l₄.interleave l₃
-- Lean.DocString.Types
Lean.Doc.Block.concat.injEq : ∀ {i : Type u} {b : Type v} (content content_1 : Array (Lean.Doc.Block i b)),
  (Lean.Doc.Block.concat content = Lean.Doc.Block.concat content_1) = (content = content_1)
-- Init.Data.Vector.Lemmas
Vector.map_eq_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β} {b : β},
  Vector.map f xs = Vector.replicate n b ↔ ∀ x ∈ xs, f x = b
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
DirectedOn.isGLB_ciInf_set : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderInf α] {f : β → α} {s : Set β},
  DirectedOn (fun x1 x2 => x2 ≤ x1) (f '' s) → BddBelow (f '' s) → s.Nonempty → IsGLB (f '' s) (⨅ i, f ↑i)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- Unexpander for `μ[f | m]` notation.  -/
MeasureTheory.condExpUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.instFunLikeBox : {ι : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommMonoid M] →
      {I₀ : WithTop (BoxIntegral.Box ι)} → FunLike (BoxIntegral.BoxAdditiveMap ι M I₀) (BoxIntegral.Box ι) M
-- Lean.Elab.Binders
Lean.Elab.Term.elabFun : Lean.Elab.Term.TermElab
-- Std.Time.Date.Unit.Year
/-- Returns the `Era` of the `Year`.
 -/
Std.Time.Year.Offset.era : Std.Time.Year.Offset → Std.Time.Year.Era
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_le_one : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α)
  (x : ℝ), ↑(hf.stieltjesFunction a) x ≤ 1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {w₀ : NumberField.InfinitePlace K},
  w₀.IsComplex →
    ∀ {B : NNReal},
      NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLT'Factor K) * ↑B →
        ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : NumberField.InfinitePlace K), w ↑a < √(1 + ↑B ^ 2)
-- Lean.Expr
Lean.instInhabitedMVarIdMap : {α : Type} → Inhabited (Lean.MVarIdMap α)
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `tangentMapWithin I I' f s` is the derivative of `f : M → M'` within a set `s`,
as a map between the tangent bundles `TM` and `TM'`.  -/
tangentMapWithin : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                (I' : ModelWithCorners 𝕜 E' H') →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        (M → M') → Set M → TangentBundle I M → TangentBundle I' M'
-- Mathlib.Tactic.TacticAnalysis
/-- Information about a tactic in a sequence, parsed from infotrees and passed to a tactic
analysis pass.  -/
Mathlib.TacticAnalysis.TacticNode : Type
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
AddEquiv.addSubgroupCongr.congr_simp : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H = K),
  AddEquiv.addSubgroupCongr h = AddEquiv.addSubgroupCongr h
-- Mathlib.Algebra.Order.Monovary
Antivary.pow_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g : ι → β}, 0 ≤ g → Antivary f g → ∀ (n : ℕ), Antivary f (g ^ n)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.basis.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e e_1 : ι → M} (e_e : e = e_1) {ε ε_1 : ι → Module.Dual R M} (e_ε : ε = ε_1) (h : Module.DualBases e ε),
  h.basis = ⋯.basis
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.JointlyMono₂.right_cancellation : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R X₁ X₂ : C} {p₁ : R ⟶ X₁} {p₂ : R ⟶ X₂}
  [self : CategoryTheory.JointlyMono₂ p₁ p₂] ⦃Y : C⦄ (f g : Y ⟶ R),
  CategoryTheory.CategoryStruct.comp f p₁ = CategoryTheory.CategoryStruct.comp g p₁ →
    CategoryTheory.CategoryStruct.comp f p₂ = CategoryTheory.CategoryStruct.comp g p₂ → f = g
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_le_dual : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I J : FractionalIdeal (nonZeroDivisors B) L},
  I ≠ 0 → J ≠ 0 → (FractionalIdeal.dual A K I ≤ FractionalIdeal.dual A K J ↔ J ≤ I)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.neg_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (-φ).τ₂ = -φ.τ₂
-- Mathlib.Algebra.Torsor.Defs
/-- Convert between an equality with multiplying a group element with a point
and an equality of a division of two points with a group element.  -/
eq_smul_iff_sdiv_eq : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p₁ : P) (g : G) (p₂ : P), p₁ = g • p₂ ↔ p₁ /ₛ p₂ = g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {W : C} {k l : W ⟶ CategoryTheory.Limits.pullback f g},
  k = l ↔
    CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.pullback.fst f g) =
        CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.fst f g) ∧
      CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.pullback.snd f g) =
        CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.snd f g)
-- Init.Data.List.Lemmas
List.isEqv.eq_1 : ∀ {α : Type u} (x : α → α → Bool), [].isEqv [] x = true
-- Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
/-- Given an algebra isomorphism `f : End K V ≃ₐ[K] End K W`, there exists a linear isomorphism `T`
such that `f` is given by `x ↦ T ∘ₗ x ∘ₗ T.symm`.  -/
AlgEquiv.eq_linearEquivConjAlgEquiv : ∀ {K : Type u_1} {V : Type u_2} {W : Type u_3} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V] [inst_4 : AddCommMonoid W] [inst_5 : Module K W] [Module.Projective K W]
  (f : Module.End K V ≃ₐ[K] Module.End K W), ∃ T, f = LinearEquiv.conjAlgEquiv K T
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Ioi_of_tendsto_atTop_atTop : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R],
  Filter.Tendsto (↑f) Filter.atTop Filter.atTop → ∀ (x : R), f.measure (Set.Ioi x) = ⊤
-- Std.Time.Format.Basic
/-- If the format is aware of some timezone data it parses or if it parses any timezone.
 -/
Std.Time.Awareness : Type
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.prodCompExternalProduct_hom_app : ∀ {J₁ : Type u₁} {J₂ : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] {I₁ : Type u₃} {I₂ : Type u₄}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} I₁] [inst_5 : CategoryTheory.Category.{v₄, u₄} I₂]
  (F₁ : CategoryTheory.Functor I₁ J₁) (G₁ : CategoryTheory.Functor J₁ C) (F₂ : CategoryTheory.Functor I₂ J₂)
  (G₂ : CategoryTheory.Functor J₂ C) (X : I₁ × I₂),
  (CategoryTheory.MonoidalCategory.prodCompExternalProduct F₁ G₁ F₂ G₂).hom.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (G₁.obj (F₁.obj X.1)) (G₂.obj (F₂.obj X.2)))
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_takeWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String.Slice},
  (s.takeWhile pat).isEmpty = !s.startsWith pat
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.mono_measure : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {ν : MeasureTheory.Measure α},
  MeasureTheory.AEStronglyMeasurable f μ → ν ≤ μ → MeasureTheory.AEStronglyMeasurable f ν
-- Mathlib.Algebra.BrauerGroup.Defs
CSA.mk.injEq : ∀ {K : Type u} [inst : Field K] (toAlgCat : AlgCat K) [isCentral : Algebra.IsCentral K ↑toAlgCat]
  [isSimple : IsSimpleRing ↑toAlgCat] [fin_dim : FiniteDimensional K ↑toAlgCat] (toAlgCat_1 : AlgCat K)
  (isCentral_1 : Algebra.IsCentral K ↑toAlgCat_1) (isSimple_1 : IsSimpleRing ↑toAlgCat_1)
  (fin_dim_1 : FiniteDimensional K ↑toAlgCat_1),
  ({ toAlgCat := toAlgCat, isCentral := isCentral, isSimple := isSimple, fin_dim := fin_dim } =
      { toAlgCat := toAlgCat_1, isCentral := isCentral_1, isSimple := isSimple_1, fin_dim := fin_dim_1 }) =
    (toAlgCat = toAlgCat_1)
-- Init.Prelude
instMonadEvalTOfMonadEval : (m : Type u_1 → Type u_2) →
  (n : Type u_1 → Type u_3) → (o : Type u_1 → Type u_4) → [MonadEval n o] → [MonadEvalT m n] → MonadEvalT m o
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sdiv : ∀ {w : ℕ} {x y : BitVec w},
  (x.sdiv y).toNat =
    match x.msb, y.msb with
    | false, false => (x.udiv y).toNat
    | false, true => (-x.udiv (-y)).toNat
    | true, false => (-(-x).udiv y).toNat
    | true, true => ((-x).udiv (-y)).toNat
-- Mathlib.Geometry.Convex.ConvexSpace.Module
/-- **Alias** of `Convexity.IsModuleConvexSpace.sConvexComb_eq_sum`. -/
convexCombination_eq_sum : ∀ {R : Type u_2} {M : Type u_3} {inst : Semiring R} {inst_1 : PartialOrder R} {inst_2 : IsStrictOrderedRing R}
  {inst_3 : AddCommMonoid M} {inst_4 : Module R M} {inst_5 : Convexity.ConvexSpace R M}
  [self : Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R M),
  Convexity.sConvexComb w = w.weights.sum fun m r => r • m
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.coe_iSup_of_chain : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a : ℕ →o Submodule R M), ↑(⨆ k, a k) = ⋃ k, ↑(a k)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_antitoneOn : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  AntitoneOn ArchimedeanClass.mk (Set.Ici 0)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_symmDiff_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s t u : Set α),
  μ (symmDiff s u) ≤ μ (symmDiff s t) + μ (symmDiff t u)
-- Std.Async.Basic
/-- Obtain the `IO.TaskState` of `x`.
 -/
Std.Async.ETask.getState : {ε α : Type} → Std.Async.ETask ε α → BaseIO IO.TaskState
-- Mathlib.Algebra.Lie.OfAssociative
LieSubmodule.toEnd_restrict_eq_toEnd : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (N : LieSubmodule R L M) (x : L)
  (h : optParam (∀ (m : M) (hm : m ∈ ↑N), ((LieModule.toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N) ⋯),
  LinearMap.restrict ((LieModule.toEnd R L M) x) h = (LieModule.toEnd R L ↥N) x
-- Init.Data.List.Nat.Erase
List.getElem?_eraseIdx_of_lt : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, j < i → (l.eraseIdx i)[j]? = l[j]?
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- A `Triangle k P` is a collection of three affinely independent points.  -/
Affine.Triangle : (k : Type u_1) →
  {V : Type u_2} →
    (P : Type u_5) → [inst : Ring k] → [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → Type u_5
-- Init.Data.List.Lemmas
List.filterMap_replicate_of_isSome : ∀ {α : Type u_1} {β : Type u_2} {a : α} {n : ℕ} {f : α → Option β} (h : (f a).isSome = true),
  List.filterMap f (List.replicate n a) = List.replicate n ((f a).get h)
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.derivative_succ : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ),
  Polynomial.derivative (bernsteinPolynomial R n (ν + 1)) =
    ↑n * (bernsteinPolynomial R (n - 1) ν - bernsteinPolynomial R (n - 1) (ν + 1))
-- Mathlib.Algebra.Order.Group.Action.Flag
Flag.coe_smul : ∀ {α : Type u_1} [inst : Preorder α] (e : α ≃o α) (s : Flag α), ↑(e • s) = e • ↑s
-- Init.Data.Range.Polymorphic.Basic
/-- If the smallest value in the range satisfies the upper bound and has a successor, the size is
  one larger than the size of the range starting at the successor.  -/
Std.Rxo.LawfulHasSize.size_eq_succ_of_succ?_eq_some : ∀ {α : Type u} {inst : LT α} {inst_1 : Std.PRange.UpwardEnumerable α} {inst_2 : Std.Rxo.HasSize α}
  [self : Std.Rxo.LawfulHasSize α] (lo hi lo' : α),
  lo < hi → Std.PRange.succ? lo = some lo' → Std.Rxo.HasSize.size lo hi = Std.Rxo.HasSize.size lo' hi + 1
-- Init.Data.Int.Gcd
Int.gcd_gcd_self_left_left : ∀ (m n : ℤ), (↑(m.gcd n)).gcd m = m.gcd n
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Also see `Finset.sum_ite_mem_eq`  -/
Finset.sum_eq_sum_extend : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] (f : ↥s → M),
  ∑ x, f x = ∑ x ∈ s, Function.extend Subtype.val f 0 x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Rat.instUniqueInfinitePlace : Unique (NumberField.InfinitePlace ℚ)
-- Std.Time.Date.ValidDate
Std.Time.instOrdValidDate : {leap : Bool} → Ord (Std.Time.ValidDate leap)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bddAbove_add_one_image_iff : ∀ {s : Set Ordinal.{u_3}}, BddAbove ((fun x => x + 1) '' s) ↔ BddAbove s
-- Mathlib.Tactic.Linarith.Preprocessing
/-- Get proofs for products of inequalities from `ls`.

Note that the length of the resulting list is proportional to `ls.length^2`, which can make a large
amount of work for the linarith oracle.
 -/
_private.Mathlib.Tactic.Linarith.Preprocessing.0.Mathlib.Tactic.Linarith.nlinarithGetProductsProofs : List Lean.Expr → Lean.MetaM (List Lean.Expr)
-- Mathlib.Data.Multiset.Filter
/-- `Multiset.map f` preserves `count` if `f` is injective  -/
Multiset.count_map_eq_count' : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → β) (s : Multiset α),
  Function.Injective f → ∀ (x : α), Multiset.count (f x) (Multiset.map f s) = Multiset.count x s