mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.LinearDisjoint
/-- Linear disjointness is symmetric.  -/
IntermediateField.LinearDisjoint.symm : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.LinearDisjoint ↥B → B.LinearDisjoint ↥A
-- Std.Async.System
Std.Async.System.Environment.get? : Std.Async.System.Environment → String → Option String
-- Lean.Elab.Tactic.RCases
/-- A named pattern like `foo`  -/
Lean.Elab.Tactic.RCases.RCasesPatt.one : Lean.Syntax → Lean.Name → Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.w₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₁ (CategoryTheory.CategoryStruct.comp f₁ h_1) =
    CategoryTheory.CategoryStruct.comp h.p h_1
-- Init.Data.List.Impl
List.find?_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : List α}, List.find? p (xs ++ ys) = (List.find? p xs).or (List.find? p ys)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Equivalence.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : B} {hom : a ⟶ b} {inv : b ⟶ a}
  {unit : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom inv}
  {counit : CategoryTheory.CategoryStruct.comp inv hom ≅ CategoryTheory.CategoryStruct.id b}
  {left_triangle :
    autoParam
      (CategoryTheory.Bicategory.leftZigzagIso unit counit =
        CategoryTheory.Bicategory.leftUnitor hom ≪≫ (CategoryTheory.Bicategory.rightUnitor hom).symm)
      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam}
  {hom_1 : a ⟶ b} {inv_1 : b ⟶ a}
  {unit_1 : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom_1 inv_1}
  {counit_1 : CategoryTheory.CategoryStruct.comp inv_1 hom_1 ≅ CategoryTheory.CategoryStruct.id b}
  {left_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.leftZigzagIso unit_1 counit_1 =
        CategoryTheory.Bicategory.leftUnitor hom_1 ≪≫ (CategoryTheory.Bicategory.rightUnitor hom_1).symm)
      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam},
  { hom := hom, inv := inv, unit := unit, counit := counit, left_triangle := left_triangle } =
      { hom := hom_1, inv := inv_1, unit := unit_1, counit := counit_1, left_triangle := left_triangle_1 } →
    hom = hom_1 ∧ inv = inv_1 ∧ unit ≍ unit_1 ∧ counit ≍ counit_1
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsTwoSided.mul_one : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} [I.IsTwoSided], I * 1 = I
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- `MeasureTheory.Lp.const` as a `LinearMap`.  -/
MeasureTheory.Lp.constₗ : {α : Type u_1} →
  {E : Type u_2} →
    {m : MeasurableSpace α} →
      (p : ENNReal) →
        (μ : MeasureTheory.Measure α) →
          [inst : NormedAddCommGroup E] →
            [MeasureTheory.IsFiniteMeasure μ] →
              (𝕜 : Type u_3) →
                [inst_2 : NormedRing 𝕜] →
                  [inst_3 : Module 𝕜 E] → [inst_4 : IsBoundedSMul 𝕜 E] → E →ₗ[𝕜] ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.hasLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat),
  CategoryTheory.Limits.HasLimitsOfSize.{v₂, v, max u₁ v, max (max (max (v + 1) u) u₁) v₁} (SheafOfModules R)
-- Mathlib.LinearAlgebra.LinearPMap
/-- A `LinearPMap σ E F` or `E →ₛₗ.[σ] F` is a (semi)linear map from a submodule of `E` to `F`.  -/
LinearPMap : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (R →+* S) →
          (E : Type u_3) →
            [inst_2 : AddCommGroup E] →
              [Module R E] → (F : Type u_4) → [inst : AddCommGroup F] → [Module S F] → Type (max u_3 u_4)
-- Mathlib.Tactic.DepRewrite
/-- `rw!` is like `rewrite!`, but also cleans up introduced refl-casts after every substitution.
It is available as an ordinary tactic and a `conv` tactic.
 -/
Mathlib.Tactic.DepRewrite.Conv.depRw : Lean.ParserDescr
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.le_def : ∀ {M : Type u_1} [inst : Group M] [inst_1 : Lattice M] {a b : MulArchimedeanOrder M},
  a ≤ b ↔ ∃ n, |MulArchimedeanOrder.val b|ₘ ≤ |MulArchimedeanOrder.val a|ₘ ^ n
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.of_pow_associated_of_prime' : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ},
  Prime p₁ → Prime p₂ → 0 < k₂ → Associated (p₁ ^ k₁) (p₂ ^ k₂) → Associated p₁ p₂
