mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.nonneg_iff_eq_sqrt_mul_sqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A}, 0 ≤ a ↔ a = CFC.sqrt a * CFC.sqrt a
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.nsmul_vadd_mem_closure_vadd : ∀ {M : Type u_3} [inst : AddMonoid M] {N : Type u_7} [inst_1 : AddCommMonoid N] [inst_2 : AddAction M N]
  [VAddAssocClass M N N] (r : M) (s : Set N) {x : N},
  x ∈ AddSubmonoid.closure s → ∃ n, n • r +ᵥ x ∈ AddSubmonoid.closure (r +ᵥ s)
-- Init.Data.Int.Gcd
Int.le_lcm_left : ∀ {b : ℤ} (a : ℤ), b ≠ 0 → a ≤ ↑(a.lcm b)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.mk : Lean.Meta.Grind.GoalState → Lean.MVarId → Lean.Meta.Grind.Goal
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
GroupLieAlgebra.bracket_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] (v w : GroupLieAlgebra I G),
  ⁅v, w⁆ = VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.lift_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = 0) [CategoryTheory.Mono k],
  CategoryTheory.Mono (CategoryTheory.Limits.kernel.lift f k h)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly.beq_spec : ∀ (x x_1 : Lean.Grind.CommRing.Poly),
  (x == x_1) =
    match x, x_1 with
    | Lean.Grind.CommRing.Poly.num a, Lean.Grind.CommRing.Poly.num b => a == b
    | Lean.Grind.CommRing.Poly.add a a_1 a_2, Lean.Grind.CommRing.Poly.add b b_1 b_2 =>
      a == b && (a_1 == b_1 && a_2 == b_2)
    | x, x_2 => false
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {fallback : α},
  (t.insertIfNew k v).minKeyD fallback = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Lean.Parser.Term
/-- `debug_assert! cond` panics if `cond` evaluates to `false` and the executing code has been built
with debug assertions enabled (see the `debugAssertions` option).
 -/
