mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk_simplex : ∀ {X : SSet} {A : X.Subcomplex} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n)
  (hx' : x ∉ A.obj (Opposite.op { len := n })), (SSet.Subcomplex.N.mk x hx hx').simplex = x
-- Mathlib.RingTheory.Ideal.Maps
Ideal.eq_map_of_comap_eq_ker_sup : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] (f : A →+* B),
  Function.Surjective ⇑f → ∀ {I : Ideal B} {J : Ideal A}, Ideal.comap f I = RingHom.ker f ⊔ J → I = Ideal.map f J
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_of_mem_unitary : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Algebra ℝ A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {U : A}, U ∈ unitary A → CFC.abs U = 1
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.isPrefixOf.eq_1 : ∀ {α : Type u} [inst : BEq α] (as bs : Array α),
  as.isPrefixOf bs = if h : as.size ≤ bs.size then as.isPrefixOfAux bs h 0 else false
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.exp_sub_sum_range_isBigO_pow : ∀ (n : ℕ), (fun x => Real.exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i.factorial) =O[nhds 0] fun x => x ^ n
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocsArray.erase : Lean.Meta.Simp.SimprocsArray → Lean.Name → Lean.Meta.Simp.SimprocsArray
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.topology_eq_scottHausdorff : ∀ {α : Type u_3} {D : Set (Set α)} {inst : Preorder α} {inst_1 : TopologicalSpace α}
  [self : Topology.IsScottHausdorff α D], inst_1 = Topology.scottHausdorff α D
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lcs_add_le_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] {N₁ N₂ : LieSubmodule R L M}
  [inst_6 : LieModule R L M] (l k : ℕ), LieSubmodule.lcs (l + k) N₁ ≤ N₂ ↔ LieSubmodule.lcs l N₁ ≤ LieSubmodule.ucs k N₂
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.map_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : PowerSeries R) (T : Subring R) (hp : ∀ (n : ℕ), (PowerSeries.coeff n) p ∈ T),
  (PowerSeries.map T.subtype) (p.toSubring T hp) = p
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_inv_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).counitIso.inv.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Lean.Util.Profile
_private.Lean.Util.Profile.0.Lean.get_profiler : Lean.Options → Bool
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative of a sum of two measures.
See also `rnDeriv_add'`, which requires sigma-finite `ν₁`, `ν₂` and `μ`.  -/
MeasureTheory.Measure.rnDeriv_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν₁ ν₂ μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν₁]
  [MeasureTheory.IsFiniteMeasure ν₂] [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ]
  [(ν₁ + ν₂).HaveLebesgueDecomposition μ], (ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.mk.injEq : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G] (inl : N →* E)
  (rightHom : E →* G) (inl_injective : Function.Injective ⇑inl) (range_inl_eq_ker_rightHom : inl.range = rightHom.ker)
  (rightHom_surjective : Function.Surjective ⇑rightHom) (inl_1 : N →* E) (rightHom_1 : E →* G)
  (inl_injective_1 : Function.Injective ⇑inl_1) (range_inl_eq_ker_rightHom_1 : inl_1.range = rightHom_1.ker)
  (rightHom_surjective_1 : Function.Surjective ⇑rightHom_1),
  ({ inl := inl, rightHom := rightHom, inl_injective := inl_injective,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom, rightHom_surjective := rightHom_surjective } =
      { inl := inl_1, rightHom := rightHom_1, inl_injective := inl_injective_1,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom_1, rightHom_surjective := rightHom_surjective_1 }) =
    (inl = inl_1 ∧ rightHom = rightHom_1)
