mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} [inst_1 : SizeOf C]
  (toJointlyMono₂ : CategoryTheory.JointlyMono₂ p₁ p₂) (s : R ⟶ R)
  (symmetry₁ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₁ = p₂) CategoryTheory.SymmetricRelation.symmetry₁._autoParam)
  (symmetry₂ :
    autoParam (CategoryTheory.CategoryStruct.comp s p₂ = p₁) CategoryTheory.SymmetricRelation.symmetry₂._autoParam),
  sizeOf { toJointlyMono₂ := toJointlyMono₂, s := s, symmetry₁ := symmetry₁, symmetry₂ := symmetry₂ } =
    1 + sizeOf toJointlyMono₂ + sizeOf s + sizeOf symmetry₁ + sizeOf symmetry₂
-- Init.Data.Iterators.Basic
Std.Iterators.FinitenessRelation.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        (Rel : Std.IterM m β → Std.IterM m β → Prop) →
          WellFounded Rel →
            (∀ {it it' : Std.IterM m β}, it'.IsPlausibleSuccessorOf it → Rel it' it) →
              Std.Iterators.FinitenessRelation α m
-- Mathlib.Data.PNat.Xgcd
/-- Final value of `y`  -/
PNat.gcdY : ℕ+ → ℕ+ → ℕ
-- Mathlib.Algebra.Star.Pi
Pi.single_star : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → AddMonoid (f i)] [inst_1 : (i : I) → StarAddMonoid (f i)]
  [inst_2 : DecidableEq I] (i : I) (a : f i), Pi.single i (star a) = star (Pi.single i a)
-- Mathlib.Tactic.IntervalCases
/-- Assuming `Bound` represents a lower bound, this returns the (inclusive)
least integer value which is allowed. So `3 ≤ e` means the lower bound is 3 and
`3 < e` means the lower bound is `4`.
 -/
Mathlib.Tactic.IntervalCases.Bound.asLower : Mathlib.Tactic.IntervalCases.Bound → ℤ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_pow : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Monoid (G i)] [inst_3 : ∀ (i : ι), SubmonoidClass (S i) (G i)] (i : ι)
  (r : G i) (n : ℕ), RestrictedProduct.mulSingle A i (r ^ n) = RestrictedProduct.mulSingle A i r ^ n
-- Init.Data.Subtype.Order
Subtype.instReflLE : ∀ {α : Type u} [inst : LE α] [i : Std.Refl fun x1 x2 => x1 ≤ x2] {P : α → Prop}, Std.Refl fun x1 x2 => x1 ≤ x2
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.node' : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α}, l.Sized → r.Sized → (l.node' x r).Sized
-- Mathlib.RingTheory.RingHom.OpenImmersion
/-- The composition of two standard open immersions is a standard open immersion.  -/
RingHom.IsStandardOpenImmersion.comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T},
  f.IsStandardOpenImmersion → g.IsStandardOpenImmersion → (g.comp f).IsStandardOpenImmersion
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.topologicalClosure_coe : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G] {s : AddSubgroup G},
  ↑s.topologicalClosure = closure ↑s
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_whisker_right : ∀ {B : Type u} [inst : Quiver B] {a b c : CategoryTheory.FreeBicategory B} {f g : a ⟶ b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g) (h : b ⟶ c),
  (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η).mk = CategoryTheory.Bicategory.whiskerRight η.mk h
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₄_of_isCharTwoJEqZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF], W.b₄ = 2 * W.a₄
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.congr_refl : ∀ (p : ENNReal) {V : Type u_4}, WithLp.congr p (Equiv.refl V) = Equiv.refl (WithLp p V)
-- Mathlib.Data.Fin.Embedding
/-- `Fin.succAbove p` as an `Embedding`.  -/
Fin.succAboveEmb : {n : ℕ} → Fin (n + 1) → Fin n ↪ Fin (n + 1)
-- Mathlib.Order.Category.BddOrd
BddOrd.instConcreteCategoryBoundedOrderHomCarrier : CategoryTheory.ConcreteCategory BddOrd fun x1 x2 => BoundedOrderHom ↑x1.toPartOrd ↑x2.toPartOrd
-- Lean.Parser.Term
Lean.Parser.Term.negConfigItem.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.LinearTopology
isLinearTopology_iff_hasBasis_twoSidedIdeal : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R],
  IsLinearTopology R R ∧ IsLinearTopology Rᵐᵒᵖ R ↔ (nhds 0).HasBasis (fun I => ↑I ∈ nhds 0) fun I => ↑I
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableOn.dist : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f g : G → E}
  {s : Set G},
  DifferentiableOn ℝ f s →
    DifferentiableOn ℝ g s → (∀ x ∈ s, f x ≠ g x) → DifferentiableOn ℝ (fun y => dist (f y) (g y)) s
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.subgroup_quotient_eq_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Subgroup G}
  {x : MulAction.orbitRel.Quotient G α} {a b : ↑x.orbit}, ⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧
