mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Independent
/-- To check convex independence, one only has to check finsets thanks to Carathéodory's theorem.  -/
convexIndependent_iff_finset : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {p : ι → E},
  ConvexIndependent 𝕜 p ↔ ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(Finset.image p s) → x ∈ s
-- Lean.Environment
Lean.Environment.instBEqVisibility : BEq Lean.Environment.Visibility
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- A permutation is a cycle on `s` when any two points of `s` are related by repeated application
of the permutation. Note that this means the identity is a cycle of subsingleton sets.  -/
Equiv.Perm.IsCycleOn : {α : Type u_2} → Equiv.Perm α → Set α → Prop
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_eq_head_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅},
  t.min he = t.toList.head ⋯
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Inversion on a topological group, as a uniform equivalence between the right uniformity and
the left uniformity.  -/
UniformEquiv.inv : (G : Type u_1) → [inst : Group G] → [inst_1 : TopologicalSpace G] → [inst_2 : IsTopologicalGroup G] → G ≃ᵤ G
-- Mathlib.Topology.Maps.Proper.Basic
/-- A map `f : X → Y` between two topological spaces is said to be **proper** if it is continuous
and, for all `ℱ : Filter X`, any cluster point of `map f ℱ` is the image by `f` of a cluster point
of `ℱ`.  -/
IsProperMap : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_int_eq_zero_add_tsum_pnat : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] [T2Space G]
  {f : ℤ → G}, Summable f → ∑' (n : ℤ), f n = f 0 + ∑' (n : ℕ+), f ↑↑n + ∑' (n : ℕ+), f (-↑↑n)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_hom_snd_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd f₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
        (CategoryTheory.Limits.pullback.snd f₃ f₄)) =
    CategoryTheory.Limits.pullback.snd
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.instAddLeftStrictMono : AddLeftStrictMono Ordinal.{u}
-- Mathlib.SetTheory.Cardinal.Aleph
/-- An ordinal is initial when it is the first ordinal with a given cardinality.

This is written as `o.card.ord = o`, i.e. `o` is the smallest ordinal with cardinality `o.card`.  -/
Ordinal.IsInitial : Ordinal.{u_1} → Prop
-- Init.Data.List.Lemmas
List.head_eq_of_cons_eq : ∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → h₁ = h₂
-- Std.Do.SPred.Laws
Std.Do.SVal.evalsTo_cons : ∀ {α σ : Type u} {σs : List (Type u)} {f : Std.Do.SVal (σ :: σs) α} {a : α} {s : σ}, f.evalsTo a s = (f s).evalsTo a
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.add_eq_right_iff_mul_omega0_le : ∀ {a b : Ordinal.{u_1}}, a + b = b ↔ a * Ordinal.omega0 ≤ b
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey?_modifyKey_eq_maxKey? : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α]
  {k : α} {f : β → β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.maxKey? (Std.Internal.List.Const.modifyKey k f l) = Std.Internal.List.maxKey? l
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- Unexpander for the `!₂[x, y, ...]` notation.  -/
EuclideanSpace.delabVecNotation : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Data.Fin.Tuple.Basic
/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
given by separating out the `p`-th element of the tuple.

This is `Fin.insertNth` as an `Equiv`.  -/
Fin.insertNthEquiv : {n : ℕ} →
  (α : Fin (n + 1) → Type u) → (p : Fin (n + 1)) → α p × ((i : Fin n) → α (p.succAbove i)) ≃ ((i : Fin (n + 1)) → α i)
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instCoeOutLinearMapId : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → CoeOut (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- `f` is line-differentiable at the point `x` in the direction `v` if there
exists `f'` such that `f (x + t v) = f x + t • f' + o (t)` when `t` tends to `0`.  -/
LineDifferentiableAt : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} →
      [inst_1 : NormedAddCommGroup F] →
        [NormedSpace 𝕜 F] → {E : Type u_3} → [inst_3 : AddCommGroup E] → [Module 𝕜 E] → (E → F) → E → E → Prop
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_eq_zero_of_constantCoeff_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.constantCoeff p ≠ 0 → p.natTrailingDegree = 0
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.id_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.CategoryStruct.id S).τ₁ = CategoryTheory.CategoryStruct.id S.X₁
-- Init.Data.Fin.Lemmas
Fin.one_mul : ∀ {n : ℕ} [inst : NeZero n] (k : Fin n), 1 * k = k
-- Mathlib.Tactic.Sat.FromLRAT
/-- `v.neg lit` asserts that literal `lit` is falsified in the valuation.  -/
Sat.Valuation.neg : Sat.Valuation → Sat.Literal → Prop
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (j : C), ((t.triangleω₁δ a b c hab hbc).obj j).obj₃ = (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj j)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter_eq_affineCombination : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.excenter signs = (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The type of smoothness exponents, consisting of all natural numbers and two special terms `∞`
and `ω`.
Natural numbers `n` correspond to `n`-fold continuous differentiability, `∞` to smoothness, and `ω`
to analyticity.  -/
ContDiff.«termℕ∞ω» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RicSliceData.mk : {α : Type u} →
  [inst : Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Std.Ric α → Std.DTreeMap.Internal.Unit.RicSliceData α
-- Mathlib.LinearAlgebra.FreeModule.IdealQuotient
Ideal.finrank_quotient_eq_sum : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
  [inst_4 : IsPrincipalIdealRing R] [inst_5 : IsDomain S] (F : Type u_4) [inst_6 : CommRing F] [inst_7 : Algebra F R]
  [inst_8 : Algebra F S] [IsScalarTower F R S] {I : Ideal S} (hI : I ≠ ⊥) {ι : Type u_5} [inst_10 : Fintype ι]
  (b : Module.Basis ι R S) [Nontrivial F] [∀ (i : ι), Module.Free F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})]
  [∀ (i : ι), Module.Finite F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})],
  Module.finrank F (S ⧸ I) = ∑ i, Module.finrank F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})
