mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that
the exponentiation to power `s : ℕ` of (± `y`) (here taking the specified signs) is ± `y ^ s`;
return this proof and the computed sign.  -/
Mathlib.Tactic.FieldSimp.Sign.pow : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (y : Q(«$M»)) →
        (g : Mathlib.Tactic.FieldSimp.Sign M) →
          (s : ℕ) →
            Lean.MetaM
              ((G : Mathlib.Tactic.FieldSimp.Sign M) ×
                have a := G.expr q(«$y» ^ «$s»);
                have a_1 := g.expr y;
                Q(«$a_1» ^ «$s» = «$a»))
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_mul_cos_add_sin_mul_I_coe_angle : ∀ {r : ℝ}, 0 < r → ∀ (θ : Real.Angle), ↑(↑r * (↑θ.cos + ↑θ.sin * Complex.I)).arg = θ
-- Batteries.Data.ByteArray
ByteArray.get_set_eq : ∀ (a : ByteArray) (i : Fin a.size) (v : UInt8), (a.set (↑i) v ⋯)[↑i] = v
-- Mathlib.NumberTheory.SmoothNumbers
/-- The `Finset` of prime factors of an `s`-factored number is contained in `s`.  -/
Nat.primeFactors_subset_of_mem_factoredNumbers : ∀ {s : Finset ℕ} {m : ℕ}, m ∈ Nat.factoredNumbers s → m.primeFactors ⊆ s
-- Mathlib.Data.Set.Sigma
Set.image_sigmaMk_subset_sigma_left : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {a : (i : ι) → α i},
  (∀ (i : ι), a i ∈ t i) → (fun i => ⟨i, a i⟩) '' s ⊆ s.sigma t
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.PrefixTable.step.match_3.splitter : {α : Type u_1} →
  (t : Array.PrefixTable α) →
    (motive : Fin (t.size + 1) → Sort u_2) →
      (x : Fin (t.size + 1)) → ((k : ℕ) → (hk : k < t.size + 1) → motive ⟨k, hk⟩) → motive x
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MorApplication.exact.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.MorApplication.exact = 1
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.negMulLog_def : Real.negMulLog = fun x => -x * Real.log x
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.associator : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [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]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} J] {F₁ : CategoryTheory.Functor C D} (G : CategoryTheory.Functor D E)
  (H : CategoryTheory.Functor E J) (A : Type u_5) [inst_4 : AddMonoid A] [inst_5 : CategoryTheory.HasShift C A]
  [inst_6 : CategoryTheory.HasShift D A] [inst_7 : CategoryTheory.HasShift E A] [inst_8 : CategoryTheory.HasShift J A]
  [inst_9 : F₁.CommShift A] [inst_10 : G.CommShift A] [inst_11 : H.CommShift A],
  CategoryTheory.NatTrans.CommShift (F₁.associator G H).hom A
-- Batteries.Data.AssocList
Batteries.AssocList.cons.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (key : α) (value : β)
  (tail : Batteries.AssocList α β),
  sizeOf (Batteries.AssocList.cons key value tail) = 1 + sizeOf key + sizeOf value + sizeOf tail
-- Mathlib.RingTheory.Finiteness.Defs
/-- An ideal of `R` is finitely generated if it is the span of a finite subset of `R`.

This is defeq to `Submodule.FG`, but unfolds more nicely.  -/
Ideal.FG : {R : Type u_1} → [inst : Semiring R] → Ideal R → Prop
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.baseChangeFromBaseChange_apply : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T]
  (x : P.toExtension.baseChange.Ring),
  (P.baseChangeFromBaseChange T).toRingHom x = (MvPolynomial.algebraTensorAlgEquiv R T) x
