mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (x : Std.DTreeMap.Internal.Impl α β)
  (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.getEntryGE k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      match h : compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryGED k l ⟨ky, y⟩
      | Ordering.eq => ⟨ky, y⟩
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryGE k r ⋯ ⋯
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.x_neg : ∀ {d : ℤ} (a : Pell.Solution₁ d), (-a).x = -a.x
-- Mathlib.Data.Nat.Init
Nat.leRecOn_trans : ∀ {C : ℕ → Sort u_1} {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  Nat.leRecOn ⋯ next x = Nat.leRecOn hmk next (Nat.leRecOn hnm next x)
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.whiskerLeft_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable]
  (c x x_1 : CategoryTheory.WideSubcategory P) (f : x ⟶ x_1),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c f).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft c.obj f.hom
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the right adjoint is full, then each component of the counit is a split monomorphism.  -/
CategoryTheory.Adjunction.counit_isSplitMono_of_R_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Full] (X : D),
  CategoryTheory.IsSplitMono (h.counit.app X)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.asSquare_iso : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X),
  CategoryTheory.CatCommSq.iso S.fst S.snd F G = S.iso
-- Init.Data.Array.Lemmas
Array.find?_toList : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, List.find? p xs.toList = Array.find? p xs
-- Mathlib.Tactic.Linarith.Datatypes
/-- Metadata about preprocessors, for trace output.  -/
Mathlib.Tactic.Linarith.PreprocessorBase : Type
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.hasSum_e2Summand_symmetricIcc : ∀ (z : UpperHalfPlane),
  HasSum (fun x => EisensteinSeries.e2Summand x z)
    (2 * riemannZeta 2 -
      8 * ↑Real.pi ^ 2 *
        ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n)
    (SummationFilter.symmetricIcc ℤ)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_map_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  {Y X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)}
  (f : Y ⟶ X),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).functor.map f).left =
    CategoryTheory.CategoryStruct.id Y.left
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree.eq_1 : ∀ {σ : Type u_1} {R : Type u_4} [inst : AddCommMonoid R],
  Finsupp.degree = { toFun := fun d => ∑ i ∈ d.support, d i, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Order.Cover
Set.Ico_eq_singleton_left_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Ico a b = {a} ↔ a ⋖ b
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.instCommRingObjForgetBialgHomCarrier : {R : Type u} → [inst : CommRing R] → {A : CommBialgCat R} → CommRing ((CategoryTheory.forget (CommBialgCat R)).obj A)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.singleton : ∀ {α : Type u_1} {a : α} {le : α → α → Bool},
  Batteries.BinomialHeap.Imp.Heap.WF le 0 (Batteries.BinomialHeap.Imp.Heap.singleton a)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.isomorphisms_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.isomorphisms C).op = CategoryTheory.MorphismProperty.isomorphisms Cᵒᵖ
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
CategoryTheory.Pseudofunctor.DescentData.faithful_pullFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j),
  CategoryTheory.Sieve.ofArrows X' f' ∈ J S → (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).Faithful
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqRhs : Bool → Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.Condensed.Discrete.LocallyConstant
CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete : (Condensed.discrete (Type (u_1 + 1))).Full
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_zero : ∀ {a b : ℝ} (x y : ↑(Set.Icc a b)), Set.Icc.convexComb x y 0 = x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.forIn'_eq_if : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_8 : Monad m] [LawfulMonad m] {γ : Type u}
  {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f =
    if hu : r.lower ≤ r.upper then
      have hle := ⋯;
      do
      let __do_lift ← f r.lower ⋯ init
      match __do_lift with
        | ForInStep.yield c => forIn' (r.lower<...=r.upper) c fun a ha acc => f a ⋯ acc
        | ForInStep.done c => pure c
    else pure init
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.of_forall_get?_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → (∀ (k : α), m₁.get? k = m₂.get? k) → m₁.Equiv m₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasGoodReduction.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W W_1 : WeierstrassCurve K),
  W = W_1 → WeierstrassCurve.HasGoodReduction R W = WeierstrassCurve.HasGoodReduction R W_1
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.divBy_mul_by : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : ↥S) (p : LocalizedModule S M),
  (LocalizedModule.divBy s) (((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) p) = p
-- Mathlib.RingTheory.RingHom.OpenImmersion
RingHom.IsStandardOpenImmersion.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.IsStandardOpenImmersion = Algebra.IsStandardOpenImmersion R S
-- Mathlib.Order.Monotone.Basic
StrictMono.ite' : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  StrictMono f →
    StrictMono g →
      ∀ {p : α → Prop} [inst_2 : DecidablePred p],
        (∀ ⦃x y : α⦄, x < y → p y → p x) →
          (∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y) → StrictMono fun x => if p x then f x else g x
-- Mathlib.Data.Finset.NAry
Finset.image₂_comm : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {g : β → α → γ}, (∀ (a : α) (b : β), f a b = g b a) → Finset.image₂ f s t = Finset.image₂ g t s
-- Mathlib.Order.Minimal
/-- **Alias** of `setOfPred_minimal_subset`. -/
setOf_minimal_subset : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), {x | Minimal (fun x => x ∈ s) x} ⊆ s
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.directive.withFenceSize : ℕ → (ℕ → Lean.Parser.ParserFn) → Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_union_inv_smul : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (s ∪ c⁻¹ • t) = μ (c • s ∪ t)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.algHom_ext_iff : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddMonoid M]
  {φ₁ φ₂ : AddMonoidAlgebra A M →ₐ[R] B},
  φ₁ = φ₂ ↔
    (∀ (m : M), φ₁ (AddMonoidAlgebra.single m 1) = φ₂ (AddMonoidAlgebra.single m 1)) ∧
      φ₁.comp AddMonoidAlgebra.singleZeroAlgHom = φ₂.comp AddMonoidAlgebra.singleZeroAlgHom
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.comp_toLinearMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : AddCommMonoid C]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C]
  (φ₁ : B →ₗc[R] C) (φ₂ : A →ₗc[R] B), ↑(φ₁.comp φ₂) = ↑φ₁ ∘ₗ ↑φ₂
