mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- Composition of two `ContinuousAffineEquiv`alences, applied left to right.  -/
ContinuousAffineEquiv.trans : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {P₃ : Type u_4} →
        {V₁ : Type u_6} →
          {V₂ : Type u_7} →
            {V₃ : Type u_8} →
              [inst : Ring k] →
                [inst_1 : AddCommGroup V₁] →
                  [inst_2 : Module k V₁] →
                    [inst_3 : AddTorsor V₁ P₁] →
                      [inst_4 : TopologicalSpace P₁] →
                        [inst_5 : AddCommGroup V₂] →
                          [inst_6 : Module k V₂] →
                            [inst_7 : AddTorsor V₂ P₂] →
                              [inst_8 : TopologicalSpace P₂] →
                                [inst_9 : AddCommGroup V₃] →
                                  [inst_10 : Module k V₃] →
                                    [inst_11 : AddTorsor V₃ P₃] →
                                      [inst_12 : TopologicalSpace P₃] → (P₁ ≃ᴬ[k] P₂) → (P₂ ≃ᴬ[k] P₃) → P₁ ≃ᴬ[k] P₃
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.Config.mk : Lean.Meta.TransparencyMode → Bool → Bool → Mathlib.Tactic.AtomM.Recurse.Config
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_sdiff_Ico_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a ≤ b → Finset.Icc a b \ Finset.Ico a b = {b}
-- Mathlib.Data.Num.Lemmas
PosNum.cast_inj : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [CharZero α] {m n : PosNum}, ↑m = ↑n ↔ m = n
-- Mathlib.Data.Finset.Image
Finset.image_sdiff : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] {f : α → β} (s t : Finset α),
  Function.Injective f → Finset.image f (s \ t) = Finset.image f s \ Finset.image f t
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, (t₁ ∩ t₂).getKeyD k fallback = if k ∈ t₂ then t₁.getKeyD k fallback else fallback
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- **Alias** of `Hypergraph.subset_vertexSet_of_mem_edgeSet`. -/
Membership.mem.subset_vertexSet : ∀ {α : Type u_1} {e : Set α} {H : Hypergraph α}, e ∈ H.edgeSet → e ⊆ H.vertexSet
-- Std.Http.Protocol.H1.Parser
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseMethod : Std.Internal.Parsec.ByteArray.Parser Std.Http.Method
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.SeparatingRight.congr : ∀ {R : Type u_1} {M : Type u_5} {Mₗ₁ : Type u_9} {Mₗ₁' : Type u_10} {Mₗ₂ : Type u_11} {Mₗ₂' : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid Mₗ₁]
  [inst_4 : AddCommMonoid Mₗ₂] [inst_5 : AddCommMonoid Mₗ₁'] [inst_6 : AddCommMonoid Mₗ₂'] [inst_7 : Module R Mₗ₁]
  [inst_8 : Module R Mₗ₂] [inst_9 : Module R Mₗ₁'] [inst_10 : Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M}
  (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'),
  B.SeparatingRight → ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingRight
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Insert the entries `maps` into the pre-discrimination trees `pres`.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.PreDiscrTrees.append : Mathlib.Tactic.ClickSuggestions.PreDiscrTrees →
  Mathlib.Tactic.ClickSuggestions.Entries✝ → Mathlib.Tactic.ClickSuggestions.PreDiscrTrees
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.extendScalars_ε : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  CategoryTheory.Functor.LaxMonoidal.ε (ModuleCat.extendScalars f) =
    ModuleCat.ofHom ↑(TensorProduct.AlgebraTensorModule.rid R S S).symm
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.smulRight_apply : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] [inst_5 : Semiring S] [inst_6 : Module R S]
  [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M) (c : M₁), (f.smulRight x) c = f c • x
-- Mathlib.Order.Filter.Extr
isMinOn_univ_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {a : α}, IsMinOn f Set.univ a ↔ ∀ (x : α), f a ≤ f x
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
/-- This says that `p` has `natDegree` `n` and is monic.  -/
Polynomial.IsMonicOfDegree : {R : Type u_1} → [inst : Semiring R] → Polynomial R → ℕ → Prop
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Monotone.const_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} [MulLeftMono α],
  Monotone f → ∀ (a : α), Monotone fun x => a * f x
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.mkOrderEmbedding.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α} (b : ↥s),
  AddLocalization.mkOrderEmbedding b = { toFun := fun a => AddLocalization.mk a b, inj' := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Probability.Distributions.Uniform
/-- A real uniform random variable `X` with support `s` has expectation
`(λ s)⁻¹ * ∫ x in s, x ∂λ` where `λ` is the Lebesgue measure.  -/
MeasureTheory.pdf.IsUniform.integral_eq : ∀ {Ω : Type u_2} {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {s : Set ℝ},
  MeasureTheory.pdf.IsUniform X s ℙ MeasureTheory.volume →
    ∫ (x : Ω), X x ∂ℙ = (MeasureTheory.volume s)⁻¹.toReal * ∫ (x : ℝ) in s, x
-- Lean.ImportingFlag
/-- Toggle the "importing" flag.

This is intended for C code that needs to emulate multiple `withImporting` calls.
As with `withImporting`, users must make sure there is only one execution thread accessing
the global references.
 -/
_private.Lean.ImportingFlag.0.Lean.setInitializing : Bool → BaseIO Unit
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_add_erase : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ),
  (Polynomial.monomial n) (p.coeff n) + Polynomial.erase n p = p
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.inv_mul_eq_one : ∀ {α : Type u} [inst : DivisionMonoid α] {a b : α}, IsUnit a → (a⁻¹ * b = 1 ↔ a = b)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.mk.injEq : ∀ {M : Type u_1} [inst : Add M] (toSetoid : Setoid M)
  (add' : ∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w + y) (x + z)) (toSetoid_1 : Setoid M)
  (add'_1 : ∀ {w x y z : M}, toSetoid_1 w x → toSetoid_1 y z → toSetoid_1 (w + y) (x + z)),
  ({ toSetoid := toSetoid, add' := add' } = { toSetoid := toSetoid_1, add' := add'_1 }) = (toSetoid = toSetoid_1)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_smul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (x : Submonoid A)
  {α : Type u_4} [inst_2 : SMul α A] [inst_3 : IsScalarTower α A A] [inst_4 : SMulMemClass σ α A]
  (i : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (m : α),
  HomogeneousLocalization.mk (m • i) = m • HomogeneousLocalization.mk i
-- Batteries.Data.Fin.Coding
Fin.decodeBool_encodeBool : ∀ (x : Bool), Fin.decodeBool (Fin.encodeBool x) = x
-- Init.Data.String.Lemmas.Splits
String.splits_nextn_startPos : ∀ (s : String) (n : ℕ),
  (s.startPos.nextn n).Splits (String.ofList (List.take n s.toList)) (String.ofList (List.drop n s.toList))
-- Aesop.Tree.Data
Aesop.Rapp.setAssignedMVars : Aesop.UnorderedArraySet Lean.MVarId → Aesop.Rapp → Aesop.Rapp
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_closure : ∀ {M : Type u_2} [inst : Mul M] (s : Set M), (Subsemigroup.closure s).op = Subsemigroup.closure (MulOpposite.unop ⁻¹' s)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.baseChange_symm : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] (e : M ≃ₗ[R] N), LinearEquiv.baseChange R A N M e.symm = (LinearEquiv.baseChange R A M N e).symm
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.mulConst_NonnegCoeffs : ∀ {p : Lean.Grind.CommRing.Poly} {k : ℤ}, k ≥ 0 → p.NonnegCoeffs → (Lean.Grind.CommRing.Poly.mulConst k p).NonnegCoeffs
-- Lean.Expr
Lean.Expr.rawNatLit? : Lean.Expr → Option ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.isPushout : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  CategoryTheory.IsPushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight S.ι T.toSSet)
    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft S.toSSet T.ι) (SSet.Subcomplex.unionProd.ι₁ S T)
    (SSet.Subcomplex.unionProd.ι₂ S T)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.dist_toLp_fst : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x₁ x₂ : α), dist (WithLp.toLp p (x₁, 0)) (WithLp.toLp p (x₂, 0)) = dist x₁ x₂
-- Mathlib.Topology.Homotopy.Lifting
/-- Lift a homotopy class of paths to a covering space.  -/
IsCoveringMap.liftPathQuotient : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} →
          (cov : IsCoveringMap p) →
            {x y : X} →
              (γ : Path.Homotopic.Quotient x y) → (e : ↑(p ⁻¹' {x})) → Path.Homotopic.Quotient ↑e ↑(cov.monodromy γ e)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.sub_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Sub β]
  [inst_3 : ContinuousSub β] (f g : C(α, β)) (x : α), (f - g) x = f x - g x
-- Mathlib.Tactic.Simps.Basic
_private.Mathlib.Tactic.Simps.Basic.0.Simps.findAutomaticProjectionsAux.unsafe_impl_2 : Lean.Name → Lean.Elab.TermElabM Simps.findArgType
-- Batteries.Data.List.Lemmas
List.idxOfNth_eq_idxOfNth_iff_of_left_lt_count : ∀ {α : Type u_1} {n : ℕ} {x : α} {m : ℕ} [inst : BEq α] {xs : List α},
  n < List.count x xs → (List.idxOfNth x xs n = List.idxOfNth x xs m ↔ n = m)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_multiset_map_count : ∀ {ι : Type u_1} [inst : DecidableEq ι] (s : Multiset ι) {M : Type u_5} [inst_1 : AddCommMonoid M] (f : ι → M),
  (Multiset.map f s).sum = ∑ m ∈ s.toFinset, Multiset.count m s • f m
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.findIdx.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n),
  (match [], n with
    | [], n => h_1 n
    | a :: l, n => h_2 a l n) =
    h_1 n
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`.  -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              CategoryTheory.Functor.id (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) ≅
                (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).comp
                  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
/-- If `f` and `g` have derivatives `df` and `dg` within `s` at `x`, respectively,
then `x ↦ (f x, g x)` has derivative `df.prod dg` within `s`.  -/
HasMFDerivWithinAt.prodMk : ∀ {𝕜 : 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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {s : Set M} {x : M} {f : M → M'} {g : M → M''} {df : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  HasMFDerivAt[s] f x df →
    ∀ {dg : TangentSpace I x →L[𝕜] TangentSpace I'' (g x)},
      HasMFDerivAt[s] g x dg → HasMFDerivAt[s] (fun y => (f y, g y)) x (df.prod dg)
-- Init.Prelude
Nat.pow_pos : ∀ {a n : ℕ}, 0 < a → 0 < a ^ n
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- An unbounded operator is closed iff its graph is closed.  -/
LinearPMap.IsClosed : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] → [TopologicalSpace E] → [TopologicalSpace F] → (E →ₗ.[R] F) → Prop
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.enorm_fst_le : ∀ {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : WithLp p (α × β)), ‖x.fst‖ₑ ≤ ‖x‖ₑ
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_two_neg : Real.cos 2 < 0
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.right_unitor.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  sizeOf (CategoryTheory.FreeBicategory.Hom₂.right_unitor f) = 1 + sizeOf a + sizeOf b + sizeOf f
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.iUnion_image_mk_rightRel : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  ⋃ q, Quot.mk ⇑(QuotientGroup.rightRel H) '' DoubleCoset.doubleCoset (Quotient.out q) ↑H ↑K = Set.univ
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.coe_inf : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α] (s t : ClopenUpperSet α), ↑(s ⊓ t) = ↑s ∩ ↑t
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.positionsFrom.eq_1 : ∀ (s : String) (p : s.Pos),
  s.positionsFrom p = Std.Iter.map String.Internal.ofToSliceWithProof (String.Slice.positionsFrom p.toSlice)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.comp_id : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y), CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Ordered.zoom : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t' : RBTree.RBNode α} {path' : RBTree.RBNode.Path α}
  {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t →
    RBTree.RBNode.zoom cut t = (t', path') →
      RBTree.RBNode.Ordered cmp t' ∧
        RBTree.RBNode.Path.Ordered cmp path' ∧
          RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp path') t' ∧ RBTree.RBNode.Path.Zoomed cut path'
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.instLawfulOperatorBinaryInputMkXorCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkXorCached
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.dist_smul_Lp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f g : ↥(MeasureTheory.Lp E p μ)), dist (c • f) (c • g) = dist f g
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.coe_topologicalClosure_bot : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G],
  ↑⊥.topologicalClosure = closure {1}
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
/-- `ZMod.toCircle` as an `AddChar` into `rootsOfUnity n Circle`.  -/
ZMod.rootsOfUnityAddChar : (n : ℕ) → [NeZero n] → AddChar (ZMod n) ↥(rootsOfUnity n Circle)
-- Mathlib.Probability.StrongLaw
/-- Truncating a real-valued function to the interval `(-A, A]`.  -/
ProbabilityTheory.truncation : {α : Type u_1} → (α → ℝ) → ℝ → α → ℝ
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.domainUniqueUpToIso_inv_isHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R R' S : 𝒮} {a a' b : 𝒳} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R}
  (h : f' = CategoryTheory.CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  [inst_3 : p.IsStronglyCartesian f' φ'],
  p.IsHomLift g.hom (CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p h φ φ').hom
-- Lean.Meta.DiscrTree.Main
/-- Reduction procedure for the discrimination tree indexing.
 -/
Lean.Meta.DiscrTree.reduce : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.LawfulHashable
/-- A lawful hash function respects its Boolean equality test.
 -/
hash_eq : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α] {a b : α}, (a == b) = true → hash a = hash b
-- Mathlib.FieldTheory.Perfect
frobeniusEquiv_apply : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (a : R),
  (frobeniusEquiv R p) a = (frobenius R p) a
-- Init.Data.Slice.Array.Lemmas
Array.toArray_mkSlice_rcc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = xs.extract lo (hi + 1)
-- Mathlib.Order.Basic
/-- **Alias** of `le_trans`. -/
LE.le.trans : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.default_consistent : ∀ (F : PFunctor.{uA, uB}) [inst : Inhabited F.A] (n : ℕ), PFunctor.Approx.Agree default default
-- Mathlib.Data.Set.Restrict
Set.domRestrict_piecewise_compl : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [inst : (x : α) → Decidable (x ∈ s)],
  sᶜ.domRestrict (s.piecewise f g) = sᶜ.domRestrict g
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback_fst_map_snd_isPullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂],
  CategoryTheory.IsPullback
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂)
      (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)))
    (CategoryTheory.Limits.pullback.map i₁ i₂
      (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
      (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))
      (CategoryTheory.CategoryStruct.id V₁) (CategoryTheory.CategoryStruct.id V₂)
      (CategoryTheory.Limits.pullback.snd f i) ⋯ ⋯)
    (CategoryTheory.Limits.pullback.diagonal f)
    (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
      (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
      (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
      (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.mu_property : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) {x y : R}
  (hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)) (n : ℕ),
  μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ mu✝ μ hn n) * μ (y ^ (n - mu✝ μ hn n))) ^ (1 / ↑n)
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cone on `F : J ⥤ Cᵒᵖ` to a cocone on `F.leftOp : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.coconeLeftOpOfCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J Cᵒᵖ} → CategoryTheory.Limits.Cone F → CategoryTheory.Limits.Cocone F.leftOp
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.restrictionToTruncGE'_naturality_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i'] {Z : HomologicalComplex C c}
  (h : L.truncGE' e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.restrictionToTruncGE' e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'Map φ e) h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap φ e)
      (CategoryTheory.CategoryStruct.comp (L.restrictionToTruncGE' e) h)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Replacing a set by its closure does not change the Hausdorff edistance.  -/
Metric.hausdorffEDist_closure_left : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Metric.hausdorffEDist (closure s) t = Metric.hausdorffEDist s t
-- Init.Data.Int.Bitwise.Basic
Int.instHShiftRightNat : HShiftRight ℤ ℕ ℤ
-- Mathlib.Analysis.BoundedVariation
/-- A real function into a finite-dimensional real vector space with bounded variation on a set
is differentiable almost everywhere in this set.  -/
LocallyBoundedVariationOn.ae_differentiableWithinAt : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {f : ℝ → V}
  {s : Set ℝ},
  LocallyBoundedVariationOn f s →
    MeasurableSet s → ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt ℝ f s x
-- Mathlib.MeasureTheory.Function.Holder
/-- `MeasureTheory.Lp.holder` as a bilinear map.  -/
ContinuousLinearMap.holderₗ : {α : Type u_1} →
  {𝕜 : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        {G : Type u_5} →
          {m : MeasurableSpace α} →
            (μ : MeasureTheory.Measure α) →
              (p q r : ENNReal) →
                [hpqr : p.HolderTriple q r] →
                  [inst : NontriviallyNormedField 𝕜] →
                    [inst_1 : NormedAddCommGroup E] →
                      [inst_2 : NormedAddCommGroup F] →
                        [inst_3 : NormedAddCommGroup G] →
                          [inst_4 : NormedSpace 𝕜 E] →
                            [inst_5 : NormedSpace 𝕜 F] →
                              [inst_6 : NormedSpace 𝕜 G] →
                                (E →L[𝕜] F →L[𝕜] G) →
                                  ↥(MeasureTheory.Lp E p μ) →ₗ[𝕜]
                                    ↥(MeasureTheory.Lp F q μ) →ₗ[𝕜] ↥(MeasureTheory.Lp G r μ)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} [inst_1 : SizeOf C] (Y : C) (f : Y ⟶ X) (hf : (↑S).arrows f),
  sizeOf { Y := Y, f := f, hf := hf } = 1 + sizeOf Y + sizeOf f + sizeOf hf
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.FaithfullyFlat.flat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.FaithfullyFlat → f.Flat
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.dualPairing_separatingLeft : ∀ (R : Type u_4) (M : Type u_5) [inst : SeminormedCommRing R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M], (topDualPairing R M).SeparatingLeft