-- Mathlib.Data.ZMod.Basic
ZMod.val_inv_mul : ∀ {m n : ℕ}, m.Coprime n → ↑(↑m)⁻¹.val * ↑m = 1
-- Batteries.Tactic.Lint.Frontend
/-- `high`: print output of every check.  -/
Batteries.Tactic.Lint.LintVerbosity.high : Batteries.Tactic.Lint.LintVerbosity
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_union_eq : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s t : Set α),
  MeasureTheory.ae (μ.restrict (s ∪ t)) = MeasureTheory.ae (μ.restrict s) ⊔ MeasureTheory.ae (μ.restrict t)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.norm_lt_iff : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)) {M : ℝ}, 0 < M → (‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
/-- Rewrite the Gamma integral as an example of a Mellin transform.  -/
Complex.GammaIntegral_eq_mellin : Complex.GammaIntegral = mellin fun x => ↑(Real.exp (-x))
-- Mathlib.NumberTheory.ModularForms.Basic
SlashInvariantForm.mul.congr_simp : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] {k₁ k₂ : ℤ} (f f_1 : SlashInvariantForm Γ k₁),
  f = f_1 → ∀ (g g_1 : SlashInvariantForm Γ k₂), g = g_1 → f.mul g = f_1.mul g_1
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObj.toRingObj : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {R : C} → [self : CategoryTheory.CommRingObj R] → CategoryTheory.RingObj R
-- Init.Data.Array.Lemmas
Array.exists_mem_of_size_eq_add_one : ∀ {α : Type u_1} {n : ℕ} {xs : Array α}, xs.size = n + 1 → ∃ a, a ∈ xs
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAt_const_add_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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasFDerivAt (fun x => c + f x) f' x ↔ HasFDerivAt f f' x
-- Mathlib.Data.Set.Sigma
Set.mk_preimage_sigma_fn_eq_if : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {β : Type u_7}
  [inst : DecidablePred fun x => x ∈ s] (g : β → α i),
  (fun b => ⟨i, g b⟩) ⁻¹' s.sigma t = if i ∈ s then g ⁻¹' t i else ∅
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.String.mangleAux : (s : String) → s.Pos → String → String
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.extend.eq_1 : ∀ {B : Type u_2} (F : Type u_3) {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] [inst_3 : (x : B) → Zero (E x)]
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_5 : FiberBundle F E] {x : B} (v₀ : E x) (x' : B),
  FiberBundle.extend F v₀ x' = (trivializationAt F E x).symm x' (↑(trivializationAt F E x) ⟨x, v₀⟩).2
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instTopologicalSpaceHomFintypeCatObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C},
  CategoryTheory.PreGaloisCategory.instTopologicalSpaceHomFintypeCatObj F =
    TopologicalSpace.coinduced (fun f => CategoryTheory.ObjectProperty.homMk (TypeCat.ofHom f)) inferInstance
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_dite_compl`. -/
Set.restrict_dite_compl : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : (x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β)
  (g : (a : α) → a ∉ s → β), (sᶜ.domRestrict fun a => if h : a ∈ s then f a h else g a h) = fun a => g ↑a ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_mul' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightMono α] {a b c d : α},
  a ≤ b → c ≤ d → a * c ≤ b * d
-- Mathlib.Order.Bounds.Basic
directedOn_or_directedOn_of_union' : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α},
  (s ∪ t).Nonempty →
    DirectedOn (fun x1 x2 => x1 ≤ x2) (s ∪ t) →
      DirectedOn (fun x1 x2 => x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 => x1 ≤ x2) t ∧ t.Nonempty
-- Mathlib.GroupTheory.Congruence.Basic
Con.quotientKerEquivOfRightInverse.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P) (g : P → M)
  (hf : Function.RightInverse g ⇑f),
  Con.quotientKerEquivOfRightInverse f g hf =
    { toFun := ⇑(Con.kerLift f), invFun := Con.toQuotient ∘ g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Order.Filter.Basic
Filter.frequently_iff : ∀ {α : Type u} {f : Filter α} {P : α → Prop}, (∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.IntFractPair.coe_stream'_rat_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] {v : K}
  {q : ℚ},
  v = ↑q →
    Stream'.map (Option.map (GenContFract.IntFractPair.mapFr Rat.cast)) (GenContFract.IntFractPair.stream q) =
      GenContFract.IntFractPair.stream v
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.bot_ext_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y : ↥⊥},
  x = y ↔ True
-- Mathlib.Analysis.Matrix.PosDef
/-- A Hermitian matrix is positive-definite if and only if its eigenvalues are positive.  -/
Matrix.IsHermitian.posDef_iff_eigenvalues_pos : ∀ {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype n] [inst_1 : RCLike 𝕜] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.PosDef ↔ ∀ (i : n), 0 < hA.eigenvalues i
-- Mathlib.Analysis.Normed.Group.BallSphere
/-- We equip the closed ball, in a seminormed group, with a formal operation of negation, namely the
antipodal map.  -/
instInvolutiveNegElemClosedBallOfNat : {E : Type u_1} → [i : SeminormedAddCommGroup E] → {r : ℝ} → InvolutiveNeg ↑(Metric.closedBall 0 r)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂).get k h' = m₁.get k ⋯
-- Std.Data.TreeMap.Lemmas
/-- Simpler variant of `getElem!_filterMap` when `LawfulEqCmp` is available.  -/
Std.TreeMap.getElem!_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited γ] {f : α → β → Option γ} {k : α},
  (Std.TreeMap.filterMap f t)[k]! = (t[k]?.bind (f k)).get!
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Bundled version of lax monoidal functors. This type is equipped with a category
structure in `CategoryTheory.Monoidal.NaturalTransformation`.  -/
CategoryTheory.LaxMonoidalFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      (D : Type u₂) →
        [inst : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory D] → Type (max (max (max u₁ u₂) v₁) v₂)
-- Init.Control.StateRef
/-- A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref ω σ`).

