mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsCocartesian.map.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p p_1 : CategoryTheory.Functor 𝒳 𝒮) (e_p : p = p_1) {R S : 𝒮} {a b : 𝒳} (f f_1 : R ⟶ S) (e_f : f = f_1)
  (φ φ_1 : a ⟶ b) (e_φ : φ = φ_1) [inst_2 : p.IsCocartesian f φ] {b' : 𝒳} (φ' φ'_1 : a ⟶ b') (e_φ' : φ' = φ'_1)
  [inst_3 : p.IsHomLift f φ'],
  CategoryTheory.Functor.IsCocartesian.map p f φ φ' = CategoryTheory.Functor.IsCocartesian.map p_1 f_1 φ_1 φ'_1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- Construct a continuous linear map between two (dependent) function spaces
by applying index-dependent linear maps to the coordinates.
A bundled version of `Pi.map`.

If the index type is finite, then this map can be seen as a “block diagonal” map
between indexed products of modules.  -/
ContinuousLinearMap.piMap : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_4} →
      {φ : ι → Type u_5} →
        [inst_1 : (i : ι) → TopologicalSpace (φ i)] →
          [inst_2 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_3 : (i : ι) → Module R (φ i)] →
              {ψ : ι → Type u_6} →
                [inst_4 : (i : ι) → TopologicalSpace (ψ i)] →
                  [inst_5 : (i : ι) → AddCommMonoid (ψ i)] →
                    [inst_6 : (i : ι) → Module R (ψ i)] →
                      ((i : ι) → φ i →L[R] ψ i) → ((i : ι) → φ i) →L[R] (i : ι) → ψ i
-- Mathlib.Order.Category.Preord
Preord.id_apply : ∀ (X : Preord) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
/-- If `P` is stable under base change, so is `affineAnd P`.  -/
AlgebraicGeometry.affineAnd_isStableUnderBaseChange : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q) →
      (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q).IsStableUnderBaseChange
-- Mathlib.Topology.Order.NhdsSet
Ico_mem_nhdsSet_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a ≤ b → c < d → Set.Ico a d ∈ nhdsSet (Set.Ioc b c)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_add_intCast' : ∀ {y : ℝ} {n : ℤ}, y + ↑n ≠ 0 → ∀ (x : NNReal), x ^ (y + ↑n) = x ^ y * x ^ n
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.prod_ite_eq'`.  -/
Fintype.prod_ite_eq' : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι) (f : ι → M),
  (∏ j, if j = i then f j else 1) = f i
-- Mathlib.Control.Functor.Multivariate
/-- predicate lifting over multivariate functors  -/
MvFunctor.LiftP : {n : ℕ} → {F : TypeVec.{u} n → Type v} → [MvFunctor F] → {α : TypeVec.{u} n} → ((i : Fin2 n) → α i → Prop) → F α → Prop
-- Lean.DocString.Types
Lean.Doc.MathMode.noConfusionType : Sort v✝ → Lean.Doc.MathMode → Lean.Doc.MathMode → Sort v✝
-- Mathlib.Order.Disjointed
/-- An induction principle for `disjointed`. To prove something about `disjointed f i`, it's
enough to prove it for `f i` and being able to extend through diffs.
 -/
disjointedRec : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι] {f : ι → α} {p : α → Prop},
  (∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)) → ∀ ⦃i : ι⦄, p (f i) → p (disjointed f i)
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuous_empty : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] [h : IsEmpty ι]
  (F : ι → β → α), UniformEquicontinuous F
