mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.dvd_count_of_dvd_count_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {a b : Associates α},
  b ≠ 0 →
    ∀ {p : Associates α},
      Irreducible p →
        (∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) →
          ∀ {k : ℕ}, k ∣ p.count (a * b).factors → k ∣ p.count a.factors
-- Mathlib.RingTheory.Perfection
PerfectionMap.equiv_apply : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₃}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π)
  (x : P), m.equiv x = ((Perfection.lift p P R) π) x
-- Init.Data.Nat.Lemmas
Nat.pred_eq_of_eq_succ : ∀ {m n : ℕ}, m = n.succ → m.pred = n
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.map_nhds_eq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (a : A), Filter.map (⇑e) (nhds a) = nhds (e a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forM_eq_forM_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → m PUnit.{w + 1}}, (forM t fun a => f a.1) = t.keys.forM f
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.pushLine : Lean.PrettyPrinter.FormatterM Unit
-- Lean.Server.InfoUtils
Lean.Elab.instBEqHoverableInfoPrio : BEq Lean.Elab.HoverableInfoPrio
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.card_right : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G},
  AddSubgroup.IsComplement (↑H) T → Nat.card ↑T = H.index
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isEmbedding_coe_of_top : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  Topology.IsEmbedding DFunLike.coe
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.basisAt.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {M : Type u_4} [inst_1 : TopologicalSpace M] {F : Type u_5}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_5 : (x : M) → AddCommGroup (V x)]
  [inst_6 : (x : M) → Module 𝕜 (V x)] [inst_7 : (x : M) → TopologicalSpace (V x)] [inst_8 : FiberBundle F V]
  [inst_9 : VectorBundle 𝕜 F V] {ι : Type u_7} {x : M} (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj)
  (e_e : e = e_1) [inst_10 : MemTrivializationAtlas e] (b b_1 : Module.Basis ι 𝕜 F),
  b = b_1 → ∀ (hx : x ∈ e.baseSet), e.basisAt b hx = e_1.basisAt b_1 ⋯
-- Mathlib.CategoryTheory.Filtered.Connected
CategoryTheory.IsCofilteredOrEmpty.isPreconnected : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C],
  CategoryTheory.IsPreconnected C
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w n : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go aig distance curr acc =
    if curr < n - 1 then
      let res :=
        Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.twoPowShift aig
          { n := n, lhs := acc, rhs := distance, pow := curr + 1 };
      let aig_1 := res.aig;
      have acc_1 := res.vec;
      have this := ⋯;
      have distance := distance.cast this;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go aig_1 distance (curr + 1) acc_1
    else { aig := aig, vec := acc }
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) [X.IsGE n] [X.IsLE n],
  ∃ Y, Nonempty (X ≅ (DerivedCategory.singleFunctor C n).obj Y)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
List.tail.eq_2 : ∀ {α : Type u} (a : α) (as : List α), (a :: as).tail = as
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.mkIso_inv : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (e : ρ.Equiv σ), (Rep.mkIso e).inv = Rep.ofHom ↑e.symm
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_comp_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u_4} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (x : AdicCompletion I M),
  (AdicCompletion.map I g) ((AdicCompletion.map I f) x) = (AdicCompletion.map I (g ∘ₗ f)) x
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.rangeIcc_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i) (i : ι),
  (f.rangeIcc g) i = Finset.Icc (f i) (g i)
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.closure.congr_simp : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] (f f_1 : E →ₗ.[R] F), f = f_1 → f.closure = f_1.closure
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_fstX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij)
      (HomologicalComplex.homotopyCofiber.fstX φ j i hij) =
    CategoryTheory.CategoryStruct.id (F.X i)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.max_const : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : α → ℝ} {Kf : NNReal},
  LipschitzWith Kf f → ∀ (a : ℝ), LipschitzWith Kf fun x => max (f x) a
