mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.prod_mulIndicator_eq_prod_inter : ∀ {ι : Type u_1} {β : Type u_4} [inst : CommMonoid β] [inst_1 : DecidableEq ι] (s t : Finset ι) (f : ι → β),
  ∏ i ∈ s, (↑t).mulIndicator f i = ∏ i ∈ s ∩ t, f i
-- Mathlib.Algebra.Group.End
/-- `Equiv.Perm.sigmaCongrRight` as a `MonoidHom`.

This is particularly useful for its `MonoidHom.range` projection, which is the subgroup of
permutations which do not exchange elements between fibers.  -/
Equiv.Perm.sigmaCongrRightHom : {α : Type u_7} → (β : α → Type u_8) → ((a : α) → Equiv.Perm (β a)) →* Equiv.Perm ((a : α) × β a)
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
/-- The canonical embedding from a tensor power to the tensor algebra  -/
TensorPower.toTensorAlgebra : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {n : ℕ} → TensorPower R n M →ₗ[R] TensorAlgebra R M
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionTriggerKind : Type
-- Mathlib.Order.Monotone.Defs
StrictAntiOn.antitoneOn : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → AntitoneOn f s
-- Init.Data.SInt.Basic
instOrOpInt64 : OrOp Int64
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_iInf : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {ι : Sort u_9} [Nonempty ι] {p : ι → Submodule R M} (f : M →ₛₗ[σ₁₂] M₂),
  Function.Injective ⇑f → Submodule.map f (⨅ i, p i) = ⨅ i, Submodule.map f (p i)
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
TensorialAt.add : ∀ {𝕜 : 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] {A : Type u_9} [inst_13 : AddCommGroup A]
  [inst_14 : Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M},
  TensorialAt I F Φ x → ∀ {σ σ' : (x : M) → V x}, MDiffAt (T% σ) x → MDiffAt (T% σ') x → Φ (σ + σ') = Φ σ + Φ σ'
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.fiber_map : ∀ (R : Type u) [inst : CommRing R] (Ω : Type w) [inst_1 : Field Ω] [inst_2 : Algebra R Ω]
  {S T : (CommAlgCat.FiniteEtale R)ᵒᵖ} (f : S ⟶ T),
  (CommAlgCat.FiniteEtale.fiber R Ω).map f = FintypeCat.homMk fun x => AlgHom.comp x (CommAlgCat.Hom.hom f.unop.hom)
-- Mathlib.Data.Matrix.Block
/-- Let `p` pick out certain rows and columns of a square matrix `M`. Then
`toSquareBlockProp M p` is the corresponding block matrix.  -/
Matrix.toSquareBlockProp : {m : Type u_2} → {α : Type u_12} → Matrix m m α → (p : m → Prop) → Matrix { a // p a } { a // p a } α
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If `C` is filtered, and we have a functor `R : C ⥤ D` with a left adjoint, then `D` is filtered.
 -/
CategoryTheory.IsFiltered.of_right_adjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor D C} {R : CategoryTheory.Functor C D}
  (h : L ⊣ R), CategoryTheory.IsFiltered D
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The forgetful functor from `LocallyRingedSpace` to `SheafedSpace CommRing`.  -/
AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace : CategoryTheory.Functor AlgebraicGeometry.LocallyRingedSpace (AlgebraicGeometry.SheafedSpace CommRingCat)
-- Mathlib.Topology.VectorBundle.Basic
/-- A continuous linear equivalence between the fiber at `b` and the model fiber,
induced by the preferred trivialisation at each `b`.  -/
VectorBundle.continuousLinearEquivAt : (R : Type u_1) →
  {B : Type u_2} →
    (F : Type u_3) →
      (E : B → Type u_4) →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)] →
                      [inst_7 : (x : B) → TopologicalSpace (E x)] →
                        [inst_8 : FiberBundle F E] → [VectorBundle R F E] → (b : B) → E b ≃L[R] F
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.restoreCont : Lean.Elab.Do.ControlStack → Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont
-- Mathlib.Order.Lattice
instAssociativeMax_mathlib : ∀ {α : Type u} [inst : SemilatticeSup α], Std.Associative fun x1 x2 => x1 ⊔ x2
-- Lean.Parser.Command
/-- `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions.  -/
Lean.Parser.Command.declModifiers : Bool → Lean.Parser.Parser
-- Mathlib.Algebra.Order.ToIntervalMod
AddCommGroup.modEq_iff_toIcoDiv_eq_toIocDiv_add_one : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_15.eq_3 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithTerminal Cᵒᵖ) → (x ⟶ y) → Sort u_3)
  (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y)) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op x)) (CategoryTheory.WithTerminal.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op unop)) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => h_2 unop x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_3 x
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.nullMeasurableSet_iff_eventuallyMeasurableSet : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α),
  MeasureTheory.NullMeasurableSet s μ ↔ EventuallyMeasurableSet m0 (MeasureTheory.ae μ) s
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.smul_subset_self : ∀ {S : Type u_1} {R : Type u_2} {M : Type u_3} [inst : SetLike S M] [inst_1 : SMul R M] [SMulMemClass S R M] (r : R)
  (s : S), r • ↑s ⊆ ↑s
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.instProductive : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] [inst_1 : Std.IteratorAccess α m]
  [inst_2 : Monad m] [Std.Iterators.Productive α m],
  Std.Iterators.Productive (Std.Iterators.Types.StepSizeIterator α m β) m
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffWithinAt.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℂ n f s x → ContDiffWithinAt ℂ n (fun x => Complex.cosh (f x)) s x
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.uncurry_curryLeft : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂),
  f.curryLeft.uncurryLeft = f
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.insert k).minD fallback = t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {inst : Add A} {inst_1 : Add B} {inst_2 : Mul A} {inst_3 : Mul B}
  {inst_4 : SMul R A} {inst_5 : SMul R B} {inst_6 : Star A} {inst_7 : Star B} {toStarRingEquiv : A ≃⋆+* B}
  {map_smul' : ∀ (r : R) (a : A), toStarRingEquiv.toFun (r • a) = r • toStarRingEquiv.toFun a}
  {toStarRingEquiv_1 : A ≃⋆+* B}
  {map_smul'_1 : ∀ (r : R) (a : A), toStarRingEquiv_1.toFun (r • a) = r • toStarRingEquiv_1.toFun a},
  { toStarRingEquiv := toStarRingEquiv, map_smul' := map_smul' } =
      { toStarRingEquiv := toStarRingEquiv_1, map_smul' := map_smul'_1 } →
    toStarRingEquiv = toStarRingEquiv_1
-- Std.Http.Data.Headers.Value
Std.Http.Header.instBEqValue : BEq Std.Http.Header.Value
-- Init.Data.Format.Basic
Std.Format.FlattenBehavior.fill.sizeOf_spec : sizeOf Std.Format.FlattenBehavior.fill = 1
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.eval_sumIDeriv_of_pos : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R] [NoZeroDivisors R] (p : Polynomial R) {q : ℕ},
  0 < q →
    ∃ gp,
      gp.natDegree ≤ p.natDegree - q ∧
        ∀ (r : R) {p' : Polynomial R},
          p = (Polynomial.X - Polynomial.C r) ^ (q - 1) * p' →
            Polynomial.eval r (Polynomial.sumIDeriv p) =
              (q - 1).factorial • Polynomial.eval r p' + q.factorial • Polynomial.eval r gp
-- Mathlib.Data.List.Range
List.isChain_range : ∀ (r : ℕ → ℕ → Prop) (n : ℕ), List.IsChain r (List.range n) ↔ ∀ m < n - 1, r m m.succ
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.comapEq_trans : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β γ : Type w} {f g h : β → γ} (k : f = g) (l : g = h),
  CategoryTheory.GradedObject.comapEq C ⋯ =
    CategoryTheory.GradedObject.comapEq C k ≪≫ CategoryTheory.GradedObject.comapEq C l
-- Mathlib.Analysis.Normed.Module.Ball.Action
isScalarTower_closedBall_closedBall_closedBall : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [inst_5 : NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E],
  IsScalarTower ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.imp_eq_cert : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Var → Bool
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Given `act : (a = a') → hb₁ → hb₂ → ... → hbₙ → goal` where `hb₁, ..., hbₙ` are hypotheses
obtained when unpacking existential quantifiers with variables from `exs`, it proves `goal` using
`Exists.elim`. We use this to prove implication in the forward direction.  -/
ExistsAndEq.withExistsElimAlongPath : {u : Lean.Level} →
  {α : Q(Sort u)} →
    {P goal : Q(Prop)} →
      Q(«$P») →
        {a a' : Q(«$α»)} →
          List ExistsAndEq.VarQ →
            ExistsAndEq.Path → (Q(«$a» = «$a'») → List ExistsAndEq.HypQ → Lean.MetaM Q(«$goal»)) → Lean.MetaM Q(«$goal»)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDFReal_mul : ∀ {μ : ℝ} {v : NNReal} {c : ℝ},
  c ≠ 0 →
    ∀ (x : ℝ),
      ProbabilityTheory.gaussianPDFReal μ v (c * x) =
        |c⁻¹| * ProbabilityTheory.gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (c ^ 2)⁻¹ ⋯ * v) x
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.inducedMap_comp_assoc : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {R S : 𝒮} {a : 𝒳} {b b' : HasFibers.Fib p R} (f : R ⟶ S)
  (ψ : (HasFibers.ι R).obj b' ⟶ a) [inst_3 : p.IsCartesian f ψ] (φ : (HasFibers.ι R).obj b ⟶ a)
  [inst_4 : p.IsHomLift f φ] {Z : 𝒳} (h : a ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HasFibers.ι R).map (HasFibers.inducedMap f ψ φ))
      (CategoryTheory.CategoryStruct.comp ψ h) =
    CategoryTheory.CategoryStruct.comp φ h
-- Mathlib.RingTheory.Ideal.Defs
Ideal.IsTwoSided.mk : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, (∀ {a : α} (b : α), a ∈ I → a * b ∈ I) → I.IsTwoSided
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.neg_nsmul_eq_nsmul_neg : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) (n : ℕ), ↑(-(n • a)) = n • ↑(-a)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreDivSMulChar'.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ : ↥S),
  OreLocalization.oreDivSMulChar' r₁ r₂ s₁ s₂ = ⟨OreLocalization.oreNum r₁ s₂, ⟨OreLocalization.oreDenom r₁ s₂, ⋯⟩⟩
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE._auto_3),
  (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.opcycles f₂ f₃ n₁
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The morphism `m` in a factorisation `f = e ≫ m` through a monomorphism is uniquely
determined.  -/
CategoryTheory.Limits.MonoFactorisation.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F F' : CategoryTheory.Limits.MonoFactorisation f} (hI : F.I = F'.I),
  F.m = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hI) F'.m → F = F'
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_le_maxVar : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y}
  {x y : X ⊕ Y}, f ∈ GromovHausdorff.candidates X Y → f (x, y) ≤ ↑(GromovHausdorff.maxVar✝ X Y)