-- Mathlib.Probability.Process.Filtration
/-- Given a sequence of functions, the natural filtration is the smallest sequence
of σ-algebras such that the sequence of functions is measurable with respect to
the filtration.  -/
MeasureTheory.Filtration.natural : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      {β : ι → Type u_3} →
        [inst : (i : ι) → TopologicalSpace (β i)] →
          [∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)] →
            [mβ : (i : ι) → MeasurableSpace (β i)] →
              [∀ (i : ι), BorelSpace (β i)] →
                [inst_3 : Preorder ι] →
                  (u : (i : ι) → Ω → β i) →
                    (∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)) → MeasureTheory.Filtration ι m
-- Mathlib.Analysis.InnerProductSpace.LinearMap
ContinuousLinearMap.reApplyInnerSelf_continuous : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E), Continuous T.reApplyInnerSelf
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.precomposeId`.

---

Precomposing by the identity does not change the cocone up to isomorphism.  -/
CategoryTheory.Limits.Cocones.postcomposeId : {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.Cocone.precompose (CategoryTheory.CategoryStruct.id F) ≅
            CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)
-- Batteries.Data.List.Basic
/-- Auxliary definition used to define `toChunks`.
`toChunks.go xs acc₁ acc₂` pushes elements into `acc₁` until it reaches size `n`,
then it pushes the resulting list to `acc₂` and continues until `xs` is exhausted.  -/
List.toChunks.go : {α : Type u_1} → ℕ → List α → Array α → Array (List α) → List (List α)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.of.injEq : ∀ {C : Type u} (a a_1 : C), (CategoryTheory.WithInitial.of a = CategoryTheory.WithInitial.of a_1) = (a = a_1)
-- Mathlib.Topology.Path
/-- A continuous map extending a path to `ℝ`, constant before `0` and after `1`.  -/
Path.extend : {X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → Path x y → C(ℝ, X)
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- A version of `conditionallyCompleteLatticeOfsSup` when we already know that `α` is a lattice.

This should only be used when it is both hard and unnecessary to provide `sInf` explicitly.  -/
conditionallyCompleteLatticeOfLatticeOfsSup : (α : Type u_5) →
  [H1 : Lattice α] →
    [inst : SupSet α] → (∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)) → ConditionallyCompleteLattice α
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} (s₀ : E.I₀ → F.I₀) (h₀ : (i : E.I₀) → E.X i ⟶ F.X (s₀ i))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i) (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreZeroHypercover.Hom.w₀._autoParam)
  (s₀_1 : E.I₀ → F.I₀) (h₀_1 : (i : E.I₀) → E.X i ⟶ F.X (s₀_1 i))
  (w₀_1 :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀_1 i) (F.f (s₀_1 i)) = E.f i)
      CategoryTheory.PreZeroHypercover.Hom.w₀._autoParam),
  ({ s₀ := s₀, h₀ := h₀, w₀ := w₀ } = { s₀ := s₀_1, h₀ := h₀_1, w₀ := w₀_1 }) = (s₀ = s₀_1 ∧ h₀ ≍ h₀_1)
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumDiffSubset_apply_inl : ∀ {α : Type u_3} {s t : Set α} (h : s ⊆ t) [inst : DecidablePred fun x => x ∈ s] (x : ↑s),
  (Equiv.Set.sumDiffSubset h) (Sum.inl x) = Set.inclusion h x
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelFactorThruImage.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasImage f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)],
  CategoryTheory.Limits.kernelFactorThruImage f =
    (CategoryTheory.Limits.kernelCompMono (CategoryTheory.Limits.factorThruImage f)
          (CategoryTheory.Limits.image.ι f)).symm ≪≫
      CategoryTheory.Limits.kernelIsoOfEq ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.rightHomologyIso_hom_comp_homologyι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.rightHomologyIso.hom (CategoryTheory.CategoryStruct.comp S.homologyι h) =
    CategoryTheory.CategoryStruct.comp S.rightHomologyι h
-- Mathlib.Logic.Equiv.Option
Equiv.optionCongr_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : Option α), e.optionCongr a = Option.map (⇑e) a
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepRet.eq_def : ∀ (x : Turing.ToPartrec.Cont) (x_1 : List ℕ),
  Turing.ToPartrec.stepRet x x_1 =
    match x, x_1 with
    | Turing.ToPartrec.Cont.halt, v => Turing.ToPartrec.Cfg.halt v
    | Turing.ToPartrec.Cont.cons₁ fs as k, v => Turing.ToPartrec.stepNormal fs (Turing.ToPartrec.Cont.cons₂ v k) as
    | Turing.ToPartrec.Cont.cons₂ ns k, v => Turing.ToPartrec.stepRet k (ns.headI :: v)
    | Turing.ToPartrec.Cont.comp f k, v => Turing.ToPartrec.stepNormal f k v
    | Turing.ToPartrec.Cont.fix f k, v =>
      if v.headI = 0 then Turing.ToPartrec.stepRet k v.tail
      else Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) v.tail
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.curry_apply : ∀ (ι : Type u_6) (κ : Type u_7) (X : Type u_8) [inst : MeasurableSpace X] (a : ι × κ → X) (a_1 : ι) (a_2 : κ),
  (MeasurableEquiv.curry ι κ X) a a_1 a_2 = a (a_1, a_2)
-- Mathlib.RingTheory.Polynomial.GaussNorm
Polynomial.le_gaussNorm : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} (p : Polynomial R)
  [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ], 0 ≤ c → ∀ (i : ℕ), v (p.coeff i) * c ^ i ≤ Polynomial.gaussNorm v c p
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k}, (m.modify k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
-- Init.Data.String.Lemmas.Slice
String.Pos.get?_eq_some_get : ∀ {s : String} {p : s.Pos} (h : p ≠ s.endPos), p.get? = some (p.get h)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharTwoNF_spec : ∀ {F : Type u_2} [inst : Field F] [CharP F 2] (W : WeierstrassCurve F) [inst_2 : DecidableEq F],
  (W.toCharTwoNF • W).IsCharTwoNF
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_eq_of_isInvalidContinuationByte_eq_false : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte b = false → b.toBitVec = 2#2 ++ BitVec.setWidth 6 b.toBitVec
-- Mathlib.Order.Lattice
inf_sup_self : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊓ (a ⊔ b) = a
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.epi_of_cokernel_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f 0)],
  CategoryTheory.Limits.cokernel.π f = 0 → CategoryTheory.Epi f
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.ofHom_hom : ∀ {M N : MonCat} (f : M ⟶ N), MonCat.ofHom (MonCat.Hom.hom f) = f
-- Mathlib.Data.ZMod.Basic
/-- The unique ring isomorphism between `ZMod p` and a ring `R` of cardinality a prime `p`.

If you need any property of this isomorphism, first of all use `ringEquivOfPrime_eq_ringEquiv`
below (after `have : CharP R p := ...`) and deduce it by the results about `ZMod.ringEquiv`.  -/
ZMod.ringEquivOfPrime : (R : Type u_1) → [inst : Ring R] → [inst_1 : Fintype R] → {p : ℕ} → Nat.Prime p → Fintype.card R = p → ZMod p ≃+* R
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- The set of all (nontrivial) isotypic components of a module.  -/
isotypicComponents : (R : Type u_2) →
  (M : Type u) → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Set (Submodule R M)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.liftCM.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (T : Bundle.Trivialization F proj),
  T.liftCM = { toFun := fun ex => ⟨T.lift ↑ex.1 ↑ex.2, ⋯⟩, continuous_toFun := ⋯ }
-- Init.System.Uri
System.Uri.UriEscape.letterF : UInt8
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_associator_hom : ∀ {B : Type u} [inst : Quiver B] {a b c d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator f g h) =
    (CategoryTheory.Bicategory.associator f g h).hom
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabitedKey : Inhabited Lean.Meta.LazyDiscrTree.Key
-- Mathlib.Tactic.Simps.Basic
_private.Mathlib.Tactic.Simps.Basic.0.NameStruct.mk.inj : ∀ {parent : Lean.Name} {components : List String} {parent_1 : Lean.Name} {components_1 : List String},
  { parent := parent, components := components } = { parent := parent_1, components := components_1 } →
    parent = parent_1 ∧ components = components_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 ≠ W'.negY Q * P 2 → W'.dblZ P ≠ 0
-- Mathlib.NumberTheory.Dioph
Dioph.diophFn_vec_comp1 : ∀ {n : ℕ} {S : Set (Vector3 ℕ n.succ)},
  Dioph S → ∀ {f : Vector3 ℕ n → ℕ}, Dioph.DiophFn f → Dioph {v | Vector3.cons (f v) v ∈ S}
-- Mathlib.LinearAlgebra.Matrix.Adjugate
RingHom.map_adjugate : ∀ {n : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_1} {S : Type u_2} [inst_2 : CommRing R]
  [inst_3 : CommRing S] (f : R →+* S) (M : Matrix n n R), f.mapMatrix M.adjugate = (f.mapMatrix M).adjugate
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.self_mem_orthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P), p ∈ s.orthRadius p
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany_eq_get : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {n : ℕ} {a : α},
  Std.PRange.succMany n a = (Std.PRange.succMany? n a).get ⋯
-- Init.Data.Dyadic.Basic
Dyadic.blt.eq_3 : ∀ (n k : ℤ) (hn : n % 2 = 1), (Dyadic.ofOdd n k hn).blt Dyadic.zero = decide (n < 0)
-- Lean.Elab.DeclModifiers
Lean.Elab.Visibility.noConfusionType : Sort v✝ → Lean.Elab.Visibility → Lean.Elab.Visibility → Sort v✝
-- Mathlib.Algebra.Order.Group.Abs
max_zero_add_max_neg_zero_eq_abs_self : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a : G),
  max a 0 + max (-a) 0 = |a|
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.ofPresheaf_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : CategoryTheory.Functor Cᵒᵖ Ab) [inst_1 : (X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)]
  (map_smul :
    ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)),
      (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
        (CategoryTheory.ConcreteCategory.hom (R.map f)) r • (CategoryTheory.ConcreteCategory.hom (M.map f)) m)
  {X Y : Cᵒᵖ} (f : X ⟶ Y),
  (PresheafOfModules.ofPresheaf M map_smul).map f =
    ModuleCat.ofHom
      { toFun := fun x => (CategoryTheory.ConcreteCategory.hom (M.map f)) x, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Group.End
Equiv.Perm.extendDomain_one : ∀ {α : Type u_4} {β : Type u_5} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
  Equiv.Perm.extendDomain 1 f = 1
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_hom_snd : ∀ (X Y : TopCat),
  CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom TopCat.prodSnd = CategoryTheory.Limits.prod.snd
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.ae_ae_eq_curry_of_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {γ : Type u_4} {f g : α × β → γ},
  f =ᵐ[μ.prod ν] g → ∀ᵐ (x : α) ∂μ, Function.curry f x =ᵐ[ν] Function.curry g x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.mateEquiv_symm_apply' : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c}
  {l₂ : e ⟶ f} {r₂ : f ⟶ e} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (β : CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₂),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₂).symm β =
    CategoryTheory.bicategoricalComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp g l₂))
      (CategoryTheory.bicategoricalComp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight adj₁.unit g) l₂)
        (CategoryTheory.bicategoricalComp
          (CategoryTheory.Bicategory.whiskerLeft l₁ (CategoryTheory.Bicategory.whiskerRight β l₂))
          (CategoryTheory.bicategoricalComp
            (CategoryTheory.Bicategory.whiskerLeft l₁ (CategoryTheory.Bicategory.whiskerLeft h adj₂.counit))
            (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp l₁ h)))))
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_div_add : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a‖ ≤ ‖a / b‖ + ‖b‖
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.length_nonneg : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (s : NonemptyInterval α),
  0 ≤ s.length
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- Preimage of an analytic set is an analytic set.  -/
MeasureTheory.AnalyticSet.preimage : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PolishSpace X] [T2Space Y]
  {s : Set Y}, MeasureTheory.AnalyticSet s → ∀ {f : X → Y}, Continuous f → MeasureTheory.AnalyticSet (f ⁻¹' s)
-- Mathlib.GroupTheory.GroupAction.Hom
instMulActionSemiHomClassMulActionHom : ∀ {M : Type u_2} {N : Type u_3} (φ : M → N) (X : Type u_5) [inst : SMul M X] (Y : Type u_6) [inst_1 : SMul N Y],
  MulActionSemiHomClass (X →ₑ[φ] Y) φ X Y
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.instIsArtinianRingCarrierObjFiniteEtale : ∀ (k : Type u) [inst : Field k] (R : CommAlgCat.FiniteEtale k), IsArtinianRing ↑R.obj
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.coe_mk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → MeasureTheory.Measure β)
  (hf : Measurable f), ⇑{ toFun := f, measurable' := hf } = f
-- Init.Data.List.Attach
List.attach_reverse : ∀ {α : Type u_1} {xs : List α},
  xs.reverse.attach =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.attach.reverse
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.equivMeasure_symm_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α),
  MeasureTheory.VectorMeasure.equivMeasure.symm μ = μ.toENNRealVectorMeasure
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage_univ : ∀ {X : Type u_1} {T : X → X} {n : ℕ}, Dynamics.dynEntourage T Set.univ n = Set.univ
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.compl : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsLowerSet s → IsUpperSet sᶜ
-- Init.Meta.Defs
/-- Appends two tactic configurations.
The configurations can be `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`,
or these wrapped in null nodes (for example because the syntax is `(config)?`).
 -/
Lean.Parser.Tactic.appendConfig : Lean.Syntax → Lean.Syntax → Lean.TSyntax `Lean.Parser.Tactic.optConfig
-- Mathlib.Algebra.Group.Defs
RightCancelSemigroup.toSemigroup : {G : Type u} → [self : RightCancelSemigroup G] → Semigroup G
-- Std.Data.DHashMap.Internal.AssocList.Basic
Std.DHashMap.Internal.AssocList.cons.injEq : ∀ {α : Type u} {β : α → Type v} (key : α) (value : β key) (tail : Std.DHashMap.Internal.AssocList α β) (key_1 : α)
  (value_1 : β key_1) (tail_1 : Std.DHashMap.Internal.AssocList α β),
  (Std.DHashMap.Internal.AssocList.cons key value tail = Std.DHashMap.Internal.AssocList.cons key_1 value_1 tail_1) =
    (key = key_1 ∧ value ≍ value_1 ∧ tail = tail_1)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Subfield.extendScalars_self : ∀ {L : Type u_2} [inst : Field L] (F : Subfield L), Subfield.extendScalars ⋯ = ⊥
