mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.Algebra.kerSquareLift : {R : Type u} →
  [inst : CommRing R] →
    {A : Type u_1} → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → Algebra (R ⧸ RingHom.ker (algebraMap R A) ^ 2) A
-- Init.Data.Bool
Bool.or_self_right : ∀ (a b : Bool), (a || b || b) = (a || b)
-- Mathlib.LinearAlgebra.Pi
LinearMap.pi_ext : ∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] [Finite ι] [inst_5 : AddCommMonoid M]
  [inst_6 : Module R M] {f g : ((i : ι) → φ i) →ₗ[R] M},
  (∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x)) → f = g
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.nonempty_ord_toType : ∀ {c : Cardinal.{u_1}}, c ≠ 0 → Nonempty c.ord.ToType
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.instIsGaussianMapHSub_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] (c : E),
  ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (fun x => c - x) μ)
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.constVSub.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p : P),
  Homeomorph.constVSub p = { toEquiv := Equiv.constVSub p, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_lt_of_sub_lt : ∀ {a b c : ENNReal}, c ≤ a → a ≠ ⊤ ∨ b ≠ ⊤ → a - b < c → a - c < b
-- Mathlib.Algebra.Free
FreeAddSemigroup.traverse_add' : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) [LawfulApplicative m],
  Function.comp (traverse F) ∘ HAdd.hAdd = fun x y => (fun x1 x2 => x1 + x2) <$> traverse F x <*> traverse F y
-- Mathlib.Algebra.Order.Module.Defs
Prod.instSMulPosReflectLT : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : PartialOrder β]
  [inst_3 : PartialOrder γ] [inst_4 : Zero β] [inst_5 : Zero γ] [inst_6 : SMulWithZero α β] [inst_7 : SMulWithZero α γ]
  [SMulPosReflectLT α β] [SMulPosReflectLT α γ], SMulPosReflectLT α (β × γ)
-- Std.Http.Protocol.H1.Writer
/-- Completed writing a single message and ready to begin the next one.
 -/
Std.Http.Protocol.H1.Writer.State.complete : Std.Http.Protocol.H1.Writer.State
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.id_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (E : J.OneHypercover S) {i j : E.I₀} (a : E.I₁ i j), (CategoryTheory.CategoryStruct.id E).s₁ a = a
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_div_Icc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a / x) '' Set.Icc b c = Set.Icc (a / c) (a / b)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_le_eRk_inter_add_eRk_sdiff : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), M.eRk X ≤ M.eRk (X ∩ Y) + M.eRk (X \ Y)
-- Mathlib.LinearAlgebra.Determinant
/-- If we fix a background basis `e`, then for any other basis `v`, we can characterise the
coordinates provided by `v` in terms of determinants relative to `e`.  -/
Module.Basis.det_smul_mk_coord_eq_det_update : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) {v : ι → M} (hli : LinearIndependent R v)
  (hsp : ⊤ ≤ Submodule.span R (Set.range v)) (i : ι),
  e.det v • (Module.Basis.mk hli hsp).coord i = (↑e.det).toLinearMap v i
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.comap_surjective : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W), Function.Surjective (SimpleGraph.comap ⇑f)
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.IsCardinalFiltered.multicoequalizer : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] {ι : Type v'} {j : ι → J} {k : J} (f₁ f₂ : (i : ι) → j i ⟶ k),
  HasCardinalLT ι κ →
    ∃ l a, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f₁ i) a = CategoryTheory.CategoryStruct.comp (f₂ i) a
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fract_mem_fundamentalDomain : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (x : E), ZSpan.fract b x ∈ ZSpan.fundamentalDomain b
-- Mathlib.Analysis.Asymptotics.Defs
Filter.EventuallyEq.trans_isBigO : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
  {g : α → F}, f₁ =ᶠ[l] f₂ → f₂ =O[l] g → f₁ =O[l] g
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_not_contains_map_fst : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValueCastD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
      if Std.Internal.List.containsKey k l₂ = true then fallback else Std.Internal.List.getValueCastD k l₁ fallback
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.prod_cyclotomic_eq_geom_sum : ∀ {n : ℕ},
  0 < n →
    ∀ (R : Type u_1) [inst : CommRing R],
      ∏ i ∈ n.divisors.erase 1, Polynomial.cyclotomic i R = ∑ i ∈ Finset.range n, Polynomial.X ^ i
