mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The forgetful functor from the full subcategory of `Under X` defined by `P` to `Under X`.  -/
CategoryTheory.MorphismProperty.Under.forget : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P Q : CategoryTheory.MorphismProperty T) →
      (X : T) → [inst_1 : Q.IsMultiplicative] → CategoryTheory.Functor (P.Under Q X) (CategoryTheory.Under X)
-- Mathlib.Algebra.Group.Action.Pretransitive
AddAction.isPretransitive_iff : ∀ (M : Type u_5) (α : Type u_6) [inst : VAdd M α], AddAction.IsPretransitive M α ↔ ∀ (x y : α), ∃ g, g +ᵥ x = y
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `k` is a monomorphism, then `k.left` is a monomorphism. In other words, `Over.forget X` preserves
monomorphisms.
The converse of `CategoryTheory.Over.mono_of_mono_left`.
 -/
CategoryTheory.Over.mono_left_of_mono : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (k : f ⟶ g)
  [CategoryTheory.Mono k], CategoryTheory.Mono (CategoryTheory.Over.Hom.left k)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.contains k = t.contains k'
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Clause.eval_cons : ∀ {α : Type u_1} {i : Std.Sat.Literal α} {c : List (Std.Sat.Literal α)} (a : α → Bool),
  Std.Sat.CNF.Clause.eval a (i :: c) = (a i.1 == i.2 || Std.Sat.CNF.Clause.eval a c)
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Division `y ↦ x / y` as an `IsometryEquiv`.  -/
IsometryEquiv.divLeft : {G : Type v} →
  [inst : Group G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricSMul G G] → [IsIsometricSMul Gᵐᵒᵖ G] → G → G ≃ᵢ G
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Show two functors out of a wide pullback shape are isomorphic by showing their components are
isomorphic.  -/
CategoryTheory.Limits.WidePullbackShape.functorExt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {F G : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C} →
        (base : F.obj none ≅ G.obj none) →
          (comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)) →
            autoParam
                (∀ (i : ι),
                  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i))
                      base.hom =
                    CategoryTheory.CategoryStruct.comp (comp i).hom
                      (G.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)))
                CategoryTheory.Limits.WidePullbackShape.functorExt._auto_1 →
              (F ≅ G)
-- Mathlib.Data.Matrix.Basic
Matrix.piEquiv_apply : ∀ {m : Type u_2} {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} (f : Matrix m n ((i : ι) → β i)) (i : ι),
  Matrix.piEquiv f i = f.map fun x => x i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {he : t.isEmpty = false}, (compare (t.maxKey he) k).isLE = true ↔ ∀ k' ∈ t, (compare k' k).isLE = true
-- Mathlib.Geometry.Manifold.BumpFunction
/-- The closures of supports of smooth bump functions centered at `c` form a basis of `𝓝 c`.
In other words, each of these closures is a neighborhood of `c` and each neighborhood of `c`
includes `tsupport f` for some `f : SmoothBumpFunction I c`.  -/
SmoothBumpFunction.nhds_basis_tsupport : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] (c : M)
  [inst_5 : FiniteDimensional ℝ E] [T2Space M], (nhds c).HasBasis (fun x => True) fun f => tsupport ↑f
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalGrobner : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus.congr_simp : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] {inst_1 : (a : α) → DecidableEq (N a)}
  [inst_2 : (a : α) → DecidableEq (N a)] [inst_3 : (a : α) → Zero (N a)] (f f_1 : Π₀ (a : α), N a),
  f = f_1 → ∀ (g g_1 : Π₀ (a : α), N a), g = g_1 → f.neLocus g = f_1.neLocus g_1
-- Mathlib.Topology.Connected.Basic
IsPreconnected.preimage_of_isOpenMap : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set β},
  IsPreconnected s → Function.Injective f → IsOpenMap f → s ⊆ Set.range f → IsPreconnected (f ⁻¹' s)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.map_smul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {M : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M] {R : Type u_4} [inst_3 : Semiring R]
  [inst_4 : DistribMulAction R M] [inst_5 : ContinuousConstSMul R M] {v : MeasureTheory.VectorMeasure α M} {f : α → β}
  (c : R), (c • v).map f = c • v.map f
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_functor_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D),
  (CategoryTheory.WithInitial.equivComma.functor.obj F).left = F.obj CategoryTheory.WithInitial.star
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.seq : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {β γ : Type u_6} {f : α → Part (β → γ)} {g : α → Part β},
  OmegaCompletePartialOrder.ωScottContinuous f →
    OmegaCompletePartialOrder.ωScottContinuous g → OmegaCompletePartialOrder.ωScottContinuous fun x => f x <*> g x
