mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_shift_unop_assoc : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] {X Y : Cᵒᵖ}
  (f : X ⟶ Y) (n : ℤ) {Z : D} (h : F.obj (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F.op n).inv.app Y).unop
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Dᵒᵖ n).map (F.map f.unop).op).unop
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F.op n).hom.app X).unop h))
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.intro.inj : ∀ {x : Lean.Name} {p : Mathlib.Tactic.ITauto.Proof} {x_1 : Lean.Name} {p_1 : Mathlib.Tactic.ITauto.Proof},
  Mathlib.Tactic.ITauto.Proof.intro x p = Mathlib.Tactic.ITauto.Proof.intro x_1 p_1 → x = x_1 ∧ p = p_1
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- A subset `v` of a null-set `w` has zero measure if `w` is a subset of a positive set `u`.  -/
MeasureTheory.SignedMeasure.subset_positive_null_set : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v w : Set α},
  MeasurableSet u →
    MeasurableSet v →
      MeasurableSet w →
        MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u →
          s w = 0 → w ⊆ u → v ⊆ w → s v = 0
-- Init.Data.List.Sublist
List.nil_sublist : ∀ {α : Type u_1} (l : List α), [].Sublist l
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.add : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] [ContinuousAdd ε'] {f g : α → ε'},
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn g s μ → MeasureTheory.IntegrableOn (f + g) s μ
-- Mathlib.RingTheory.Etale.Basic
/-- A ring homomorphism `R →+* A` is formally étale if it is formally unramified and formally smooth.
See `Algebra.FormallyEtale`.
 -/
RingHom.FormallyEtale : {R : Type u_1} → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.Analysis.Normed.Group.Basic
nndist_eq_nnnorm_neg_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), nndist a b = ‖-a + b‖₊
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.instPartialOrder : {R : Type v} → [inst : NonAssocSemiring R] → [inst_1 : Star R] → PartialOrder (StarSubsemiring R)
-- Mathlib.Topology.Instances.Matrix
HasSum.matrix_diag : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} {f : X → Matrix n n R} {a : Matrix n n R},
  HasSum f a L → HasSum (fun x => (f x).diag) a.diag L
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] (C : CategoryTheory.Cat) (x : CategoryTheory.Join (↑C) D),
  CategoryTheory.CategoryStruct.id x = x.id
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] P) (x : TensorProduct R M N),
  (LinearMap.lTensor N f) ((TensorProduct.comm R M N) x) = (TensorProduct.comm R P N) ((LinearMap.rTensor N f) x)
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- This instance is split off from the `Ring (End X)` instance to speed up instance search.  -/
CategoryTheory.Preadditive.instSemiringEnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Preadditive C] → {X : C} → Semiring (CategoryTheory.End X)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.neg_apply : ∀ (G : Type u_4) [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : MeasurableNeg G],
  ⇑(MeasurableEquiv.neg G) = Neg.neg
-- Init.Prelude
/-- Parses using the category parser `catName` with right binding power
(i.e. precedence) `rbp`.  -/
Lean.ParserDescr.cat : Lean.Name → ℕ → Lean.ParserDescr
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
OrderIso.mulRight₀_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [inst_2 : MulPosReflectLT G₀] (a : G₀)
  (ha : 0 < a) (x : G₀), (OrderIso.mulRight₀ a ha) x = x * a
-- Mathlib.Analysis.Convex.Quasiconvex
quasilinearOn_iff_monotoneOn_or_antitoneOn : ∀ {𝕜 : Type u_1} {β : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜}
  {f : 𝕜 → β} [inst_3 : LinearOrder β], Convex 𝕜 s → (QuasilinearOn 𝕜 s f ↔ MonotoneOn f s ∨ AntitoneOn f s)
-- Mathlib.CategoryTheory.Bicategory.End
/-- The endomorphisms of an object in a bicategory can be considered as a monoidal category.  -/
CategoryTheory.EndMonoidal : {C : Type u} → [CategoryTheory.Bicategory C] → C → Type v
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
MeasureTheory.lintegral_sub : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  Measurable g → ∫⁻ (a : α), g a ∂μ ≠ ⊤ → g ≤ᵐ[μ] f → ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence of functions `Fₙ` converges uniformly on a filter `p'` to a limiting function `f` w.r.t.
filter `p` iff the function `(n, x) ↦ (f x, Fₙ x)` converges along `p ×ˢ p'` to the uniformity.
In other words: one knows nothing about the behavior of `x` in this limit besides it being in `p'`.
 -/