-- Std.Time.Duration
/-- Converts a `Duration` to a `Second.Offset`
 -/
Std.Time.Duration.toSeconds : Std.Time.Duration → Std.Time.Second.Offset
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanLocationLink.mk.inj : ∀ {toLocationLink : Lean.Lsp.LocationLink} {ident? : Option Lean.Lsp.LeanDeclIdent} {isDefault : Bool}
  {toLocationLink_1 : Lean.Lsp.LocationLink} {ident?_1 : Option Lean.Lsp.LeanDeclIdent} {isDefault_1 : Bool},
  { toLocationLink := toLocationLink, ident? := ident?, isDefault := isDefault } =
      { toLocationLink := toLocationLink_1, ident? := ident?_1, isDefault := isDefault_1 } →
    toLocationLink = toLocationLink_1 ∧ ident? = ident?_1 ∧ isDefault = isDefault_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.δ_injective : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d + 1} {l : Fin (d + 1)} (hl : SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ)
  {y : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d' : ℕ} {hd' : y.dim = d' + 1}
  {l' : Fin (d' + 1)} (hl' : SSet.prodStdSimplex.pairingCore.IsIndex y hd' l'.succ), hl.δ = hl'.δ → x = y
-- Std.Tactic.BVDecide.Syntax
/-- Suggest a proof script for a `bv_decide` tactic call. Useful for caching LRAT proofs.

Note: include `import Std.Tactic.BVDecide`
 -/
Lean.Parser.Tactic.bvTrace : Lean.ParserDescr
-- Init.Grind.Ring.Field
Lean.Grind.Field.inv_one : ∀ {α : Type u_1} [inst : Lean.Grind.Field α], 1⁻¹ = 1
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
instLieRingAddGroupLieAlgebra.eq_1 : ∀ {𝕜 : 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 : AddGroup G]
  [inst_7 : LieAddGroup I (minSmoothness 𝕜 3) G] [inst_8 : CompleteSpace E],
  instLieRingAddGroupLieAlgebra =
    { toAddCommGroup := instAddCommGroupTangentSpace I 0, toBracket := instBracketAddGroupLieAlgebra, add_lie := ⋯,
      lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_eq_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {x : R}, WithAbs.toAbs v x = 0 ↔ x = 0
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instGetElem?Mem : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        [inst_2 : EquivBEq α] → [inst_3 : LawfulHashable α] → GetElem? (Std.ExtHashMap α β) α β fun m a => a ∈ m
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tfst_id : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t] {α β : Type u},
  Bitraversable.tfst pure = pure
-- Mathlib.RingTheory.PowerBasis
/-- `pb.lift y hy` is the algebra map sending `pb.gen` to `y`,
where `hy` states the higher powers of `y` are the same as the higher powers of `pb.gen`.

See `PowerBasis.liftEquiv` for a bundled equiv sending `⟨y, hy⟩` to the algebra map.
 -/
PowerBasis.lift : {S : Type u_2} →
  [inst : Ring S] →
    {A : Type u_4} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra A S] →
          {S' : Type u_7} →
            [inst_3 : Ring S'] →
              [inst_4 : Algebra A S'] →
                (pb : PowerBasis A S) → (y : S') → (Polynomial.aeval y) (minpoly A pb.gen) = 0 → S →ₐ[A] S'
-- Batteries.Data.Fin.Coding
/-- Encode `(i : Fin n) → Fin (f i)` into `Fin (Fin.prod f)`.  -/
Fin.encodePi : {n : ℕ} → (f : Fin n → ℕ) → ((i : Fin n) → Fin (f i)) → Fin (Fin.prod f)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.support_hsum_subset : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s : HahnSeries.SummableFamily Γ R α}, s.hsum.support ⊆ ⋃ a, (s a).support
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_surjective : Function.Surjective ⇑Circle.exp
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.refl_symm : ∀ {M : Type u_4} [inst : Add M], (AddEquiv.refl M).symm = AddEquiv.refl M
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β) (a : α) (b : β a),
  (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t).1 = t.containsₘ a
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft_apply : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ : ZMod N → E)
  (k : ZMod N), ZMod.dft Φ k = ∑ j, ZMod.stdAddChar (-(j * k)) • Φ j
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.stableUnderSpecialization_singleton : ∀ {R : Type u} [inst : CommSemiring R] {x : PrimeSpectrum R}, StableUnderSpecialization {x} ↔ x.asIdeal.IsMaximal
-- Mathlib.RepresentationTheory.Intertwining
Representation.isIntertwiningMap_iff : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W),
  ρ.IsIntertwiningMap σ f ↔ ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ),
  (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.T R n) =
    (2 * ↑k + 1) * Polynomial.X * (⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.T R n) -
      (↑n ^ 2 - ↑k ^ 2) * (⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The single functors `C ⥤ DerivedCategory C` for all `n : ℤ` along with
their compatibilities with shifts.  -/
DerivedCategory.singleFunctors : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.SingleFunctors C (DerivedCategory C) ℤ
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_iff_norm_inv_mul_lt : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r ↔ ‖b⁻¹ * a‖ < r
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- Given a weight `W : J ⥤ Type w` and `F : J ⥤ C`, this is the `W`-weighted
limit of `F`.  -/
CategoryTheory.Functor.weightedLimObjObj : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (W : CategoryTheory.Functor J (Type w)) →
          (F : CategoryTheory.Functor J C) → [CategoryTheory.Limits.HasWeightedLimit W F] → C
-- Mathlib.RingTheory.DividedPowers.DPMorphism
/-- A bundled divided power morphism between rings endowed with divided power structures.  -/
DividedPowers.DPMorphism : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] → {I : Ideal A} → {J : Ideal B} → DividedPowers I → DividedPowers J → Type (max u_3 u_4)
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.instMembership : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → Membership α (Ordnode α)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.maximalIdeal_eq_span_p : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], IsLocalRing.maximalIdeal ℤ_[p] = Ideal.span {↑p}
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.homeomorph_apply_fst : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X}
  [inst_4 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (U : TopologicalSpace.Opens ↑X)
  (hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (F.germ U x hx))) (x : ↑X)
  (hx : x ∈ U) (s : ↑(TopCat.Presheaf.EtaleSpace.base ⁻¹' ↑U)),
  ((TopCat.Presheaf.EtaleSpace.homeomorph U hF_bij x hx) s).1 = ⟨(↑s).base, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (G : CategoryTheory.ComposableArrows C n),
  (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows G).isoBot = CategoryTheory.Iso.refl (G.obj ⊥)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_C : ∀ {R : Type u} {a : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a).degree = 0
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.comul_counit_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.ComonObj M] {Z : C} (f : M ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.ComonObj.counit) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).inv h)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_one_of_utf8Size_eq_two : ∀ {c : Char} (h : c.utf8Size = 2), (String.utf8EncodeChar c)[1].toBitVec = 2#2 ++ BitVec.extractLsb' 0 6 c.val.toBitVec
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.isEmpty = false ↔
    ∃ k,
      ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true),
        (f (t.getKey k h) (Std.DTreeMap.Internal.Impl.Const.get t k h)).isSome = true
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.constOn_of_comp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f →
    ∀ {A : Type u_3} [inst_2 : TopologicalSpace A] {s : Set A} {g : A → E},
      IsPreconnected s →
        ContinuousOn g s → (∀ a ∈ s, ∀ a' ∈ s, f (g a) = f (g a')) → ∀ {a a' : A}, a ∈ s → a' ∈ s → g a = g a'
-- Lean.Meta.Tactic.Grind.Types
/-- Number of splits performed to get to this goal.  -/
Lean.Meta.Grind.Split.State.num : Lean.Meta.Grind.Split.State → ℕ
-- Mathlib.Tactic.Explode.Datatypes
/-- `├` Start intro (top-level)  -/
Mathlib.Explode.Status.sintro : Mathlib.Explode.Status
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.mapEq_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type w} [inst_1 : LinearOrder K] {x : K}
  {F G : CategoryTheory.Functor (↑(Set.Iic x)) C} (k : K) (hk : k ≤ x),
  F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩ → CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq F G k k ⋯ hk
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemView.mk : Array (Lean.Ident × Lean.Name) →
  Array Lean.Elab.ConfigEval.EvalConfigItemHandler → Lean.Elab.ConfigEval.EvalConfigItemView