-- Init.Data.List.Count
List.one_le_countP_iff : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, 1 ≤ List.countP p l ↔ ∃ a ∈ l, p a = true
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.induction_on₃ : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M}
  {p : AddLocalization S → AddLocalization S → AddLocalization S → Prop} (x y z : AddLocalization S),
  (∀ (x y z : M × ↥S), p (AddLocalization.mk x.1 x.2) (AddLocalization.mk y.1 y.2) (AddLocalization.mk z.1 z.2)) →
    p x y z
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.sumStructure : (L₁ : FirstOrder.Language) →
  (L₂ : FirstOrder.Language) → (S : Type u_3) → [L₁.Structure S] → [L₂.Structure S] → (L₁.sum L₂).Structure S
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.foldM_filterWithPostcondition : ∀ {α β δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Monad o] [LawfulMonad n] [LawfulMonad o]
  [inst_6 : Std.IteratorLoop α Id n] [inst_7 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id o] [inst_10 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ} {it : Std.Iter β},
  Std.IterM.foldM g init (Std.Iter.filterWithPostcondition f it) =
    Std.Iter.foldM
      (fun d b => do
        let __do_lift ← liftM (f b).run
        if __do_lift.down = true then g d b else pure d)
      init it
-- Init.Data.SInt.Basic
instReprInt32 : Repr Int32
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Data exhibiting that a morphism `f` has an image.  -/
CategoryTheory.Limits.ImageFactorisation.F : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Limits.ImageFactorisation f → CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.finsetSup'_mem : ∀ {α : Type u_2} {s : Set α} {ι : Type u_4} {f : ι → α} {t : Finset ι} [inst : SemilatticeSup α],
  CountableSupClosed s → ∀ (ht : t.Nonempty), (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s
-- Mathlib.Topology.EMetricSpace.Defs
instEMetricSpaceULift : {α : Type u_2} → [EMetricSpace α] → EMetricSpace (ULift.{u_3, u_2} α)
-- Init.Data.List.Lemmas
List.getElem?_nil : ∀ {α : Type u_1} {i : ℕ}, [][i]? = none
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.arg.injEq : ∀ (a b : Lean.Expr) (i : ℕ) (eq : Lean.Expr) (source : Lean.Meta.Grind.SplitSource) (a_1 b_1 : Lean.Expr) (i_1 : ℕ)
  (eq_1 : Lean.Expr) (source_1 : Lean.Meta.Grind.SplitSource),
  (Lean.Meta.Grind.SplitInfo.arg a b i eq source = Lean.Meta.Grind.SplitInfo.arg a_1 b_1 i_1 eq_1 source_1) =
    (a = a_1 ∧ b = b_1 ∧ i = i_1 ∧ eq = eq_1 ∧ source = source_1)
-- Init.Data.Nat.Basic
Nat.le_sub_one_iff_lt : ∀ {m n : ℕ}, 0 < m → (n ≤ m - 1 ↔ n < m)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_iSup : ∀ {R : Type u} [inst : CommSemiring R] {ι : Sort u_1} (I : ι → Ideal R),
  PrimeSpectrum.zeroLocus ↑(⨆ i, I i) = ⋂ i, PrimeSpectrum.zeroLocus ↑(I i)
-- Mathlib.Algebra.Field.IsField
/-- A predicate to express that a (semi)ring is a (semi)field.

This is mainly useful because such a predicate does not contain data,
and can therefore be easily transported along ring isomorphisms.
Additionally, this is useful when trying to prove that
a particular ring structure extends to a (semi)field.  -/
IsField : (R : Type u) → [Semiring R] → Prop
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization
CategoryTheory.Limits.instHasExactColimitsOfShapeIndOfHasFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.HasExactColimitsOfShape J (CategoryTheory.Ind C)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_inter!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → Std.DTreeMap.Internal.Impl.Const.get? (m₁.inter! m₂) k = none
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addLeftCancelMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddLeftCancelMonoid (f i)],
  Pi.addLeftCancelMonoid =
    { toAddSemigroup := Pi.addLeftCancelSemigroup.toAddSemigroup, toZero := Pi.addMonoid.toZero, zero_add := ⋯,
      add_zero := ⋯, toNSMul := Pi.addMonoid.toNSMul, nsmul_zero := ⋯, nsmul_succ := ⋯, toIsLeftCancelAdd := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_inter_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true →
        Std.DTreeMap.Internal.Impl.Const.get! (m₁.inter m₂ ⋯) k = Std.DTreeMap.Internal.Impl.Const.get! m₁ k
-- Init.Data.SInt.Lemmas
Int64.toBitVec_minValue : Int64.minValue.toBitVec = BitVec.intMin 64
-- Std.Data.TreeMap.Basic
Std.TreeMap.instUnion : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Union (Std.TreeMap α β cmp)
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (H : LieSubalgebra R L),
  H.IsCartanSubalgebra ↔ H.toLieSubmodule.IsUcsLimit
-- Mathlib.Analysis.Convex.EGauge
egauge_union : ∀ {𝕜 : Type u_1} [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] (s t : Set E) (x : E),
  egauge 𝕜 (s ∪ t) x = min (egauge 𝕜 s x) (egauge 𝕜 t x)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Rep.toCoinvariants.congr_simp : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] (A A_1 : Rep.{w, u, v} k G),
  A = A_1 → ∀ (S S_1 : Subgroup G) (e_S : S = S_1) [inst_2 : S.Normal], A.toCoinvariants S = A_1.toCoinvariants S_1
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (fuel guess : ℕ) (h_1 : (guess : ℕ) → motive 0 guess)
  (h_2 : (fuel guess : ℕ) → motive fuel.succ guess),
  (match fuel.succ, guess with
    | 0, guess => h_1 guess
    | fuel.succ, guess => h_2 fuel guess) =
    h_2 fuel guess
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.eq_biUnion_of_isOpen : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  IsOpen s → s = ⋃ r, ⋃ (_ : ↑(PrimeSpectrum.basicOpen r) ⊆ s), ↑(PrimeSpectrum.basicOpen r)
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.mk_as : ∀ (B : Type u₁) (b : CategoryTheory.Bicategory.Pith B), { as := b.as } = b
-- Mathlib.Algebra.Order.SuccPred
Order.IsSuccPrelimit.add_natCast_lt : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α],
  Order.IsSuccPrelimit x → y < x → ∀ (n : ℕ), y + ↑n < x