-- Mathlib.GroupTheory.GroupAction.Hom
instFunLikeMulActionHom.eq_1 : ∀ {M : Type u_2} {N : Type u_3} (φ : M → N) (X : Type u_5) [inst : SMul M X] (Y : Type u_6) [inst_1 : SMul N Y],
  instFunLikeMulActionHom φ X Y = { coe := MulActionHom.toFun, coe_injective := ⋯ }
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.nhds_zero_eq_of_basis : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F] {ι : Type u_7}
  {p : ι → Prop} {b : ι → Set F},
  (nhds 0).HasBasis p b →
    nhds 0 = ⨅ s, ⨅ (_ : Bornology.IsVonNBounded 𝕜₁ s), ⨅ i, ⨅ (_ : p i), Filter.principal {f | Set.MapsTo (⇑f) s (b i)}
-- Mathlib.RingTheory.Coprime.Basic
not_isCoprime_zero_zero : ∀ {R : Type u} [inst : CommSemiring R] [Nontrivial R], ¬IsCoprime 0 0
-- Std.Http.Data.URI
/-- Parses a `URI` from the given string. Panics if parsing fails. Use `parse?` if you need a safe
option-returning version.
 -/
Std.Http.URI.parse! : String → Std.Http.URI
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : ℕ}, p.natDegree < x → (⇑Polynomial.derivative)^[x] p = 0
-- Init.Data.Vector.Attach
Vector.attachWith_empty : ∀ {α : Type u_1} {P : α → Prop} (H : ∀ x ∈ #v[], P x), #v[].attachWith P H = #v[]
-- Init.Data.Array.Lemmas
Array.filterMap_size_eq_size : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {xs : Array α},
  (Array.filterMap f xs).size = xs.size ↔ ∀ a ∈ xs, (f a).isSome = true
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F)
  {x : E} {s : Set E}, UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (⇑f) s x = f.contLinear
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, (t.insert k).isEmpty = false
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Normalized expressions for 2-morphisms.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr : Type
-- Mathlib.Analysis.PSeries
Finset.sum_schlomilch_le : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} {u : ℕ → ℕ}
  {C : ℕ},
  (∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) →
    (∀ (n : ℕ), 0 < u n) →
      (∀ (n : ℕ), 0 ≤ f n) →
        Monotone u →
          SuccDiffBounded C u →
            ∀ (n : ℕ),
              ∑ k ∈ Finset.range (n + 1), (u (k + 1) - u k) • f (u k) ≤
                (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Finset.Ico (u 0 + 1) (u n + 1), f k
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `(h : IsAdjoinRoot S f).root` is the root of `f` that can be adjoined to generate `S`.  -/
IsAdjoinRoot.root : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] → [inst_1 : Ring S] → {f : Polynomial R} → [inst_2 : Algebra R S] → IsAdjoinRoot S f → S
-- Lean.Expr
Lean.MVarId.mk.inj : ∀ {name name_1 : Lean.Name}, { name := name } = { name := name_1 } → name = name_1
-- Mathlib.Order.RelSeries
RelSeries.toList_eraseLast : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.length ≠ 0 → p.eraseLast.toList = p.toList.dropLast
-- Lean.Data.Lsp.Internal
/-- Converts `RefIdent` to a JSON for `RefIdentJsonRepr`.  -/
Lean.Lsp.RefIdent.toJson : Lean.Lsp.RefIdent → Lean.Json
-- Init.SimpLemmas
Bool.not_beq_to_not_eq : ∀ (a b : Bool), ((!a == b) = true) = ¬a = b
-- Mathlib.CategoryTheory.Abelian.Basic
/-- Factoring through the image is a strong epi-mono factorisation.  -/
CategoryTheory.Abelian.imageStrongEpiMonoFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Abelian C] → {P Q : C} → (f : P ⟶ Q) → CategoryTheory.Limits.StrongEpiMonoFactorisation f
-- Mathlib.Topology.Constructions
nhdsWithin_subtype_eq_bot_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} {x : ↑s},
  nhdsWithin x (Subtype.val ⁻¹' t) = ⊥ ↔ nhdsWithin (↑x) t ⊓ Filter.principal s = ⊥
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.sub_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (a b : DoubleCentralizer 𝕜 A), (a - b).toProd.1 = a.toProd.1 - b.toProd.1
-- Std.Time.Format.Modifier
Std.Time.Number.mk.sizeOf_spec : ∀ (padding : ℕ), sizeOf { padding := padding } = 1 + sizeOf padding
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits a 1.  -/
Subgroup.one : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → One ↥H
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.mem_iff_iSup_of_isClosed : ∀ {s : Set Ordinal.{u}} {a : Ordinal.{u}},
  IsClosed s → (a ∈ s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.supp_map : ∀ {F : Type u → Type u} [q : QPF F],
  QPF.IsUniform → ∀ {α β : Type u} (g : α → β) (x : F α), Functor.supp (g <$> x) = g '' Functor.supp x
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.conditionallyCompleteLattice.eq_1 : ∀ {α : Type u_5} [inst : ConditionallyCompleteLattice α],
  WithTop.conditionallyCompleteLattice =
    { toLattice := WithTop.lattice, toSupSet := WithTop.instSupSet, toInfSet := WithTop.instInfSet, isLUB_csSup := ⋯,
      isGLB_csInf := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.Functions.0.Lean.Meta.Grind.Arith.CommRing.mkOne : {m : Type → Type} → [Lean.Meta.Sym.Arith.MonadCanon m] → Lean.Level → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionSemiHomClass.toMonoidHomClass : ∀ {F : Type u_15} {M : outParam (Type u_16)} {N : outParam (Type u_17)} {inst : Monoid M} {inst_1 : Monoid N}
  {φ : outParam (M → N)} {R : outParam (Type u_18)} {S : outParam (Type u_19)} {inst_2 : Semiring R}
  {inst_3 : Semiring S} {inst_4 : DistribMulAction M R} {inst_5 : DistribMulAction N S} {inst_6 : FunLike F R S}
  [self : MulSemiringActionSemiHomClass F φ R S], MonoidHomClass F R S
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.bot_notMem : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α}, s.Intersecting → ⊥ ∉ s
-- Mathlib.RingTheory.Coalgebra.Basic
DFinsupp.comul_comp_lapply : ∀ (R : Type u) (ι : Type v) (A : ι → Type w) [inst : DecidableEq ι] [inst_1 : CommSemiring R]
  [inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : (i : ι) → Module R (A i)]
  [inst_4 : (i : ι) → CoalgebraStruct R (A i)] (i : ι),
  CoalgebraStruct.comul ∘ₗ DFinsupp.lapply i =
    TensorProduct.map (DFinsupp.lapply i) (DFinsupp.lapply i) ∘ₗ CoalgebraStruct.comul
-- Mathlib.Topology.Semicontinuity.Basic
upperSemiContinuous_inv_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} [inst_1 : PartialOrder β] [inst_2 : CommGroup β]
  [IsOrderedMonoid β], UpperSemicontinuous f⁻¹ ↔ LowerSemicontinuous f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.admit : Lean.Meta.Grind.Goal → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.isoSourceOfSelf_inv : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y),
  (CategoryTheory.Limits.equalizer.isoSourceOfSelf f).inv =
    CategoryTheory.Limits.equalizer.lift (CategoryTheory.CategoryStruct.id X) ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [Nontrivial A]
  (a : A),
  autoParam (p a) IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum._auto_1 →
    IsGreatest ((fun x => ‖x‖₊) '' spectrum 𝕜 a) ‖a‖₊
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.exists_algebraMap_quot_eq_of_mem_quot : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Sₚ : Type u_4) [inst_4 : CommRing Sₚ] [inst_5 : Algebra S Sₚ]
  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [hPp : P.LiesOver p] [P.IsMaximal]
  (x : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P), ∃ a, (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) a = x
