mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Basic
LieHom.mk.congr_simp : ∀ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (toLinearMap toLinearMap_1 : L →ₗ[R] L')
  (e_toLinearMap : toLinearMap = toLinearMap_1)
  (map_lie' : ∀ {x y : L}, toLinearMap.toFun ⁅x, y⁆ = ⁅toLinearMap.toFun x, toLinearMap.toFun y⁆),
  { toLinearMap := toLinearMap, map_lie' := map_lie' } = { toLinearMap := toLinearMap_1, map_lie' := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.erase_equiv_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α}, (↑(m₁.erase k)).Equiv ↑(m₂.erase k)
-- Mathlib.Data.Nat.Factors
Nat.mem_primeFactorsList_mul : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → ∀ {p : ℕ}, p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The intermediate object in the factorization.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.mid : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CochainComplex C ℤ → CochainComplex C ℤ → [CategoryTheory.EnoughInjectives C] → ℤ → CochainComplex C ℤ
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum.eq_1 : ∀ {M : Type u_3} [inst : AddCommMonoid M], Multiset.sum = Multiset.foldr (fun x1 x2 => x1 + x2) 0
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Normed space structure constructed from an `InnerProductSpace.Core` structure, adjusting the
topology to make sure it is defeq to an already existing topology.  -/
InnerProductSpace.Core.toNormedAddCommGroupOfTopology : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] →
          [cd : InnerProductSpace.Core 𝕜 F] →
            [tF : TopologicalSpace F] →
              [IsTopologicalAddGroup F] →
                [ContinuousConstSMul 𝕜 F] →
                  ContinuousAt (fun v => inner 𝕜 v v) 0 →
                    Bornology.IsVonNBounded 𝕜 {v | RCLike.re (inner 𝕜 v v) < 1} → NormedAddCommGroup F
-- Mathlib.Topology.PartialHomeomorph.Basic
Set.partialHomeomorphSubtypeCoe_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X) (hs : Nonempty ↑s),
  ↑(s.partialHomeomorphSubtypeCoe hs) = Subtype.val
-- Mathlib.Algebra.BigOperators.Finprod
finsum_sum_comm : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (s : Finset β) (f : α → β → M),
  (∀ b ∈ s, Function.HasFiniteSupport fun a => f a b) → ∑ᶠ (a : α), ∑ b ∈ s, f a b = ∑ b ∈ s, ∑ᶠ (a : α), f a b
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.Quot.ι_desc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  (c : CategoryTheory.Limits.Cocone F) [inst_1 : DecidableEq J] (j : J) (x : ↑(F.obj j)),
  (AddCommGrpCat.Colimits.Quot.desc F c) ((AddCommGrpCat.Colimits.Quot.ι F j) x) =
    (CategoryTheory.ConcreteCategory.hom (c.ι.app j)) x
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.zsmul_le_zsmul : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.IntModule M] [Lean.Grind.OrderedAdd M]
  {a b : M} {k : ℤ}, 0 ≤ k → a ≤ b → k • a ≤ k • b
-- Init.Data.Array.Lemmas
Array.mem_flatten_of_mem : ∀ {α : Type u_1} {xss : Array (Array α)} {xs : Array α} {a : α}, xs ∈ xss → a ∈ xs → a ∈ xss.flatten
-- Mathlib.Topology.Algebra.Group.Basic
/-- Eta-expanded form of `ContinuousWithinAt.zpow` -/
ContinuousWithinAt.fun_zpow : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α} {s : Set α},
  ContinuousWithinAt f s x → ∀ (z : ℤ), ContinuousWithinAt (fun i => f i ^ z) s x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- This is the homology data for a short complex `S` that is obtained
from a left homology data `h₁` and a right homology data `h₂` when the comparison
morphism `leftRightHomologyComparison' h₁ h₂ : h₁.H ⟶ h₂.H` is an isomorphism.  -/
CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h₁ : S.LeftHomologyData) →
          (h₂ : S.RightHomologyData) →
            [CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)] → S.HomologyData
-- Mathlib.RepresentationTheory.Homological.Resolution
Representation.linearizeOfMulActionIso.eq_1 : ∀ (k : Type u) (G : Type v) [inst : Monoid G] [inst_1 : Semiring k] (H : Type w) [inst_2 : MulAction G H],
  Representation.linearizeOfMulActionIso k G H =
    Representation.Equiv.mk (LinearEquiv.refl k (MonoidAlgebra k (Action.ofMulAction G H).V)) ⋯
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsFunctor_map_hom : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] {X Y : Rep.{w, u, v} k G} (f : X ⟶ Y),
  ModuleCat.Hom.hom ((Rep.coinvariantsFunctor k G).map f) = Representation.Coinvariants.map X.ρ Y.ρ (Rep.Hom.hom f)