-- Mathlib.Order.BooleanAlgebra.Basic
Pi.instGeneralizedBooleanAlgebra : {ι : Type u_2} →
  {α : ι → Type u_3} → [(i : ι) → GeneralizedBooleanAlgebra (α i)] → GeneralizedBooleanAlgebra ((i : ι) → α i)
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_self : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (V : Submodule R M), Submodule.restrictScalars R V = V
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.ExtractMonadResult.mk.injEq : ∀ (m returnType expectedType m_1 returnType_1 expectedType_1 : Lean.Expr),
  ({ m := m, returnType := returnType, expectedType := expectedType } =
      { m := m_1, returnType := returnType_1, expectedType := expectedType_1 }) =
    (m = m_1 ∧ returnType = returnType_1 ∧ expectedType = expectedType_1)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.tensor_hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {F G H : CategoryTheory.MonoidalCategory.DayFunctor C V}
  {α β : CategoryTheory.MonoidalCategoryStruct.tensorObj F G ⟶ H},
  (∀ (x y : C),
      CategoryTheory.CategoryStruct.comp ((F.η G).app (x, y))
          (α.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
        CategoryTheory.CategoryStruct.comp ((F.η G).app (x, y))
          (β.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))) →
    α = β
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.contMDiff_transContinuousLinearEquiv_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] {M' : Type u_10}
  [inst_11 : TopologicalSpace M'] [inst_12 : ChartedSpace H' M'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] F) {f : M → M'},
  ContMDiff (I.transContinuousLinearEquiv e) I' n f ↔ ContMDiff I I' n f
-- Lean.Server.RequestCancellation
Lean.Server.MonadCancellable.mk : {m : Type → Type v} → m PUnit.{1} → Lean.Server.MonadCancellable m
-- Mathlib.RingTheory.RingHom.Locally
RingHom.locally_iff_span_eq_top : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {R S : Type u}
  [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f ↔
    Ideal.span {g | P ((algebraMap S (Localization.Away g)).comp f)} = ⊤
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to a `UInt16`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toUInt16 : Float32.Model → UInt16
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_coe_nnreal_restrict : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α NNReal) (s : Set α),
  MeasureTheory.SimpleFunc.map NNReal.toReal (f.restrict s) = (MeasureTheory.SimpleFunc.map NNReal.toReal f).restrict s
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instInfSet : {R : Type u} →
  {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → InfSet (LieSubalgebra R L)
-- Aesop.Forward.State
Aesop.RawHyp.patSubst.sizeOf_spec : ∀ (subst : Aesop.Substitution), sizeOf (Aesop.RawHyp.patSubst subst) = 1 + sizeOf subst
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`.  -/
CategoryTheory.Center.tensorUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Center C
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.map.eq_1 : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W' : WeierstrassCurve.Affine R) (f : R →+* S),
  WeierstrassCurve.Affine.CoordinateRing.map W' f =
    AdjoinRoot.lift ((AdjoinRoot.of (W'.map f).polynomial).comp (Polynomial.mapRingHom f))
      (AdjoinRoot.root (W'.map f).polynomial) ⋯
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.centralAlgebraMul.congr_simp : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V) {z z_1 : MonoidAlgebra A G} (e_z : z = z_1)
  (hz : z ∈ Submonoid.center (MonoidAlgebra A G)),
  Representation.IntertwiningMap.centralAlgebraMul ρ hz = Representation.IntertwiningMap.centralAlgebraMul ρ ⋯
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_subLeft_nhds : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G},
  Filter.map (fun x => c - x) (nhds a) = nhds (c - a)
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.instInhabited : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → [Inhabited ι] → Inhabited (BumpCovering ι X s)
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- An integral domain is equal to the intersection of its localizations at all its maximal ideals
viewed as subalgebras of its field of fractions.  -/
MaximalSpectrum.iInf_localization_eq_bot : ∀ (R : Type u_4) [inst : CommRing R] [inst_1 : IsDomain R] (K : Type u_5) [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K], ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Asymptotically, the logarithmic counting function for the poles of `f + g` is less than or equal to
the sum of the logarithmic counting functions for the poles of `f` and `g`, respectively.
 -/
ValueDistribution.logCounting_add_top_eventuallyLE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E},
  Meromorphic f₁ →
    Meromorphic f₂ →
      ValueDistribution.logCounting (f₁ + f₂) ⊤ ≤ᶠ[Filter.atTop]
        ValueDistribution.logCounting f₁ ⊤ + ValueDistribution.logCounting f₂ ⊤
-- Mathlib.Data.Seq.Defs
_private.Mathlib.Data.Seq.Defs.0.Stream'.Seq.«term_~_» : Lean.TrailingParserDescr
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^32 - 1` for natural numbers greater than or equal to `2^32`.
 -/
UInt32.ofNatClamp : ℕ → UInt32
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.matrix_strictMono_of_nonempty : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype n] [Nonempty n],
  StrictMono (RingCon.matrix n)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.containsKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α), Std.Internal.List.containsKey a [] = false
-- Init.Data.List.Find
List.find?_replicate_of_length_pos : ∀ {n : ℕ} {α : Type u_1} {p : α → Bool} {a : α},
  0 < n → List.find? p (List.replicate n a) = if p a = true then some a else none
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The diagram
```
v.adicCompletionIntegers ℚ  ----->  ℤ_[primesEquiv v]
      |                               |
      |                               |
      v                               v
v.adicCompletion ℚ  ------------->  ℚ_[primesEquiv v]
```
commutes.  -/
Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v)),
  ↑((Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv v) x) =
    (Rat.HeightOneSpectrum.adicCompletion.padicEquiv v) ↑x
-- Mathlib.CategoryTheory.HomCongr
CategoryTheory.Iso.homCongr_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂)
  (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃) (f : X₁ ⟶ Y₁),
  ((α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂)) f = ((α₁.homCongr β₁).trans (α₂.homCongr β₂)) f