-- Batteries.Data.PairingHeap
/-- Amortized `O(log n)`. Removes the smallest element from the heap, if possible.  -/
Batteries.PairingHeap.tail : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → Batteries.PairingHeap α le
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- **Legendre's Theorem**

Taking (`p - 1`) times the `p`-adic valuation of `n!` equals `n` minus the sum of base `p` digits
of `n`.  -/
sub_one_mul_padicValNat_factorial : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ), (p - 1) * padicValNat p n.factorial = n - (p.digits n).sum
-- Mathlib.Data.Finset.Update
Function.updateFinset.congr_simp : ∀ {ι : Type u_1} {π : ι → Sort u_2} {inst : DecidableEq ι} [inst_1 : DecidableEq ι] (x x_1 : (i : ι) → π i),
  x = x_1 →
    ∀ (s : Finset ι) (y y_1 : (i : ↥s) → π ↑i),
      y = y_1 → ∀ (i : ι), Function.updateFinset x s y i = Function.updateFinset x_1 s y_1 i
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.erase.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.erase a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => Std.DHashMap.Internal.AssocList.nil
    | Std.DHashMap.Internal.AssocList.cons k v l =>
      bif k == a then l else Std.DHashMap.Internal.AssocList.cons k v (Std.DHashMap.Internal.AssocList.erase a l)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getEntry_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α}
  {h : Std.DHashMap.Internal.AssocList.contains a l = true},
  Std.DHashMap.Internal.AssocList.getEntry a l h = Std.Internal.List.getEntry a l.toList ⋯
-- Aesop.Tree.Free
Aesop.freeTree : Aesop.TreeM Unit
-- Batteries.Recycling.MonadSatisfying.List
List.satisfiesM_foldlM : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {motive : β → Prop} {l : List α} {b : β} [inst : Monad m]
  [LawfulMonad m] {f : β → α → m β},
  motive b → (∀ (b : β), motive b → ∀ a ∈ l, SatisfiesM motive (f b a)) → SatisfiesM motive (List.foldlM f b l)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' fallback : α}, (k == k') = true → m.getKeyD k fallback = m.getKeyD k' fallback
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instInhabited.eq_1 : AddCommMonCat.instInhabited = { default := AddCommMonCat.of PUnit.{u_1 + 1} }
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
CompHausLike.isoOfBijective.congr_simp : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  (bij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)),
  CompHausLike.isoOfBijective f bij = CompHausLike.isoOfBijective f_1 ⋯
-- Lean.Setup
Lean.ModuleHeader.mk.sizeOf_spec : ∀ (imports : Array Lean.Import) (isModule : Bool),
  sizeOf { imports := imports, isModule := isModule } = 1 + sizeOf imports + sizeOf isModule
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.isLocalization_iff_of_algEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : Algebra R P] (h : S ≃ₐ[R] P),
  IsLocalization M S ↔ IsLocalization M P
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (α : CategoryTheory.Arrow.mk sq₁₂.ι ⟶ CategoryTheory.Arrow.mk f₃) {Z : C₂} (h : (G.obj (Opposite.op X₁)).obj X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α))
      (CategoryTheory.CategoryStruct.comp sq₁₃.fst h) =
    CategoryTheory.CategoryStruct.comp
      (adj₂.homEquiv (CategoryTheory.CategoryStruct.comp sq₁₂.inr (CategoryTheory.Arrow.Hom.left α))) h
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- `Ω^M (Ω^N X) ≃ₜ Ω^(M ⊕ N) X`.  -/
GenLoop.genLoopGenLoopEquiv : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {M : Type u_3} → (x : X) → ↑(GenLoop M (↑(GenLoop N X x)) GenLoop.const) ≃ₜ ↑(GenLoop (M ⊕ N) X x)
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
Differentiable.restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → F},
  Differentiable 𝕜' f → Differentiable 𝕜 f
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {T : CategoryTheory.Over A} {X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A}
  (f : CategoryTheory.yoneda.obj X ⟶ (CategoryTheory.overEquivPresheafCostructuredArrow A).functor.obj T),
  (CategoryTheory.overEquivPresheafCostructuredArrow A).functor.map
      ((CategoryTheory.ConcreteCategory.hom
          ((CategoryTheory.CostructuredArrow.toOverCompYoneda A T).inv.app (Opposite.op X)))
        f) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).hom.app X) f
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.smul : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] →
      [inst_1 : SeminormedAddCommGroup V₂] →
        {R : Type u_5} →
          [inst_2 : MonoidWithZero R] →
            [inst_3 : DistribMulAction R V₂] →
              [inst_4 : PseudoMetricSpace R] → [IsBoundedSMul R V₂] → SMul R (NormedAddGroupHom V₁ V₂)
