mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.Iter.step_drop.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
IsGLB.csInf_eq : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, IsGLB s a → s.Nonempty → sInf s = a
-- Mathlib.Data.FunLike.Group
FunLike.coe_coeAddHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [inst_3 : IsAddApply F α β], ⇑(FunLike.coeAddHom F α β) = DFunLike.coe
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an
equivalence between cones over `F` and cones over `F ⋙ e.functor`.
 -/
CategoryTheory.Limits.Cone.functorialityEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (F : CategoryTheory.Functor J C) →
              (e : C ≌ D) → CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (F.comp e.functor)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.map_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (s : Stream'.WSeq α),
  Stream'.WSeq.map (g ∘ f) s = Stream'.WSeq.map g (Stream'.WSeq.map f s)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.inv_conjMap_comp_apply : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g • a)
  (x : ↥(SubMulAction.ofStabilizer G b)),
  (SubMulAction.ofStabilizer.conjMap hg) ((SubMulAction.ofStabilizer.conjMap ⋯) x) = x
-- Mathlib.Analysis.Fourier.FourierTransform
Real.Lp.fourierTransformCLM_apply : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : ↥(MeasureTheory.Lp E 1 MeasureTheory.volume)), (Real.Lp.fourierTransformCLM V E) f = Real.Lp.fourierTransform f
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} [inst_6 : F.Braided] (hF : F.FullyFaithful) {X Y : CategoryTheory.CommMon C}
  (f : F.mapCommMon.obj X ⟶ F.mapCommMon.obj Y),
  hF.mapCommMon.preimage f = CategoryTheory.CommMon.homMk (hF.mapMon.preimage f.hom)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_symm : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.symm.symm = e
-- Init.Data.String.Lemmas.Order
String.Pos.byteIdx_offset_le_utf8ByteSize : ∀ {s : String} {p : s.Pos}, p.offset.byteIdx ≤ s.utf8ByteSize
-- Mathlib.Order.SuccPred.Basic
Order.Iio_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α),
  Set.Iio (Order.succ a) = Set.Iic a
-- Mathlib.GroupTheory.OrderOfElement
orderOf_dvd_iff_zpow_eq_one : ∀ {G : Type u_1} [inst : Group G] {x : G} {i : ℤ}, ↑(orderOf x) ∣ i ↔ x ^ i = 1
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
/-- Regarding the `LieRing` of a `LieAlgebra` as a `NonUnitalNonAssocRing`, we can
reinterpret the `smul_lie` law as an `IsScalarTower`.  -/
LieAlgebra.isScalarTower : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  IsScalarTower R (CommutatorRing L) (CommutatorRing L)
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of the forward direction of `le_compl_comm`. -/
le_compl_of_le_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ → b ≤ aᶜ
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.instMonoidWithZero : {𝕜 : Type u_1} → [inst : SeminormedRing 𝕜] → [NormOneClass 𝕜] → MonoidWithZero ↑(Metric.closedBall 0 1)
-- Mathlib.Condensed.Light.TopCatAdjunction
lightCondSetToTopCat_obj_carrier : ∀ (X : LightCondSet), ↑(lightCondSetToTopCat.obj X) = X.obj.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
-- Mathlib.Order.Interval.Finset.Fin
Fin.card_Ico : ∀ {n : ℕ} (a b : Fin n), (Finset.Ico a b).card = ↑b - ↑a
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.deriv2_mul_log : ∀ (x : ℝ), deriv^[2] (fun x => x * Real.log x) x = x⁻¹
-- Mathlib.MeasureTheory.Constructions.Projective
MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {I J : Finset ι},
  MeasureTheory.IsProjectiveMeasureFamily P →
    ∀ {S : Set ((i : ↥I) → α ↑i)} {T : Set ((i : ↥J) → α ↑i)},
      MeasurableSet S → MeasurableSet T → MeasureTheory.cylinder I S = MeasureTheory.cylinder J T → (P I) S = (P J) T
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.eq_univ_of_subsingleton_span_eq_top : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s : Set P}, s.Subsingleton → affineSpan k s = ⊤ → s = Set.univ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homology.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S S_1 : CategoryTheory.ShortComplex C) (e_S : S = S_1) [inst_2 : S.HasHomology], S.homology = S_1.homology
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- When `x` is fixed, `(f : α →ᵇ β) ↦ f x` is continuous.  -/
BoundedContinuousFunction.instContinuousEvalConst : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β],
  ContinuousEvalConst (BoundedContinuousFunction α β) α β
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Precoverage.toGrothendieck_toCoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.HasPullbacks] [inst_2 : J.IsStableUnderBaseChange], J.toCoverage.toGrothendieck = J.toGrothendieck
-- Std.Do.WP.SimpLemmas
Std.Do.WP.modifyGet_EStateM : ∀ {σ α ε : Type u_1} {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))}
  (f : σ → α × σ), (Std.Do.wp (MonadStateOf.modifyGet f)).apply Q = fun s => Q.1 (f s).1 (f s).2
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Delab : Type
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below.prec : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop} {f h : ℕ →. ℕ} (hf : Nat.RecursiveIn O f)
  (hh : Nat.RecursiveIn O h),
  Nat.RecursiveIn.below hf → motive f hf → Nat.RecursiveIn.below hh → motive h hh → Nat.RecursiveIn.below ⋯
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.iteratedDeriv_weierstrassPExcept_self : ∀ (L : PeriodPair) (l : ℂ) {n : ℕ},
  iteratedDeriv n (L.weierstrassPExcept l) l =
    if n = 0 then L.weierstrassPExcept l l else ↑(n + 1).factorial * L.sumInvPow l (n + 2)
