mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- Oplax functoriality.  -/
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (self : F.StrongTrans G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c)
  {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (self.app a) (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g).hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (self.app c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom h)))))
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- Homogeneous power series  -/
MvPowerSeries.IsHomogeneous : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → MvPowerSeries σ R → ℕ → Prop
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_sub_theta_le_psi_add_psi_add_psi : ∀ (x : ℝ),
  Chebyshev.psi x - Chebyshev.theta x ≤ Chebyshev.psi (x ^ 2⁻¹) + Chebyshev.psi (x ^ 3⁻¹) + Chebyshev.psi (x ^ 5⁻¹)
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
/-- Internal implementation detail of the iterator library.  -/
Std.Iterators.Types.TakeWhile.inner : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
        Std.Iterators.Types.TakeWhile α m β P → Std.IterM m β
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSet_zero_right : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {s t : Set Ω}, ProbabilityTheory.Kernel.IndepSet s t κ 0
-- Mathlib.AlgebraicTopology.CechNerve
/-- The product `Xᶥ` is the vertex of a limit cone on `wideCospan ι X`.  -/
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] →
      (ι : Type w) →
        [CategoryTheory.Limits.HasFiniteProducts C] →
          [Finite ι] → (X : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsRefl.flip_isRefl_iff : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.flip.IsRefl ↔ B.IsRefl
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.inf : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormula α n}, φ.IsQF → ψ.IsQF → (φ ⊓ ψ).IsQF
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.AddCommMonCat.Hom.mk.injEq : ∀ {A B : AddCommMonCat} (hom' hom'_1 : ↑A →+ ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Topology.Separation.Basic
strictMono_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], StrictMono nhdsSet
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.or.sizeOf_spec : sizeOf Std.Tactic.BVDecide.Gate.or = 1
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.mulAntidiagonal.congr_simp : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s s_1 : Set α}
  (e_s : s = s_1) {t t_1 : Set α} (e_t : t = t_1) (hs : s.IsPWO) (ht : t.IsPWO) (a a_1 : α),
  a = a_1 → Finset.mulAntidiagonal hs ht a = Finset.mulAntidiagonal ⋯ ⋯ a_1
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_div₀ : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → GroupWithZero (G i)] [inst_7 : GroupWithZero C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)]
  [∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x y : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h (x / y) =
    DirectLimit.lift f (fun x => ⇑(g x)) h x / DirectLimit.lift f (fun x => ⇑(g x)) h y
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.one_fin_three : ∀ {α : Type u} [inst : Zero α] [inst_1 : One α], 1 = !![1, 0, 0; 0, 1, 0; 0, 0, 1]
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.ext_iff : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
  π₁ = π₂ ↔ ∀ (J : BoxIntegral.Box ι), J ∈ π₁ ↔ J ∈ π₂
-- Mathlib.Algebra.MvPolynomial.Basic
/-- The finset of nonzero coefficients of a multivariate polynomial.  -/
MvPolynomial.coeffs : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → MvPolynomial σ R → Finset R
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- The image of an open immersion as an open set.  -/
AlgebraicGeometry.Scheme.Hom.opensRange : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [H : AlgebraicGeometry.IsOpenImmersion f] → Y.Opens
-- Mathlib.GroupTheory.IsSubnormal
/-- The whole additive subgroup `G` is subnormal in itself.  -/
AddSubgroup.IsSubnormal.top : ∀ {G : Type u_2} [inst : AddGroup G], ⊤.IsSubnormal
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.sub_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ - ν ≤ μ
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.smul_opposite_image_mul_preimage' : ∀ {G : Type u_2} [inst : Group G] (g : G) (h : Gᵐᵒᵖ) (s : Set G),
  (fun y => h • y) '' (fun x => g * x) ⁻¹' s = (fun x => g * x) ⁻¹' (fun y => h • y) '' s
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.dvd_C_mul : ∀ {R : Type u} {a : R} [inst : Field R] {p q : Polynomial R}, a ≠ 0 → (p ∣ Polynomial.C a * q ↔ p ∣ q)
-- Mathlib.RepresentationTheory.FDRep
/-- Lift an unbundled representation to `FDRep`.  -/
FDRep.of : {R : Type u} →
  {G : Type v} →
    [inst : CommRing R] →
      [inst_1 : Monoid G] →
        {V : Type u} →
          [inst_2 : AddCommGroup V] → [inst_3 : Module R V] → [Module.Finite R V] → Representation R G V → FDRep R G
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- The seminorm of a scalar multiplication is the product of the absolute value of the scalar
and the original seminorm.  -/
MulAlgebraNorm.smul' : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  (self : MulAlgebraNorm R S) (a : R) (x : S), self.toFun (a • x) = ‖a‖ * self.toFun x
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An object `X` is initial iff for every `Y` there is a unique morphism `X ⟶ Y`.  -/
CategoryTheory.Limits.isInitialEquivUnique : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{1}) C) →
      (X : C) →
        CategoryTheory.Limits.IsColimit
            { pt := X,
              ι := { app := fun X_1 => id (CategoryTheory.Discrete.casesOn X_1 fun as => ⋯.elim), naturality := ⋯ } } ≃
          ((Y : C) → Unique (X ⟶ Y))
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.eval_relabel : ∀ {α : Type u_1} {β : Type u_2} (r : α → β) (a : β → Bool) (f : Std.Sat.CNF α),
  Std.Sat.CNF.eval a (Std.Sat.CNF.relabel r f) = Std.Sat.CNF.eval (a ∘ r) f