-- Init.Data.Iterators.Producers.Monadic.List
_private.Init.Data.Iterators.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_1.eq_3 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- Multiseries representing `basis[n] ^ r`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow : (basis : Tactic.ComputeAsymptotics.Basis) → ℕ → ℝ → Tactic.ComputeAsymptotics.MultiseriesExpansion basis
-- Aesop.Nanos
Aesop.Nanos.mk : ℕ → Aesop.Nanos
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄}
  [inst_4 : CategoryTheory.Category.{v₄, u₄} B] (H : CategoryTheory.Functor E B)
  [CategoryTheory.Limits.PreservesColimitsOfShape C H], CategoryTheory.Limits.PreservesColimitsOfShape D H
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.mul_length : ∀ {m1 m2 : Tactic.ComputeAsymptotics.UnitMonomial},
  List.length m1 = List.length m2 → List.length (m1.mul m2) = List.length m1
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsIntegral X] (U : X.Opens),
  AlgebraicGeometry.IsAffineOpen U →
    ∀ [inst_1 : Nonempty ↥↑U], IsFractionRing ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField
-- Mathlib.CategoryTheory.Filtered.Final
/-- The inclusion of the terminal object is final.  -/
CategoryTheory.Functor.final_const_terminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFiltered C] [inst_3 : CategoryTheory.Limits.HasTerminal D],
  ((CategoryTheory.Functor.const C).obj (⊤_ D)).Final
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_update : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i)
  [inst_3 : Decidable (b = 0)],
  (f.update i b).support = if b = 0 then (DFinsupp.erase i f).support else insert i f.support
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.sSup_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {Ss : Set (CategoryTheory.Sieve X)} {Y : C}
  (f : Y ⟶ X), (sSup Ss).arrows f ↔ ∃ S, ∃ (_ : S ∈ Ss), S.arrows f
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.LocallyOfFinitePresentation.SpecMap_iff : ∀ {R S : CommRingCat} (f : R ⟶ S),
  AlgebraicGeometry.LocallyOfFinitePresentation (AlgebraicGeometry.Spec.map f) ↔
    (CommRingCat.Hom.hom f).FinitePresentation
-- Init.Data.Int.Order
Int.lt_of_add_lt_add_left : ∀ {a b c : ℤ}, a + b < a + c → b < c
-- Batteries.Data.Array.Match
Array.Matcher.Iterator.mk.sizeOf_spec : ∀ {σ : Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [inst : BEq α] {m : Array.Matcher α}
  [inst_1 : Std.Iterator σ n α] [inst_2 : SizeOf σ] [inst_3 : (a : Type u_1) → SizeOf (n a)] [inst_4 : SizeOf α]
  (inner : Std.IterM n α) (state : Fin (m.table.size + 1)),
  sizeOf { inner := inner, state := state } = 1 + sizeOf inner + sizeOf state
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_apply_eq_zero : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {s : Set X},
  MeasurableSet s → (μ.variation s = 0 ↔ ∀ t ⊆ s, MeasurableSet t → μ t = 0)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_singleton_natCast : ∀ (R : Type uR) (A : Type uA) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (n : ℕ), R[↑n] = ⊥
-- Std.Async.Process
/-- Returns the available memory for allocation in bytes.
 -/
Std.IO.Process.availableMemory : IO UInt64
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {γ : Sort u_3} (I : γ → HomogeneousIdeal 𝒜),
  ProjectiveSpectrum.zeroLocus 𝒜 ↑(⨆ i, I i) = ⋂ i, ProjectiveSpectrum.zeroLocus 𝒜 ↑(I i)
-- Init.Data.Int.Order
Int.max_self : ∀ (a : ℤ), max a a = a
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso : ∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso], P.diagonal.toProperty.RespectsIso
-- Mathlib.Algebra.Group.Units.Equiv
Units.mulRight.eq_1 : ∀ {M : Type u_3} [inst : Monoid M] (u : Mˣ),
  u.mulRight = { toFun := fun x => x * ↑u, invFun := fun x => x * ↑u⁻¹, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂),
  (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 1 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁₂ f₃ f₄).obj 1)
-- Mathlib.Order.Directed
directedOn_pair' : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {a b : α}, r a b → DirectedOn r {b, a}
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.replaceVertex.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (s t : V) [inst : DecidableEq V],
  G.replaceVertex s t =
    { Adj := fun v w => if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
      symm := ⋯, loopless := ⋯ }
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.forall : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  {p : MulArchimedeanClass M → Prop}, (∀ (A : MulArchimedeanClass M), p A) ↔ ∀ (a : M), p (MulArchimedeanClass.mk a)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.conjStarAlgEquiv_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] (e : H ≃ₗᵢ[𝕜] K) (x : H →L[𝕜] H), e.conjStarAlgEquiv x = ↑↑e ∘SL x ∘SL ↑↑e.symm
-- Mathlib.CategoryTheory.Yoneda
/-- Variant of the Yoneda embedding which allows a raise in the universe level
for the category of types.  -/
CategoryTheory.uliftYoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁)))
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntryD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3)
  (fallback : (a : α) × β a) (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : (a : α) × β a) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_1 fallback