-- Lean.Elab.Tactic.Simp
/-- The result of elaborating a full array of simp arguments and applying them to the simp context.
 -/
Lean.Elab.Tactic.ElabSimpArgsResult : Type
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_vadd_right_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P} {v : V}, v ∈ s.direction → (s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y)
-- Mathlib.CategoryTheory.Adjunction.Evaluation
/-- The adjunction showing that evaluation is a left adjoint.  -/
CategoryTheory.evaluationAdjunctionLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] →
          (c : C) → (CategoryTheory.evaluation C D).obj c ⊣ CategoryTheory.evaluationRightAdjoint D c
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.zeroLocus_bot : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3},
  MvPolynomial.zeroLocus K ⊥ = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.comp_whiskerLeft_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {τ τ' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} (γ : τ ⟶ τ')
  {Z : CategoryTheory.Limits.CatCospanTransform F G F''' G'''} (h : (ψ.comp φ).comp τ' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft (ψ.comp φ) γ) h =
    CategoryTheory.CategoryStruct.comp (ψ.associator φ τ).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ
          (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ γ))
        (CategoryTheory.CategoryStruct.comp (ψ.associator φ τ').inv h))
-- Mathlib.RingTheory.Congruence.Basic
RingCon.subsingleton_iff : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R], Subsingleton (RingCon R) ↔ Subsingleton R
-- Mathlib.Order.Filter.Finite
Filter.biInter_finset_mem : ∀ {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} (is : Finset β), ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
-- Lean.MonadEnv
Lean.findModuleOf? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m (Option Lean.Name)
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteBooleanAlgebra.mk : {α : Type u_1} →
  [toCompleteLattice : CompleteLattice α] →
    (∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z) →
      [toCompl : Compl α] →
        [toSDiff : SDiff α] →
          [toHImp : HImp α] →
            (∀ (x : α), x ⊓ xᶜ ≤ ⊥) →
              (∀ (x : α), ⊤ ≤ x ⊔ xᶜ) →
                autoParam (∀ (x y : α), x \ y = x ⊓ yᶜ) BooleanAlgebra.sdiff_eq._autoParam →
                  autoParam (∀ (x y : α), x ⇨ y = y ⊔ xᶜ) BooleanAlgebra.himp_eq._autoParam → CompleteBooleanAlgebra α
-- Mathlib.Data.FunLike.Graded
/-- A graded isomorphism descends to an isomorphism on each component.  -/
Graded.equiv : {E : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_4} →
        {τ : Type u_5} →
          {ι : Type u_6} →
            [inst : SetLike σ A] →
              [inst_1 : SetLike τ B] →
                {𝒜 : ι → σ} →
                  {ℬ : ι → τ} → [inst_2 : EquivLike E A B] → [GradedEquivLike E 𝒜 ℬ] → E → (i : ι) → ↥(𝒜 i) ≃ ↥(ℬ i)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- Given two restricted products `Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁]` and
`Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂]` of additive monoids, `RestrictedProduct.mapAlongAddMonoidHom`
gives an additive monoid homomorphism between them. The data needed is a function `f : ι₂ → ι₁` such
that `𝓕₂` tends to `𝓕₁` along `f`, and additive monoid homomorphisms `φ j : R₁ (f j) → R₂ j`
sending `B₁ (f j)` into `B₂ j` for an `𝓕₂`-large set of `j`'s.  -/
RestrictedProduct.mapAlongAddMonoidHom : {ι₁ : Type u_3} →
  {ι₂ : Type u_4} →
    (R₁ : ι₁ → Type u_5) →
      (R₂ : ι₂ → Type u_6) →
        {𝓕₁ : Filter ι₁} →
          {𝓕₂ : Filter ι₂} →
            {S₁ : ι₁ → Type u_7} →
              {S₂ : ι₂ → Type u_8} →
                [inst : (i : ι₁) → SetLike (S₁ i) (R₁ i)] →
                  [inst_1 : (j : ι₂) → SetLike (S₂ j) (R₂ j)] →
                    {B₁ : (i : ι₁) → S₁ i} →
                      {B₂ : (j : ι₂) → S₂ j} →
                        (f : ι₂ → ι₁) →
                          Filter.Tendsto f 𝓕₂ 𝓕₁ →
                            [inst_2 : (i : ι₁) → AddMonoid (R₁ i)] →
                              [inst_3 : (i : ι₂) → AddMonoid (R₂ i)] →
                                [inst_4 : ∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] →
                                  [inst_5 : ∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)] →
                                    (φ : (j : ι₂) → R₁ (f j) →+ R₂ j) →
                                      (∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)) →
                                        RestrictedProduct (fun i => R₁ i) (fun i => ↑(B₁ i)) 𝓕₁ →+
                                          RestrictedProduct (fun j => R₂ j) (fun j => ↑(B₂ j)) 𝓕₂