-- Mathlib.GroupTheory.Congruence.Defs
Con.conGen_monotone : ∀ {M : Type u_1} [inst : Mul M], Monotone conGen
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.comap_map_eq_self : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {f : R →+* S} {s : Subring R},
  ⇑f ⁻¹' {0} ⊆ ↑s → Subring.comap f (Subring.map f s) = s
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The lambda function of the incidence algebra is the function that assigns `1` to every nonempty
interval of cardinality one or two.  -/
IncidenceAlgebra.lambda : (𝕜 : Type u_2) →
  {α : Type u_5} →
    [inst : Zero 𝕜] → [One 𝕜] → [inst_2 : Preorder α] → [DecidableRel fun x1 x2 => x1 ⩿ x2] → IncidenceAlgebra 𝕜 α
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.equivQuotMaximalIdeal_apply_mk : ∀ {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] (Rₚ : Type u_8) [inst_2 : CommRing Rₚ]
  [inst_3 : Algebra R Rₚ] [inst_4 : IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ] (x : R),
  (IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) x) =
    (Ideal.Quotient.mk (IsLocalRing.maximalIdeal Rₚ)) ((algebraMap R Rₚ) x)
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpace_add_chainTop : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  α ≠ 0 → LieModule.genWeightSpace M (α + ⇑(LieModule.chainTop α β)) = ⊥
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.decidableMemPow.eq_1 : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α} [inst_1 : Fintype α] [inst_2 : DecidableEq α]
  [inst_3 : DecidablePred fun x => x ∈ s] (n : ℕ),
  Set.decidableMemPow n = Nat.recAux (⋯.mpr inferInstance) (fun n ih => ⋯.mpr inferInstance) n