-- Init.Data.Vector.Lemmas
Vector.ne_and_not_mem_of_not_mem_push : ∀ {α : Type u_1} {n : ℕ} {a y : α} {xs : Vector α n}, a ∉ xs.push y → a ≠ y ∧ a ∉ xs
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.node.injEq : ∀ {α : Type u} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α) (c_1 : RBTree.RBColor)
  (l_1 : RBTree.RBNode α) (v_1 : α) (r_1 : RBTree.RBNode α),
  (RBTree.RBNode.node c l v r = RBTree.RBNode.node c_1 l_1 v_1 r_1) = (c = c_1 ∧ l = l_1 ∧ v = v_1 ∧ r = r_1)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Bounding the Hausdorff edistance by exhibiting, for any point in each set,
another point in the other set at controlled distance  -/
Metric.hausdorffEDist_le_of_mem_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α} {r : ENNReal},
  (∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r) → (∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r) → Metric.hausdorffEDist s t ≤ r
-- Mathlib.Topology.Defs.Filter
/-- A point `x` is a cluster point of a sequence `u` along a filter `F` if it is a cluster point
of `map u F`.  -/
MapClusterPt : {X : Type u_1} → [TopologicalSpace X] → {ι : Type u_3} → X → Filter ι → (ι → X) → Prop
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.instInhabitedCode : Inhabited Lean.Elab.Term.Do.Code
-- Init.Data.List.MapIdx
/-- Auxiliary for `mapFinIdx`:
`mapFinIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀ ⋯, f 1 a₁ ⋯, ...]`  -/
List.mapFinIdx.go : {α : Type u_1} →
  {β : Type u_2} →
    (as : List α) →
      ((i : ℕ) → α → i < as.length → β) → (bs : List α) → (acc : Array β) → bs.length + acc.size = as.length → List β
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing.inj : ∀ {h : Lean.Expr} {x : Int.Internal.Linear.Var} {e' : Int.Internal.Linear.Expr} {p : Int.Internal.Linear.Poly}
  {re : Lean.Meta.Grind.Arith.CommRing.RingExpr} {rp : Lean.Grind.CommRing.Poly} {p' : Int.Internal.Linear.Poly}
  {h_1 : Lean.Expr} {x_1 : Int.Internal.Linear.Var} {e'_1 : Int.Internal.Linear.Expr} {p_1 : Int.Internal.Linear.Poly}
  {re_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr} {rp_1 : Lean.Grind.CommRing.Poly} {p'_1 : Int.Internal.Linear.Poly},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing h x e' p re rp p' =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing h_1 x_1 e'_1 p_1 re_1 rp_1 p'_1 →
    h = h_1 ∧ x = x_1 ∧ e' = e'_1 ∧ p = p_1 ∧ re = re_1 ∧ rp = rp_1 ∧ p' = p'_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc.eq_1 : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] {j : ι} [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (c : f.Cell j),
  c.mapToSucc = SSet.Subcomplex.lift c.map ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- The composition of two left exact functors is left exact.  -/
CategoryTheory.Limits.comp_preservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteLimits F]
  [CategoryTheory.Limits.PreservesFiniteLimits G], CategoryTheory.Limits.PreservesFiniteLimits (F.comp G)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.map_mul : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (f : A →ₑ*[φ] B) (x y : A), f (x * y) = f x * f y
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
/-- The complex power function `x ↦ x^s` is integrable on `(0, t)` iff `-1 < s.re`.  -/
intervalIntegral.integrableOn_Ioo_cpow_iff : ∀ {s : ℂ} {t : ℝ}, 0 < t → (MeasureTheory.IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) MeasureTheory.volume ↔ -1 < s.re)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.insertNew.eq_1 : ∀ {α : Type u_1} (path : RBTree.RBNode.Path α) (v : α),
  path.insertNew v = path.ins (RBTree.RBNode.node RBTree.RBColor.red RBTree.RBNode.nil v RBTree.RBNode.nil)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.not_of_one_left : ∀ {α : Type u_1} [inst : Monoid α] (b : α), ¬FiniteMultiplicity 1 b
-- Mathlib.Order.Atoms
OrderIso.isCoatom_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] (f : α ≃o β) (a : α), IsCoatom (f a) ↔ IsCoatom a
-- Std.Time.Date.Unit.Day
Std.Time.Day.instOrdOrdinal : Ord Std.Time.Day.Ordinal
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_diff_of_contains_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        m₂.contains k = true → Std.DHashMap.Internal.Raw₀.Const.getD (m₁.diff m₂) k fallback = fallback
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- For `P` a property of ring homomorphisms, `affineLocally P` holds for `f : X ⟶ Y` if for each
affine open `U = Spec A ⊆ Y` and `V = Spec B ⊆ f ⁻¹' U`, the ring hom `A ⟶ B` satisfies `P`.
Also see `affineLocally_iff_affineOpens_le`.  -/
AlgebraicGeometry.affineLocally : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) →
  CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_eq_add_disjointOfDiffUnion_of_subset : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} {G : Type u_2} [inst : AddCommMonoid G]
  {m : MeasureTheory.AddContent G C} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C),
  (∀ t ∈ I, t ⊆ s) → (↑I).PairwiseDisjoint id → m s = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RcoSliceData.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rco α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α β) (range_1 : Std.Rco α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Init.Meta.Defs
Lean.instQuoteCharCharLitKind : Lean.Quote Char Lean.charLitKind
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_neg_of_nonpos_of_neg`.  -/
add_neg_of_nonpos_of_neg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b : α},
  a ≤ 0 → b < 0 → a + b < 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- **Alias** of `SimpleGraph.Walk.darts_dropUntil_subset_darts`. -/
SimpleGraph.Walk.darts_dropUntil_subset : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).darts ⊆ p.darts
-- Mathlib.NumberTheory.ModularForms.Cusps
IsCusp.smul : ∀ {c : OnePoint ℝ} {𝒢 : Subgroup (GL (Fin 2) ℝ)},
  IsCusp c 𝒢 → ∀ (g : GL (Fin 2) ℝ), IsCusp (g • c) (ConjAct.toConjAct g • 𝒢)
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.uncurry_two_eq_uncurry : ∀ (p : Fin 2 → Type u) (τ : Type u) (f : Function.FromTypes p τ), f.uncurry = Function.uncurry f ∘ ⇑(piFinTwoEquiv p)
-- Mathlib.Combinatorics.Hindman
Hindman.FS.below.tail' : ∀ {M : Type u_1} [inst : AddSemigroup M] {motive : (a : Stream' M) → (a_1 : M) → Hindman.FS a a_1 → Prop}
  (a : Stream' M) (m : M) (h : Hindman.FS a.tail m), Hindman.FS.below h → motive a.tail m h → Hindman.FS.below ⋯
-- Lean.DocString.Extension
/-- A custom inline element. The type of the value in the `Dynamic` determines how it is interpreted
and rendered.
 -/
Lean.ElabInline.custom : Dynamic → Lean.ElabInline
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.SpaceResult.mk : Bool → Bool → ℕ → Std.Format.SpaceResult✝
-- Mathlib.Data.Set.Card
/-- This is the same as `ncard_sdiff` but we require `t` to be finite instead.  -/
Set.ncard_sdiff' : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → autoParam t.Finite Set.ncard_sdiff'._auto_1 → (t \ s).ncard = t.ncard - s.ncard
-- Mathlib.Data.TypeVec
TypeVec.lastFun_appendFun : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : α.Arrow α') (g : β → β'),
  TypeVec.lastFun (f ::: g) = g
-- Mathlib.Algebra.Polynomial.FieldDivision
_private.Mathlib.Algebra.Polynomial.FieldDivision.0.Polynomial.remainder_lt_aux : ∀ {R : Type u} [inst : Field R] {q : Polynomial R} (p : Polynomial R), q ≠ 0 → (p.mod q).degree < q.degree
-- Mathlib.Data.FP.Basic
FP.nextUpPos : [C : FP.FloatCfg] → (e : ℤ) → (m : ℕ) → FP.ValidFinite e m → FP.Float
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
/-- If `C` is a Grothendieck abelian category, `X : C`, if `F : J ⥤ MonoOver X` is a
functor from a filtered category `J`, `c` is a colimit cocone for the corresponding
functor `J ⥤ C`, and `f : c.pt ⟶ X` is induced by the inclusions,
then `f` is a monomorphism.  -/
CategoryTheory.IsGrothendieckAbelian.mono_of_isColimit_monoOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [inst_3 : CategoryTheory.SmallCategory J]
  (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X)) [CategoryTheory.IsFiltered J]
  {c : CategoryTheory.Limits.Cocone (F.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X)))}
  (hc : CategoryTheory.Limits.IsColimit c) (f : c.pt ⟶ X),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) f = (F.obj j).obj.hom) → CategoryTheory.Mono f