-- Mathlib.Algebra.Quandle
/-- A verification that `act` is self-distributive  -/
Shelf.self_distrib : ∀ {α : Type u} [self : Shelf α] {x y z : α}, Shelf.act x (Shelf.act y z) = Shelf.act (Shelf.act x y) (Shelf.act x z)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly_nc.eq_def : ∀ (x : Lean.Grind.CommRing.Expr),
  x.toPoly_nc =
    match x with
    | Lean.Grind.CommRing.Expr.num k => Lean.Grind.CommRing.Poly.num k
    | Lean.Grind.CommRing.Expr.intCast k => Lean.Grind.CommRing.Poly.num k
    | Lean.Grind.CommRing.Expr.natCast k => Lean.Grind.CommRing.Poly.num ↑k
    | Lean.Grind.CommRing.Expr.var x => Lean.Grind.CommRing.Poly.ofVar x
    | a.add b => a.toPoly_nc.combine b.toPoly_nc
    | a.mul b => a.toPoly_nc.mul_nc b.toPoly_nc
    | a.neg => Lean.Grind.CommRing.Poly.mulConst (-1) a.toPoly_nc
    | a.sub b => a.toPoly_nc.combine (Lean.Grind.CommRing.Poly.mulConst (-1) b.toPoly_nc)
    | a.pow k =>
      bif k == 0 then Lean.Grind.CommRing.Poly.num 1
      else
        match a with
        | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num (n ^ k)
        | Lean.Grind.CommRing.Expr.intCast n => Lean.Grind.CommRing.Poly.num (n ^ k)
        | Lean.Grind.CommRing.Expr.natCast n => Lean.Grind.CommRing.Poly.num (↑n ^ k)
        | Lean.Grind.CommRing.Expr.var x =>
          Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit)
        | x => a.toPoly_nc.pow_nc k
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.lt_of_lt : ∀ {α : Type u_1} {a a' b b' : α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α],
  a < b → a' + b ≤ b' + a → a' < b'
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndepOn_id_insert_iff : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {a : V}
  {s : Set V}, LinearIndepOn K id (insert a s) ↔ LinearIndepOn K id s ∧ (a ∈ Submodule.span K s → a ∈ s)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_preimage_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β},
  Function.Injective f → s ⊆ Set.range f → Nat.card ↑(f ⁻¹' s) = Nat.card ↑s
-- Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
/-- If `a` is any complex number, the function `(log ‖· - a‖)` is circle integrable over every circle.
 -/
circleIntegrable_log_norm_sub_const : ∀ {a c : ℂ} (r : ℝ), CircleIntegrable (fun x => Real.log ‖x - a‖) c r
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} {h₁ h₂ : CategoryTheory.ModObj M X},
  h₁ = h₂ ↔ CategoryTheory.ModObj.smul = CategoryTheory.ModObj.smul
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousNeg.measurableNeg : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [inst_3 : Neg γ]
  [ContinuousNeg γ], MeasurableNeg γ