-- Init.Data.String.Lemmas.Pattern.Find.String
String.Slice.contains_string_iff : ∀ {t : String} {s : String.Slice}, s.contains t = true ↔ t.toList <:+: s.copy.toList
-- Init.Data.Slice.Lemmas
Std.Slice.Internal.foldlM_iter : ∀ {γ : Type u} {α β : Type v} {m : Type u_1 → Type u_2} {δ : Type u_1} [inst : Monad m]
  [inst_1 : Std.ToIterator (Std.Slice γ) Id α β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id m]
  {s : Std.Slice γ} {init : δ} {f : δ → β → m δ},
  Std.Iter.foldM f init (Std.Slice.Internal.iter s) = Std.Slice.foldlM f init s
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.proj : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup F]
  [inst_2 : TopologicalSpace F] [inst_3 : Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8}
  [inst_4 : (i : ι) → AddCommGroup (E i)] [inst_5 : (i : ι) → Module 𝕜 (E i)]
  [inst_6 : (i : ι) → TopologicalSpace (E i)] {f : α → (i : ι) → E i},
  f =O[𝕜; l] g → ∀ (i : ι), (fun x => f x i) =O[𝕜; l] g
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.comapDomain.congr_simp : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f f_1 : M → N) (e_f : f = f_1)
  (hf : Function.Injective f) (x x_1 : MonoidAlgebra R N),
  x = x_1 → MonoidAlgebra.comapDomain f hf x = MonoidAlgebra.comapDomain f_1 ⋯ x_1
-- Mathlib.Algebra.Free
/-- Lifts a function `α → β` to an additive semigroup
homomorphism `FreeAddSemigroup α → β` given an additive semigroup `β`.  -/
FreeAddSemigroup.lift : {α : Type u} → {β : Type v} → [inst : AddSemigroup β] → (α → β) ≃ (FreeAddSemigroup α →ₙ+ β)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₂.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G),
  groupCohomology.coboundaries₂ A = (ModuleCat.Hom.hom (groupCohomology.d₁₂ A)).range
-- Mathlib.Topology.MetricSpace.Isometry
/-- `α` and `β` are isometric if there is an isometric bijection between them.  -/
«term_≃ᵢ_» : Lean.TrailingParserDescr
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.coe_mapCocycles₂ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_1, u, u} k H}
  {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(ModuleCat.of k ↥(groupCohomology.cocycles₂ A))),
  ⇑((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₂ f φ)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsMap₂ f φ)) ⇑x
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.aevalAeval_X : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (x y : A),
  (Polynomial.aevalAeval x y) (Polynomial.C Polynomial.X) = x
-- Mathlib.Algebra.Group.Int.TypeTags
Int.toAdd_pow : ∀ (a : Multiplicative ℤ) (b : ℕ), Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * ↑b
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrderBot.mk : {α : Type u_1} →
  [inst : Preorder α] →
    (finsetIio finsetIic : α → Finset α) →
      (∀ (a x : α), x ∈ finsetIic a ↔ x ≤ a) → (∀ (a x : α), x ∈ finsetIio a ↔ x < a) → LocallyFiniteOrderBot α
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.em.inj : ∀ {classical : Bool} {p : Lean.Name} {classical_1 : Bool} {p_1 : Lean.Name},
  Mathlib.Tactic.ITauto.Proof.em classical p = Mathlib.Tactic.ITauto.Proof.em classical_1 p_1 →
    classical = classical_1 ∧ p = p_1
-- Mathlib.Data.Set.Image
Subtype.coe_image_subset : ∀ {α : Type u_1} (s : Set α) (t : Set ↑s), Subtype.val '' t ⊆ s
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.instStarHomClass : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B], StarHomClass (A →⋆ₐ[R] B) A B
-- Lean.Parser.Types
Lean.Parser.TokenCacheEntry.mk.inj : ∀ {startPos stopPos : String.Pos.Raw} {token : Lean.Syntax} {startPos_1 stopPos_1 : String.Pos.Raw}
  {token_1 : Lean.Syntax},
  { startPos := startPos, stopPos := stopPos, token := token } =
      { startPos := startPos_1, stopPos := stopPos_1, token := token_1 } →
    startPos = startPos_1 ∧ stopPos = stopPos_1 ∧ token = token_1
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.h_feq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (self : WeakFEPair E),
  ∀ x ∈ Set.Ioi 0, self.f (1 / x) = (self.ε * ↑(x ^ self.k)) • self.g x
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_sSup_of_directed : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s : Set (Submodule R M)} {z : M}, s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → (z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.symplComp_sup : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S T : ClosedSubmodule ℝ H),
  (S ⊔ T).symplComp = S.symplComp ⊓ T.symplComp
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullbackArrows_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Presieve X)
  [inst_1 : R.HasPullbacks f],
  CategoryTheory.Sieve.generate (CategoryTheory.Presieve.pullbackArrows f R) =
    CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.generate R)
