mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
/-- **Alias** of the forward direction of `MeasureTheory.integrable_piLp_iff`. -/
MeasureTheory.Integrable.eval_piLp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {ι : Type u_2} [inst_1 : Fintype ι] {E : ι → Type u_3} [inst_2 : (i : ι) → NormedAddCommGroup (E i)]
  {f : X → PiLp q E}, MeasureTheory.Integrable f μ → ∀ (i : ι), MeasureTheory.Integrable (fun x => (f x).ofLp i) μ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_bool : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : Bool → α),
  ∏' (i : Bool), f i = f false * f true
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_full_objs_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (D : Set C) {c : C},
  c ∈ (CategoryTheory.Subgroupoid.full D).objs ↔ c ∈ D
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The centroid lines in the affine span of the simplex's vertices.  -/
Affine.Simplex.centroid_mem_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [CharZero k] {n : ℕ} (s : Affine.Simplex k P n),
  s.centroid ∈ affineSpan k (Set.range s.points)
-- Mathlib.Algebra.Order.Ring.WithTop
/-- A version of `WithTop.map` for `RingHom`s.  -/
RingHom.withTopMap : {R : Type u_2} →
  {S : Type u_3} →
    [inst : NonAssocSemiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : CanonicallyOrderedAdd R] →
          [inst_3 : DecidableEq R] →
            [inst_4 : Nontrivial R] →
              [inst_5 : NonAssocSemiring S] →
                [inst_6 : PartialOrder S] →
                  [inst_7 : CanonicallyOrderedAdd S] →
                    [inst_8 : DecidableEq S] →
                      [inst_9 : Nontrivial S] → (f : R →+* S) → Function.Injective ⇑f → WithTop R →+* WithTop S