-- Lean.Elab.InfoTree.Types
/-- Assignments fulfilled by other elaboration tasks. We substitute them only just before reporting
the info tree via a snapshot to avoid premature blocking.
 -/
Lean.Elab.InfoState.lazyAssignment : Lean.Elab.InfoState → Lean.PersistentHashMap Lean.MVarId (Task Lean.Elab.InfoTree)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l l_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_2 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l_1 = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r))
                          h)
  (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β)
  (x_2 : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false),
  x = Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf →
    x_1 ≍ x_2 →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
        | Std.DTreeMap.Internal.Impl.inner size k v l l_1@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r),
          h_3 => h_2 size k v l l_1 size_1 k_1 v_1 l_2 r h h_3) ≍
        h_1 size k v l x_2
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.trunc'_expand_trunc' : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ),
  p ≠ 0 →
    ∀ {n m : σ →₀ ℕ},
      n ≤ m →
        ∀ [inst_1 : DecidableEq σ] (f : MvPowerSeries σ R),
          (MvPolynomial.expand p) ((MvPowerSeries.trunc' R n) f) =
            (MvPowerSeries.trunc' R (p • n)) ↑((MvPolynomial.expand p) ((MvPowerSeries.trunc' R m) f))
-- Mathlib.Data.Finset.Sum
Finset.card_disjSum : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β), (s.disjSum t).card = s.card + t.card
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.readResponseAs : IO.FS.Stream → ℕ → Lean.JsonRpc.RequestID → (α : Type) → [Lean.FromJson α] → IO (Lean.JsonRpc.Response α)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.inter_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α}, m₁.inter m₂ = m₁ ∩ m₂
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_natCast_eq_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ}, ‖↑n‖ = 1 ↔ p.Coprime n
-- Init.Data.UInt.Lemmas
UInt64.sub_def : ∀ (a b : UInt64), a - b = { toBitVec := a.toBitVec - b.toBitVec }
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The pullback of `f` and `g` in `Cᵒᵖ` is isomorphic to the pushout of
`f.unop` and `g.unop` in `C`.  -/
CategoryTheory.Limits.pullbackIsoOpPushout : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [h : CategoryTheory.Limits.HasPullback f g] →
            CategoryTheory.Limits.pullback f g ≅ Opposite.op (CategoryTheory.Limits.pushout f.unop g.unop)
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.atIdxSlow?_eq_match.match_3.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of `Order.not_isSuccPrelimit_of_isSuccArchimedean`. -/
Order.not_isSuccPrelimit : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] [NoMinOrder α],
  ¬Order.IsSuccPrelimit a
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isDefEqBindingS.go : Lean.LocalContext →
  Lean.LocalInstances → Array Lean.Expr → Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.compMeasurePreserving_iterate : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → α} (hf : MeasureTheory.MeasurePreserving f μ μ) (n : ℕ),
  (⇑(MeasureTheory.Lp.compMeasurePreserving f hf))^[n] = ⇑(MeasureTheory.Lp.compMeasurePreserving f^[n] ⋯)
-- Mathlib.Data.Set.Pairwise.Basic
Set.Pairwise.mono' : ∀ {α : Type u_1} {r p : α → α → Prop} {s : Set α}, r ≤ p → s.Pairwise r → s.Pairwise p
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.instAddCommMonoid : (ι : Type u_1) → (β : ι → Type u_2) → [inst : (i : ι) → AddCommMonoid (β i)] → AddCommMonoid (DirectSum ι β)
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The ball of radius zero is empty.  -/
SimpleGraph.ball_zero : ∀ {V : Type u_1} {G : SimpleGraph V} {c : V}, G.ball c 0 = ∅
-- Mathlib.Data.Set.Finite.Range
Set.finite_range : ∀ {α : Type u} {ι : Sort w} (f : ι → α) [Finite ι], (Set.range f).Finite
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- The adjunction `reflector i ⊣ i` when `i` is reflective.  -/
CategoryTheory.reflectorAdjunction : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (i : CategoryTheory.Functor D C) → [inst_2 : CategoryTheory.Reflective i] → CategoryTheory.reflector i ⊣ i
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subtractionMonoid.eq_1 : ∀ {α : Type u_2} [inst : SubtractionMonoid α],
  Set.subtractionMonoid =
    { toAddMonoid := Set.addMonoid, toNeg := Set.involutiveNeg.toNeg, toSub := Set.sub, toZSMul := ZSMul.ofSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_neg := ⋯, neg_add_rev := ⋯,
      neg_eq_of_add := ⋯ }
-- Mathlib.Topology.ContinuousMap.ContinuousSqrt
instContinuousSqrtReal : ContinuousSqrt ℝ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.ModObj.leftSMul_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ModObj.leftSMul M X)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X X) =
    CategoryTheory.ModObj.smul
