mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
  (CategoryTheory.ConcreteCategory.hom
        (F.map
          ((CategoryTheory.PreGaloisCategory.AutGalois.π F A)
              (MulOpposite.unop ((CategoryTheory.PreGaloisCategory.endMulEquivAutGalois F) f))).hom))
      A.pt =
    (CategoryTheory.ConcreteCategory.hom (f.app A.obj)) A.pt
-- Mathlib.Data.Nat.Cast.Basic
NeZero.nat_of_neZero : ∀ {R : Type u_6} {S : Type u_7} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {F : Type u_8}
  [inst_2 : FunLike F R S] [RingHomClass F R S] (f : F) {n : ℕ} [hn : NeZero ↑n], NeZero ↑n
-- Mathlib.Data.Ordmap.Invariants
Ordnode.eraseMax.eq_2 : ∀ {α : Type u_1} (size : ℕ) (l : Ordnode α) (x_1 : α), (Ordnode.node size l x_1 Ordnode.nil).eraseMax = l
-- Mathlib.Topology.Category.LightProfinite.Sequence
LightProfinite.continuous_iff_convergent : ∀ {Y : Type u_1} [inst : TopologicalSpace Y] (f : ↑LightProfinite.NatUnionInfty.toTop → Y),
  Continuous f ↔ Filter.Tendsto (fun x => f ↑x) Filter.atTop (nhds (f OnePoint.infty))
-- Mathlib.Data.Finsupp.Lex
Finsupp.lex_def : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] {r : α → α → Prop} {s : N → N → Prop} {a b : α →₀ N},
  Finsupp.Lex r s a b ↔ ∃ j, (∀ (d : α), r d j → a d = b d) ∧ s (a j) (b j)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- If a function and its derivative are integrable on `(-∞, a]`, then the function tends to zero
at `-∞`.  -/
MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Iic : ∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  (∀ x ∈ Set.Iic a, HasDerivAt f (f' x) x) →
    MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume →
      MeasureTheory.IntegrableOn f (Set.Iic a) MeasureTheory.volume → Filter.Tendsto f Filter.atBot (nhds 0)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_smul : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {R : Type u_4} [inst_1 : SMul R Y] (r : R)
  (f : LocallyConstant X Y), ⇑(r • f) = r • ⇑f
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
StarAlgHom.continuous_realContinuousMapOfNNReal : ∀ {X : Type u_1} [inst : TopologicalSpace X] {A : Type u_2} [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra ℝ A] [inst_4 : TopologicalSpace A] [IsSemitopologicalRing A] (φ : C(X, NNReal) →⋆ₐ[NNReal] A),
  Continuous ⇑φ → Continuous ⇑φ.realContinuousMapOfNNReal
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.lim_preservesLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.PreservesLimits CategoryTheory.Limits.lim
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- The functor `Type u ⥤ SheafOfModules.{u} R` which sends a type `I` to
`free I` which is a coproduct indexed by `I` of copies of `R` (thought of as a
presheaf of modules over itself).  -/
SheafOfModules.freeFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [J.WEqualsLocallyBijective AddCommGrpCat] → CategoryTheory.Functor (Type u) (SheafOfModules R)
-- Init.Data.Order.Ord
Std.LawfulBEqCmp.compare_beq_eq_beq : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering} [Std.LawfulBEqCmp cmp] {a b : α},
  (cmp a b == Ordering.eq) = (a == b)
-- Mathlib.Algebra.Ring.Basic
/-- Vieta's formula for a quadratic equation, relating the coefficients of the polynomial with
its roots. This particular version states that if we have a root `x` of a monic quadratic
polynomial, then there is another root `y` such that `x + y` is negative the `a_1` coefficient
and `x * y` is the `a_0` coefficient.  -/
vieta_formula_quadratic : ∀ {α : Type u_3} [inst : NonUnitalCommRing α] {b c x : α},
  x * x - b * x + c = 0 → ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
-- Init.Data.Int.Order
Int.pos_of_neg_neg : ∀ {a : ℤ}, -a < 0 → 0 < a
-- Mathlib.Order.Hom.Basic
OrderEmbedding.ltEmbedding_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) (x : α), f.ltEmbedding x = f x
-- Mathlib.Data.Int.Cast.Lemmas
AddMonoidHom.eq_intCastAddHom : ∀ {A : Type u_5} [inst : AddGroupWithOne A] (f : ℤ →+ A), f 1 = 1 → f = Int.castAddHom A
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ}
  {k : α} (h : (↑m).WF) {h' : (Std.DHashMap.Internal.Raw₀.filterMap f m).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (Std.DHashMap.Internal.Raw₀.filterMap f m) k h' =
    (f (m.getKey k ⋯) (Std.DHashMap.Internal.Raw₀.Const.get m k ⋯)).get ⋯
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.isLocalization_of_base_ringEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [IsLocalization M S] (h : R ≃+* P),
  IsLocalization (Submonoid.map h M) S
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMaxSteps : Lean.Options → ℕ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α}, (Std.DHashMap.Const.insertManyIfNewUnit m l).size ≤ m.size + l.length
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.tendsto_exp_nhds_zero_iff : ∀ {α : Type u_1} {l : Filter α} {f : α → ℂ},
  Filter.Tendsto (fun x => Complex.exp (f x)) l (nhds 0) ↔ Filter.Tendsto (fun x => (f x).re) l Filter.atBot
