mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- **Alias** of `CategoryTheory.Functor.map_isPullback`. -/
CategoryTheory.IsPullback.map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan h i) F],
  CategoryTheory.IsPullback f g h i → CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.mk.inj : ∀ {ref : Lean.Syntax} {hasExpose : Bool} {cls : Lean.Term} {ref_1 : Lean.Syntax} {hasExpose_1 : Bool}
  {cls_1 : Lean.Term},
  { ref := ref, hasExpose := hasExpose, cls := cls } = { ref := ref_1, hasExpose := hasExpose_1, cls := cls_1 } →
    ref = ref_1 ∧ hasExpose = hasExpose_1 ∧ cls = cls_1
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_pow_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, (p ^ n).natDegree ≤ n * p.natDegree
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.adjoint_innerₛₗ_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (x : E), LinearMap.adjoint ((innerₛₗ 𝕜) x) = LinearMap.toSpanSingleton 𝕜 E x
-- Std.Data.Internal.Cut
Std.Internal.IsCut.lt : ∀ {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering} [self : Std.Internal.IsCut cmp cut] {k k' : α},
  cut k' = Ordering.lt → cmp k' k = Ordering.lt → cut k = Ordering.lt
-- Mathlib.NumberTheory.Transcendental.Liouville.Basic
Liouville.exists_pos_real_of_irrational_root : ∀ {α : ℝ},
  Irrational α →
    ∀ {f : Polynomial ℤ},
      f ≠ 0 →
        Polynomial.eval α (Polynomial.map (algebraMap ℤ ℝ) f) = 0 →
          ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instAddLeftMono : ∀ {α : Type u_4} {β : Type u_5} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  AddLeftMono (ProbabilityTheory.Kernel α β)
-- Init.Core
iff_of_eq : ∀ {a b : Prop}, a = b → (a ↔ b)
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
alternatingGroup.map_kleinFour_conj : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset α),
  s.card = 4 →
    ∀ (g : ↥(alternatingGroup α)),
      Subgroup.map (alternatingGroup.ofSubtype (g • s)) (alternatingGroup.kleinFour ↥(g • s)) =
        MulAut.conj g • Subgroup.map (alternatingGroup.ofSubtype s) (alternatingGroup.kleinFour ↥s)
-- Mathlib.Order.SuccPred.Basic
WithTop.instIsEmptyPredOrderOfNonempty : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] [hα : Nonempty α], IsEmpty (PredOrder (WithTop α))
-- Mathlib.Topology.Algebra.ConstMulAction
/-- **Alias** of `isClosed_setOfPred_map_smul`. -/
isClosed_setOf_map_smul : ∀ {M : Type u_1} {N : Type u_4} (α : Type u_5) (β : Type u_6) [inst : SMul M α] [inst_1 : SMul N β]
  [inst_2 : TopologicalSpace β] [T2Space β] [ContinuousConstSMul N β] (σ : M → N),
  IsClosed {f | ∀ (c : M) (x : α), f (c • x) = σ c • f x}
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.toMulRingNorm : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} → [inst_1 : Ring S] → [inst_2 : Algebra R S] → MulAlgebraNorm R S → MulRingNorm S
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instNormedSpaceLieAddGroup : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], LieAddGroup (modelWithCornersSelf 𝕜 E) n E
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- Take `Y` to be `iSup U` and obtain a presieve over `iSup U`.  -/
TopCat.Presheaf.presieveOfCovering : {X : TopCat} → {ι : Type v} → (U : ι → TopologicalSpace.Opens ↑X) → CategoryTheory.Presieve (iSup U)
-- Std.Do.PostCond
Std.Do.ExceptConds.fst_imp : ∀ {ps : Std.Do.PostShape} {ε : Type u} {x₁ x₂ : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)},
  (x₁ →ₑ x₂).1 = fun e => spred(x₁.1 e → x₂.1 e)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- Use the axiom of choice to extract explicit `ColimitCocone F` from `HasColimit F`.  -/