-- Mathlib.RingTheory.Kaehler.Basic
/-- The quotient ring of `S ⊗ S ⧸ J ^ 2` by `Ω[S⁄R]` is isomorphic to `S` as an `S`-algebra.  -/
KaehlerDifferential.quotientCotangentIdeal : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸
              (KaehlerDifferential.ideal R S).cotangentIdeal) ≃ₐ[S]
            S
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Reachable.rfl : ∀ {V : Type u} [inst : Quiver V] {a : V}, Quiver.Reachable a a
-- Mathlib.FieldTheory.Cardinality
/-- Any infinite type can be endowed a field structure.  -/
Infinite.nonempty_field : ∀ {α : Type u} [Infinite α], Nonempty (Field α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Inhabited α] [inst_3 : BEq α]
  [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km : α}, Std.Internal.List.maxKey? l = some km → Std.Internal.List.getKey! km l = km
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_eq_zero : ∀ {o : Ordinal.{u_1}}, Cardinal.preBeth o = 0 ↔ o = 0
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.eval_zero_ae_eq_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P → ∀ᵐ (ω : Ω) ∂P, B 0 ω = 0
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.image_coe_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some '' Set.Iio a = Set.Iio ↑a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.localGeneratorsData_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.QuasicoherentData) (a : q.I), q.localGeneratorsData.X a = q.X a
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The bundled additive commutative monoid giving the filtered colimit of a diagram.  -/
AddCommMonCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J AddCommMonCat → AddCommMonCat
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
  IsDenseEmbedding e → ∀ (p : α → Prop), IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)
-- Mathlib.Order.CompactlyGenerated.Basic
/-- An element `k` of is compact if any set with `sSup`
above `k` has a finite subset with `sSup` above `k`.  -/
CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup : ∀ (α : Type u_2) [inst : CompleteLattice α] (k : α),
  IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderAddMonoidHom_apply : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G] (x : G),
  (LocallyFiniteOrder.orderAddMonoidHom G) x = (LocallyFiniteOrder.addMonoidHom G) x
-- Mathlib.Algebra.Order.Field.Power
/-- For any `a > 1` and a natural `n` we have `n ≤ a ^ n / (a - 1)`. See also
`Nat.cast_le_pow_sub_div_sub` for a stronger inequality with `a ^ n - 1` in the numerator.  -/
Nat.cast_le_pow_div_sub : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  1 < a → ∀ (n : ℕ), ↑n ≤ a ^ n / (a - 1)
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigits.eq_1 : ∀ {b : ℕ} (digits : ℕ → Fin b), Real.ofDigits digits = ∑' (n : ℕ), Real.ofDigitsTerm digits n
-- Mathlib.Order.CountableDenseLinearOrder
/-- A partial isomorphism between `α` and `β` is also a partial isomorphism between `β` and `α`.  -/
Order.PartialIso.comm : {α : Type u_1} →
  {β : Type u_2} → [inst : LinearOrder α] → [inst_1 : LinearOrder β] → Order.PartialIso α β → Order.PartialIso β α
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (i : ℕ) (hi : i ≤ len)
  (s : aig.RefVec i) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [inst_3 : Std.Sat.AIG.RefVec.LawfulMapOperator α f]
  (idx : ℕ) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.map.go aig i hi s input f).aig.decls.size),
  (Std.Sat.AIG.RefVec.map.go aig i hi s input f).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Order.Filter.Pi
/-- The indexed product of a (possibly, infinite) family of principal filters
is generated by the finite `Set.pi` cylinders.