-- Mathlib.Data.List.Chain
List.isChain_replicate_of_rel : ∀ {α : Type u_1} {r : α → α → Prop} (n : ℕ) {a : α}, r a a → List.IsChain r (List.replicate n a)
-- Init.Data.BitVec.Lemmas
BitVec.clz_eq_zero_iff : ∀ {w : ℕ} {x : BitVec w}, 0 < w → (x.clz.toNat = 0 ↔ 2 ^ (w - 1) ≤ x.toNat)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiable.continuous : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}, MDiff f → Continuous f
-- Lean.Meta.Basic
/-- Enables proof irrelevance at `isDefEq`  -/
Lean.Meta.Config.proofIrrelevance : Lean.Meta.Config → Bool
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.subsingleton_of_bot : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], Subsingleton (LieSubmodule R L ↥⊥)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccPrelimit_iff_omega0_dvd : ∀ {a : Ordinal.{u_4}}, Order.IsSuccPrelimit a ↔ Ordinal.omega0 ∣ a
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate.eq_1 : ∀ {n : ℕ} (x : BitVec n), BitVec.Signed.rotate✝ x = x + BitVec.Signed.intMinSealed✝ n
-- Mathlib.Data.List.Sublists
List.sublists'Aux_eq_map : ∀ {α : Type u} (a : α) (r₁ r₂ : List (List α)), List.sublists'Aux a r₁ r₂ = r₂ ++ List.map (List.cons a) r₁
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_univ : ∀ {M : Type u_1} [inst : AddGroup M], SimpleGraph.addCayley Set.univ = ⊤
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_succ_Ici : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.succ (Finset.Ici i) = Finset.Ici i.succ
-- Init.Data.Array.Lemmas
Array.back_append_of_size_pos : ∀ {α : Type u_1} {xs ys : Array α} {h₁ : 0 < (xs ++ ys).size} (h₂ : 0 < ys.size), (xs ++ ys).back h₁ = ys.back h₂
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.tensorEquivSum_X_tmul_X : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (i : σ) (j : ι),
  (MvPolynomial.tensorEquivSum R σ ι S) (MvPolynomial.X i ⊗ₜ[R] MvPolynomial.X j) =
    MvPolynomial.X (Sum.inl i) * MvPolynomial.X (Sum.inr j)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The simplicial circle.  -/