CategoryTheory.Limits.getColimitCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) → [CategoryTheory.Limits.HasColimit F] → CategoryTheory.Limits.ColimitCocone F
-- Init.Data.Int.DivMod.Lemmas
Int.le_ediv_of_mul_le : ∀ {a b c : ℤ}, 0 < c → a * c ≤ b → a ≤ b / c
-- Init.System.IO
/-- Configuration for the process' stderr handle.  -/
IO.Process.StdioConfig.stderr : IO.Process.StdioConfig → IO.Process.Stdio
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.completedSinZeta.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.completedSinZeta a s = (HurwitzZeta.hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.equivAwayAdjoinRoot.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R),
  P.equivAwayAdjoinRoot =
    AlgEquiv.ofAlgHom
      (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯)
      (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯) ⋯ ⋯
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_coe_toNNReal : ∀ {a : ENNReal}, a ≠ ⊤ → Filter.Tendsto ENNReal.ofNNReal (nhds a.toNNReal) (nhds a)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.freeVarFinset.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (x l : ℕ) (_R : L.Relations l)
  (ts : Fin l → L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.rel _R ts).freeVarFinset = Finset.univ.biUnion fun i => (ts i).varFinsetLeft
-- Mathlib.RingTheory.Bialgebra.GroupLike
/-- Group-like elements in a bialgebra are stable under power.  -/
IsGroupLikeElem.pow : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] {a : A} {n : ℕ},
  IsGroupLikeElem R a → IsGroupLikeElem R (a ^ n)