-- Aesop.RuleTac.Cases
_private.Aesop.RuleTac.Cases.0.Aesop.RuleTac.cases.findFirstApplicableHyp : Aesop.CasesTarget → Lean.Meta.TransparencyMode → Array Lean.FVarId → Lean.MVarId → Lean.MetaM (Option Lean.FVarId)
-- Plausible.DeriveShrinkable
/-- Creates the auxiliary shrink function definition for one inductive type.  -/
_private.Plausible.DeriveShrinkable.0.Plausible.mkAuxFunction : Lean.Elab.Deriving.Context → ℕ → Lean.Elab.TermElabM Lean.Command
-- Mathlib.Order.Monotone.Defs
Antitone.reflect_lt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ {a b : α}, f a < f b → b < a
-- Aesop.Tree.Data
Aesop.instBEqGoalState : BEq Aesop.GoalState
-- Mathlib.Order.Lattice
le_inf_iff : ∀ {α : Type u} [inst : SemilatticeInf α] {c a b : α}, c ≤ a ⊓ b ↔ c ≤ a ∧ c ≤ b
-- Mathlib.Algebra.Group.Subgroup.Map
/-- For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`.  -/
AddSubgroup.addSubgroupOf : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → (K : AddSubgroup G) → AddSubgroup ↥K
-- Lean.Setup
/-- Available during run time and compile time.  -/
Lean.IRPhases.all : Lean.IRPhases
-- Mathlib.Data.Num.Bitwise
/-- The predecessor of a `SNum` (i.e. the operation of removing one).  -/
SNum.pred : SNum → SNum
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_comp_le_range : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
  {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [inst_10 : RingHomSurjective τ₂₃]
  [inst_11 : RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃), (g ∘ₛₗ f).range ≤ g.range
-- Mathlib.Algebra.Ring.Defs
Ring.toSub : {R : Type u} → [self : Ring R] → Sub R
-- Init.Data.List.Sublist
List.singleton_suffix_iff_getLast?_eq_some : ∀ {α : Type u_1} {a : α} {l : List α}, [a] <:+ l ↔ l.getLast? = some a
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.factors.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a : α),
  UniqueFactorizationMonoid.factors a = if h : a = 0 then 0 else Classical.choose ⋯
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_op : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂),
  Φ.IsRightDerivabilityStructure ↔ Φ.op.IsLeftDerivabilityStructure
-- Init.Data.List.Lemmas
List.map_concat : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {l : List α}, List.map f (l.concat a) = (List.map f l).concat (f a)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_symm_toEquiv : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  ⇑e.toEquiv.symm = ⇑e.symm
-- Mathlib.Algebra.Lie.OfAssociative
LieRing.of_associative_ring_bracket : ∀ {A : Type v} [inst : Ring A] (x y : A), ⁅x, y⁆ = x * y - y * x
-- Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
CategoryTheory.MorphismProperty.HasCardinalLT.iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {P : ι → CategoryTheory.MorphismProperty C}
  {κ : Cardinal.{w}} [Fact κ.IsRegular],
  (∀ (i : ι), (P i).HasCardinalLT κ) → HasCardinalLT ι κ → (⨆ i, P i).HasCardinalLT κ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instRingCoeOfSubringClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Ring (R i)] →
              [∀ (i : ι), SubringClass (S i) (R i)] → Ring (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.tail : ∀ {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {le : α → α → Bool} {n : ℕ},
  Batteries.BinomialHeap.Imp.Heap.WF le n s →
    Batteries.BinomialHeap.Imp.Heap.WF le 0 (Batteries.BinomialHeap.Imp.Heap.tail le s)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_eq_iff : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α],
  s.Nonempty → ∀ (n : α), sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
/-- The `ℤ`-linear map induced by precomposition of the projection `C → π C (· ∈ s)`.  -/
Profinite.NobelingProof.πJ : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      (s : Finset I) → LocallyConstant ↑(Profinite.NobelingProof.π C fun x => x ∈ s) ℤ →ₗ[ℤ] LocallyConstant ↑C ℤ
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.inner_toEuclideanCLM : ∀ {n : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] (A : Matrix n n ℝ) (x y : EuclideanSpace ℝ n),
  inner ℝ x ((Matrix.toEuclideanCLM A) y) = x.ofLp ⬝ᵥ A.mulVec y.ofLp
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.instTensorProduct : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [Algebra.IsLocalIso R S], Algebra.IsLocalIso T (TensorProduct R T S)
-- Mathlib.GroupTheory.HNNExtension
/-- The `NormalWord` representing an element `g` of the group `G`, which is just the element `g`
itself.  -/
HNNExtension.NormalWord.ofGroup : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} → {d : HNNExtension.NormalWord.TransversalPair G A B} → G → HNNExtension.NormalWord d
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.sectionsMonoid : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J MonCat) → Monoid ↑(F.comp (CategoryTheory.forget MonCat)).sections
-- Mathlib.Algebra.Group.Basic
pow_sub_mul_pow : ∀ {M : Type u_4} [inst : Monoid M] {m n : ℕ} (a : M), m ≤ n → a ^ (n - m) * a ^ m = a ^ n
-- Aesop.Forward.State
/-- Add a hypothesis or pattern substitution to the queue for its slot.  -/
Aesop.ClusterState.enqueueRawHyp : Aesop.RawHyp → Aesop.PremiseIndex → Aesop.ClusterState → Aesop.ClusterState
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComonObjX_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X M.X.X))
      CategoryTheory.MonObj.mul.hom
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_I₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S], (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver S 𝒰 f).I₀ = 𝒰.I₀
-- Mathlib.Order.Hom.Bounded
TopHom.coe_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : SemilatticeInf β] [inst_2 : OrderTop β] (f g : TopHom α β),
  ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.instIsLeftKanExtensionProdFunctorTensorObjη : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (F G : CategoryTheory.MonoidalCategory.DayFunctor C V),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).functor.IsLeftKanExtension (F.η G)
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The GCD is normalized to itself.  -/
StrongNormalizedGCDMonoid.normalize_gcd : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : StrongNormalizedGCDMonoid α] (a b : α),
  normalize (gcd a b) = gcd a b
-- Mathlib.Topology.Constructions.SumProd
continuous_diag : ∀ {X : Type u} [inst : TopologicalSpace X], Continuous Function.diag
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ \ m₂).get? k = m₁.get? k
-- Std.Time.Date.Unit.Day
Std.Time.Day.instTransOrdOffset : Std.TransOrd Std.Time.Day.Offset
-- Mathlib.Algebra.Order.BigOperators.Group.List
/-- See also `List.le_prod_of_mem`.  -/
List.single_le_prod : ∀ {M : Type u_3} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : List M},
  (∀ x ∈ l, 1 ≤ x) → ∀ x ∈ l, x ≤ l.prod
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.restrict_presheaf_map : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (V W : (TopologicalSpace.Opens ↥(X.restrict h))ᵒᵖ) (i : V ⟶ W),
  (X.restrict h).presheaf.map i = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Algebra.Algebra.Unitization
Unitization.linearEquiv_apply : ∀ (S : Type u_2) (R : Type u_3) (A : Type u_4) [inst : Semiring S] [inst_1 : AddCommMonoid R] [inst_2 : AddCommMonoid A]
  [inst_3 : Module S R] [inst_4 : Module S A] (a : Unitization R A), (Unitization.linearEquiv S R A) a = a.toProd
-- Mathlib.GroupTheory.Perm.Support
/-- **Alias** of `Equiv.Perm.Disjoint.stdSymm`. -/
Equiv.Perm.Disjoint.symmetric : ∀ {α : Type u_1}, Std.Symm Equiv.Perm.Disjoint
-- Mathlib.Algebra.Star.Unitary
isStarNormal_of_mem_unitary : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {u : R}, u ∈ unitary R → IsStarNormal u
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.instEntailsPosFinArray : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.Entails (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
    (Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ_le : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α] {a b : α}, ↑a ≤ ↑b ↔ a ≤ b
-- Mathlib.Data.Nat.ModEq
Nat.modulus_modEq_zero : ∀ {n : ℕ}, n ≡ 0 [MOD n]
-- Init.Data.SInt.Lemmas
instLawfulCommIdentityISizeHMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.LawfulForwardPattern.startsWith_eq : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.ForwardPattern pat}
  [self : String.Slice.Pattern.LawfulForwardPattern pat] (s : String.Slice),
  String.Slice.Pattern.ForwardPattern.startsWith pat s = (String.Slice.Pattern.ForwardPattern.skipPrefix? pat s).isSome
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instSub : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → Sub (CauSeq β abv)
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.vId_iso_inv_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] (T : CategoryTheory.Functor C₁ C₂) (X : C₁),
  (CategoryTheory.CatCommSq.iso T (CategoryTheory.Functor.id C₁) (CategoryTheory.Functor.id C₂) T).inv.app X =
    CategoryTheory.CategoryStruct.id (T.obj X)
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.measure_compl_sigmaFiniteSetWRT : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → ∀ [MeasureTheory.SigmaFinite μ] [MeasureTheory.SFinite ν], ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft W)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso X₁ X₂).inv.right =
    (CategoryTheory.MonoidalCategoryStruct.associator W X₁.right X₂.right).hom
-- Mathlib.RingTheory.AdjoinRoot
/-- Two `R`-`AlgHom` from `AdjoinRoot f` to the same `R`-algebra are the same iff
they agree on `root f`.  -/
AdjoinRoot.algHom_ext : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {f : Polynomial R} [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {g₁ g₂ : AdjoinRoot f →ₐ[R] S}, g₁ (AdjoinRoot.root f) = g₂ (AdjoinRoot.root f) → g₁ = g₂
-- Mathlib.Data.Bool.Count
List.IsChain.two_mul_count_bool_of_even : ∀ {l : List Bool}, List.IsChain (fun x1 x2 => x1 ≠ x2) l → Even l.length → ∀ (b : Bool), 2 * List.count b l = l.length
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go.induct_unfolding : ∀ (pat : ByteArray) (stackPos : ℕ) (hst : stackPos < pat.size) (motive : ℕ → ℕ → Prop),
  (∀ (x : ℕ), String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat x (stackPos + 1) → motive x x) →
    (∀ (x : ℕ),
        ¬String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat x (stackPos + 1) →
          x ≠ 0 →
            motive (x - 1)
                (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go✝ pat stackPos hst (x - 1)) →
              motive x (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go✝ pat stackPos hst (x - 1))) →
      ∀ (k : ℕ), motive k (String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go✝ pat stackPos hst k)
-- Mathlib.Order.WellFoundedSet
Set.isWF_min_singleton : ∀ {α : Type u_2} [inst : Preorder α] (a : α) {hs : {a}.IsWF} {hn : {a}.Nonempty}, hs.min hn = a
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_neg_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] (d : ℤ), selfZPow x B (-d) * selfZPow x B d = 1
-- Init.Data.Vector.Lemmas
Vector.map_eq_push_iff : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α (n + 1)} {ys : Vector β n} {b : β},
  Vector.map f xs = ys.push b ↔ ∃ xs' a, xs = xs'.push a ∧ Vector.map f xs' = ys ∧ f a = b
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.comp_apply : ∀ {X Y Z : FinPartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toPartOrd),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Std.Time.Format.Modifier
/-- 12:00–18:00
 -/
Std.Time.ExtendedDayPeriod.afternoon : Std.Time.ExtendedDayPeriod
-- Mathlib.Order.SuccPred.Archimedean
/-- `IsPredArchimedean` transfers across equivalences between `PredOrder`s.  -/
IsPredArchimedean.of_orderIso : ∀ {X : Type u_3} {Y : Type u_4} [inst : PartialOrder X] [inst_1 : PartialOrder Y] [inst_2 : PredOrder X]
  [IsPredArchimedean X] [inst_4 : PredOrder Y] (f : X ≃o Y), IsPredArchimedean Y
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisionAt.degree_lt : ∀ {A : Type u_1} [inst : CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A},
  f.IsWeierstrassDivisionAt g q r I → r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRight_obj_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRight L r).obj X).right = X.right
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_insertListₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {l : List ((a : α) × β a)},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(m.insertListₘ l)).buckets).Perm
      (Std.Internal.List.insertList (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
-- Mathlib.Data.Finset.NoncommProd
/-- Fold of a `s : Multiset α` with `f : α → β → β`, given a proof that `LeftCommutative f`
on all elements `x ∈ s`.  -/
Multiset.noncommFoldr : {α : Type u_3} →
  {β : Type u_4} →
    (f : α → β → β) → (s : Multiset α) → ({x | x ∈ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)) → β → β
-- Init.Data.Int.OfNat
Int.Nonneg.natCast : ∀ (a : ℕ), ↑a ≥ 0
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- `ContMDiffWithinAt I I' n f x` indicates that the function `f : M → M'` between manifolds
is `n` times continuously differentiable at `x : M` within the set `s`.

`f` is `n` times continuously differentiable within `s` at `x` if it is continuous and it is `n`
times continuously differentiable in this set around `x`, when read in the preferred chart at `x`.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions.  -/
ContMDiffWithinAt : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                ModelWithCorners 𝕜 E' H' →
                                  {M' : Type u_7} →
                                    [inst : TopologicalSpace M'] →
                                      [ChartedSpace H' M'] → WithTop ℕ∞ → (M → M') → Set M → M → Prop
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_triangle4 : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z w : α), dist x w ≤ dist x y + dist y z + dist z w
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_3 : ∀ (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.read q) = Turing.TM2.Stmt.goto q
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
intEquivOfZPowersEqTop.eq_1 : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : Group G] (g : G) (hg : Subgroup.zpowers g = ⊤),
  intEquivOfZPowersEqTop g hg = MulEquiv.ofBijective ((zpowersHom G) g) ⋯
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_mul_descFactorial : ∀ {k m n : ℕ}, k ≤ m → (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m