-- Mathlib.Algebra.Category.Grp.Basic
/-- The category of groups and group morphisms.  -/
CommGrpCat : Type (u + 1)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable.  -/
MDifferentiable.mpullback_vectorField : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} [inst_11 : IsManifold I 2 M] [inst_12 : IsManifold I' 2 M']
  [CompleteSpace E],
  MDiff (T% V) →
    ContMDiff I I' n f →
      (∀ (x : M), (mfderiv% f x).IsInvertible) → 2 ≤ n → MDiff fun x => ⟨x, VectorField.mpullback I I' f V x⟩
-- Lean.Language.Basic
Lean.Language.SnapshotTask.ReportingRange.some.injEq : ∀ (range range_1 : Lean.Syntax.Range),
  (Lean.Language.SnapshotTask.ReportingRange.some range = Lean.Language.SnapshotTask.ReportingRange.some range_1) =
    (range = range_1)
-- Mathlib.GroupTheory.Finiteness
/-- An additive group is finitely generated if it is finitely generated as an additive subgroup of
itself.  -/
AddGroup.FG : (H : Type u_4) → [AddGroup H] → Prop
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.lcm_one : ∀ (a : ℤ), a.lcm 1 = a.natAbs
-- Std.Time.DateTime.WallTime
/-- Converts a `WallTime` to a `Duration`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.toDuration : Std.Time.WallTime → Std.Time.Duration
-- Mathlib.Tactic.Finiteness
/-- `finiteness` proves goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
nonnegative reals (`ℝ≥0∞`). If the goal cannot be proven, `finiteness` prints a warning and shows
its intermediate progress.

This tactic is based on `aesop`. It calls `assumption`, `intros`, `positivity`, and any
lemma or rule added to the `finiteness` ruleset, except that all `simp` rules are disabled.

This tactic is extensible. By adding more rules, `finiteness` can prove more goals. For example:
* `@[aesop (rule_sets := [finiteness]) safe 50] lemma ...`
* `add_aesop_rules safe tactic (rule_sets := [finiteness]) (by ...)`

(Note that a `simp` rule cannot be added this way, since all `simp` rules are disabled.)

* `finiteness (clause)` customizes the `aesop` call using the given clause. See `aesop`
  documentation for detailed explanation. Note that `finiteness` disables `simp`, so
  `finiteness (add simp [lemma1, lemma2])` does not do anything more than a bare `finiteness`.