-- Init.Data.AC
Lean.Data.AC.Context.eval_toList : ∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α) (e : Lean.Data.AC.Expr),
  Lean.Data.AC.evalList α ctx e.toList = Lean.Data.AC.eval α ctx e
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.congr' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f f₁ : E → F} {f' : F}
  {s : Set E} {x v : E},
  HasLineDerivWithinAt 𝕜 f f' s x v → Set.EqOn f₁ f s → x ∈ s → HasLineDerivWithinAt 𝕜 f₁ f' s x v
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.prod : ∀ {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Finset α},
  (∀ x ∈ s, f x ≡ g x [MOD n]) → ∏ x ∈ s, f x ≡ ∏ x ∈ s, g x [MOD n]
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.cdf_expMeasure_eq_integral : ∀ {r : ℝ},
  0 < r →
    ∀ (x : ℝ),
      ↑(ProbabilityTheory.cdf (ProbabilityTheory.expMeasure r)) x =
        ∫ (x : ℝ) in Set.Iic x, ProbabilityTheory.exponentialPDFReal r x
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.sqLe_mul : ∀ {d x y z w : ℕ},
  (Zsqrtd.SqLe x 1 y d → Zsqrtd.SqLe z 1 w d → Zsqrtd.SqLe (x * w + y * z) d (x * z + d * y * w) 1) ∧
    (Zsqrtd.SqLe x 1 y d → Zsqrtd.SqLe w d z 1 → Zsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
      (Zsqrtd.SqLe y d x 1 → Zsqrtd.SqLe z 1 w d → Zsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
        (Zsqrtd.SqLe y d x 1 → Zsqrtd.SqLe w d z 1 → Zsqrtd.SqLe (x * w + y * z) d (x * z + d * y * w) 1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_insertMany_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ} {k : α},
  k ∈ m → k ∈ Std.ExtDHashMap.Const.insertMany m l
-- Init.Data.SInt.Bitwise
ISize.neg_one_and : ∀ {a : ISize}, -1 &&& a = a
-- Mathlib.FieldTheory.Finite.Basic
/-- **Fermat's Little Theorem**: for all `n : ℕ` coprime to `p`, we have
`(n ^ (p - 1) - 1) % p = 0`.  -/
Nat.pow_card_sub_one_sub_one_mod_card : ∀ {p : ℕ}, Nat.Prime p → ∀ {n : ℕ}, n.Coprime p → (n ^ (p - 1) - 1) % p = 0
-- Mathlib.Analysis.Normed.Group.Defs
ENormedMonoid.mk : {E : Type u_8} →
  [inst : TopologicalSpace E] →
    [toESeminormedMonoid : ESeminormedMonoid E] → (∀ (x : E), ‖x‖ₑ = 0 ↔ x = 1) → ENormedMonoid E
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
/-- Auxiliary definition for `CategoryTheory.Functor.closed`.
The internal hom functor `F ⟶[C] -`  -/
CategoryTheory.Functor.closedIhom : {D : Type u} →
  {C : Type u_1} →
    [inst : CategoryTheory.Groupoid D] →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalClosed C] →
            CategoryTheory.Functor D C →
              CategoryTheory.Functor (CategoryTheory.Functor D C) (CategoryTheory.Functor D C)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_symm_app : ∀ {S : SSet} (n : SimplexCategory) (x : S.obj (Opposite.op n)) (α : (SSet.stdSimplex.obj n).obj (Opposite.op n)),
  (CategoryTheory.ConcreteCategory.hom ((SSet.yonedaEquiv.symm x).app (Opposite.op n))) α =
    (CategoryTheory.ConcreteCategory.hom (S.map (SSet.stdSimplex.objEquiv α).op)) x
-- Init.Data.Nat.Basic
Nat.max_def : ∀ {n m : ℕ}, max n m = if n ≤ m then m else n
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.existsUnique : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T → ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- A variant of `IsHausdorff.StrictMono.funext`, where the target is a ring instead of a module.
 -/
IsHausdorff.StrictMono.funext' : ∀ {R : Type u_6} {S : Type u_7} [inst : CommRing S] (I : Ideal S) [IsHausdorff I S] {f g : R → S} {a : ℕ → ℕ},
  StrictMono a → (∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (f r) = (Ideal.Quotient.mk (I ^ a n)) (g r)) → f = g
-- Init.Data.UInt.Basic
/-- The modulo operator for word-sized unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `USize.mod 5 2 = 1`
* `USize.mod 4 2 = 0`
* `USize.mod 4 0 = 4`
 -/
USize.mod : USize → USize → USize
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.mk.inj : ∀ {label : String} {detail? : Option String} {documentation? : Option Lean.Lsp.MarkupContent}
  {kind? : Option Lean.Lsp.CompletionItemKind} {textEdit? : Option Lean.Lsp.InsertReplaceEdit}
  {sortText? : Option String} {data? : Option Lean.Json} {tags? : Option (Array Lean.Lsp.CompletionItemTag)}
  {label_1 : String} {detail?_1 : Option String} {documentation?_1 : Option Lean.Lsp.MarkupContent}
  {kind?_1 : Option Lean.Lsp.CompletionItemKind} {textEdit?_1 : Option Lean.Lsp.InsertReplaceEdit}
  {sortText?_1 : Option String} {data?_1 : Option Lean.Json} {tags?_1 : Option (Array Lean.Lsp.CompletionItemTag)},
  { label := label, detail? := detail?, documentation? := documentation?, kind? := kind?, textEdit? := textEdit?,
        sortText? := sortText?, data? := data?, tags? := tags? } =
      { label := label_1, detail? := detail?_1, documentation? := documentation?_1, kind? := kind?_1,
        textEdit? := textEdit?_1, sortText? := sortText?_1, data? := data?_1, tags? := tags?_1 } →
    label = label_1 ∧
      detail? = detail?_1 ∧
        documentation? = documentation?_1 ∧
          kind? = kind?_1 ∧ textEdit? = textEdit?_1 ∧ sortText? = sortText?_1 ∧ data? = data?_1 ∧ tags? = tags?_1
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddRightCancelSemigroup : {α : Type u_1} → [AddRightCancelSemigroup α] → AddRightCancelSemigroup (Lex α)
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The `R`-module whose elements are functions `ι → A` which are zero on all but finitely many
elements of `ι` has a coalgebra structure. The coproduct `Δ` is given by `Δ(fᵢ a) = fᵢ a₁ ⊗ fᵢ a₂`
where `Δ(a) = a₁ ⊗ a₂` and the counit `ε` by `ε(fᵢ a) = ε(a)`, where `fᵢ a` is the function sending
`i` to `a` and all other elements of `ι` to zero.  -/
Finsupp.instCoalgebra : (R : Type u) →
  (ι : Type v) →
    (A : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [Coalgebra R A] → Coalgebra R (ι →₀ A)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.continuous_pow : ∀ (f : CircleDeg1Lift), Continuous ⇑f → ∀ (n : ℕ), Continuous ⇑(f ^ n)
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
/-- The `ith` reflection as a term of the Weyl group.  -/
RootPairing.weylGroup.ofIdx : {ι : 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) → ι → ↥P.weylGroup
-- Lean.Server.RequestCancellation
Lean.Server.MonadCancellable : (Type → Type v) → Type v
-- Init.Control.Lawful.MonadLift.Basic
/-- Lifting preserves `pure`  -/
LawfulMonadLiftT.monadLift_pure : ∀ {m : Type u → Type v} {n : Type u → Type w} {inst : Monad m} {inst_1 : Monad n} {inst_2 : MonadLiftT m n}
  [self : LawfulMonadLiftT m n] {α : Type u} (a : α), monadLift (pure a) = pure a
-- Mathlib.Order.CompleteLattice.Basic
sSup_apply_eq_sSup_image : ∀ {α : Type u_8} {β : α → Type u_9} [inst : (i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α},
  sSup s a = sSup (Function.eval a '' s)
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.aeval_eq_sum : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : MvPowerSeries.HasEval a)
  (f : MvPowerSeries σ R),
  (MvPowerSeries.aeval ha) f = ∑' (d : σ →₀ ℕ), (MvPowerSeries.coeff d) f • d.prod fun s e => a s ^ e
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.uniformContinuous_map : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) (f : α → β), UniformContinuous (pkg.map pkg' f)
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSum_symm_lof_tmul : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type v₁}
  {ι₂ : Type v₂} [inst_3 : DecidableEq ι₁] [inst_4 : DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂}
  [inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [inst_6 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)]
  [inst_7 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_8 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_9 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_10 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁)
  (i₂ : ι₂) (m₂ : M₂ i₂),
  (TensorProduct.directSum R S M₁ M₂).symm
      ((DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) =
    (DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.divLeft_toEquiv : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G] (c : G), (IsometryEquiv.divLeft c).toEquiv = Equiv.divLeft c
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flip_flip : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂),
  K.flip.flip = K
-- Mathlib.Analysis.CStarAlgebra.Basic
norm_star : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E] (x : E),
  ‖star x‖ = ‖x‖
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_base : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X x x_1 : F.Grothendieck}
  (f : X.Hom x) (g : x.Hom x_1),
  (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
-- Mathlib.Data.Fin.Basic
Fin.ofNat_eq_cast : ∀ (n : ℕ) [inst : NeZero n] (a : ℕ), Fin.ofNat n a = ↑a
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.mk : {G : Type u_1} →
  [inst : CommGroup G] →
    (toSubmonoid : Submonoid G) → (∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1) → GroupCone G
-- Mathlib.RingTheory.WittVector.Teichmuller
_private.Mathlib.RingTheory.WittVector.Teichmuller.0.WittVector.ghostComponent_teichmullerFun : ∀ (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (r : R) (n : ℕ),
  (WittVector.ghostComponent n) (WittVector.teichmullerFun p r) = r ^ p ^ n
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.Total.ext_iff : ∀ {V : Type u} {inst : Quiver V} {x y : Quiver.Total V}, x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.hom ≍ y.hom
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- Given `x : R`, `LocalizedModule.Away x M` is the localization of `M` at the
submonoid generated by `x`.  -/
LocalizedModule.Away : {R : Type u_1} →
  [inst : CommSemiring R] → R → (M : Type u_2) → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_1 u_2)
-- Mathlib.Algebra.Module.Presentation.Tensor
/-- Given solutions in `M₁` and `M₂` to systems of linear equations, this is the obvious
solution to the tensor product of these systems in `M₁ ⊗[A] M₂`.  -/
Module.Relations.Solution.tensor : {A : Type u} →
  [inst : CommRing A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module A M₁] →
              [inst_4 : Module A M₂] →
                {relations₁ : Module.Relations A} →
                  {relations₂ : Module.Relations A} →
                    relations₁.Solution M₁ →
                      relations₂.Solution M₂ → (relations₁.tensor relations₂).Solution (TensorProduct A M₁ M₂)
-- Init.Data.Fin.Fold
Fin.foldlM_succ : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : α → Fin (n + 1) → m α),
  Fin.foldlM (n + 1) f = fun x => f x 0 >>= Fin.foldlM n fun x j => f x j.succ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_if : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} {ι : Type u_4} {x : ι} {B : Set ι} {A : Set α} [inst_2 : Decidable (x ∈ B)],
  v (if x ∈ B then A else ∅) = B.indicator (fun x => v A) x
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
summable_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  Summable (fun x => 0) L
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.instInhabitedState : Inhabited Lean.Parser.ParserExtension.State
-- Lean.Meta.Constructions.NoConfusion
Lean.mkNoConfusion : Lean.Name → Lean.MetaM Unit
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.eq_1 : ∀ (p q : ℝ), p.HolderConjugate q = p.HolderTriple q 1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof : Type
-- Init.Data.Nat.Div.Basic
Nat.add_mod_left : ∀ (x z : ℕ), (x + z) % x = z % x
-- Mathlib.Topology.MetricSpace.Similarity
/-- If two triangles have two pairs of proportional adjacent sides, then the triangles are similar.
 -/