-- Mathlib.Logic.Equiv.Option
/-- Given an equivalence between two `Option` types, eliminate `none` from that equivalence by
mapping `e.symm none` to `e none`.  -/
Equiv.removeNone : {α : Type u_1} → {β : Type u_2} → Option α ≃ Option β → α ≃ β
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Subshift.mk : {A : Type u_1} →
  [inst : TopologicalSpace A] →
    {G : Type u_2} →
      [inst_1 : AddMonoid G] →
        (carrier : Set (G → A)) →
          IsClosed carrier →
            (∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.shift g) carrier carrier) →
              SymbolicDynamics.FullShift.Subshift A G
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformly.hasSumLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], HasSumLocallyUniformly f g → HasSumLocallyUniformlyOn f g s
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Naturality of the oplax functoriality constraint, on the right.  -/
CategoryTheory.OplaxFunctor.mapComp_naturality_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) (self.mapComp f g') =
    CategoryTheory.CategoryStruct.comp (self.mapComp f g)
      (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.mem_traceDual : ∀ {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] {I : Submodule B L} {x : L},
  x ∈ Submodule.traceDual A K I ↔ ∀ a ∈ I, ((Algebra.traceForm K L) x) a ∈ (algebraMap A K).range
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkIso_inv_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map eₗ.hom) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (G.map eᵣ.hom))
      CategoryTheory.Limits.CategoricalPullback.mkIso._auto_1),
  (CategoryTheory.Limits.CategoricalPullback.mkIso eₗ eᵣ w).inv.snd = eᵣ.inv
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx?.induct_unfolding : ∀ {α : Type u} {β : Type v} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → Option (α × β) → Prop),
  (∀ (x : ℕ), motive Std.DTreeMap.Internal.Impl.leaf x none) →
    (∀ (size : ℕ) (k : α) (v : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β) (n : ℕ),
        compare n l.size = Ordering.lt →
          motive l n (Std.DTreeMap.Internal.Impl.Const.entryAtIdx? l n) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n
              (Std.DTreeMap.Internal.Impl.Const.entryAtIdx? l n)) →
      (∀ (size : ℕ) (k : α) (v : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β) (n : ℕ),
          compare n l.size = Ordering.eq → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n (some (k, v))) →
        (∀ (size : ℕ) (k : α) (v : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β) (n : ℕ),
            compare n l.size = Ordering.gt →
              motive r (n - l.size - 1) (Std.DTreeMap.Internal.Impl.Const.entryAtIdx? r (n - l.size - 1)) →
                motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n
                  (Std.DTreeMap.Internal.Impl.Const.entryAtIdx? r (n - l.size - 1))) →
          ∀ (a : Std.DTreeMap.Internal.Impl α fun x => β) (a_1 : ℕ),
            motive a a_1 (Std.DTreeMap.Internal.Impl.Const.entryAtIdx? a a_1)
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
instIsAddKleinFourProdZModOfNatNat : IsAddKleinFour (ZMod 2 × ZMod 2)
-- Mathlib.Order.Hom.Basic
OrderHom.Subtype.val_coe : ∀ {α : Type u_2} [inst : Preorder α] (p : α → Prop), ⇑(OrderHom.Subtype.val p) = Subtype.val
-- Std.Data.DTreeMap.Internal.Model
Ord.opposite.eq_1 : ∀ {α : Type u_1} (ord : Ord α), ord.opposite = { compare := fun x y => compare y x }
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- `ULift` commutes with tensor products.  -/
TensorProduct.AlgebraTensorModule.uliftEquiv : (R : Type uR) →
  (A : Type uA) →
    (M : Type uM) →
      (N : Type uN) →
        [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] →
                      [inst_7 : AddCommMonoid N] →
                        [inst_8 : Module R N] →
                          ULift.{u₁, max uN uM} (TensorProduct R M N) ≃ₗ[A]
                            TensorProduct (ULift.{u₃, uR} R) (ULift.{u₂, uM} M) (ULift.{u₄, uN} N)
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.instContinuousOpenMapClass : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  ContinuousOpenMapClass (α →CO β) α β
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.cycleCons.eq_1 : ∀ (n : ℕ) (h : 0 < n + 3), SimpleGraph.cycleGraph.cycleCons✝ n ⟨0, h⟩ = SimpleGraph.Walk.nil
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : T.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.snd R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom) T.hom))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom) h
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.CategoryTheory.Skeletal
/-- Two categories which are categorically equivalent have skeletons with equivalent objects.
 -/