tendstoUniformlyOnFilter_iff_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α},
  TendstoUniformlyOnFilter F f p p' ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (uniformity β)
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.leadingCoeff_opRingEquiv : ∀ {R : Type u_1} [inst : Semiring R] (p : (Polynomial R)ᵐᵒᵖ),
  ((Polynomial.opRingEquiv R) p).leadingCoeff = MulOpposite.op (MulOpposite.unop p).leadingCoeff
-- Mathlib.Combinatorics.Matroid.Basic
_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.ground_subset_ground : ∀ {α : Type u_1} {M : Matroid α}, M.E ⊆ M.E
-- Mathlib.AlgebraicGeometry.Modules.Tilde
_private.Mathlib.AlgebraicGeometry.Modules.Tilde.0.AlgebraicGeometry.QuasicoherentTilde.Aux.existence : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {V : (AlgebraicGeometry.Spec R).Opens},
  AlgebraicGeometry.QuasicoherentTilde.Aux✝ M V →
    ∀ (f : ↑R) (hf : PrimeSpectrum.basicOpen f ≤ V) (s : ↑(M.presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))),
      ∃ n t, (CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE hf).op)) t = f ^ n • s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.contains_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF → t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k t₁ = Std.DTreeMap.Internal.Impl.contains k t₂
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.dvd_iff : ∀ {m a b d : ℕ}, a ≡ b [MOD m] → d ∣ m → (d ∣ a ↔ d ∣ b)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_map_inv' : ∀ {G : Type u_4} [inst : DivisionCommMonoid G] (m : Multiset G), (Multiset.map Inv.inv m).prod = m.prod⁻¹
-- Lean.Data.Lsp.CodeActions
/-- Whether the client supports resolving additional code action properties via a separate `codeAction/resolve` request.  -/
Lean.Lsp.CodeActionClientCapabilities.resolveSupport? : Lean.Lsp.CodeActionClientCapabilities → Option Lean.Lsp.ResolveSupport
-- Init.Data.BitVec.Lemmas
BitVec.and_assoc : ∀ {w : ℕ} (x y z : BitVec w), x &&& y &&& z = x &&& (y &&& z)
-- Mathlib.Algebra.Algebra.Tower
Submodule.span_smul_of_span_eq_top : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {s : Set S},
  Submodule.span R s = ⊤ → ∀ (t : Set A), Submodule.span R (s • t) = Submodule.restrictScalars R (Submodule.span S t)
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.factorₐ_comp_liftAdicCompletionAux : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (I : Ideal S) (f : A →ₐ[R] S ⧸ I) [inst_5 : Algebra.FormallySmooth R A]
  (m : ℕ),
  (Ideal.Quotient.factorₐ R ⋯).comp (Algebra.FormallySmooth.liftAdicCompletionAux✝ I f (m + 1)) =
    Algebra.FormallySmooth.liftAdicCompletionAux✝ I f m
-- Mathlib.Algebra.Order.Ring.Abs
abs_le_of_sq_le_sq' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  a ^ 2 ≤ b ^ 2 → 0 ≤ b → -b ≤ a ∧ a ≤ b
-- Mathlib.AlgebraicGeometry.QuasiAffine
/-- Any quasicompact locally closed subscheme of a quasi-affine scheme is quasi-affine.  -/
AlgebraicGeometry.Scheme.IsQuasiAffine.of_isImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [Y.IsQuasiAffine] [AlgebraicGeometry.IsImmersion f] [CompactSpace ↥X],
  X.IsQuasiAffine
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- Nondegenerate `d`-dimensional simplices of the standard simplex `Δ[n]`
identify to subsets of `Fin (n + 1)` of cardinality `d + 1`.  -/
SSet.stdSimplex.nonDegenerateEquiv' : {n d : ℕ} → ↑((SSet.stdSimplex.obj { len := n }).nonDegenerate d) ≃ ↑{S | S.card = d + 1}
-- Lean.Elab.DefView
Lean.Elab.DefView.modifiers : Lean.Elab.DefView → Lean.Elab.Modifiers
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
/-- *Integration by parts* for absolutely continuous functions.  -/
AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul : ∀ {f g : ℝ → ℝ} {a b : ℝ},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b →
      ∫ (x : ℝ) in a..b, f x * deriv g x = f b * g b - f a * g a - ∫ (x : ℝ) in a..b, deriv f x * g x
-- Mathlib.LinearAlgebra.Span.Basic
LinearEquiv.toSpanNonzeroSingleton_symm_apply_smul : ∀ (R : Type u_1) (M : Type u_4) [inst : Ring R] [inst_1 : IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.IsTorsionFree R M] (x : M) (h : x ≠ 0) (m : ↥(R ∙ x)),
  (LinearEquiv.toSpanNonzeroSingleton R M x h).symm m • x = ↑m
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.eqToHomTransIso_refl_refl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B),
  CategoryTheory.Bicategory.eqToHomTransIso ⋯ ⋯ =
    (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.id x)).symm