* `finiteness [t₁, ..., tₙ]` adds the terms `t₁`, ..., `tₙ` as local hypotheses before applying
  the search rules.
* `finiteness?` additionally shows the proof that `finiteness` found.
* `finiteness_nonterminal` is a version of `finiteness` that does not report a warning if it fails
  to close the goal.
 -/
finiteness : Lean.ParserDescr
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- For a ℤ-lattice `Submodule.span ℤ (Set.range b)`, proves that the set defined
by `ZSpan.fundamentalDomain` is a fundamental domain.  -/
ZSpan.isAddFundamentalDomain : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [Finite ι] [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E),
  MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑b))) (ZSpan.fundamentalDomain b) μ
-- Mathlib.Data.Set.Finite.Lattice
Set.eq_finite_iUnion_of_finite_subset_iUnion : ∀ {α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set α},
  t.Finite →
    t ⊆ ⋃ i, s i →
      ∃ I, I.Finite ∧ ∃ σ, (∀ (i : ↑{i | i ∈ I}), (σ i).Finite) ∧ (∀ (i : ↑{i | i ∈ I}), σ i ⊆ s ↑i) ∧ t = ⋃ i, σ i
-- Mathlib.Algebra.Polynomial.Degree.Domain
Polynomial.not_dvd_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R}, q ≠ 0 → q.degree < p.degree → ¬p ∣ q
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- The cocone `coconeOfHasStrongEpiMonoFactorisation F` is a colimit  -/
CategoryTheory.MonoOver.isColimitCoconeOfHasStrongEpiMonoFactorisation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y : C} →
      [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
        [inst_2 : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] →
          {J : Type u₂} →
            [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
              (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.MonoOver.coconeOfHasStrongEpiMonoFactorisation F)
-- ProofWidgets.Component.RefreshComponent
/-- Update the current HTML tree to be `html`. See also `updateLazy`.  -/
ProofWidgets.RefreshToken.update : ProofWidgets.RefreshToken → ProofWidgets.Html → BaseIO Unit
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.LiftActionCoreResult.closed : Lean.Elab.Tactic.Grind.LiftActionCoreResult
-- Mathlib.Topology.Spectral.Prespectral
PrespectralSpace.exists_isCompact_and_isOpen_between : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PrespectralSpace X] {K U : Set X},
  IsCompact K → IsOpen U → K ⊆ U → ∃ W, IsCompact W ∧ IsOpen W ∧ K ⊆ W ∧ W ⊆ U
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The proposition that the function preserves addition  -/
AddEquiv.map_add' : ∀ {A : Type u_9} {B : Type u_10} [inst : Add A] [inst_1 : Add B] (self : A ≃+ B) (x y : A),
  self.toFun (x + y) = self.toFun x + self.toFun y
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.le_slope_of_hasDerivAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ}, ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivAt f f' y → f' ≤ slope f x y
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instBoundedOrder : {α : Type u} → [inst : AddGroup α] → BoundedOrder (AddGroupTopology α)
-- Mathlib.Algebra.Regular.Opposite
isRegular_op : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsRegular (MulOpposite.op a) ↔ IsRegular a
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ico_succ_left_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {a b : α},
  a < b → insert a (Finset.Ico (Order.succ a) b) = Finset.Ico a b
