mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffOn.clm_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5} [inst_7 : NormedAddCommGroup X]
  [inst_8 : NormedSpace 𝕜 X] {n : WithTop ℕ∞} {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} {s : Set X},
  ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (fun x => g x ∘SL f x) s
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Epi S.v₂₃.τ₃
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkColGt.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.π_comp_cokernelComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (G.map f))
      (CategoryTheory.Limits.cokernelComparison f G) =
    G.map (CategoryTheory.Limits.cokernel.π f)
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.ElementaryEmbedding M N), L.ElementarilyEquivalent M N
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point}
  {f g : Φ₁ ⟶ Φ₂}, f = g ↔ f.hom = g.hom
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.mk_coe : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {f : 𝒜 →ₐᵍ[R] ℬ}
  (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x y : A),
      { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) =
        { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x y : A),
      (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
        (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x +
          (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y)
  (h₅ :
    ∀ (r : R),
      (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
        (algebraMap R B) r)
  (h₆ :
    ∀ {i : ι} {x : A},
      x ∈ 𝒜 i →
        { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom x ∈
          ℬ i),
  { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_mem := h₆ } = f
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- If `v` and `w` are two non-trivial and inequivalent absolute values then we can find an `a : R`
such that `1 < v a` while `w a < 1`.
 -/
AbsoluteValue.exists_one_lt_lt_one_of_not_isEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : Semifield S] [inst_2 : LinearOrder S] [IsStrictOrderedRing S]
  [Archimedean S] [ExistsAddOfLE S] {v w : AbsoluteValue R S},
  v.IsNontrivial → w.IsNontrivial → ¬v.IsEquiv w → ∃ a, 1 < v a ∧ w a < 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} [inst_1 : Inhabited (β a)], t.isEmpty = true → t.get! a = default
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.leftInverse_of_injective_of_isClosed_range.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_5} {F : Type u_6} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : CompleteSpace E]
  [inst_6 : CompleteSpace F] (f : E →L[𝕜] F) (hf : Function.Injective ⇑f) (hf' : IsClosed (Set.range ⇑f)),
  f.leftInverse_of_injective_of_isClosed_range hf hf' = f.leftInverse_of_injective_of_isClosed_range hf hf'
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.trans_eq`. -/
HasSubset.subset.trans_eq : ∀ {α : Type u_1} {a b c : α} [inst : LE α], a ≤ b → b = c → a ≤ c
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.toDilation : {X : Type u_1} → {Y : Type u_2} → [inst : PseudoEMetricSpace X] → [inst_1 : PseudoEMetricSpace Y] → X ≃ᵈ Y → X →ᵈ Y
-- Mathlib.GroupTheory.Torsion
/-- Torsion groups are closed under extensions.  -/
IsMulTorsion.extension_closed : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] {N : Subgroup G} [inst_1 : Group H] {f : G →* H},
  N = f.ker → IsMulTorsion H → IsMulTorsion ↥N → IsMulTorsion G
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- `X ⟶ X` is the terminal object of `P.Over ⊤ X`.  -/
CategoryTheory.MorphismProperty.Over.mkIdTerminal : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      (X : T) →
        [inst_1 : P.ContainsIdentities] →
          CategoryTheory.Limits.IsTerminal
            (CategoryTheory.MorphismProperty.Over.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Use the axiom of choice to extract explicit `BinaryBiproductData F` from `HasBinaryBiproduct F`.
 -/
CategoryTheory.Limits.getBinaryBiproductData : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P Q : C) → [CategoryTheory.Limits.HasBinaryBiproduct P Q] → CategoryTheory.Limits.BinaryBiproductData P Q
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.isTheta_sub : ∀ {𝕜 : 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} {s : Set E},
  HasFDerivWithinAt f f' s x → Topology.IsInducing ⇑f' → (fun x_1 => f x_1 - f x) =Θ[nhdsWithin x s] fun x_1 => x_1 - x
-- Mathlib.Analysis.Analytic.Inverse
/-- The right inverse to a formal multilinear series is indeed a right inverse, provided its linear
term is invertible and its constant term vanishes.  -/
FormalMultilinearSeries.comp_rightInv : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E),
  p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i →
    p.comp (p.rightInv i x) = FormalMultilinearSeries.id 𝕜 F ((p 0) 0)
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Binder name for the parameter.  -/
Lean.PrettyPrinter.Delaborator.ParamKind.name : Lean.PrettyPrinter.Delaborator.ParamKind → Lean.Name
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.mem_fundCircuit : ∀ {α : Type u_1} (M : Matroid α) (e : α) (I : Set α), e ∈ M.fundCircuit e I
-- Mathlib.RingTheory.WittVector.Identities
/-- The “projection formula” for Frobenius and Verschiebung.  -/
WittVector.verschiebung_mul_frobenius : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x y : WittVector p R),
  WittVector.verschiebung (x * WittVector.frobenius y) = WittVector.verschiebung x * y
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instNSMul : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [VectorBundle 𝕜 F V] → SMul ℕ (ContMDiffSection I F n V)
-- Mathlib.Topology.Category.Stonean.Basic
/-- `Stonean` is the category of extremally disconnected compact Hausdorff spaces.  -/
Stonean : Type (u_1 + 1)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_add_right_eq_map : ∀ {m n : ℤ}, (m...m + n).toList = List.map (fun x => x + m) (0...n).toList
-- Mathlib.Order.Filter.Pointwise
Filter.mem_sub : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α} {s : Set α}, s ∈ f - g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ - t₂ ⊆ s
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.keep.sizeOf_spec : ∀ (basis_hd : ℝ → ℝ) {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (ex : Tactic.ComputeAsymptotics.BasisExtension basis_tl),
  sizeOf (Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex) = 1 + sizeOf basis_tl + sizeOf ex
-- Mathlib.Order.FixedPoints
OrderHom.isLeast_lfp_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), IsLeast {a | f a ≤ a} (OrderHom.lfp f)
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_add_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [inst : ProbabilityTheory.IsSFiniteKernel κ] {f g : α → β → ENNReal},
  Measurable (Function.uncurry f) →
    Measurable (Function.uncurry g) → κ.withDensity (f + g) = κ.withDensity f + κ.withDensity g
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prevn_le : ∀ {s : String.Slice} {p : s.Pos} {n : ℕ}, p.prevn n ≤ p
-- Mathlib.GroupTheory.SpecificGroups.Alternating
Equiv.Perm.closure_three_cycles_eq_alternating : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], Subgroup.closure {σ | σ.IsThreeCycle} = alternatingGroup α
-- Mathlib.Topology.MetricSpace.Infsep
Set.le_einfsep_pi_of_le : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoEMetricSpace (X b)]
  {s : (b : β) → Set (X b)} {c : ENNReal}, (∀ (b : β), c ≤ (s b).einfsep) → c ≤ (Set.univ.pi s).einfsep
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_c_ne_zero' : ∀ {R : Type u_1} {c d : R} [inst : Semiring R], c ≠ 0 → { a := 0, b := 0, c := c, d := d }.toPoly.natDegree = 1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFactor_ne_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.mixedEmbedding.convexBodySumFactor K ≠ 0
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.pointwise_smul_le_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S T : Subring R}, a • S ≤ a • T ↔ S ≤ T
-- Mathlib.Data.Finset.Image
Finset.map_val : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α), (Finset.map f s).val = Multiset.map (⇑f) s.val
-- Mathlib.CategoryTheory.Localization.Bifunctor
/-- the isomorphism `(((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F` expressing
that `F` is induced by `F'` up to an isomorphism  -/
CategoryTheory.Localization.Lifting₂.iso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          {inst : CategoryTheory.Category.{v_1, u_1} C₁} →
            {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} →
              {inst_2 : CategoryTheory.Category.{v_3, u_3} D₁} →
                {inst_3 : CategoryTheory.Category.{v_4, u_4} D₂} →
                  {inst_4 : CategoryTheory.Category.{v_5, u_5} E} →
                    (L₁ : CategoryTheory.Functor C₁ D₁) →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                              (F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) →
                                [self : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F F'] →
                                  (((CategoryTheory.Functor.whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseP_eq_eraseIdx.match_1.splitter : (motive : Option ℕ → Sort u_1) → (x : Option ℕ) → (Unit → motive none) → ((i : ℕ) → motive (some i)) → motive x
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformInducing_iff_uniformSpace : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f ↔ UniformSpace.comap f inst_1 = inst
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.prod.eq_1 : ∀ {α : Type u} [inst : Group α], FreeGroup.prod = FreeGroup.lift id
-- Mathlib.NumberTheory.Dioph
Poly.sumsq.eq_2 : ∀ {α : Type u_1} (p : Poly α) (ps : List (Poly α)), Poly.sumsq (p :: ps) = p * p + Poly.sumsq ps
-- Mathlib.GroupTheory.Coset.Basic
mem_leftAddCoset_leftAddCoset : ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) {a : α}, a +ᵥ ↑s = ↑s → a ∈ s
-- Mathlib.Order.Filter.Pointwise
Filter.frequently_zero : ∀ {α : Type u_2} [inst : Zero α] {p : α → Prop}, (∃ᶠ (x : α) in 0, p x) ↔ p 0
-- Mathlib.Order.BoundedOrder.Basic
ULift.instTop.eq_1 : ∀ {α : Type u} [inst : Top α], ULift.instTop = { top := { down := ⊤ } }
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.isQuasiInverse_subtype_projectionOnto_iff : ∀ {K : Type u_1} {V : Type u_2} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S T : Submodule K V} (hST : IsCompl S T), S.subtype.IsQuasiInverse (S.projectionOnto T hST) ↔ IsNoetherian K ↥T
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {k a : α} {v : β}, (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.sSameSide_affineSpan_pair_point_incenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → line[ℝ, t.points i₂, t.points i₃].SSameSide (t.points i₁) (Affine.Simplex.incenter t)
-- Std.Do.Triple.SpecLemmas
List.Cursor.current.congr_simp : ∀ {α : Type u_1} {l : List α} (c c_1 : l.Cursor) (e_c : c = c_1) (h : 0 < c.suffix.length), c.current h = c_1.current ⋯
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_takeWhile_eq_true : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.startsWith pat = false → (s.takeWhile pat).isEmpty = true
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_X : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C))
  (j : J), ((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).obj j).X = P.X.obj j
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Restrict a cocone to the diagram under `j`. This preserves being colimiting if the forgetful functor
`Over j ⥤ J` is final (see `CategoryTheory.Limits.IsColimit.underPost`).
 -/
CategoryTheory.Limits.Cocone.underPost : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {D : CategoryTheory.Functor J C} →
          CategoryTheory.Limits.Cocone D → (j : J) → CategoryTheory.Limits.Cocone (CategoryTheory.Under.post D)
-- Mathlib.Data.Finset.Dedup
Finset.coe_toList : ∀ {α : Type u_1} (s : Finset α), ↑s.toList = s.val
-- Init.Data.String.Basic
String.Slice.Pos.lt_cast_iff : ∀ {s t : String.Slice} {pos : t.Pos} {pos' : s.Pos} {h : s.copy = t.copy}, pos < pos'.cast h ↔ pos.cast ⋯ < pos'
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.mem_range_derivFamily : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι],
  (∀ (i : ι), Order.IsNormal (f i)) → ∀ {a : Ordinal.{u}}, a ∈ Set.range (Ordinal.derivFamily f) ↔ ∀ (i : ι), f i a = a
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
/-- Returns the pair `(charInst, c)`. If the ring does not have a `IsCharP` instance, then throws internal error.
 -/
Lean.Meta.Grind.Arith.CommRing.getCharInst : Lean.Meta.Grind.Arith.CommRing.RingM (Lean.Expr × ℕ)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.of.injEq : ∀ (a a_1 : Mathlib.Tactic.BicategoryLike.Atom₁),
  (Mathlib.Tactic.BicategoryLike.Mor₁.of a = Mathlib.Tactic.BicategoryLike.Mor₁.of a_1) = (a = a_1)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.nonuniformWitnesses.eq_1 : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] (ε : 𝕜) (s t : Finset α),
  G.nonuniformWitnesses ε s t = if h : ¬G.IsUniform ε s t then (⋯.choose, ⋯.choose) else (s, t)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryGE.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive :
            (x : Std.DTreeMap.Internal.Impl α fun x => β) →
              x.Ordered → (∃ a ∈ x, (compare a k).isGE = true) → Sort u_3) →
          (x : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x_1 : x.Ordered) →
              (x_2 : ∃ a ∈ x, (compare a k).isGE = true) →
                ((x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
                    (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true) →
                      motive Std.DTreeMap.Internal.Impl.leaf x he) →
                  ((size : ℕ) →
                      (ky : α) →
                        (y : β) →
                          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
                            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
                              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true) →
                                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he) →
                    motive x x_1 x_2
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univBall.eq_1 : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ),
  OpenPartialHomeomorph.univBall c r =
    if h : 0 < r then OpenPartialHomeomorph.univUnitBall.trans' (OpenPartialHomeomorph.unitBallBall c r h) ⋯
    else (IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph
-- Mathlib.CategoryTheory.Abelian.Basic
/-- An abelian category has finite biproducts.  -/
CategoryTheory.Abelian.hasFiniteBiproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasFiniteBiproducts C
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.nonempty_of_prop : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : C},
  P X → P.Nonempty
-- Mathlib.Analysis.Normed.MulAction
edist_smul_le : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
  [inst_2 : SMulZeroClass α β] [IsBoundedSMul α β] (s : α) (x y : β), edist (s • x) (s • y) ≤ ‖s‖₊ • edist x y
-- Mathlib.CategoryTheory.Action.Basic
Action.mk.inj : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {G : Type u_2} {inst_1 : Monoid G} {V_1 : V}
  {ρ : G →* CategoryTheory.End V_1} {V_2 : V} {ρ_1 : G →* CategoryTheory.End V_2},
  { V := V_1, ρ := ρ } = { V := V_2, ρ := ρ_1 } → V_1 = V_2 ∧ ρ ≍ ρ_1
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The backward direction of the homeomorphism
between the cube $I^N$ and $I × I^{N\setminus\{j\}}$.  -/
Cube.insertAt : {N : Type u_1} → [DecidableEq N] → (i : N) → ↑unitInterval × ({ j // j ≠ i } → ↑unitInterval) ≃ₜ (N → ↑unitInterval)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.map_lift_pullbackComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPullback f g] [inst_3 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  {W : C} {h : W ⟶ X} {k : W ⟶ Y} (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.lift h k w))
      (CategoryTheory.Limits.pullbackComparison G f g) =
    CategoryTheory.Limits.pullback.lift (G.map h) (G.map k) ⋯
-- Mathlib.Algebra.DirectSum.Module
DirectSum.coeLinearMap_eq_dfinsuppSum : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (A : ι → Submodule R M) [inst_3 : DecidableEq M] (x : DirectSum ι fun i => ↥(A i)),
  (DirectSum.coeLinearMap A) x = DFinsupp.sum x fun i x => ↑x
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.prop_inf_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) (X : C),
  (P ⊓ Q) X ↔ P X ∧ Q X
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DeclarationParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.DeclarationParams
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.mul.injEq : ∀ {R : Type u} (a b a_1 b_1 : Rack.PreEnvelGroup R), (a.mul b = a_1.mul b_1) = (a = a_1 ∧ b = b_1)
-- Init.Data.Array.Range
/-- Variant of `mem_zipIdx` specialized at `k = 0`.  -/
Array.mem_zipIdx' : ∀ {α : Type u_1} {x : α} {i : ℕ} {xs : Array α} (h : (x, i) ∈ xs.zipIdx), i < xs.size ∧ x = xs[i]
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.mk.injEq : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} (inner inner_1 : Std.IterM m β),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- `HasSum` over `Nat.Primes` iff over `ℕ` extending `f` by `0`.  -/
Nat.Primes.hasSum_iff_hasSum_ite : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] (f : ℕ → M) {a : M},
  HasSum (fun p => f ↑p) a ↔ HasSum (fun n => if Nat.Prime n then f n else 0) a