SSet.S1 : SSet
-- Mathlib.Order.Partition.Basic
/-- Convert a `Partition s` into a `Partition t` via an equality `s = t`.  -/
Partition.copy : {α : Type u_1} → {s t : α} → [inst : CompleteLattice α] → Partition s → s = t → Partition t
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_toSubsemiring : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R), S.op.toSubsemiring = S.op
-- Mathlib.RepresentationTheory.Action
/-- The comultiplication of the linearize functor.  -/
Representation.LinearizeMonoidal.δ : {G : Type v} →
  [inst : Monoid G] →
    (X Y : Action (Type w) G) →
      {k : Type u} →
        [inst_1 : CommSemiring k] →
          (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).IntertwiningMap
            ((Representation.linearize k G X).tprod (Representation.linearize k G Y))
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.mem_centeredArc : ∀ {r : ℝ}, r ≤ Real.pi → ∀ {z : Circle}, z ∈ Circle.centeredArc r ↔ |(↑z).arg| < r
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.mfderivWithin : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt[s] f x f' → UniqueMDiffAt[s] x → mfderiv[s] f x = f'
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {l : List ((a : α) × β a)},
  l.isEmpty = true → Std.Internal.List.minKey? l = none
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y}
  {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a)
  (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g) [inst_2 : F.Full],
  hf.lift i h hi = F.preimage (CategoryTheory.Limits.PullbackCone.IsLimit.lift ⋯.isLimit i (F.map h) hi)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.ExtHashMap.ofList l).getKey! k' = k
-- Mathlib.CategoryTheory.Quotient
/-- A `HomRel` on `C` consists of a relation on every hom-set.  -/
HomRel : (C : Type u_1) → [Quiver C] → Type (max u_1 u_2)
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.lanPresheafIso.eq_1 : ∀ {S : LightProfinite} {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)}
  (hF : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))),
  LightCondensed.lanPresheafIso hF =
    (CategoryTheory.Functor.Final.colimitIso (LightProfinite.Extend.functorOp S.asLimitCone)
          ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op (Opposite.op S)).comp
            (FintypeCat.toLightProfinite.op.comp F))).symm ≪≫
      (CategoryTheory.Limits.colimit.isColimit (S.diagram.rightOp.comp F)).coconePointUniqueUpToIso hF
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.GeometricallyIrreducible.geometrically_irreducibleSpace : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.GeometricallyIrreducible f],
  AlgebraicGeometry.geometrically (fun x => IrreducibleSpace ↥x) f
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.instId : MonadSatisfying Id