CategoryTheory.Equivalence.skeletonEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → CategoryTheory.Skeleton C ≃ CategoryTheory.Skeleton D
-- Init.Data.Rat.Lemmas
Rat.mkRat_self : ∀ (a : ℚ), mkRat a.num a.den = a
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_mul : ∀ (a b : BitVec 8), { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.ne_zero : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R] (i : ι), LinearIndependent R v → v i ≠ 0
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- The Hausdorff dimension of any set in a finite-dimensional real normed space is finite.  -/
Real.dimH_lt_top : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Set E),
  dimH s < ⊤
-- Mathlib.Algebra.Ring.GeomSum
geom_sum₂_mul_of_le : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R]
  [ExistsAddOfLE R] [inst_5 : Sub R] [OrderedSub R] {x y : R},
  x ≤ y → ∀ (n : ℕ), (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- If `𝒰` is an open cover such that the images of the components form a basis of the topology
of `X`, `𝒰` is directed by the ordering of subset inclusion of the images.  -/
AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange : {X : AlgebraicGeometry.Scheme} →
  {𝒰 : X.OpenCover} →
    [inst : Preorder 𝒰.I₀] →
      (∀ {i j : 𝒰.I₀},
          i ≤ j ↔ AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i) ≤ AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f j)) →
        TopologicalSpace.Opens.IsBasis (Set.range fun i => AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i)) →
          AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.card_biUnion : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : DecidableEq M] {t : ι → Finset M},
  (↑s).PairwiseDisjoint t → (s.biUnion t).card = ∑ u ∈ s, (t u).card