The macro `StateRefT σ m α` infers `ω` from `m`. It should normally be used instead.
 -/
StateRefT' : Type → Type → (Type → Type) → Type → Type
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.sheafify_sheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F),
  CategoryTheory.Presieve.IsSheaf J F →
    CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.sheafify J G) =
      CategoryTheory.Subfunctor.sheafify J G
-- Mathlib.Algebra.Category.Ring.Constructions
_private.Mathlib.Algebra.Category.Ring.Constructions.0.CategoryTheory.Limits.WalkingPair.swap.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) (h_1 : Unit → motive CategoryTheory.Limits.WalkingPair.left)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingPair.right),
  (match CategoryTheory.Limits.WalkingPair.right with
    | CategoryTheory.Limits.WalkingPair.left => h_1 ()
    | CategoryTheory.Limits.WalkingPair.right => h_2 ()) =
    h_2 ()
-- Mathlib.Data.Finsupp.MonomialOrder
/-- Given a monomial order, notation for the corresponding strict order relation on `σ →₀ ℕ`  -/
MonomialOrder.«term_≺[_]_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Reindexing by the composition of two equivalences is the same as reindexing twice.  -/
Affine.Simplex.reindex_trans : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n₁ n₂ n₃ : ℕ} (e₁₂ : Fin (n₁ + 1) ≃ Fin (n₂ + 1)) (e₂₃ : Fin (n₂ + 1) ≃ Fin (n₃ + 1))
  (s : Affine.Simplex k P n₁), s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.SplitIf.reduceIte' : ℕ → Bool → Lean.Meta.Simp.Simproc
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiableOn_section_of_subsingleton : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x} {u : Set B}
  [Subsingleton F], MDiff[u] (T% s)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_uncurry : ∀ {ι : Type u_6} {κ : Type u_7} {X : Type u_8} [inst : MeasurableSpace X], Measurable Function.uncurry
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterWithPostcondition.match_1.splitter : {β : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} →
      (out : β) →
        (motive : Subtype (f out).Property → Sort u_3) →
          (__do_lift : Subtype (f out).Property) →
            ((h' : (f out).Property { down := false }) → motive ⟨{ down := false }, h'⟩) →
              ((h' : (f out).Property { down := true }) → motive ⟨{ down := true }, h'⟩) → motive __do_lift
-- Mathlib.Data.Finsupp.Basic
Finsupp.sigmaFinsuppAddEquivPiFinsupp_apply : ∀ {η : Type u_13} [inst : Fintype η] {α : Type u_15} {ιs : η → Type u_16} [inst_1 : AddMonoid α]
  (f : (j : η) × ιs j →₀ α) (j : η) (i : ιs j), (Finsupp.sigmaFinsuppAddEquivPiFinsupp f j) i = f ⟨j, i⟩
-- Mathlib.FieldTheory.IsPerfectClosure
pNilradical.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (p : ℕ), pNilradical R p = if 1 < p then nilradical R else ⊥
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.negDvdTight : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.combine'.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  (match 0 with
    | 0 => h_1 ()
    | fuel.succ => h_2 fuel) =
    h_1 ()
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.isCollinear_singleton' : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (a : Projectivization K V), Projectivization.IsCollinear {a}
-- Init.Data.Array.Lemmas
Array.flatMap_reverse : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β},
  Array.flatMap f xs.reverse = (Array.flatMap (Array.reverse ∘ f) xs).reverse
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHSubOffset_1 : HSub Std.Time.WallTime Std.Time.Week.Offset Std.Time.WallTime
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.coe_nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] (x : ↑(Set.Ico 0 1)), 0 ≤ ↑x
-- Lean.Parser.Extra
Lean.Parser.leadingNode.formatter : Lean.SyntaxNodeKind → ℕ → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Hom.WithTopBot
InfHom.withTop.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (f : InfHom α β),
  f.withTop = { toFun := WithTop.map ⇑f, map_inf' := ⋯, map_top' := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Expressions for coherence isomorphisms (i.e., structural 2-morphisms
given by `BicategoricalCoherence.iso`).  -/
Mathlib.Tactic.BicategoryLike.CoherenceHom : Type
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_min : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Group α] (a b : α), (a ⊓ b)⁺ᵐ = a⁺ᵐ ⊓ b⁺ᵐ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_nat : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k] (n : ℕ), SkewMonoidAlgebra.single 1 ↑n = ↑n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ {l : List α} {k : α}, k ∈ t.insertMany l ↔ k ∈ t ∨ l.contains k = true
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' fallback : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → (t.insertMany l).getKeyD k' fallback = k
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_inter_le_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (m₁ ∩ m₂).size ≤ m₁.size
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- The Mellin transform of `P.f` is globally convergent. Private since it is superseded by
`IsStrongFEPair.differentiable_Λ` below.  -/
_private.Mathlib.NumberTheory.LSeries.AbstractFuncEq.0.IsStrongFEPair.differentiable_mellin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → Differentiable ℂ (mellin P.f)
-- Mathlib.Order.Antichain
isAntichain_coe_univ_iff : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain (fun x1 x2 => r ↑x1 ↑x2) Set.univ ↔ IsAntichain r s
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.cobounded_neBot : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [Nontrivial E], (Bornology.cobounded E).NeBot
-- Mathlib.Algebra.Order.Interval.Basic
Interval.bot_pow : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] {n : ℕ}, n ≠ 0 → ⊥ ^ n = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.NoAccidental.eq_or_eq_or_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)}
  [self : SimpleGraph.TripartiteFromTriangles.NoAccidental t] ⦃a a' : α⦄ ⦃b b' : β⦄ ⦃c c' : γ⦄,
  (a', b, c) ∈ t → (a, b', c) ∈ t → (a, b, c') ∈ t → a = a' ∨ b = b' ∨ c = c'
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom : ∀ {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} {r s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G),
  CategoryTheory.CategoryStruct.comp (P.lift r) (P.conePointsIsoOfNatIso Q w).hom =
    CategoryTheory.Limits.IsLimit.map r Q w.hom
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.centerToMulOpposite_symm_apply_coe : ∀ {M : Type u_2} [inst : MulOneClass M] (r : ↥(Subsemigroup.center Mᵐᵒᵖ)),
  ↑(Submonoid.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.map_of_preservesLeftHomologyOf : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C},
  S.Exact →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S]
      [(S.map F).HasHomology], (S.map F).Exact