-- Mathlib.Topology.Semicontinuity.Defs
semicontinuous_restrict_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {s : Set α},
  Semicontinuous (s.domRestrict r) ↔ SemicontinuousOn r s
-- Mathlib.Algebra.Star.Unitary
Unitary.toUnits_injective : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R], Function.Injective ⇑Unitary.toUnits
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.brecOn.eq : ∀ {dir : Std.Http.Protocol.H1.Direction} {motive : Std.Http.Protocol.H1.Reader.State dir → Sort u}
  (t : Std.Http.Protocol.H1.Reader.State dir)
  (F_1 : (t : Std.Http.Protocol.H1.Reader.State dir) → Std.Http.Protocol.H1.Reader.State.below t → motive t),
  Std.Http.Protocol.H1.Reader.State.brecOn t F_1 = F_1 t (Std.Http.Protocol.H1.Reader.State.brecOn.go t F_1).2
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_neg : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f : MvPolynomial σ R},
  m.leadingCoeff (-f) = -m.leadingCoeff f
-- Mathlib.Tactic.Algebra.Basic
/-- The data used by the `algebra` tactic to normalize the constant coefficients, which are
expressions in `R` normalized by `ring`.  -/
Mathlib.Tactic.Algebra.ringCompute : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            Mathlib.Tactic.Algebra.Cache sR →
              Mathlib.Tactic.Algebra.Cache sA →
                Mathlib.Tactic.Ring.Common.RingCompute (Mathlib.Tactic.Algebra.BaseType sAlg) sA
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.instInvSubtypeMem : {K : Type u} → [inst : DivisionRing K] → (s : Subfield K) → Inv ↥s
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.comap_ne_bot_of_root_mem : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S} {I : Ideal S} [IsDomain S]
  {r : S}, r ≠ 0 → r ∈ I → ∀ {p : Polynomial R}, p ≠ 0 → Polynomial.eval₂ f r p = 0 → Ideal.comap f I ≠ ⊥
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The set of conjugates of `s` is closed under conjugation.  -/
Group.conj_mem_conjugatesOfSet : ∀ {G : Type u_1} [inst : Group G] {s : Set G} {x c : G},
  x ∈ Group.conjugatesOfSet s → c * x * c⁻¹ ∈ Group.conjugatesOfSet s
-- Mathlib.Topology.Defs.Filter
/-- A function between topological spaces is continuous on a subset `s`
when it's continuous at every point of `s` within `s`.  -/
ContinuousOn : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Set X → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.symm : ∀ {p q : NNReal}, p.HolderConjugate q → q.HolderConjugate p
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitCoconeIsColimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  AddMonCat.FilteredColimits.colimitCoconeIsColimit F =
    { desc := AddMonCat.FilteredColimits.colimitDesc F, fac := ⋯, uniq := ⋯ }