-- Init.Data.BitVec.Lemmas
BitVec.toInt_sub_toInt_lt_twoPow_iff : ∀ {w : ℕ} {x y : BitVec w},
  x.toInt - y.toInt < -2 ^ (w - 1) ↔ x.toInt < 0 ∧ 0 ≤ y.toInt ∧ 0 ≤ (x.toInt - y.toInt).bmod (2 ^ w)
-- Mathlib.Topology.Algebra.ConstMulAction
smul_closure_subset : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α] (c : M)
  (s : Set α), c • closure s ⊆ closure (c • s)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.subset_inter_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : β k → β k}, m.WF → (m.modify k f).isEmpty = m.isEmpty
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.sigmaOpenCover_X : ∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Small.{u, v} σ] (a : σ),
  (AlgebraicGeometry.sigmaOpenCover g).X a = g a
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_eq_ncard_iff_ncard_sdiff_eq_ncard_sdiff`. -/
Set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff : ∀ {α : Type u_1} {s t : Set α},
  autoParam s.Finite Set.ncard_eq_ncard_iff_ncard_sdiff_eq_ncard_sdiff._auto_1 →
    autoParam t.Finite Set.ncard_eq_ncard_iff_ncard_sdiff_eq_ncard_sdiff._auto_3 →
      (s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard)
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.toImplicit : Lean.Expr → Lean.Expr
-- Aesop.Util.EqualUpToIds
Aesop.exprsEqualUpToIds : Lean.MetavarContext →
  Lean.MetavarContext →
    Lean.LocalContext →
      Lean.LocalContext →
        Lean.LocalInstances → Lean.LocalInstances → Lean.Expr → Lean.Expr → optParam Bool false → Lean.MetaM Bool
-- Init.Data.Vector.Lemmas
Vector.rightpad_mk : ∀ {α : Type u_1} {m n : ℕ} {a : α} {xs : Array α} (h : xs.size = m),
  Vector.rightpad n a (Vector.mk xs h) = Vector.mk (Array.rightpad n a xs) ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_natCast : ∀ (x : ℂ) (n : ℕ), x ^ ↑n = x ^ n
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp.congr_simp : ∀ {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]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F],
  CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp L W F G =
    CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp L W F G
-- Mathlib.RingTheory.PowerSeries.GaussNorm
/-- Given a power series `f` in, a function `v : R → ℝ` and a real number `c`, the Gauss norm is
defined as the supremum of the set of all values of `v (coeff t f) * c ^ t` for all `t : ℕ`.  -/
PowerSeries.gaussNorm : {R : Type u_1} → [Semiring R] → (R → ℝ) → ℝ → PowerSeries R → ℝ
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.constLinearEquivOfIsEmpty_symm_apply : ∀ {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [inst : CommSemiring R']
  [inst_1 : AddCommMonoid M''] [inst_2 : AddCommMonoid N''] [inst_3 : Module R' M''] [inst_4 : Module R' N'']
  [inst_5 : IsEmpty ι] (f : M'' [⋀^ι]→ₗ[R'] N''), AlternatingMap.constLinearEquivOfIsEmpty.symm f = f 0
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.limitConeOfComp_isLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone (F.comp G)),
  (CategoryTheory.Functor.Initial.limitConeOfComp F t).isLimit =
    (CategoryTheory.Functor.Initial.isLimitExtendConeEquiv F t.cone).symm t.isLimit
-- Std.Sat.AIG.CachedGates
/-- Create an implication gate in the input AIG. This uses the builtin cache to enable automated subterm
sharing.
 -/
Std.Sat.AIG.mkImpCached : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
-- Mathlib.Order.RelClasses
IsPartialOrder.swap : ∀ {α : Type u} (r : α → α → Prop) [IsPartialOrder α r], IsPartialOrder α (Function.swap r)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split_ineq_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℤ → Int.Internal.Linear.Poly → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] [inst : Inhabited α]
  {k : α}, k ∈ m → m.getKey! k = k
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.inl_union_inr : ∀ {R : Type u_2} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] {s : Set M} {t : Set M'},
  (LinearIndependent R fun (x : ↑s) => ↑x) →
    (LinearIndependent R fun (x : ↑t) => ↑x) →
      LinearIndependent R fun (x : ↑(⇑(LinearMap.inl R M M') '' s ∪ ⇑(LinearMap.inr R M M') '' t)) => ↑x
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.instIsMulCommutative_closure : ∀ {S : Type u_1} {R : Type u_2} [inst : NonUnitalRing R] [inst_1 : SetLike S R] [inst_2 : MulMemClass S R] (s : S)
  [IsMulCommutative ↥s], IsMulCommutative ↥(NonUnitalSubring.closure ↑s)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_id : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.AffineSpace.map n (CategoryTheory.CategoryStruct.id S) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.AffineSpace n S)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_succ_right_eq_append_map : ∀ {m n : ℕ}, m < n → (m<...n + 1).toArray = #[m + 1] ++ Array.map (fun x => x + 1) (m<...n).toArray
-- Mathlib.ModelTheory.Definability
_private.Mathlib.ModelTheory.Definability.0.Set.DefinableFun.comp.match_1_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (i : α) → motive (some i)),
  (match none with
    | none => h_1 ()
    | some i => h_2 i) =
    h_1 ()
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toArray_rcc_eq : ∀ {m n i : ℕ}, ((m...=n).toArray[i]?.isNone = true) = (n + 1 ≤ i + m)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs.injEq : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (ofAbs ofAbs_1 : R), (WithAbs.toAbs v ofAbs = WithAbs.toAbs v ofAbs_1) = (ofAbs = ofAbs_1)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableWithinAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x → DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (c • f) s x
-- Std.Time.Format
Std.Time.PlainTime.instRepr : Repr Std.Time.PlainTime
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.equiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y Z : C} [inst_7 : W.IsCompatibleWithShift M]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z]
  [inst_10 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z]
  [inst_11 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] {a b c : M}
  (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (g : CategoryTheory.Localization.SmallShiftedHom W Y Z b)
  (h : b + a = c),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (f.comp g h) =
    ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) f).comp
      ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) g) h
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Iso.toEquiv_fun : ∀ {X Y : Type u} (i : X ≅ Y), ⇑i.toEquiv = ⇑(CategoryTheory.ConcreteCategory.hom i.hom)
-- Init.Core
/-- You should not use this function  -/
NonScalar.mk : ℕ → NonScalar
-- Lean.Server.RequestCancellation
Lean.Server.CancellableM : Type → Type
-- Mathlib.Data.NNRat.BigOperators
NNRat.cast_sum : ∀ {α : Type u_1} {K : Type u_2} [inst : DivisionSemiring K] [CharZero K] (s : Finset α) (f : α → ℚ≥0),
  ↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)
-- Lean.Data.Json.Parser
Lean.Json.Parser.exponent : Lean.JsonNumber → Std.Internal.Parsec.String.Parser Lean.JsonNumber
-- Mathlib.Topology.Compactness.SigmaCompact
instSigmaCompactSpaceULift : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] [SigmaCompactSpace Y], SigmaCompactSpace (ULift.{u, u_2} Y)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instMulLeftMono : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  MulLeftMono (FractionalIdeal S P)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_maxKey!_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∈ t → (cmp k t.maxKey!).isLE = true
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongr_symm : ∀ {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
  (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
AddMonoidHom.uniformContinuous_of_continuousAt_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [IsUniformAddGroup β] (f : α →+ β),
  ContinuousAt (⇑f) 0 → UniformContinuous ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.fiberwiseColim_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  (H : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  [inst_2 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H),
  (CategoryTheory.Limits.fiberwiseColim F H).obj G = CategoryTheory.Limits.fiberwiseColimit G
-- Mathlib.Logic.Encodable.Basic
/-- A decidable subtype of an encodable type is encodable.  -/
Subtype.encodable : {α : Type u_1} → {P : α → Prop} → [encA : Encodable α] → [decP : DecidablePred P] → Encodable { a // P a }