-- Mathlib.Order.Category.Frm
/-- The category of frames.  -/
Frm : Type (u_1 + 1)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- **Alias** of the reverse direction of `curveIntegrable_cast_iff`. -/
CurveIntegrable.cast : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c d : E}
  {ω : E → E →L[𝕜] F} {γ : Path a b} (hc : c = a) (hd : d = b), CurveIntegrable ω γ → CurveIntegrable ω (γ.cast hc hd)
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instReprState : {dir : Std.Http.Protocol.H1.Direction} → Repr (Std.Http.Protocol.H1.Reader.State dir)
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.isDeniedModule : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
Finset.sum_mul_self_eq_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R]
  (s : Finset ι) (f : ι → R), ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_hasStrictFDerivAt_iff : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E},
  HasStrictFDerivAt (⇑iso ∘ f) (↑↑iso ∘SL f') x ↔ HasStrictFDerivAt f f' x
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.mul`. -/
MeasureTheory.ProgMeasurable.mul : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u v : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : Mul β]
  [ContinuousMul β],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f v → MeasureTheory.IsStronglyProgressive f fun i ω => u i ω * v i ω
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node : Type u → Type v → Type (max u v)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.cocone_pt : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂),
  (CategoryTheory.Limits.Types.Pushout.cocone f g).pt = CategoryTheory.Limits.Types.Pushout f g
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_piecewise`. -/
Set.restrict_piecewise : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [inst : (x : α) → Decidable (x ∈ s)],
  s.domRestrict (s.piecewise f g) = s.domRestrict f
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → (toContinuousMap : C(α, β)) → IsOpenMap toContinuousMap.toFun → α →CO β
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_injective_of_left : ∀ {α : Sort u_1} [inst : DecidableEq α] (a : α), Function.Injective fun x => Equiv.swap a x
-- Mathlib.Data.Holor
Holor.CPRankMax.brecOn : ∀ {α : Type} [inst : Mul α] [inst_1 : AddMonoid α]
  {motive : (a : ℕ) → {ds : List ℕ} → (a_1 : Holor α ds) → Holor.CPRankMax a a_1 → Prop} {a : ℕ} {ds : List ℕ}
  {a_1 : Holor α ds} (t : Holor.CPRankMax a a_1),
  (∀ (a : ℕ) {ds : List ℕ} (a_2 : Holor α ds) (t : Holor.CPRankMax a a_2), Holor.CPRankMax.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] [inst : X.IsQuasiAffine]
  [inst_1 : Y.IsQuasiAffine],
  (TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f)).base).obj
      (AlgebraicGeometry.Scheme.Hom.opensRange Y.toSpecΓ) =
    AlgebraicGeometry.Scheme.Hom.opensRange X.toSpecΓ
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Any matrix can be reduced to diagonal form by elementary operations.  -/
Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal : ∀ {n : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n 𝕜),
  ∃ L L' D,
    (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod =
      Matrix.diagonal D
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we let `S.u₁` and `S.X` be any elements such that
`S.X ^ 3 * S.u₁ = S.x`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.X : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → NumberField.RingOfIntegers K
-- Mathlib.Order.JordanHolder
/-- A `JordanHolderLattice` is the class for which the Jordan Hölder theorem is proved. A
Jordan Hölder lattice is a lattice equipped with a notion of maximality, `IsMaximal`.

Examples include `Subgroup G` if `G` is a group, and `Submodule R M` if `M` is an `R`-module.

In the example of subgroups, `IsMaximal H K` means that `H` is a maximal normal subgroup of `K`.
In the example of submodules, `IsMaximal M N` means that `M` is a maximal submodule of `N`.  -/
JordanHolderLattice : (X : Type u) → [Lattice X] → Type u
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Finset.hasProd : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α)
  (L : optParam (SummationFilter ↑↑s) (SummationFilter.unconditional ↑↑s)) [L.LeAtTop],
  HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b) L
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k : α} {h' : k ∈ Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l} (contains : k ∈ t),
      (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKey k h' = t.getKey k contains
-- LeanSearchClient.LoogleSyntax
/-- The argument to `#find`, a list of filters  -/
LeanSearchClient.loogle_filters : Lean.ParserDescr
-- Mathlib.Algebra.Exact.Basic
Function.Exact.of_comp_eq_zero_of_ker_in_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : Zero P],
  g ∘ f = 0 → (∀ (y : N), g y = 0 → y ∈ Set.range f) → Function.Exact f g
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toList_map : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → γ},
  (Std.Iter.map f it).toList = List.map f it.toList
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.map_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {d : CategoryTheory.Limits.Cone G}
  (hd : CategoryTheory.Limits.IsLimit d) (α : F ⟶ G) (j : J) {Z : C} (h : G.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.map c hd α)
      (CategoryTheory.CategoryStruct.comp (d.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (c.π.app j) (CategoryTheory.CategoryStruct.comp (α.app j) h)
-- Init.Data.Option.Lemmas
Option.guard_beq_some : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {x : α} {p : α → Bool}, (Option.guard p x == some x) = p x
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_sub_self_of_emod_eq : ∀ {a b c : ℤ}, a % b = c → b ∣ c - a
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.AEEqFun.Integrable.neg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α →ₘ[μ] β}, f.Integrable → (-f).Integrable
-- Mathlib.Topology.UniformSpace.Separation
IndiscreteTopology.eq_top_uniformSpace : ∀ {α : Type u_1} [u : UniformSpace α] [IndiscreteTopology α], u = ⊤
-- Mathlib.NumberTheory.WellApproximable
/-- In a seminormed group `A`, given `n : ℕ` and `δ : ℝ`, `approxOrderOf A n δ` is the set of
elements within a distance `δ` of a point of order `n`.  -/
approxOrderOf : (A : Type u_1) → [SeminormedGroup A] → ℕ → ℝ → Set A
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε], MeasureTheory.eLpNorm 0 p μ = 0
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_sup_atBot : ∀ {α : Type u_6} {β : Type u_7} [inst : SemilatticeSup α] {f g : β → α} (F : Filter β),
  Filter.Tendsto f F Filter.atBot → Filter.Tendsto g F Filter.atBot → Filter.Tendsto (fun x => f x ⊔ g x) F Filter.atBot
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The bottom of the `Subgraph G` lattice is isomorphic to the empty graph on the empty
vertex type.  -/
SimpleGraph.Subgraph.botIso : {V : Type u} → {G : SimpleGraph V} → ⊥.coe ≃g SimpleGraph.emptyGraph Empty
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_le_ofNat : ∀ {r : ℝ} {n : ℕ} [inst : n.AtLeastTwo], r.toNNReal ≤ OfNat.ofNat n ↔ r ≤ ↑n
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).H = c.pt
-- Mathlib.Order.Defs.Unbundled
InvImage.isTrans : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [IsTrans β r], IsTrans α (InvImage r f)
-- Std.Data.TreeMap.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.TreeMap.insertIfNew : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → β → Std.TreeMap α β cmp
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_eq_one : ∀ {α : Type u_1} {a : FreeMonoid α}, a.length = 1 ↔ ∃ m, a = FreeMonoid.of m
-- Mathlib.Analysis.Calculus.ParametricIntervalIntegral
/-- Derivative under integral of `x ↦ ∫ F x a` at a given point `x₀ : 𝕜`, `𝕜 = ℝ` or `𝕜 = ℂ`,
assuming `F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a neighborhood of `x₀` for ae `a`
(with a neighborhood independent of `a`) with integrable Lipschitz bound, and `F x` is
ae-measurable for `x` in a possibly smaller neighborhood of `x₀`.  -/
intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_lip : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] {a b : ℝ} {bound : ℝ → ℝ} {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜}
  {s : Set 𝕜},
  s ∈ nhds x₀ →
    (∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
      IntervalIntegrable (F x₀) μ a b →
        MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b)) →
          (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) s) →
            IntervalIntegrable bound μ a b →
              (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → HasDerivAt (fun x => F x t) (F' t) x₀) →
                IntervalIntegrable F' μ a b ∧
                  HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
-- Mathlib.Topology.Order
Continuous.le_induced : ∀ {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {t' : TopologicalSpace β} {f : α → β},
  Continuous f → t ≤ TopologicalSpace.induced f t'
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...hi) = (List.drop lo (List.take hi xs)).toArray
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dTo_eq_zero : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι},
  ¬c.Rel (c.prev j) j → C.dTo j = 0
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMax'.match_3.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → Sort u_2) (l : Ordnode α) (x : α)
  (h_1 : (l : Ordnode α) → (x : α) → motive l x Ordnode.nil)
  (h_2 :
    (l : Ordnode α) →
      (x : α) → (size : ℕ) → (rl : Ordnode α) → (rx : α) → (rr : Ordnode α) → motive l x (Ordnode.node size rl rx rr)),
  (match l, x, Ordnode.nil with
    | l, x, Ordnode.nil => h_1 l x
    | l, x, Ordnode.node size rl rx rr => h_2 l x size rl rx rr) =
    h_1 l x
-- Mathlib.Algebra.Group.Invertible.Basic
isUnit_of_invertible : ∀ {α : Type u} [inst : Monoid α] (a : α) [Invertible a], IsUnit a
-- Mathlib.Algebra.Group.Subgroup.Map
/-- The `MonoidHom` from a subgroup to its image.  -/
MonoidHom.subgroupMap : {G : Type u_1} →
  {G' : Type u_2} →
    [inst : Group G] → [inst_1 : Group G'] → (f : G →* G') → (H : Subgroup G) → ↥H →* ↥(Subgroup.map f H)
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- The `r`-Hölder (semi)norm in `ℝ≥0`.  -/
nnHolderNorm : {X : Type u_1} → {Y : Type u_2} → [PseudoEMetricSpace X] → [PseudoEMetricSpace Y] → NNReal → (X → Y) → NNReal
-- Init.Control.Option
/-- Handles failures by treating them as exceptions of type `Unit`.
 -/
OptionT.tryCatch : {m : Type u → Type v} → [Monad m] → {α : Type u} → OptionT m α → (PUnit.{u_1} → OptionT m α) → OptionT m α
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_def_lt' : ∀ {p : ℕ}, Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.monotone_gamma : Monotone Ordinal.gamma