-- Mathlib.RingTheory.Localization.BaseChange
Algebra.IsPushout.of_bijective_right : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (T : Type u_5)
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : Algebra A T] [inst_6 : IsScalarTower R A T],
  Function.Bijective ⇑(algebraMap A T) → Algebra.IsPushout R A R T
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.lieSpan_mono : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s t : Set L},
  s ⊆ t → LieSubalgebra.lieSpan R L s ≤ LieSubalgebra.lieSpan R L t
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toAddSubgroup_prod : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {H : Type u_2} [inst_2 : AddGroup H]
  [inst_3 : TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H), ↑(U.prod V) = (↑U).prod ↑V
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Algebra.IsIntegral.isLocalHom : ∀ (R : Type u_1) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] [FaithfulSMul R S], IsLocalHom (algebraMap R S)
-- Init.Data.Iterators.Basic
Std.PlausibleIterStep.skip.eq_1 : ∀ {α : Type u} {β : Type w} {IsPlausibleStep : Std.IterStep α β → Prop} (it' : α)
  (h : IsPlausibleStep (Std.IterStep.skip it')), Std.PlausibleIterStep.skip it' h = ⟨Std.IterStep.skip it', h⟩
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.innerDual_iUnion : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E]
  {ι : Sort u_4} (f : ι → Set E), ProperCone.innerDual (⋃ i, f i) = ⨅ i, ProperCone.innerDual (f i)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.insertIdx.loop.eq_def : ∀ {α : Type u} (i : ℕ) (as : Array α) (j : Fin as.size),
  Array.insertIdx.loop✝ i as j =
    if i < ↑j then
      let j' := ⟨↑j - 1, ⋯⟩;
      let as_1 := as.swap ↑j' ↑j ⋯ ⋯;
      Array.insertIdx.loop✝ i as_1 ⟨↑j', ⋯⟩
    else as
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instAddLeftCancelMonoid : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddLeftCancelMonoid α] → AddLeftCancelMonoid (Matrix m n α)
-- Init.Util
/-- Returns the address at which an object is allocated.

This function is unsafe because it can distinguish between definitionally equal values.
 -/
ptrAddrUnsafe : {α : Type u} → α → USize
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A mixin for right cancellative multiplication by nonzero elements.  -/
IsRightCancelMulZero : (M₀ : Type u) → [Mul M₀] → [Zero M₀] → Prop
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.card_surjective : Function.Surjective Ordinal.card
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.self_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β k}, (cmp k (t.insertIfNew k v).maxKey!).isLE = true
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.LocalizerMorphism.equiv_smallHomMap' : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂} {D₁ : Type u₃}
  [inst_2 : CategoryTheory.Category.{v₃, u₃} D₁] {D₂ : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₂]
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁]
  (L₂ : CategoryTheory.Functor C₂ D₂) [inst_5 : L₂.IsLocalization W₂] {X Y : C₁}
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y] {X' Y' : C₂}
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' X']
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' Y']
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ Y' Y'] (eX : Φ.functor.obj X ≅ X')
  (eY : Φ.functor.obj Y ≅ Y') (G : CategoryTheory.Functor D₁ D₂) (e : Φ.functor.comp L₂ ≅ L₁.comp G)
  (f : CategoryTheory.Localization.SmallHom W₁ X Y),
  (CategoryTheory.Localization.SmallHom.equiv W₂ L₂) (Φ.smallHomMap' eX eY f) =
    CategoryTheory.CategoryStruct.comp (L₂.map eX.inv)
      (CategoryTheory.CategoryStruct.comp (e.hom.app X)
        (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Localization.SmallHom.equiv W₁ L₁) f))
          (CategoryTheory.CategoryStruct.comp (e.inv.app Y) (L₂.map eY.hom))))
-- Mathlib.Algebra.Order.Archimedean.Basic
exists_nat_one_div_lt : ∀ {K : Type u_4} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {ε : K},
  0 < ε → ∃ n, 1 / (↑n + 1) < ε
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.ofIso_I : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {Y : SSet} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B),
  (P.ofIso e hA).I = ⇑(SSet.Subcomplex.N.orderIsoOfIso e hA) ⁻¹' P.I