-- Mathlib.RingTheory.Localization.FractionRing
/-- If `L` is a fraction ring of `K` which is a fraction ring of `R`,
the `K`-algebra homomorphism from `K` to `L` is an isomorphism.  -/
IsFractionRing.algEquiv : (R : Type u_1) →
  [inst : CommRing R] →
    (K : Type u_5) →
      [inst_1 : CommRing K] →
        [inst_2 : Algebra R K] →
          [IsFractionRing R K] →
            (L : Type u_6) → [inst : CommRing L] → [inst_3 : Algebra K L] → [IsFractionRing K L] → K ≃ₐ[K] L
-- Std.Time.DateTime.PlainDateTime
/-- Getter for the `Minute` inside of a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.minute : Std.Time.PlainDateTime → Std.Time.Minute.Ordinal
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₁.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂),
  K.D₁ c₁₂ i₁₂ i₁₂' =
    K.toGradedObject.descMapObj (c₁.π c₂ c₁₂) fun x x_1 =>
      match x, x_1 with
      | (i₁, i₂), x => K.d₁ c₁₂ i₁ i₂ i₁₂'
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- A bijection between the orbits under the action of a subgroup `H` on `X`, and the orbits
under the action of `H` on each orbit under the action of `G`.  -/
MulAction.equivSubgroupOrbits : {G : Type u} →
  (X : Type v) →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        (H : Subgroup G) →
          MulAction.orbitRel.Quotient (↥H) X ≃
            (ω : Quotient (MulAction.orbitRel G X)) ×
              MulAction.orbitRel.Quotient ↥H ↑(MulAction.orbitRel.Quotient.orbit ω)
-- Mathlib.FieldTheory.Finite.GaloisField
GaloisField.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [inst : Fact (Nat.Prime p)] (n n_1 : ℕ), n = n_1 → GaloisField p n = GaloisField p_1 n_1
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.add_eq_zero' : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), a + b = 0 ↔ a = b
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisors.coe_ne_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀] (x : ↥(nonZeroDivisors M₀)), ↑x ≠ 0
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.eval_one : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L), RatFunc.eval f a 1 = 1
-- Mathlib.Data.Set.Card
Set.encard_sdiff_add_encard : ∀ {α : Type u_1} (s t : Set α), (s \ t).encard + t.encard = (s ∪ t).encard
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.NonlinearRightInverse.mk : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] →
                      {f : E →SL[σ] F} →
                        (toFun : F → E) →
                          (nnnorm : NNReal) →
                            (∀ (y : F), ‖toFun y‖ ≤ ↑nnnorm * ‖y‖) →
                              (∀ (y : F), f (toFun y) = y) → f.NonlinearRightInverse
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.WithGeneratedByTopology.equiv.eq_1 : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  Topology.WithGeneratedByTopology.equiv = Equiv.refl (Topology.WithGeneratedByTopology X Y)
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.rightUnitor_hom_congr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f'),
  (CategoryTheory.Bicategory.rightUnitor f).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.eqToHom h) (CategoryTheory.CategoryStruct.id y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f').hom (CategoryTheory.eqToHom ⋯))
-- Lean.Meta.Sym.Arith.Types
/-- Get the exponent threshold.  -/
Lean.Meta.Sym.Arith.getExpThreshold : Lean.Meta.Sym.SymM ℕ
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.piCongrRight_apply : ∀ {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [inst : (j : η) → Mul (Ms j)]
  [inst_1 : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) (x : (j : η) → Ms j) (j : η),
  (MulEquiv.piCongrRight es) x j = (es j) (x j)
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.tryAppUnexpanders.go : Lean.Term →
  Array Lean.PrettyPrinter.Delaborator.AppImplicitArg →
    List Lean.PrettyPrinter.Unexpander → ℕ → ℕ → Array Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).m =
    CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π f)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If `C` has an initial object and `G` preserves initial objects, then `D` has an initial object
also.
Note this property is somewhat unique to colimits of the empty diagram: for general `J`, if `C`
has colimits of shape `J` and `G` preserves them, then `D` does not necessarily have colimits of
shape `J`.
 -/
CategoryTheory.Limits.hasInitial_of_hasInitial_of_preservesColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G], CategoryTheory.Limits.HasInitial D
-- Init.Data.Slice.Notation
/-- Slices `carrier` from `range.lower` to `range.upper`, both inclusive.
   -/