-- Mathlib.Topology.Algebra.AsymptoticCone
/-- If a closed set `s` is star-convex at `p` and `v` is in the asymptotic cone of `s`, then the ray
of direction `v` starting from `p` is contained in `s`.  -/
StarConvex.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : TopologicalSpace k] [OrderTopology k] [inst_5 : AddCommGroup V] [inst_6 : Module k V]
  [inst_7 : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V} {c : k} {v p : V},
  StarConvex k p s → IsClosed s → 0 ≤ c → v ∈ asymptoticCone k s → c • v +ᵥ p ∈ s
-- Lean.Util.Recognizers
Lean.Expr.const? : Lean.Expr → Option (Lean.Name × List Lean.Level)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.ext_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y]
  {D₁ D₂ : Function.locallyFinsuppWithin U Y}, D₁ = D₂ ↔ ∀ (a : X), D₁ a = D₂ a
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The sequence `spectralValue_terms p` is bounded above.  -/
spectralValueTerms_bddAbove : ∀ {R : Type u_1} [inst : SeminormedRing R] (p : Polynomial R), BddAbove (Set.range (spectralValueTerms p))
-- Mathlib.Tactic.NormNum.Inv
/-- The `norm_num` extension which identifies an expression `NNRat.cast q` where `norm_num`
recognizes `q`, returning the cast of `q`.  -/
Mathlib.Meta.NormNum.evalNNRatCast : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_mul_product : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α},
  Finset.image (fun x => x.1 * x.2) (s ×ˢ t) = s * t
-- Lean.Message
/-- Atom quotes  -/
Lean.aquote : Lean.MessageData → Lean.MessageData
-- Mathlib.Tactic.Linter.TextBased
/-- Possible errors that text-based linters can report.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError : Type
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- See `SimpleGraph.adjMatrix_pow_apply_eq_card_walk` for the cardinality in terms of the `n`th
power of the adjacency matrix.  -/
SimpleGraph.card_set_walk_length_eq : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : G.LocallyFinite] (u v : V) (n : ℕ),
  Fintype.card ↑{p | p.length = n} = (G.finsetWalkLength n u v).card
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α], OrderDual.instCommMonoid = { toMonoid := OrderDual.instMonoid, mul_comm := ⋯ }
-- Mathlib.RingTheory.DedekindDomain.Basic
Ring.DimensionLEOne.integralClosure : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [Nontrivial R] [IsDomain A]
  [inst_4 : Algebra R A] [Ring.DimensionLEOne R], Ring.DimensionLEOne ↥(integralClosure R A)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instCStarRing : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : DenselyNormedField 𝕜] [inst_1 : StarRing 𝕜] [inst_2 : NonUnitalNormedRing A]
  [inst_3 : StarRing A] [inst_4 : CStarRing A] [inst_5 : NormedSpace 𝕜 A] [inst_6 : SMulCommClass 𝕜 A A]
  [inst_7 : IsScalarTower 𝕜 A A] [inst_8 : StarModule 𝕜 A], CStarRing (DoubleCentralizer 𝕜 A)
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- If `I` is a two-sided ideal of `R`, then `{op x | x ∈ I}` is a two-sided ideal in `Rᵐᵒᵖ`.  -/
TwoSidedIdeal.op : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → TwoSidedIdeal R → TwoSidedIdeal Rᵐᵒᵖ
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.support_map_of_injective : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (p : MvPolynomial σ R)
  {f : R →+* S₁}, Function.Injective ⇑f → ((MvPolynomial.map f) p).support = p.support