-- Mathlib.RingTheory.Ideal.Int
Int.ideal_span_isMaximal_of_prime : ∀ (p : ℕ) [Fact (Nat.Prime p)], (Ideal.span {↑p}).IsMaximal
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.tensorUnit_V : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (Rep.{u, u, v} k G)) = k
-- Mathlib.NumberTheory.AbelSummation
/-- A version of `sum_mul_eq_sub_sub_integral_mul` where the endpoints are `Nat`.  -/
sum_mul_eq_sub_sub_integral_mul' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} {n m : ℕ},
  n ≤ m →
    (∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t) →
      MeasureTheory.IntegrableOn (deriv f) (Set.Icc ↑n ↑m) MeasureTheory.volume →
        ∑ k ∈ Finset.Ioc n m, f ↑k * c k =
          f ↑m * ∑ k ∈ Finset.Icc 0 m, c k - f ↑n * ∑ k ∈ Finset.Icc 0 n, c k -
            ∫ (t : ℝ) in Set.Ioc ↑n ↑m, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k
-- Mathlib.Order.SuccPred.Basic
/-- A linear order with well-founded greater-than relation is a `PredOrder`.  -/
PredOrder.ofLinearWellFoundedGT : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedGT α] → PredOrder α
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.withTopOrderIso_apply_coe : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (A : FiniteArchimedeanClass M), (FiniteArchimedeanClass.withTopOrderIso M) ↑A = ↑A
-- Mathlib.Analysis.Complex.Norm
Complex.norm_add_mul_I : ∀ (x y : ℝ), ‖↑x + ↑y * Complex.I‖ = √(x ^ 2 + y ^ 2)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.instCoeFunForall : {α : Type u_1} → {β : Type u_2} → CoeFun (PartialEquiv α β) fun x => α → β
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
/-- The left localizer morphism in the Guitart exact square `iso`.  -/
_private.Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives.0.HomotopyCategory.Plus.isRightDerivabilityStructure.L : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.LocalizerMorphism
        ((CochainComplex.Plus.quasiIso C).inverseImage (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus)
        (CategoryTheory.MorphismProperty.isomorphisms (HomotopyCategory.Plus (CategoryTheory.InjectiveObject C)))
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_toList : ∀ {M : Type u_3} [inst : AddCommMonoid M] (s : Multiset M), s.toList.sum = s.sum
-- Mathlib.CategoryTheory.Action.Continuous
DiscreteContAction.instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteV : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) →
                [inst_4 : Monoid G] →
                  [inst_5 : TopologicalSpace G] → CategoryTheory.HasForget₂ (DiscreteContAction V G) (ContAction V G)
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- An analogue of `Filter.HasBasis.tendsto_iff` for `TendstoUniformlyOn`.  -/
Filter.HasBasis.tendstoUniformlyOn_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {X : Type u_5} {ιX : Type u_6} {ιβ : Type u_8} {F : X → α → β}
  {f : α → β} {l : Filter X} {s : Set α} {pX : ιX → Prop} {sX : ιX → Set X} {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)},
  l.HasBasis pX sX →
    (uniformity β).HasBasis pβ sβ →
      (TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∃ j, pX j ∧ ∀ ⦃x : X⦄, x ∈ sX j → ∀ a ∈ s, (f a, F x a) ∈ sβ i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  l.contains k = false → (Std.DTreeMap.Raw.Const.unitOfList l cmp).getKey? k = none
-- Std.Http.Data.URI.Basic
/-- Fluent builder for constructing URIs. Takes raw (unencoded) strings and handles encoding
automatically when building the final URI.
 -/
Std.Http.URI.Builder : Type
-- Lean.Meta.Closure
Lean.Meta.Closure.collectLevel : Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level
-- Init.NotationExtra
unexpandListNil : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Polynomial.Sequence
/-- A polynomial sequence spans `R[X]` if all of its elements' leading coefficients are units.  -/
Polynomial.Sequence.span : ∀ {R : Type u_1} [inst : Ring R] (S : Polynomial.Sequence R),
  (∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) → Submodule.span R (Set.range ↑S) = ⊤
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_prod_disjoint : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [ContinuousMul α]
  {ι : Type u_4} (s : Finset ι) {t : ι → Set β} {a : ι → α},
  (↑s).Pairwise (Function.onFun Disjoint t) →
    (∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)) → HasProd (f ∘ Subtype.val) (∏ i ∈ s, a i)