-- Init.Data.UInt.Lemmas
UInt32.toFin_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toFin = OfNat.ofNat n
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.isClosed_fiber : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyConstant f → ∀ (y : Y), IsClosed {x | f x = y}
-- Mathlib.Algebra.Algebra.Spectrum.Basic
IsUnit.val_subInvSMul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : Rˣ} {s : R} {a : A}
  (h : IsUnit (r • (algebraMap R A) s - a)), ↑h.subInvSMul = (algebraMap R A) s - r⁻¹ • a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km fallback : α}, t.minKey? = some km → t.getKeyD km fallback = km
-- Mathlib.Data.List.Forall2
List.forall₂_zip : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β},
  List.Forall₂ R l₁ l₂ → ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
-- Mathlib.Logic.Unique
heq_const_of_unique : ∀ {α : Sort u_1} [inst : Unique α] {β : α → Sort v} (f : (a : α) → β a), f ≍ Function.const α (f default)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.pullback_symmetry_hom_of_epi_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f],
  (CategoryTheory.Limits.pushoutSymmetry f f).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pushout f f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take_cons_eq : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (n : ℕ) (hn : n ≠ 0),
  (SimpleGraph.Walk.cons h p).take n = SimpleGraph.Walk.cons h ((p.take (n - 1)).copy ⋯ ⋯)
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_hasBasis : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_5} {p : ι → Prop} {s' : ι → Set α} {s : Set α},
  (nhdsSet s).HasBasis p s' → ∀ (t : Set α), (nhdsSetWithin s t).HasBasis p fun i => s' i ∩ t
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- If `{sᵢ}` is a local frame on a vector bundle, `F` being finite-dimensional implies the
indexing set being finite.  -/
IsLocalFrameOn.fintypeOfFiniteDimensional : {𝕜 : 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] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : FiberBundle F V] →
                                        {ι : Type u_7} →
                                          {s : ι → (x : M) → V x} →
                                            {u : Set M} →
                                              {x : M} →
                                                {n : WithTop ℕ∞} →
                                                  [VectorBundle 𝕜 F V] →
                                                    [FiniteDimensional 𝕜 F] →
                                                      IsLocalFrameOn I F n s u → x ∈ u → Fintype ι
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂).getKey! k = default
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainRingEquiv_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (e : M ≃+ N) (r : R) (m : M),
  (AddMonoidAlgebra.mapDomainRingEquiv R e) (AddMonoidAlgebra.single m r) = AddMonoidAlgebra.single (e m) r
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.D2_S : ∀ (z : UpperHalfPlane), EisensteinSeries.D2 ModularGroup.S z = 2 * ↑Real.pi * Complex.I / ↑z
-- Mathlib.NumberTheory.HeckeRing.Defs
HeckeCoset.instInhabited : {G : Type u_1} → [inst : Group G] → (Δ : Submonoid G) → (H₁ H₂ : Subgroup G) → Inhabited (HeckeCoset Δ H₁ H₂)
-- Std.Internal.Do.WP.Conjunctive
/-- `wp x` is sub-conjunctive: a meet of postconditions maps below the `wp` of their meet. A
healthiness condition of the `WP` interpretation; it holds for the base interpretations and lifts
through the transformers.  -/
Std.Internal.Do.WPConjunctive : (Prog : Type u) →
  (Value : outParam (Type v)) →
    (Pred : outParam (Type w)) →
      (EPred : outParam (Type z)) →
        [inst : Std.Internal.Do.Assertion Pred] →
          [inst_1 : Std.Internal.Do.Assertion EPred] → [Std.Internal.Do.WP Prog Value Pred EPred] → Prop
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    ChartedSpace.LiftPropWithinAt P g s x → (∀ y ∈ s, g' y = g y) → g' x = g x → ChartedSpace.LiftPropWithinAt P g' s x
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.continuous_fst : ∀ {𝕜 : Type u_3} {A : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A],
  Continuous fun x => x.toProd.1
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The identity modification.  -/
CategoryTheory.Lax.LaxTrans.Modification.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → (η : F ⟶ G) → CategoryTheory.Lax.LaxTrans.Modification η η
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.contains_string_eq_contains_toSlice : ∀ {pat : String} {s : String.Slice}, s.contains pat = s.contains pat.toSlice
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- `ToHom X Y` is the type of (bundled) functions between objects `X Y : C`.

This is an `abbrev` so that instances (e.g. `RingHomClass`) do not need to be redeclared.
 -/
CategoryTheory.ToHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [CategoryTheory.ConcreteCategory C FC] → C → C → Type u_1
-- Mathlib.Analysis.Complex.Norm
/-- The complex conjugate of a complex Cauchy sequence, as a complex Cauchy sequence.  -/
Complex.cauSeqConj : (CauSeq ℂ fun x => ‖x‖) → CauSeq ℂ fun x => ‖x‖
-- Mathlib.Analysis.Analytic.Basic
hasFPowerSeriesAt_iff' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜},
  HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in nhds z₀, HasSum (fun n => (z - z₀) ^ n • p.coeff n) (f z)
-- Mathlib.RingTheory.RingHom.Flat
CommRingCat.inl_injective_of_flat : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : R ⟶ T),
  (CommRingCat.Hom.hom f).Flat →
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom g) →
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inl f g))
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.biconeCategory : (J : Type u₁) → [CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.Category.{max u₁ v₁, u₁} (CategoryTheory.Bicone J)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.support.hcongr_5 : ∀ (V V' : Type u),
  V = V' →
    ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
      G ≍ G' →
        ∀ (u : V) (u' : V'),
          u ≍ u' →
            ∀ (v : V) (v' : V'), v ≍ v' → ∀ (a : G.Walk u v) (a' : G'.Walk u' v'), a ≍ a' → a.support ≍ a'.support
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.toNonarchAddGroupSeminorm : {G : Type u_6} → [inst : AddGroup G] → NonarchAddGroupNorm G → NonarchAddGroupSeminorm G
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- The multispan index obtained by applying a functor.  -/
CategoryTheory.Limits.MultispanIndex.map : {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] →
        {J : CategoryTheory.Limits.MultispanShape} →
          CategoryTheory.Limits.MultispanIndex J C →
            CategoryTheory.Functor C D → CategoryTheory.Limits.MultispanIndex J D
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Φ_ofNat : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ),
  W.Φ (↑n + 1) =
    (Polynomial.X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.sum : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {g' : α → F'} {l : Filter α} {ι : Type u_18} {A : ι → α → E'} {s : Finset ι},
  (∀ i ∈ s, A i =o[l] g') → (∑ i ∈ s, A i) =o[l] g'
-- Mathlib.Data.Int.Cast.Lemmas
Odd.intCast : ∀ {α : Type u_3} [inst : Ring α] {n : ℤ}, Odd n → Odd ↑n
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addEquiv_apply : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Add β] (a : α), e.addEquiv a = e a
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_ne_nil_iff : ∀ {m n : ℤ}, (m<...n).toArray ≠ #[] ↔ m + 1 < n
-- Std.Time.Format.Modifier
Std.Time.Modifier.F.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.F presentation) = 1 + sizeOf presentation
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.neg_right : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → IsCoprime x (-y)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
/-- The inclusion of a cell.  -/
HomotopicalAlgebra.RelativeCellComplex.Cells.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} → (γ : c.Cells) → B γ.j γ.i ⟶ Y
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.fromDFinsuppEquiv.eq_1 : ∀ {ι : Type uι} (κ : ι → Type uκ) (R : Type uR) {M : (i : ι) → κ i → Type uM} [inst : DecidableEq ι]
  [inst_1 : Fintype ι] [inst_2 : CommSemiring R] [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_4 : (i : ι) → (k : κ i) → Module R (M i k)] {N : Type u_1} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  [inst_7 : (i : ι) → DecidableEq (κ i)],
  MultilinearMap.fromDFinsuppEquiv κ R =
    LinearEquiv.ofLinearMap
      (LinearMap.compMultilinearMapₗ R ((DFinsupp.lsum ℕ) fun x => LinearMap.id) ∘ₗ MultilinearMap.dfinsuppFamilyₗ)
      (LinearMap.pi fun p => MultilinearMap.compLinearMapₗ fun i => DFinsupp.lsingle (p i)) ⋯ ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosMono.to_covariantClass_nonneg_mul_le : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulPosMono α],
  CovariantClass { x // 0 ≤ x } α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
-- Mathlib.LinearAlgebra.Finsupp.SumProd
Finsupp.fst_sumFinsuppLEquivProdFinsupp : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_7}
  {β : Type u_8} (f : α ⊕ β →₀ M) (x : α), ((Finsupp.sumFinsuppLEquivProdFinsupp R) f).1 x = f (Sum.inl x)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- An infinite place of the base field is unramified in a field extension if every
infinite place over it is unramified.  -/
NumberField.InfinitePlace.IsUnramifiedIn : {k : Type u_1} →
  [inst : Field k] → (K : Type u_2) → [inst_1 : Field K] → [Algebra k K] → NumberField.InfinitePlace k → Prop
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isExtTangentAt_comm : ∀ {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₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  s₁.IsExtTangentAt s₂ p ↔ s₂.IsExtTangentAt s₁ p