If the index type is finite, then the indexed product of principal filters
is a principal filter, see `pi_principal`.  -/
Filter.mem_pi_principal : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : (i : ι) → Set (α i)} {t : Set ((i : ι) → α i)},
  (t ∈ Filter.pi fun i => Filter.principal (s i)) ↔ ∃ I, I.Finite ∧ I.pi s ⊆ t
-- Mathlib.Algebra.GroupWithZero.Opposite
AddOpposite.instSemigroupWithZero : {α : Type u_1} → [SemigroupWithZero α] → SemigroupWithZero αᵃᵒᵖ
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.prod_rootFormIn_smul_coroot_mem_range_PolarizationIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : Module S N] [IsScalarTower S R N] [inst_12 : P.IsValuedIn S]
  [inst_13 : Fintype ι] (i : ι),
  (∏ j, ((P.RootFormIn S) (P.rootSpanMem S j)) (P.rootSpanMem S j)) • P.coroot i ∈ (P.PolarizationIn S).range
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {I : J → Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] →
            {D : CategoryTheory.Functor J C} →
              {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} →
                {k l : CategoryTheory.Limits.ColimitPresentation.Total P} →
                  (base : k.fst ⟶ l.fst) →
                    (hom : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd) →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base) =
                            CategoryTheory.CategoryStruct.comp hom ((P l.fst).ι.app l.snd))
                          CategoryTheory.Limits.ColimitPresentation.Total.Hom.w._autoParam →
                        k.Hom l
-- Mathlib.Order.Filter.Prod
Filter.bot_coprod : ∀ {α : Type u_1} {β : Type u_2} (l : Filter β), ⊥.coprod l = Filter.comap Prod.snd l
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
/-- Given `data : SpectralSequenceDataCore ι c r₀`, this is the property
that on the page `r₀`, indices `i₀` and `i₁` are equal,
and indices `i₂` and `i₃` are equal. This condition allows
to express the objects of the `r₀`th page of the spectral sequences
obtained using a spectral object `X` indexed by `ι` and `data` as objects
of the form `X.H`, see `SpectralObject.spectralSequenceFirstPageXIso`.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation : {ι : Type u_2} →
  {κ : Type u_3} →
    [inst : Preorder ι] →
      {c : ℤ → ComplexShape κ} → {r₀ : ℤ} → CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀ → Prop
-- Mathlib.Data.Nat.Bits
Nat.shiftLeft'.eq_2 : ∀ (b : Bool) (m n : ℕ), Nat.shiftLeft' b m n.succ = Nat.bit b (Nat.shiftLeft' b m n)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.State.exprToNCSemiringId : Lean.Meta.Grind.Arith.CommRing.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ
-- Mathlib.RingTheory.Teichmuller
Perfection.coeff_zero_symm_quotientMulEquiv : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] (x : Perfection (R ⧸ I) p),
  (Perfection.coeffMonoidHom R p 0) ((Perfection.quotientMulEquiv p I).symm x) = (Perfection.teichmuller₀ p I) x
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.equiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y : C} [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] {m : M}
  (f : CategoryTheory.Localization.SmallShiftedHom W X Y m),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W L) f =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.SmallHom.equiv W L) f)
      ((CategoryTheory.Functor.commShiftIso L m).app Y).hom
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negY_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (X Y Z : R),
  W'.negY ![X, Y, Z] = -Y - W'.a₁ * X - W'.a₃ * Z
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toListRev_zip_of_finite_left : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {it₂ : Std.Iter β₂} [Std.Iterators.Finite α₁ Id] [Std.Iterators.Productive α₂ Id],
  (it₁.zip it₂).toListRev = (it₁.toList.zip (Std.Iter.take it₁.toList.length it₂).toList).reverse
-- Init.Data.Array.Lemmas
Array.sum_append : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Add α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulLeftIdentity (fun x1 x2 => x1 + x2) 0] {as₁ as₂ : Array α}, (as₁ ++ as₂).sum = as₁.sum + as₂.sum
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntryD.eq_1 : ∀ {α : Type u} {β : Type v} (x : α × β),
  Std.DTreeMap.Internal.Impl.Const.minEntryD Std.DTreeMap.Internal.Impl.leaf x = x
-- Mathlib.Tactic.GCongr.Core
/-- The given priority of the lemma, for example as `@[gcongr high]`.  -/
Mathlib.Tactic.GCongr.GCongrLemma.prio : Mathlib.Tactic.GCongr.GCongrLemma → ℕ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.MapsTo.mul : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β},
  Set.MapsTo f₁ A B₁ → Set.MapsTo f₂ A B₂ → Set.MapsTo (f₁ * f₂) A (B₁ * B₂)