similar_of_dist_mul_eq_dist_mul_eq : ∀ {P₁ : Type u_3} {P₂ : Type u_4} [inst : PseudoMetricSpace P₁] [inst_1 : PseudoMetricSpace P₂] {a b c : P₁}
  {a' b' c' : P₂},
  dist a b ≠ 0 →
    dist a' b' ≠ 0 →
      dist a b * dist b' c' = dist b c * dist a' b' →
        dist a b * dist c' a' = dist c a * dist a' b' → Similar ![a, b, c] ![a', b', c']
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitFVar : Lean.Expr → Lean.MetaM Lean.Meta.LetToHave.Result✝
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {l : List (α × β)} {k : α}
  (h₁ : (List.map Prod.fst l).contains k = false)
  {h' : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k h' =
    Std.DHashMap.Internal.Raw₀.Const.get m k ⋯
-- Mathlib.Logic.Equiv.Basic
Equiv.coe_subtypeEquiv_eq_map : ∀ {X : Sort u_9} {Y : Sort u_10} {p : X → Prop} {q : Y → Prop} (e : X ≃ Y) (h : ∀ (x : X), p x ↔ q (e x)),
  ⇑(e.subtypeEquiv h) = Subtype.map ⇑e ⋯
-- Init.Data.Option.Basic
/-- Applies a function in some applicative functor to an optional value, returning `none` with no
effects if the value is missing.

Runs a monadic function `f` on an optional value, returning the result. If the optional value is
`none`, the function is not called and the result is also `none`.

From the perspective of `Option` as a container with at most one element, this is analogous to
`List.mapM`, returning the result of running the monadic function on all elements of the container.

This function only requires `m` to be an applicative functor. An alias `Option.mapA` is provided.
 -/
Option.mapM : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Applicative m] → (α → m β) → Option α → m (Option β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_apply_of_contains_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF)
  (h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl = true),
  (f k (t.get k ⋯)).isSome = true
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.ext_iff : ∀ {R : Type u} {S : Type v} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S} {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} {inst_3 : CommRing R'} {inst_4 : CommRing S'} {inst_5 : Algebra R' S'}
  {P' : Algebra.Extension R' S'} {inst_6 : Algebra R R'} {inst_7 : Algebra S S'} {x y : P.Hom P'},
  x = y ↔ x.toRingHom = y.toRingHom
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakPullback.lift_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.lift h k w)
      (CategoryTheory.Limits.weakPullback.fst f g) =
    h
-- Mathlib.Topology.MetricSpace.Gluing
Metric.glueDist.eq_1 : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x_2 y : X), Metric.glueDist Φ Ψ ε (Sum.inl x_2) (Sum.inl y) = dist x_2 y
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
_private.Mathlib.RingTheory.Polynomial.Resultant.Basic.0.Polynomial.sylvesterDeriv_of_natDegree_eq_three : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} (hf : f.natDegree = 3),
  (Matrix.reindex (finCongr ⋯) (finCongr ⋯)) f.sylvesterDeriv =
    !![f.coeff 0, 0, 1 * f.coeff 1, 0, 0;
      f.coeff 1, f.coeff 0, 2 * f.coeff 2, 1 * f.coeff 1, 0;
      f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, 1 * f.coeff 1;
      f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2;
      0, 1, 0, 0, 3]