-- Mathlib.Topology.MetricSpace.HausdorffDimension
_private.Mathlib.Topology.MetricSpace.HausdorffDimension.0.intrinsicInterior.eq_1 : ∀ (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicInterior 𝕜 s = Subtype.val '' interior (Subtype.val ⁻¹' s)
-- Std.Async.Process
/-- Size of unshared data segment (kilobytes)
 -/
Std.IO.Process.ResourceUsageStats.unsharedDataSizeKb : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.mkIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} (e : M.X ≅ N.X)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
        CategoryTheory.AddMonObj.add),
  CategoryTheory.AddMon.mkIso e one_f mul_f = CategoryTheory.AddMon.mkIso' e
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Composition of a continuous function with compact support with a cocompact map
yields another continuous function with compact support.  -/
CompactlySupportedContinuousMap.comp : {β : Type u_3} →
  {γ : Type u_4} →
    {δ : Type u_5} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            [inst_3 : Zero δ] →
              CompactlySupportedContinuousMap γ δ → CocompactMap β γ → CompactlySupportedContinuousMap β δ
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.instFaithfulGradedObjectForget : ∀ {ι : Type u_1} (V : Type u) [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι), (HomologicalComplex.forget V c).Faithful
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toArray_succ_succ_eq_map : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : LT α] [inst_3 : DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.PRange.InfinitelyUpwardEnumerable α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)...Std.PRange.succ hi).toArray = Array.map Std.PRange.succ (lo...hi).toArray
-- Mathlib.Algebra.Order.Group.Abs
mabs_eq_inv_self : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a : G}, |a|ₘ = a⁻¹ ↔ a ≤ 1
-- Mathlib.Order.Category.Lat
Lat.instConcreteCategoryLatticeHomCarrier : CategoryTheory.ConcreteCategory Lat fun x1 x2 => LatticeHom ↑x1 ↑x2
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_mul_inr : ∀ {R : Type u} {M : Type v} [inst : MonoidWithZero R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] (r : R) (m : M),
  TrivSqZeroExt.inl r * TrivSqZeroExt.inr m = TrivSqZeroExt.inr (r • m)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)],
  (((HomologicalComplex₂.shiftFunctor₁ C x).comp (HomologicalComplex₂.shiftFunctor₂ C y)).obj K).HasTotal
    (ComplexShape.up ℤ)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Assuming that `(C, J)` is a dense subsite of `(D, K)` (via a functor `G : C ⥤ D`)