-- Lean.Widget.InteractiveGoal
/-- The user-friendly name for each hypothesis.
Note that these are not `Name`s: they are pretty-printed
and do not remember the macro scopes.  -/
Lean.Widget.InteractiveHypothesisBundle.names : Lean.Widget.InteractiveHypothesisBundle → Array String
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.ediam_preimage_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (s : Set X),
  Metric.ediam (⇑Metric.Snowflaking.ofSnowflaking ⁻¹' s) = Metric.ediam s ^ α
-- Mathlib.Logic.Function.Basic
Function.flip_curry : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α × β → γ), flip (Function.curry f) = Function.curry (f ∘ Prod.swap)
-- Mathlib.Order.InitialSeg
PrincipalSeg.apply_subrelIso : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) (b : { b // s b f.top }),
  f.toRelEmbedding (f.subrelIso b) = ↑b
-- Lean.Elab.Tactic.Conv.Basic
/-- Mark goals of the form `⊢ a = ?m ..` with the conv goal annotation  -/
Lean.Elab.Tactic.Conv.remarkAsConvGoal : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Order.Module.Basic
abs_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [IsOrderedRing R] [inst_3 : AddCommGroup M]
  [inst_4 : LinearOrder M] [IsOrderedAddMonoid M] [inst_6 : Module R M] [PosSMulMono R M] (a : R) (b : M),
  |a • b| = |a| • |b|
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.mk.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} {w : ℕ} (aig : Std.Sat.AIG α)
  (q q_1 : aig.RefVec w),
  q = q_1 →
    ∀ (r r_1 : aig.RefVec w),
      r = r_1 →
        ∀ (hle : old.decls.size ≤ aig.decls.size),
          { aig := aig, q := q, r := r, hle := hle } = { aig := aig, q := q_1, r := r_1, hle := hle }
-- Mathlib.Condensed.Light.Functors
/-- Dot notation for the value of `lightProfiniteToLightCondSet`.  -/
LightProfinite.toCondensed : LightProfinite → LightCondSet
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.boundaries₂_le_cycles₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.boundaries₂ A ≤ groupHomology.cycles₂ A
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the numerator of the second right fraction  -/
CategoryTheory.MorphismProperty.RightFraction₂.f' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.RightFraction₂ X Y) → self.X' ⟶ Y
-- Mathlib.Logic.Relation
/-- **Alias** of `irrefl_iff_le_ne`. -/
irrefl_iff_subrelation_ne : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Irrefl r ↔ r ≤ Ne
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} {μs : ℕ → MeasureTheory.Measure Ω}
  [∀ (i : ℕ), MeasureTheory.IsProbabilityMeasure (μs i)] {f : BoundedContinuousFunction Ω ℝ},
  0 ≤ f →
    (∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) Filter.atTop) →
      ∫ (x : Ω), f x ∂μ ≤ Filter.liminf (fun i => ∫ (x : Ω), f x ∂μs i) Filter.atTop
-- Lean.Elab.Quotation
/-- check induced by the pattern  -/
Lean.Elab.Term.Quotation.HeadInfo.check : Lean.Elab.Term.Quotation.HeadInfo → Lean.Elab.Term.Quotation.HeadCheck
-- Mathlib.Topology.Convenient.Category
/-- Constructor for objects in the category of `X`-generated spaces.  -/
GeneratedByTopCat.of : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      (Y : Type v) → [inst_1 : TopologicalSpace Y] → [Topology.IsGeneratedBy X Y] → GeneratedByTopCat X
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
disjoint_closedBall_ball_iff : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} {δ ε : ℝ},
  0 ≤ δ → 0 < ε → (Disjoint (Metric.closedBall x δ) (Metric.ball y ε) ↔ δ + ε ≤ dist x y)
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_add_right_pos : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α),
  a ∈ t → (s + t).erase a = s + t.erase a
-- Mathlib.Data.Set.Prod
Set.mapsTo_snd_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, Set.MapsTo Prod.snd (s ×ˢ t) t
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_le_iff_le : ∀ {a b : ℕ} (ha : a < UInt8.size) (hb : b < UInt8.size), UInt8.ofNatLT a ha ≤ UInt8.ofNatLT b hb ↔ a ≤ b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.DHashMap.Internal.Raw₀.Const.getD
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k fallback =
      fallback