-- Mathlib.Data.List.Sublists
_private.Mathlib.Data.List.Sublists.0.List.sublistsLenAux.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : ℕ → List α → (List α → β) → List β → Sort u_3) (n : ℕ) (x : List α → β)
  (r : List β) (h_1 : (x : List α) → (f : List α → β) → (r : List β) → motive 0 x f r)
  (h_2 : (n : ℕ) → (x : List α → β) → (r : List β) → motive n.succ [] x r)
  (h_3 : (n : ℕ) → (a : α) → (l : List α) → (f : List α → β) → (r : List β) → motive n.succ (a :: l) f r),
  (match n.succ, [], x, r with
    | 0, x, f, r => h_1 x f r
    | n.succ, [], x, r => h_2 n x r
    | n.succ, a :: l, f, r => h_3 n a l f r) =
    h_2 n x r
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.All.eq_2 : ∀ {α : Type u_1} (p : α → Prop) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  RBTree.RBNode.All p (RBTree.RBNode.node c l v r) = (p v ∧ RBTree.RBNode.All p l ∧ RBTree.RBNode.All p r)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_X : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (i : data.I₀),
  data.toPreOneHypercover.X i = F.obj (data.X i)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
min_mul_of_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {c : R} [MulPosMono R] (a b : R),
  0 ≤ c → min a b * c = min (a * c) (b * c)
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
/-- Any finite basis of a module can express it as the base change
of a finite free module from any under-ring.  -/
IsBaseChange.of_fintype_basis : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (A : Type u_3)
  [inst_3 : CommSemiring A] [inst_4 : Algebra A R] [inst_5 : Module A V] [inst_6 : IsScalarTower A R V] {ι : Type u_4}
  (b : Module.Basis ι R V) [inst_7 : Fintype ι], IsBaseChange R (Fintype.linearCombination A ⇑b)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_left_as : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G)
  (g : CategoryTheory.StructuredArrow f.right F),
  ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).right.left.as = PUnit.unit
-- Mathlib.Order.RelSeries
RelSeries.map_apply : ∀ {α : Type u_1} {r : SetRel α α} {β : Type u_2} {s : SetRel β β} (p : RelSeries r) (f : r.Hom s)
  (i : Fin (p.length + 1)), (p.map f).toFun i = f (p.toFun i)
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.directLimitCocone_pt_carrier : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι] (G : ι → Type v)
  [inst_3 : (i : ι) → AddCommGroup (G i)] [inst_4 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_5 : DirectedSystem G fun i j h => ⇑(f i j h)], ↑(ModuleCat.directLimitCocone G f).pt = Module.DirectLimit G f
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- Let `A', A, B', B` be subgroups of `G`. If `A' ≤ B'` and `A ≤ B`, then there is a
map `A / (A' ⊓ A) →+ B / (B' ⊓ B)` induced by the inclusions.  -/
QuotientAddGroup.quotientMapAddSubgroupOfOfLe : {G : Type u} →
  [inst : AddGroup G] →
    {A' A B' B : AddSubgroup G} →
      [_hAN : (A'.addSubgroupOf A).Normal] →
        [_hBN : (B'.addSubgroupOf B).Normal] → A' ≤ B' → A ≤ B → ↥A ⧸ A'.addSubgroupOf A →+ ↥B ⧸ B'.addSubgroupOf B
-- Mathlib.Order.Nucleus
Nucleus.instCompleteLatticeElemRangeCoe : {X : Type u_1} → [inst : Order.Frame X] → {n : Nucleus X} → CompleteLattice ↑(Set.range ⇑n)
-- Init.Grind.AC
Lean.Grind.AC.Context.mk.inj : ∀ {α : Sort u} {vars : Lean.RArray (PLift α)} {op : α → α → α} {vars_1 : Lean.RArray (PLift α)} {op_1 : α → α → α},
  { vars := vars, op := op } = { vars := vars_1, op := op_1 } → vars = vars_1 ∧ op = op_1
-- Mathlib.CategoryTheory.Comma.Basic
/-- A natural transformation `L₁ ⟶ L₂` induces a functor `Comma L₂ R ⥤ Comma L₁ R`.  -/
CategoryTheory.Comma.mapLeft : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (R : CategoryTheory.Functor B T) →
              {L₁ L₂ : CategoryTheory.Functor A T} →
                (L₁ ⟶ L₂) → CategoryTheory.Functor (CategoryTheory.Comma L₂ R) (CategoryTheory.Comma L₁ R)