and `sheafPushforwardContinuous G A J₀ J` is an equivalence of categories, this is
the isomorphism between `sheafifyOfIsEquivalence J K G A ⋙ G.sheafPushforwardContinuous A J K`
and the functor which sends a presheaf to the sheafification of its precomposition by `G.op`.  -/
CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalenceCompIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (J : CategoryTheory.GrothendieckTopology C) →
          (K : CategoryTheory.GrothendieckTopology D) →
            (G : CategoryTheory.Functor C D) →
              (A : Type u_4) →
                [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G] →
                    [inst_4 : (G.sheafPushforwardContinuous A J K).IsEquivalence] →
                      [inst_5 : CategoryTheory.HasWeakSheafify J A] →
                        (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).comp
                            (G.sheafPushforwardContinuous A J K) ≅
                          ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp
                            (CategoryTheory.presheafToSheaf J A)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.step_dropWhile : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → Bool},
  (Std.IterM.dropWhile P it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        match hP : P out with
        | true => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhile P true it') ⋯))
        | false =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhile P false it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhile P true it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.CategoryTheory.Limits.Final.Connected
CategoryTheory.initial_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.IsConnected D], (CategoryTheory.Prod.fst C D).Initial
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientEquivProdOfLE'_symm_apply : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α)
  (hf : Function.RightInverse f QuotientAddGroup.mk) (a : (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t),
  (AddSubgroup.quotientEquivProdOfLE' h_le f hf).symm a = Quotient.map' (fun b => f a.1 + ↑b) ⋯ a.2
-- Mathlib.Data.Sym.Basic
Sym.append_inj_left : ∀ {α : Type u_1} {n n' : ℕ} {s s' : Sym α n} (t : Sym α n'), s.append t = s'.append t ↔ s = s'
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterMatrix.relation.eq_1 : ∀ {B : Type u_1} (M : CoxeterMatrix B) (i i' : B), M.relation i i' = (FreeGroup.of i * FreeGroup.of i') ^ M.M i i'
-- Mathlib.Analysis.Normed.Group.Defs
enorm_ne_top : ∀ {E : Type u_8} [inst : NNNorm E] {x : E}, ‖x‖ₑ ≠ ⊤
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.send : {α : Type} → Std.CloseableChannel.Unbounded✝ α → α → BaseIO (Task (Except Std.CloseableChannel.Error Unit))
-- Std.Time.Date.PlainDate
Std.Time.instTransOrdPlainDate : Std.TransOrd Std.Time.PlainDate
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_get_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.LawfulEqCmp cmp]
  {k : α} {v : β k} {w : k ∈ t}, t.get k w = v → k ∈ t
-- Mathlib.FieldTheory.Normal.Defs
AlgEquiv.restrictNormal_apply : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} [inst_1 : Field K₁] [inst_2 : Algebra F K₁]
  (L : IntermediateField F K₁) [inst_3 : Normal F ↥L] (σ : Gal(K₁/F)) (x : ↥L), ↑((σ.restrictNormal ↥L) x) = σ ↑x
-- Mathlib.Order.WellFounded
Function.not_lt_argminOn : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [inst : LT β] [inst_1 : WellFoundedLT β] (s : Set α) {a : α} (ha : a ∈ s),
  ¬f a < f (Function.argminOn f s ⋯)
-- Mathlib.Computability.StateTransition
StateTransition.Reaches₀.tail : ∀ {σ : Type u_1} {f : σ → Option σ} {a b c : σ},
  StateTransition.Reaches₀ f a b → c ∈ f b → StateTransition.Reaches₀ f a c
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.associator_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.Pseudofunctor B C} (I : CategoryTheory.Pseudofunctor B C) (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I)
  (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).inv.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.barComplex.d_single : ∀ {k G : Type u} [inst : CommRing k] (n : ℕ) [inst_1 : Group G] (x : Fin (n + 1) → G),
  ((Rep.Hom.hom (Rep.barComplex.d k G n)) fun₀ | x => MonoidAlgebra.single 1 1) =
    (fun₀ | fun i => x i.succ => MonoidAlgebra.single (x 0) 1) +
      ∑ j, fun₀ | j.contractNth (fun x1 x2 => x1 * x2) x => MonoidAlgebra.single 1 ((-1) ^ (↑j + 1))
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.tensor_right_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y],
  CategoryTheory.MonoidalCoherence.iso =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).symm ≪≫
      CategoryTheory.MonoidalCategory.whiskerLeftIso X CategoryTheory.MonoidalCoherence.iso
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (a : α), |a|ₘ = a ⊔ a⁻¹
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformlyOn_iff_forall_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι},
  TendstoLocallyUniformlyOn F f p s ↔
    ∀ x ∈ s, Filter.Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ nhdsWithin x s) (uniformity β)
-- Mathlib.Order.ULift
ULift.down_compl : ∀ {α : Type u} [inst : Compl α] (a : ULift.{u_1, u} α), aᶜ.down = a.downᶜ
-- Mathlib.Data.Set.Image
/-- **Alias** of the forward direction of `Function.Injective.mem_range_iff_existsUnique`. -/
Function.Injective.existsUnique_of_mem_range : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ {b : β}, b ∈ Set.range f → ∃! a, f a = b
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.exists_eventuallyEq_const_of_forall_separating : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : α → β} [Nonempty β] (p : Set β → Prop)
  [HasCountableSeparatingOn β p Set.univ],
  (∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U) → ∃ a, f =ᶠ[l] Function.const α a
-- Mathlib.Order.CompletePartialOrder
/-- Complete partial orders are partial orders where every directed set has a least upper bound.
 -/
CompletePartialOrder : Type u_4 → Type u_4
-- Mathlib.Order.SupClosed
InfClosed.image : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {s : Set α}
  [inst_2 : FunLike F α β] [InfHomClass F α β], InfClosed s → ∀ (f : F), InfClosed (⇑f '' s)