-- Mathlib.Order.DirSupClosed
/-- A predicate for a set which is closed under directed suprema of nonempty sets.
This is the complement of a `DirSupInacc` set.  -/
DirSupClosed : {α : Type u_1} → [Preorder α] → Set α → Prop
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
MaximalSpectrum.mk.inj : ∀ {R : Type u_1} {inst : CommSemiring R} {asIdeal : Ideal R} {isMaximal : asIdeal.IsMaximal} {asIdeal_1 : Ideal R}
  {isMaximal_1 : asIdeal_1.IsMaximal},
  { asIdeal := asIdeal, isMaximal := isMaximal } = { asIdeal := asIdeal_1, isMaximal := isMaximal_1 } →
    asIdeal = asIdeal_1
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_hasFDerivWithinAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G}
  {f' : G →L[𝕜] E}, HasFDerivWithinAt (⇑iso ∘ f) (↑↑iso ∘SL f') s x ↔ HasFDerivWithinAt f f' s x
-- Init.Prelude
/-- Construct a `BitVec w` from a number less than `2^w`.
O(1), because we use `Fin` as the internal representation of a bitvector.  -/
BitVec.ofFin : {w : ℕ} → Fin (2 ^ w) → BitVec w
-- Init.Grind.Propagator
/-- A user-defined propagator for the `grind` tactic.  -/
Lean.Parser.«command_Grind_propagator___(_):=_» : Lean.ParserDescr
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_addSubgroup_right_iff_bijective : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G},
  AddSubgroup.IsComplement S ↑H ↔ Function.Bijective (S.domRestrict QuotientAddGroup.mk)
-- Init.Data.List.Attach
List.getElem?_attachWith : ∀ {α : Type u_1} {xs : List α} {i : ℕ} {P : α → Prop} {H : ∀ a ∈ xs, P a},
  (xs.attachWith P H)[i]? = Option.pmap Subtype.mk xs[i]? ⋯
-- Lean.Elab.Tactic.Omega.Core
/-- A linear `combo` of two `Justifications`.  -/
Lean.Elab.Tactic.Omega.Justification.combo : {s t : Lean.Omega.Constraint} →
  {x y : Lean.Omega.Coeffs} →
    (a : ℤ) →
      Lean.Elab.Tactic.Omega.Justification s x →
        (b : ℤ) →
          Lean.Elab.Tactic.Omega.Justification t y →
            Lean.Elab.Tactic.Omega.Justification (Lean.Omega.Constraint.combo a s b t) (Lean.Omega.Coeffs.combo a x b y)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatLe.eq_2 : ∀ (p : Int.Internal.Linear.Poly), (∀ (k : ℤ), p = Int.Internal.Linear.Poly.num k → False) → p.isUnsatLe = false
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- Given a compatible family of sections over open sets, extend it to a
section of the functor `(Pairwise.diagram U).op ⋙ F`.  -/
TopCat.Presheaf.IsCompatible.sectionPairwise : {X : TopCat} →
  {F : TopCat.Presheaf (Type u_4) X} →
    {ι : Type u_5} →
      {U : ι → TopologicalSpace.Opens ↑X} →
        {sf : (i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))} →
          F.IsCompatible U sf → ↑((CategoryTheory.Pairwise.diagram U).op.comp F).sections
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- Constructor for cochains from `mappingCocone`.  -/
CochainComplex.mappingCocone.descCochain : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {M : CochainComplex C ℤ} →
              {n m : ℤ} →
                CochainComplex.HomComplex.Cochain K M m →
                  CochainComplex.HomComplex.Cochain L M n →
                    m + 1 = n → CochainComplex.HomComplex.Cochain (CochainComplex.mappingCocone φ) M m
-- Mathlib.Order.Filter.Germ.Basic
Filter.Product.coeTC : {α : Type u_1} → {l : Filter α} → {ε : α → Type u_5} → CoeTC ((a : α) → ε a) (l.Product ε)
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instMembership : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Membership α (Std.DTreeMap α β cmp)
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.fromSpecStalk_app : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} {x : ↥X} (hxU : x ∈ U),
  AlgebraicGeometry.Scheme.Hom.app (X.fromSpecStalk x) U =
    CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x hxU)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.stalk x)).inv
        ((AlgebraicGeometry.Spec (X.presheaf.stalk x)).presheaf.map (CategoryTheory.homOfLE ⋯).op))
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.integrable_gaussianPDFReal : ∀ (μ : ℝ) (v : NNReal), MeasureTheory.Integrable (ProbabilityTheory.gaussianPDFReal μ v) MeasureTheory.volume
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.density_fst_univ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  [ProbabilityTheory.IsFiniteKernel κ] (a : α), ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x Set.univ = 1