-- Mathlib.Order.SuccPred.Basic
Order.wcovBy_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] (a : α), a ⩿ Order.succ a
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_eq_primeFactorsList_multiset : ∀ (n : ℕ), n.factorization = Multiset.toFinsupp ↑n.primeFactorsList
-- Mathlib.Analysis.Complex.Periodic
/-- If `f` is periodic, holomorphic near `I∞`, and tends to zero at `I∞`, then in fact it tends to zero
exponentially fast.
 -/
Function.Periodic.exp_decay_of_zero_at_inf : ∀ {h : ℝ} {f : ℂ → ℂ},
  0 < h →
    Function.Periodic f ↑h →
      (∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) →
        (Filter.comap Complex.im Filter.atTop).ZeroAtFilter f →
          f =O[Filter.comap Complex.im Filter.atTop] fun z => Real.exp (-2 * Real.pi * z.im / h)
-- Init.Omega.Int
Lean.Omega.Int.le_of_not_lt : ∀ {x y : ℤ}, ¬x < y → y ≤ x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_snd : ∀ {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 S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (φ : S ⟶ S') (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.map φ).app x).snd = φ.snd.app x
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instIsCharPUSizeHPowNatOfNatNumBits : Lean.Grind.IsCharP USize (2 ^ System.Platform.numBits)
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
List.toList_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {l : List β}, (l.iterM m).toList = pure l
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Quotients of `X`-generated spaces are `X`-generated.  -/
Quot.isGeneratedBy : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [Topology.IsGeneratedBy X Y] {r : Y → Y → Prop}, Topology.IsGeneratedBy X (Quot r)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.mergeSort.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : α → α → Bool),
  x.mergeSort x_1 =
    match x, x_1 with
    | [], x => []
    | [a], x => [a]
    | a :: b :: xs, le =>
      have lr := List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩;
      have this := ⋯;
      have this := ⋯;
      ((↑lr.1).mergeSort le).merge ((↑lr.2).mergeSort le) le
-- Mathlib.Data.Set.Function
Set.SurjOn.image_preimage : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t t₁ : Set β} {f : α → β}, Set.SurjOn f s t → t₁ ⊆ t → f '' f ⁻¹' t₁ = t₁
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexFuel.eq_1 : ∀ (m₁ m₂ : Lean.Grind.CommRing.Mon), Lean.Grind.CommRing.Mon.revlexFuel 0 m₁ m₂ = m₁.revlexWF m₂
-- Mathlib.RingTheory.RingHom.Smooth
/-- The identity of a ring is smooth.  -/
RingHom.Smooth.id : ∀ (R : Type u_3) [inst : CommRing R], (RingHom.id R).Smooth
-- Init.Data.BitVec.Basic
BitVec.mul_eq : ∀ {w : ℕ} (x y : BitVec w), x.mul y = x * y
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extended_zero : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N),
  FractionalIdeal.extended L hf 0 = 0
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.epi_of_cancel_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q : C} (f : P ⟶ Q),
  (∀ {R : C} (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0) → CategoryTheory.Epi f
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mem_toSubmonoid : ∀ {K : Type u} [inst : DivisionRing K] {s : Subfield K} {x : K}, x ∈ s.toSubmonoid ↔ x ∈ s
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.sameCycle_symm_apply_right`. -/
Equiv.Perm.SameCycle.of_symm_apply_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x ((Equiv.symm f) y) → f.SameCycle x y
-- Mathlib.Topology.Instances.PNat
PNat.dist_coe : ∀ (x y : ℕ+), dist ↑x ↑y = dist x y
-- Mathlib.Data.List.Infix
List.map_tails : ∀ {α : Type u_1} {l : List α} {β : Type u_3} (g : α → β), (List.map g l).tails = List.map (List.map g) l.tails
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldr_eq_foldr_toList : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {f : (a : α) → β a → δ → δ}
  {init : δ}, Std.DTreeMap.Internal.Impl.foldr f init t = List.foldr (fun a b => f a.fst a.snd b) init t.toList
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_div_hasSum_exp_of_mem_ball : ∀ (𝕂 : Type u_1) {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedDivisionRing 𝔸]
  [inst_2 : NormedAlgebra 𝕂 𝔸] [CharZero 𝕂] [CompleteSpace 𝔸],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius, HasSum (fun n => x ^ n / ↑n.factorial) (NormedSpace.exp x)
-- Mathlib.GroupTheory.Schreier
/-- **Schreier's Lemma**: If `R : Set G` and `H : AddSubgroup G`
are complements with `0 ∈ R`, and if `G` is generated by `S : Set G`,
then `H` is generated by the `Set` `(R + S).image (fun g ↦ g - (hR.toRightFun g))`.  -/
AddSubgroup.closure_add_image_eq : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {R S : Set G} (hR : AddSubgroup.IsComplement (↑H) R),
  0 ∈ R → AddSubgroup.closure S = ⊤ → AddSubgroup.closure ((fun g => g + -↑(hR.toRightFun g)) '' (R + S)) = H
-- Mathlib.Analysis.Normed.Group.Basic
mem_sphere_one_iff_norm : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E} {r : ℝ}, a ∈ Metric.sphere 1 r ↔ ‖a‖ = r
-- Mathlib.Order.RelClasses
/-- Set notation form of `not_le_of_gt` -/
not_subset_of_ssuperset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → ¬b ⊆ a
-- Mathlib.Algebra.Order.Hom.Units
OrderMonoidIso.unitsCongr_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Monoid α] [inst_2 : Preorder β] [inst_3 : Monoid β]
  (e : α ≃*o β) (x : βˣ), ↑(e.unitsCongr.symm x) = e.symm ↑x
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Ioi_bot : ∀ {α : Type u_1} [inst : Preorder α], WithBot.some ⁻¹' Set.Ioi ⊥ = Set.univ
-- Init.Data.Array.Lemmas
Array.append_inj_right : ∀ {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α}, xs₁ ++ ys₁ = xs₂ ++ ys₂ → xs₁.size = xs₂.size → ys₁ = ys₂
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- On the translated support, `p.shift v` agrees with `p.config` at the preimage.

More precisely, if `w ∈ p.support`, then at the translated site `v + w`,
the configuration `p.shift v` takes the value `p.config w`.

This uses `[IsLeftCancelAdd G]` to identify the unique preimage of `v + w`
under left-translation by `v`.  -/
SymbolicDynamics.FullShift.Pattern.shift_apply_add_left_of_mem : ∀ {A : Type u_1} [inst : Inhabited A] {G : Type u_2} [inst_1 : AddMonoid G] [IsLeftCancelAdd G]
  (p : SymbolicDynamics.FullShift.Pattern A G) (v w : G), w ∈ p.support → p.shift v (v + w) = p.config w
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.«term__ⁿ» : Lean.TrailingParserDescr
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- Given a log-size ball sequence `(Vᵢ, tᵢ, rᵢ)`, we define the pair set sequence by
`Kᵢ = {tᵢ} × {x ∈ Vᵢ | dist(tᵢ, x) ≤ rᵢc}`.  -/
PairReduction.pairSetSeq : {T : Type u_1} → [PseudoEMetricSpace T] → [DecidableEq T] → Finset T → ENNReal → ENNReal → ℕ → Finset (T × T)
-- Mathlib.Combinatorics.Quiver.Symmetric
Prefunctor.mapReverseComp : ∀ {U : Type u_1} {V : Type u_2} {W : Type u_3} [inst : Quiver U] [inst_1 : Quiver V] [inst_2 : Quiver W]
  [inst_3 : Quiver.HasReverse U] [inst_4 : Quiver.HasReverse V] [inst_5 : Quiver.HasReverse W] (φ : U ⥤q V) (ψ : V ⥤q W)
  [φ.MapReverse] [ψ.MapReverse], (φ ⋙q ψ).MapReverse