Lean.Parser.Term.debugAssert : Lean.Parser.Parser
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_comp_star : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A)
  [ContinuousMapZero.UniqueHom R A],
  autoParam (ContinuousOn f (star '' quasispectrum R a)) cfcₙ_comp_star._auto_1 →
    autoParam (f 0 = 0) cfcₙ_comp_star._auto_3 →
      autoParam (p a) cfcₙ_comp_star._auto_5 → cfcₙ (fun x => f (star x)) a = cfcₙ f (star a)
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.div_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s t : Set G},
  IsOpen t → IsOpen (s / t)
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsMulApplyEqComp.mul_apply_eq_comp`. -/
mul_apply_eq_comp : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : Mul F} [self : IsMulApplyEqComp F α]
  (f g : F) (x : α), (f * g) x = f (g x)
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLike_injective : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜],
  Function.Injective (ContinuousMap.realToRCLike 𝕜)
-- Init.Prelude
instMaxUInt32 : Max UInt32
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuousWithinAt_iff_preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} {x : α}
  [inst_1 : TopologicalSpace β],
  UpperHemicontinuousWithinAt f s x ↔ ∀ u ∈ nhdsSet (f x), f ⁻¹' Set.Iic u ∈ nhdsWithin x s
-- Mathlib.Data.Fintype.Sets
Set.toFinset_sdiff : ∀ {α : Type u_1} (s t : Set α) [inst : DecidableEq α] [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t]
  [inst_3 : Fintype ↑(s \ t)], (s \ t).toFinset = s.toFinset \ t.toFinset
-- Mathlib.Data.Nat.Init
Nat.one_le_pow' : ∀ (n m : ℕ), 1 ≤ (m + 1) ^ n
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Mon.mul.go : ℕ → Nat.Internal.SOM.Mon → Nat.Internal.SOM.Mon → Nat.Internal.SOM.Mon
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.classified : ∀ {x y z : ℤ} (h : PythagoreanTriple x y z), h.IsClassified
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.instHAppendArraySyntax : HAppend Lean.Parser.SyntaxStack (Array Lean.Syntax) Lean.Parser.SyntaxStack
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.mk.inj : ∀ {symm : Bool} {proof type : Lean.Expr} {index : Lean.HeadIndex × ℕ}
  {mvarIds : Array (Lean.MVarId × Array Lean.LocalDecl)} {symm_1 : Bool} {proof_1 type_1 : Lean.Expr}
  {index_1 : Lean.HeadIndex × ℕ} {mvarIds_1 : Array (Lean.MVarId × Array Lean.LocalDecl)},
  { symm := symm, proof := proof, type := type, index := index, mvarIds := mvarIds } =
      { symm := symm_1, proof := proof_1, type := type_1, index := index_1, mvarIds := mvarIds_1 } →
    symm = symm_1 ∧ proof = proof_1 ∧ type = type_1 ∧ index = index_1 ∧ mvarIds = mvarIds_1
-- Lean.Server.References
Lean.Server.References.ParentDecl.mk.injEq : ∀ (name : String) (range selectionRange : Lean.Lsp.Range) (name_1 : String) (range_1 selectionRange_1 : Lean.Lsp.Range),
  ({ name := name, range := range, selectionRange := selectionRange } =
      { name := name_1, range := range_1, selectionRange := selectionRange_1 }) =
    (name = name_1 ∧ range = range_1 ∧ selectionRange = selectionRange_1)
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
/-- Explicit formula for the derivative of the Gamma function at positive integers, in terms of
harmonic numbers and the Euler-Mascheroni constant `γ`.  -/
Real.deriv_Gamma_nat : ∀ (n : ℕ), deriv Real.Gamma (↑n + 1) = ↑n.factorial * (-Real.eulerMascheroniConstant + ↑(harmonic n))
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instAddGroupWithOne : {R : Type u_1} → [AddGroupWithOne R] → AddGroupWithOne Rᵐᵒᵖ
-- Mathlib.RingTheory.Polynomial.GaussLemma
/-- **Gauss's Lemma** for `ℤ` states that a primitive integer polynomial is irreducible iff it is
irreducible over `ℚ`.  -/
Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast : ∀ {p : Polynomial ℤ}, p.IsPrimitive → (Irreducible p ↔ Irreducible (Polynomial.map (Int.castRingHom ℚ) p))
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The iterated derivative within a set of the composition with a linear equiv on the left is
obtained by applying the linear equiv to the iterated derivative. This is true without
differentiability assumptions.  -/
ContinuousLinearEquiv.iteratedFDerivWithin_comp_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} (g : F ≃L[𝕜] G) (f : E → F),
  UniqueDiffOn 𝕜 s →
    x ∈ s →
      ∀ (i : ℕ),
        iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Homomorphism from a connected component graph to the original graph.  -/
SimpleGraph.ConnectedComponent.toSimpleGraph_hom : {V : Type u} → {G : SimpleGraph V} → (C : G.ConnectedComponent) → C.toSimpleGraph →g G
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.comp_units_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type w}
  [inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] {X Y Z : C} (f : X ⟶ Y) (r : Rˣ) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instAdd : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] → [inst_4 : Module R M₂] → Add (MultilinearMap R M₁ M₂)
-- Mathlib.Geometry.Euclidean.Basic
/-- The squared distance between points on a line (expressed as a
multiple of a fixed vector added to a point) and another point,
expressed as a quadratic.  -/
EuclideanGeometry.dist_smul_vadd_sq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (r : ℝ) (v : V) (p₁ p₂ : P),
  dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ =
    inner ℝ v v * r * r + 2 * inner ℝ v (p₁ -ᵥ p₂) * r + inner ℝ (p₁ -ᵥ p₂) (p₁ -ᵥ p₂)
-- Mathlib.Data.Multiset.Powerset
Multiset.revzip_powersetAux : ∀ {α : Type u_1} {l : List α} ⦃x : Multiset α × Multiset α⦄, x ∈ (Multiset.powersetAux l).revzip → x.1 + x.2 = ↑l
-- Mathlib.Topology.Continuous
mem_closure_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X}
  {x : X}, ContinuousAt f x → x ∈ closure s → f x ∈ closure (f '' s)
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.tosInfHom : {α : Type u_8} →
  {β : Type u_9} → [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → CompleteLatticeHom α β → sInfHom α β
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rci_eq_mkSlice_rco_min : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ},
  Std.Rci.Sliceable.mkSlice xs lo...* = Std.Rco.Sliceable.mkSlice xs (min lo xs.size)...xs.size
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂'_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : C)
  {X Y : C} (φ : X ⟶ Y),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' C).obj X₁).obj X₂).map φ =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₂)
-- Mathlib.Topology.NhdsWithin
nhdsWithin_biUnion : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_5} {I : Set ι},
  I.Finite → ∀ (s : ι → Set α) (a : α), nhdsWithin a (⋃ i ∈ I, s i) = ⨆ i ∈ I, nhdsWithin a (s i)
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.add : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : SeminormedAddCommGroup Y] {C C' r : NNReal}
  {f g : X → Y}, HolderWith C r f → HolderWith C' r g → HolderWith (C + C') r (f + g)
-- Mathlib.Algebra.Group.Defs
NPow.toPow : {M : Type u_2} → [NPow M] → Pow M ℕ
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- A condition for `padicValRat p (n₁ / d₁) ≤ padicValRat p (n₂ / d₂)`, in terms of
divisibility by `p^n`.  -/
padicValRat.padicValRat_le_padicValRat_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n₁ n₂ d₁ d₂ : ℤ},
  n₁ ≠ 0 →
    n₂ ≠ 0 →
      d₁ ≠ 0 →
        d₂ ≠ 0 →
          (padicValRat p (Rat.divInt n₁ d₁) ≤ padicValRat p (Rat.divInt n₂ d₂) ↔
            ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁)
-- Std.Data.HashSet.Lemmas
/-- This is a restatement of `mem_insert` that is written to exactly match the proof obligation
in the statement of `get_insert`.  -/
Std.HashSet.mem_of_mem_insert' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  a ∈ m.insert k → ¬((k == a) = true ∧ k ∉ m) → a ∈ m
-- Mathlib.Topology.Instances.EReal.Lemmas
ContinuousWithinAt.ereal_toENNReal : ∀ {α : Type u_2} [inst : TopologicalSpace α] {f : α → EReal} {s : Set α} {x : α},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun x => (f x).toENNReal) s x
-- Mathlib.Topology.Algebra.Ring.Real
NNReal.instContinuousInv₀ : ContinuousInv₀ NNReal
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.mk : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      {X Y : F.CoGrothendieck} →
        (base : X.base ⟶ Y.base) → (X.fiber ⟶ (F.map base.op.toLoc).toFunctor.obj Y.fiber) → X.Hom Y
-- Mathlib.Order.BoundedOrder.Basic
ULift.instTop : {α : Type u} → [Top α] → Top (ULift.{v, u} α)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.elim0_append : ∀ {n : ℕ} {α : Sort u_1} (v : Fin n → α), Fin.append Fin.elim0 v = v ∘ Fin.cast ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- Constructor for natural transformations between spans.  -/
CategoryTheory.Limits.spanHomMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} →
      (z : F.obj CategoryTheory.Limits.WalkingSpan.zero ⟶ G.obj CategoryTheory.Limits.WalkingSpan.zero) →
        (l : F.obj CategoryTheory.Limits.WalkingSpan.left ⟶ G.obj CategoryTheory.Limits.WalkingSpan.left) →
          (r : F.obj CategoryTheory.Limits.WalkingSpan.right ⟶ G.obj CategoryTheory.Limits.WalkingSpan.right) →
            autoParam
                (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst) l =
                  CategoryTheory.CategoryStruct.comp z (G.map CategoryTheory.Limits.WalkingSpan.Hom.fst))
                CategoryTheory.Limits.spanHomMk._auto_1 →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd) r =
                    CategoryTheory.CategoryStruct.comp z (G.map CategoryTheory.Limits.WalkingSpan.Hom.snd))
                  CategoryTheory.Limits.spanHomMk._auto_3 →
                (F ⟶ G)
-- Mathlib.Order.Nucleus
Nucleus.instFrameElemRangeCoe : {X : Type u_1} → [inst : Order.Frame X] → {n : Nucleus X} → Order.Frame ↑(Set.range ⇑n)
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_single : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (Finsupp.erase a fun₀ | a => b) = 0
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamilyStruct.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {B : C} {α : Type u_2} {X : α → C}
  {π : (a : α) → X a ⟶ B}
  {desc :
    {W : C} →
      (e : (a : α) → X a ⟶ W) →
        (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
            CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
              CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
          (B ⟶ W)}
  {fac :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (a : α), CategoryTheory.CategoryStruct.comp (π a) (desc e ⋯) = e a}
  {uniq :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (m : B ⟶ W), (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = desc e ⋯}
  {desc_1 :
    {W : C} →
      (e : (a : α) → X a ⟶ W) →
        (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
            CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
              CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
          (B ⟶ W)}
  {fac_1 :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (a : α), CategoryTheory.CategoryStruct.comp (π a) (desc_1 e ⋯) = e a}
  {uniq_1 :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (m : B ⟶ W), (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = desc_1 e ⋯},
  { desc := desc, fac := fac, uniq := uniq } = { desc := desc_1, fac := fac_1, uniq := uniq_1 } → desc = desc_1
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
/-- This is the key identity for how `G2` transforms under the slash action by `S`.  -/
EisensteinSeries.G2_S_transform : ∀ (z : UpperHalfPlane),
  EisensteinSeries.G2 z = (↑z ^ 2)⁻¹ * EisensteinSeries.G2 (ModularGroup.S • z) - -2 * ↑Real.pi * Complex.I / ↑z
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.Result.mk.injEq : ∀ (status : Lean.Util.ParamMinimizer.Status) (paramMask : Array Bool) (numCalls : ℕ)
  (status_1 : Lean.Util.ParamMinimizer.Status) (paramMask_1 : Array Bool) (numCalls_1 : ℕ),
  ({ status := status, paramMask := paramMask, numCalls := numCalls } =
      { status := status_1, paramMask := paramMask_1, numCalls := numCalls_1 }) =
    (status = status_1 ∧ paramMask = paramMask_1 ∧ numCalls = numCalls_1)
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- A restatement of `Types.Limit.lift_π_apply` that uses `Pi.π` and `Pi.lift`,
with specialized universes.  -/
CategoryTheory.Limits.Types.pi_lift_π_apply' : ∀ {β : Type v} (f : β → Type v) {P : Type v} (s : (b : β) → P ⟶ f b) (b : β) (x : P),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.lift s)) x) =
    (CategoryTheory.ConcreteCategory.hom (s b)) x
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel of a monomorphism is isomorphic to the zero object  -/
CategoryTheory.Limits.kernel.ofMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
            [inst_3 : CategoryTheory.Limits.HasKernel f] → [CategoryTheory.Mono f] → CategoryTheory.Limits.kernel f ≅ 0
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.Icc_eq_closedBall : ∀ (x y : ℝ), Set.Icc x y = Metric.closedBall ((x + y) / 2) ((y - x) / 2)
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.step_intermediateDropWhile.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : false = true → motive true) (h_2 : false = false → motive false),
  (match hP : false with
    | true => h_1 hP
    | false => h_2 hP) =
    h_2 ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure.id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} (x : C),
  W.multiplicativeClosure (CategoryTheory.CategoryStruct.id x)
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.RationalMap.toRationalMap_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f.hom] (g : Y.PartialMap Z),
  f.toRationalMap.comp g.toRationalMap = (f.comp g).toRationalMap
-- Mathlib.Analysis.Analytic.Binomial
Real.one_add_rpow_hasFPowerSeriesAt_zero : ∀ {a : ℝ}, HasFPowerSeriesAt (fun x => (1 + x) ^ a) (binomialSeries ℝ a) 0
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instOne : {q : ℕ} → One (LucasLehmer.X q)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.instNeg : {G : Type u_1} → {H : Type u_2} → [inst : AddGroup G] → [inst_1 : AddGroup H] → Neg (AddMonoid.Coprod G H)
-- Init.Prelude
/-- Bijection between `α` and `ULift.{v} α`  -/
ULift.down_up : ∀ {α : Type u} (a : α), { down := a }.down = a
-- Mathlib.Data.Rat.Defs
Rat.lift_binop_eq : ∀ (f : ℚ → ℚ → ℚ) (f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ),
  (∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
      {c₂ : n₂.natAbs.Coprime d₂},
      f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
        Rat.divInt (f₁ n₁ (↑d₁) n₂ ↑d₂) (f₂ n₁ (↑d₁) n₂ ↑d₂)) →
    (∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0) →
      ∀ (a b c d : ℤ),
        b ≠ 0 →
          d ≠ 0 →
            (∀ {n₁ d₁ n₂ d₂ : ℤ},
                a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂) →
              f (Rat.divInt a b) (Rat.divInt c d) = Rat.divInt (f₁ a b c d) (f₂ a b c d)
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.normPrivateName? : Lean.Name → Lean.MetaM (Option Lean.Name)
-- Mathlib.Data.Fin.SuccPred
Fin.castLE_injective : ∀ {n m : ℕ} (hmn : m ≤ n), Function.Injective (Fin.castLE hmn)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.mono_measure : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ ν : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l : Filter α},
  MeasureTheory.IntegrableAtFilter f l μ → ν ≤ μ → MeasureTheory.IntegrableAtFilter f l ν
-- Init.Data.String.Lemmas.FindPos
String.offset_posGE_eq_self_iff : ∀ {s : String} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos}, (s.posGE p h).offset = p ↔ String.Pos.Raw.IsValid s p
-- Init.Prelude
/-- The notation typeclass for heterogeneous scalar multiplication.
This enables the notation `a • b : γ` where `a : α`, `b : β`.

It is assumed to represent a left action in some sense.
The notation `a • b` is augmented with a macro (below) to have it elaborate as a left action.
Only the `b` argument participates in the elaboration algorithm: the algorithm uses the type of `b`
when calculating the type of the surrounding arithmetic expression
and it tries to insert coercions into `b` to get some `b'`
such that `a • b'` has the same type as `b'`.
See the module documentation near the macro for more details.
 -/
HSMul : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_succ_succ : ∀ (n k : ℕ), (n + 1).stirlingFirst (k + 1) = n * n.stirlingFirst (k + 1) + n.stirlingFirst k
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.instTopologicalSpace : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Z : Type v'} →
        [inst_1 : TopologicalSpace Z] →
          {T : Type v''} → [inst_2 : TopologicalSpace T] → TopologicalSpace (Topology.ContinuousMapGeneratedBy X Z T)
-- Std.Time.Zoned.ZoneRules
/-- The offset from GMT for this local time.
 -/
Std.Time.TimeZone.LocalTimeType.gmtOffset : Std.Time.TimeZone.LocalTimeType → Std.Time.TimeZone.Offset
-- Mathlib.SetTheory.Ordinal.Rank
IsWellFounded.rank_eq : ∀ {α : Type u} (r : α → α → Prop) [hwf : IsWellFounded α r] (a : α),
  IsWellFounded.rank r a = ⨆ b, Order.succ (IsWellFounded.rank r ↑b)