-- Mathlib.Topology.Algebra.Module.LocallyConvex
/-- In a locally convex space, every two disjoint convex sets such that one is compact and the other
is closed admit disjoint convex open neighborhoods.  -/
Disjoint.exists_open_convexes : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [ZeroLEOneClass 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [LocallyConvexSpace 𝕜 E] {s t : Set E},
  Disjoint s t →
    Convex 𝕜 s →
      IsCompact s →
        Convex 𝕜 t → IsClosed t → ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.diracProbaEquiv.congr_simp : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
  [inst_3 : T0Space X], MeasureTheory.diracProbaEquiv = MeasureTheory.diracProbaEquiv
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.InternalState.mk.injEq : ∀ (footnotes : Std.HashMap String (Lean.Doc.Ref✝ (Lean.Doc.Inline Lean.ElabInline)))
  (urls : Std.HashMap String (Lean.Doc.Ref✝ String)) (deferred : Array Lean.Doc.DeferredCheck)
  (footnotes_1 : Std.HashMap String (Lean.Doc.Ref✝ (Lean.Doc.Inline Lean.ElabInline)))
  (urls_1 : Std.HashMap String (Lean.Doc.Ref✝ String)) (deferred_1 : Array Lean.Doc.DeferredCheck),
  ({ footnotes := footnotes, urls := urls, deferred := deferred } =
      { footnotes := footnotes_1, urls := urls_1, deferred := deferred_1 }) =
    (footnotes = footnotes_1 ∧ urls = urls_1 ∧ deferred = deferred_1)