-- Mathlib.Order.OrderDual
OrderDual.instTrichotomousLt : ∀ {α : Type u_1} [inst : LT α] [T : Std.Trichotomous LT.lt], Std.Trichotomous LT.lt
-- Batteries.Data.List.Basic
List.instInterOfBEq_batteries : {α : Type u_1} → [BEq α] → Inter (List α)
-- Init.Data.Int.Gcd
Int.gcd_mul_lcm : ∀ (m n : ℤ), m.gcd n * m.lcm n = m.natAbs * n.natAbs
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.isoZeroBiprod_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero X),
  (CategoryTheory.Limits.isoZeroBiprod hY).inv = CategoryTheory.Limits.biprod.snd
-- Std.Data.HashMap.RawLemmas
/-- Simpler variant of `getElem?_filter` when `LawfulBEq` is available.  -/
Std.HashMap.Raw.getElem?_filter' : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α]
  {f : α → β → Bool} {k : α}, m.WF → (Std.HashMap.Raw.filter f m)[k]? = Option.filter (f k) m[k]?
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.eq_neg_addConst_add : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote' ctx p = Int.Internal.Linear.Poly.denote' ctx (p.addConst (-p.getConst)) + p.getConst
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_nonpos : ∀ {x : ℝ}, Real.arcsin x ≤ 0 ↔ x ≤ 0
-- Batteries.Data.HashMap.Basic
/-- Make a new hash map with the specified capacity.  -/
Batteries.mkHashMap : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → optParam ℕ 0 → Batteries.HashMap α β
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.unitIso_inv_app_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] (X : Action V G),
  (Action.FunctorCategoryEquivalence.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulReflectLT_iff : ∀ (α : Type u_1) [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  PosMulReflectLT α ↔ ContravariantClass { x // 0 ≤ x } α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
-- Mathlib.MeasureTheory.Integral.TorusIntegral
_private.Mathlib.MeasureTheory.Integral.TorusIntegral.0.term___ : Lean.TrailingParserDescr