-- Mathlib.Algebra.Quandle
Quandle.dihedralAct.inv : ∀ (n : ℕ) (a : ZMod n), Function.Involutive (Quandle.dihedralAct n a)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Grind.CommRing.Poly.denoteExpr : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → Lean.Grind.CommRing.Poly → M Lean.Expr
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)},
  CategoryTheory.yonedaEquiv =
    {
      toFun := fun η =>
        (CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op X))) (CategoryTheory.CategoryStruct.id X),
      invFun := fun ξ =>
        { app := fun x => TypeCat.ofHom fun f => (CategoryTheory.ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ,
          naturality := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_mem_set : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} [WellFoundedLT ι] {m : ι},
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → u (MeasureTheory.hittingBtwn u s n m ω) ω ∈ s
-- Mathlib.LinearAlgebra.Dual.Defs
Module.apply_evalEquiv_symm_apply : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.IsReflexive R M] (f : Module.Dual R M) (g : Module.Dual R (Module.Dual R M)),
  f ((Module.evalEquiv R M).symm g) = g f
-- Lean.Elab.InfoTree.Main
Lean.Elab.FieldRedeclInfo.format : Lean.Elab.ContextInfo → Lean.Elab.FieldRedeclInfo → Std.Format
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
CategoryTheory.preservesLimits_preadditiveYonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : C),
  CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveYonedaObj X)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.logDeriv_cosh : logDeriv Complex.cosh = Complex.tanh
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = false ↔ ∃ a, a ∈ t)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_single_target : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K),
  (NumberField.mixedEmbedding.fundamentalCone.expMap_single w).target = Set.Ioi 0
-- Lean.Elab.Term.TermElabM
/-- Snapshot after finishing execution of a tactic.  -/
Lean.Elab.Tactic.TacticFinishedSnapshot : Type
-- Lean.Server.GoTo
Lean.Server.GoToKind : Type
-- Mathlib.GroupTheory.Nilpotent
/-- A subgroup is nilpotent iff its lower central series (computed in the ambient group) eventually
vanishes.  -/
Subgroup.isNilpotent_iff_lowerCentralSeries : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G), Group.IsNilpotent ↥S ↔ ∃ n, S.lowerCentralSeries n = ⊥
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.instPreservesColimitsOfShapeStructuredArrowUnderToUnderOfIsConnectedOfHasColimitsOfShape : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D} {B : D}
  [CategoryTheory.IsConnected J] [CategoryTheory.Limits.HasColimitsOfShape J C]
  [CategoryTheory.Limits.PreservesColimitsOfShape J K],
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.StructuredArrow.toUnder B K)
-- Mathlib.Combinatorics.Hindman
/-- The weak form of **Hindman's theorem**: in any finite
cover of a nonempty additive semigroup, one of the parts contains an FS-set.  -/
Hindman.exists_FS_of_finite_cover : ∀ {M : Type u_1} [inst : AddSemigroup M] [Nonempty M] (s : Set (Set M)),
  s.Finite → ⊤ ⊆ ⋃₀ s → ∃ c ∈ s, ∃ a, Hindman.FS a ⊆ c
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.postcompIsoOfIso_inv_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E] {A : Type u_5}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C D A) {G G' : CategoryTheory.Functor D E} (e : G ≅ G') [inst_6 : G.CommShift A]
  [inst_7 : G'.CommShift A] [inst_8 : CategoryTheory.NatTrans.CommShift e.hom A] (a : A) (X : C),
  ((F.postcompIsoOfIso e).inv.hom a).app X = e.inv.app ((F.functor a).obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The functor `C ⥤ (Type w)ᵒᵖ ⥤ C` which sends `X : C` and `α : Type w` to
the product of copies of `X` indexed by `α`.  -/
CategoryTheory.Limits.piFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasProducts C] → CategoryTheory.Functor C (CategoryTheory.Functor Type wᵒᵖ C)
-- Mathlib.Topology.EMetricSpace.Weak
/-- If `α` has a topology induced by a linear order and is a weak pseudo extended metric space,
so is `WithTop α`  -/
instWeakPseudoEMetricSpaceWithTop : {α : Type u} →
  [t : TopologicalSpace α] →
    [inst : LinearOrder α] →
      [inst_1 : OrderTopology α] → [m : WeakPseudoEMetricSpace α] → WeakPseudoEMetricSpace (WithTop α)
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The subalgebra of `C(UnitAddTorus d, ℂ)` generated by `mFourier n` for `n ∈ ℤᵈ` separates
points.  -/
UnitAddTorus.mFourierSubalgebra_separatesPoints : ∀ {d : Type u_1} [inst : Fintype d], (UnitAddTorus.mFourierSubalgebra d).SeparatesPoints
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- Construct a pointed cone from closure under two-element conical combinations.
I.e., a nonempty set closed under two-element conical combinations is a pointed cone.  -/
PointedCone.ofConeComb : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : Module R E] →
              (C : Set E) →
                C.Nonempty →
                  (∀ x ∈ C, ∀ y ∈ C, ∀ (a : R), 0 ≤ a → ∀ (b : R), 0 ≤ b → a • x + b • y ∈ C) → PointedCone R E
-- Mathlib.Algebra.Order.Interval.Basic
Interval.neg_bot : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α], -⊥ = ⊥