Std.Rcc.Sliceable.mkSlice : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → [self : Std.Rcc.Sliceable α β γ] → α → Std.Rcc β → γ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.IsRightAdjoint.nonempty : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : B} {right : b ⟶ a}
  [self : CategoryTheory.Bicategory.IsRightAdjoint right], Nonempty (CategoryTheory.Bicategory.LeftAdjoint right)
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a distributive lattice
with possibly different definitional equalities.  -/
DistribLattice.copy : {α : Type u} →
  (c : DistribLattice α) →
    (le : α → α → Prop) → le = LE.le → (sup : α → α → α) → sup = max → (inf : α → α → α) → inf = min → DistribLattice α
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.trans_refl : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β), f.trans (Function.Embedding.refl β) = f
-- Init.Data.Int.Order
Int.lt_of_le_sub_one : ∀ {a b : ℤ}, a ≤ b - 1 → a < b
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_map : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (X : C) {X_1 Y : D} (f : X_1 ⟶ Y),
  ((CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D).obj X).unmop.map f =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight X f
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.map_id : ∀ {X : Type u_1} {R : Type u_3} {E : Type u_4} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : CommRing R] [inst_5 : TopologicalSpace R]
  [inst_6 : IsTopologicalRing R] [inst_7 : Module R E] [inst_8 : ContinuousSMul R E] (μ : AbstractMeasure X R E),
  (AbstractMeasure.map (ContinuousMap.id X)) μ = μ
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the reverse direction of `HasDerivWithinAt.Ioi_iff_Ioo`. -/
HasDerivWithinAt.Ioo_of_Ioi : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} [inst_3 : LinearOrder 𝕜] [OrderClosedTopology 𝕜] {x y : 𝕜},
  x < y → HasDerivWithinAt f f' (Set.Ioi x) x → HasDerivWithinAt f f' (Set.Ioo x y) x
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.range_coe : ∀ {α : Type u} [inst : TopologicalSpace α], Set.range ConnectedComponents.mk = Set.univ
-- Mathlib.Topology.Order.Basic
nhds_eq_order : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a : α),
  nhds a = (⨅ b ∈ Set.Iio a, Filter.principal (Set.Ioi b)) ⊓ ⨅ b ∈ Set.Ioi a, Filter.principal (Set.Iio b)
-- Lean.Syntax
Lean.unreachIsNodeAtom : {β : Sort u_1} → {info : Lean.SourceInfo} → {val : String} → Lean.IsNode (Lean.Syntax.atom info val) → β
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.toNormSMulClass : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E],
  NormSMulClass 𝕜 E
-- Mathlib.Order.Heyting.Basic
toDual_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), OrderDual.toDual aᶜ = ￢OrderDual.toDual a
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderFiniteCoproducts.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C},
  (∀ (J : Type) [Finite J], W.IsStableUnderCoproductsOfShape J) → W.IsStableUnderFiniteCoproducts
-- Mathlib.Data.Rat.Cast.Defs
NNRat.subsingleton_ringHom : ∀ {R : Type u_5} [inst : Semiring R], Subsingleton (ℚ≥0 →+* R)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.pentagon_aux₂ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₂ : CategoryTheory.LocalizedMonoidal L W ε} (i : X₂ ≅ Y₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ i.hom)
        X₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₂ X₃).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight i.inv X₃))) =
    (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The chosen coend of a functor `Jᵒᵖ ⥤ J ⥤ C`.  -/
CategoryTheory.Limits.chosenCoend : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} J] →
        CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C) → [CategoryTheory.Limits.ChosenCoendsOfShape J C] → C
-- Mathlib.RingTheory.LocalRing.Length
CovBy.length_baseChange : ∀ {A : Type u_1} (B : Type u_2) {M : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsLocalRing A]
  [IsLocalRing B] [inst_4 : Algebra A B] [IsLocalHom (algebraMap A B)] [inst_6 : AddCommGroup M] [inst_7 : Module A M]
  [Module.Flat A B] {p q : Submodule A M},
  p ⋖ q →
    Module.length B ↥(Submodule.baseChange B q) =
      Module.length B ↥(Submodule.baseChange B p) +
        Module.length B (B ⧸ Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A))
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.relabel.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α → β) (i : α),
  FirstOrder.Language.Term.relabel g (FirstOrder.Language.var i) = FirstOrder.Language.var (g i)
-- Mathlib.Util.Export
Lean.Export.instInhabitedState : Inhabited Lean.Export.State
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postComp_hom_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor T D)
  (G : CategoryTheory.Functor D E) (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.Over.postComp F G).hom.app X_1).left = CategoryTheory.CategoryStruct.id (G.obj (F.obj X_1.left))
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.exists_distinct_next_or : ∀ {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop] (j : ι), (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j