-- Mathlib.RingTheory.TensorProduct.Maps
/-- Construct an isomorphism between tensor products of an S-algebra with an R-algebra
from S- and R- isomorphisms between the tensor factors.
 -/
Algebra.TensorProduct.congr : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        {C : Type uC} →
          {D : Type uD} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring S] →
                [inst_2 : Algebra R S] →
                  [inst_3 : Semiring A] →
                    [inst_4 : Algebra R A] →
                      [inst_5 : Algebra S A] →
                        [inst_6 : IsScalarTower R S A] →
                          [inst_7 : Semiring B] →
                            [inst_8 : Algebra R B] →
                              [inst_9 : Semiring C] →
                                [inst_10 : Algebra R C] →
                                  [inst_11 : Algebra S C] →
                                    [inst_12 : IsScalarTower R S C] →
                                      [inst_13 : Semiring D] →
                                        [inst_14 : Algebra R D] →
                                          (A ≃ₐ[S] C) → (B ≃ₐ[R] D) → TensorProduct R A B ≃ₐ[S] TensorProduct R C D
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.antisymm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E], Std.Antisymm (IsExtreme 𝕜)
-- Std.Data.String.ToNat
Break.runK.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : Option α) (h_1 : (a : α) → motive (some a))
  (h_2 : Unit → motive none),
  x = none →
    (match x with
      | some a => h_1 a
      | none => h_2 ()) ≍
      h_2 ()
-- Mathlib.Algebra.CharP.Algebra
RingHom.charP_iff_charP : ∀ {K : Type u_3} {L : Type u_4} [inst : DivisionRing K] [inst_1 : NonAssocSemiring L] [Nontrivial L] (f : K →+* L)
  (p : ℕ), CharP K p ↔ CharP L p
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.diagram_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : (J.Cover X)ᵒᵖ),
  (J.diagram P X).obj S = CategoryTheory.Limits.multiequalizer ((Opposite.unop S).index P)