mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lift_comp_includeLeft : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [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 S C] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C)
  (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)),
  (Algebra.TensorProduct.lift f g hfg).comp Algebra.TensorProduct.includeLeft = f
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.traceCls : Lean.Name
-- Lean.Data.Json.Basic
Lean.Json.Structured.obj.inj : ∀ {kvPairs kvPairs_1 : Std.TreeMap.Raw String Lean.Json compare},
  Lean.Json.Structured.obj kvPairs = Lean.Json.Structured.obj kvPairs_1 → kvPairs = kvPairs_1
-- Mathlib.RingTheory.RingHom.Flat
CommRingCat.instIsStableUnderCobaseChangeFlat : CommRingCat.flat.IsStableUnderCobaseChange
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.add_le_iff_nonpos_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : AddZeroClass α] [IsAddCommutative α] [AddLeftMono α] {a b : α},
  AddLECancellable a → (b + a ≤ a ↔ b ≤ 0)
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_values_discrete : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (a : PadicSeq p), ¬a ≈ 0 → ∃ z, a.norm = ↑p ^ (-z)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.saturation_saturation : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid}, (s.saturation M H).saturation M ⋯ = s.saturation M H
-- Init.Data.ByteArray.Lemmas
ByteArray.empty_append : ∀ {b : ByteArray}, ByteArray.empty ++ b = b
-- Init.Data.SInt.Bitwise
Int16.toBitVec_and : ∀ (a b : Int16), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_flattenList : ∀ {w : ℕ} (vs : List (BitVec w)) (i : ℕ), (BitVec.flattenList vs).getMsbD i = (vs[i / w]?.getD 0#w).getMsbD (i % w)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The derived category of an abelian category.  -/
DerivedCategory : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [HasDerivedCategory C] → Type (max u v)
-- Mathlib.Order.SuccPred.Limit
IsGLB.isPredPrelimit_of_notMem : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α] {s : Set α}, IsGLB s a → a ∉ s → Order.IsPredPrelimit a
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd.instIsProbabilityMeasure : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} [MeasureTheory.IsProbabilityMeasure ρ], MeasureTheory.IsProbabilityMeasure ρ.snd
-- Mathlib.CategoryTheory.Action.Monoidal
Action.leftDual_ρ : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {H : Type u_3} [inst_2 : Group H] (X : Action V H) [inst_3 : CategoryTheory.LeftRigidCategory V] (h : H),
  (ᘁX).ρ h = ᘁX.ρ h⁻¹
-- Mathlib.Order.InitialSeg
/-- Composition of functions shows that `≼i` is transitive  -/
InitialSeg.trans : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → InitialSeg r s → InitialSeg s t → InitialSeg r t
-- Mathlib.Logic.Function.Basic
Function.update_comm : ∀ {α : Sort u_2} [inst : DecidableEq α] {β : α → Sort u_1} {a b : α},
  a ≠ b →
    ∀ (v : β a) (w : β b) (f : (a : α) → β a),
      Function.update (Function.update f a v) b w = Function.update (Function.update f b w) a v
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_eq_some_get! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], a ∈ t → t.get? a = some (t.get! a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂)
  {h' : k ∈ m₁ ∪ m₂}, Std.DHashMap.Raw.Const.get (m₁ ∪ m₂) k h' = Std.DHashMap.Raw.Const.get m₁ k ⋯
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.Subalgebra.restrictScalars_adjoin : ∀ (R : Type uR) {S : Type uS} {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] {s : Set A},
  Subalgebra.restrictScalars R (Algebra.adjoin S s) = (IsScalarTower.toAlgHom R S A).range ⊔ Algebra.adjoin R s
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The Lévy-Prokhorov edistance between measures:
`d(μ,ν) = inf {r ≥ 0 | ∀ B, μ B ≤ ν Bᵣ + r ∧ ν B ≤ μ Bᵣ + r}`.  -/
MeasureTheory.levyProkhorovEDist : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] → [PseudoEMetricSpace Ω] → MeasureTheory.Measure Ω → MeasureTheory.Measure Ω → ENNReal
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.coherentTopology.instIsDenseSubsite : ∀ {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] (F : CategoryTheory.Functor C D)
  [inst_2 : F.PreservesFiniteEffectiveEpiFamilies] [inst_3 : F.ReflectsFiniteEffectiveEpiFamilies] [inst_4 : F.Full]
  [inst_5 : F.Faithful] [inst_6 : F.EffectivelyEnough] [inst_7 : CategoryTheory.Precoherent D],
  CategoryTheory.Functor.IsDenseSubsite (CategoryTheory.coherentTopology C) (CategoryTheory.coherentTopology D) F
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp h.rightHomologyIso.inv S.rightHomologyι =
    CategoryTheory.CategoryStruct.comp h.ι h.opcyclesIso.inv
-- Mathlib.Analysis.Calculus.Taylor
/-- The Taylor polynomial with derivatives inside of a set `s` considered as a function `ℝ → E`  -/
taylorWithinEval : {E : Type u_2} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E) → ℕ → Set ℝ → ℝ → ℝ → E
-- Init.Data.List.FinRange
Fin.foldrM_eq_foldrM_finRange : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α),
  Fin.foldrM n f x = List.foldrM f x (List.finRange n)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.ofList l cmp) k' = some v
-- Mathlib.Data.List.Sigma
List.nodupKeys_dedupKeys : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (l : List (Sigma β)), l.dedupKeys.NodupKeys
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
/-- The preimage of a finite-index normal additive subgroup under an additive homomorphism.  -/
FiniteIndexNormalAddSubgroup.comap : {G : Type u_1} →
  [inst : AddGroup G] →
    {H : Type u_2} → [inst_1 : AddGroup H] → (G →+ H) → FiniteIndexNormalAddSubgroup H → FiniteIndexNormalAddSubgroup G
-- Mathlib.Algebra.Quaternion
Quaternion.instFinite : ∀ {R : Type u_3} [inst : CommRing R], Module.Finite R (Quaternion R)
-- Lean.Parser.Command
Lean.Parser.Command.open.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ : C)
  {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' C).obj X₁).map φ).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₃)
-- Mathlib.Topology.ContinuousMap.Periodic
/-- Summing the translates of `f` by `ℤ • p` gives a map which is periodic with period `p`.
(This is true without any convergence conditions, since if the sum doesn't converge it is taken to
be the zero map, which is periodic.)  -/
ContinuousMap.periodic_tsum_comp_add_zsmul : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : AddCommGroup X]
  [inst_3 : ContinuousAdd X] [inst_4 : AddCommMonoid Y] [inst_5 : ContinuousAdd Y] [T2Space Y] (f : C(X, Y)) (p : X),
  Function.Periodic (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)))) p
-- Mathlib.RingTheory.Jacobson.Ring
RingHom.FiniteType.isJacobsonRing : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B} [IsJacobsonRing A],
  f.FiniteType → IsJacobsonRing B
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.isPrincipal_opow_ord : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Ordinal.IsPrincipal (fun x1 x2 => x1 ^ x2) c.ord
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.exists_gcf_pair_rat_eq_nth_conts : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) (n : ℕ),
  ∃ conts, (GenContFract.of v).conts n = GenContFract.Pair.map Rat.cast conts
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- If `i : X ⟶ Y` is a monomorphism of simplicial sets and `d : ℕ`, this is
a coproduct of copies of `∂Δ[d]` indexed by the nondegenerate `d`-simplices of `Y`
not in the range of `i`.  -/
SSet.relativeCellComplexOfMono.sigmaBoundary : {X Y : SSet} → (X ⟶ Y) → ℕ → SSet
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.sInf_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (S : Set (I.Filtration M)), (sInf S).N = sInf (Ideal.Filtration.N '' S)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_nonneg : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, 0 ≤ μ.real s
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_apply_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel γ δ} {x : α × γ} [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsSFiniteKernel η] (s : Set β) (t : Set δ), ((κ.parallelComp η) x) (s ×ˢ t) = (κ x.1) s * (η x.2) t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        Std.DTreeMap.Internal.Impl.Const.get? (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k =
          Std.DTreeMap.Internal.Impl.Const.get? t k
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_obj_left_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.hom = sq.f₁₂
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_getElem_length : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.support[p.length] = v
-- Mathlib.Tactic.Coe
/-- Partially applied coercion.  Equivalent to the η-reduction of `(↑ ·)`  -/
Lean.Elab.Term.CoeImpl.«term(↑)» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_fst : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀),
  CategoryTheory.CategoryStruct.comp (I.glueDataT'Aux U V W U₀ hU₀)
      (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))
        (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)))
      (CategoryTheory.CategoryStruct.comp (I.glueDataT U V)
        (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)))
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_H : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_3),
  (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).H =
    CategoryTheory.Limits.kernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)
-- Mathlib.Algebra.Group.Basic
one_div_mul_one_div_rev : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), 1 / a * (1 / b) = 1 / (b * a)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- An injective linear map with finite-dimensional domain is a closed embedding.  -/
LinearMap.isClosedEmbedding_of_injective : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E]
  [ContinuousSMul 𝕜 E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [inst_10 : Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space E] [FiniteDimensional 𝕜 E] [T2Space F] {f : E →ₗ[𝕜] F},
  f.ker = ⊥ → Topology.IsClosedEmbedding ⇑f
-- Init.SimpLemmas
Bool.true_or : ∀ (b : Bool), (true || b) = true
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `f` is a Lipschitz continuous map, then `dimH (f '' s) ≤ dimH s`.  -/
LipschitzWith.dimH_image_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {K : NNReal} {f : X → Y},
  LipschitzWith K f → ∀ (s : Set X), dimH (f '' s) ≤ dimH s
-- Init.Data.Vector.Range
/-- Replace `zipIdx` with a starting index `i+1` with `zipIdx` starting from `i`,
followed by a `map` increasing the indices by one.  -/
Vector.zipIdx_succ : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ},
  xs.zipIdx (i + 1) =
    Vector.map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      (xs.zipIdx i)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toLp_neg : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.MemLp (⇑f) p μ),
  (-f).toLp ⋯ = -f.toLp hf
-- Init.Data.UInt.Bitwise
UInt64.toUInt16_not : ∀ (a : UInt64), (~~~a).toUInt16 = ~~~a.toUInt16
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet_le_torsionBySet_of_subset : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Set R},
  s ⊆ t → Submodule.torsionBySet R M t ≤ Submodule.torsionBySet R M s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, a ∈ t.insertIfNew k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.Data.Rel
SetRel.comp_sUnion : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (𝒮 : Set (SetRel β γ)),
  R.comp (⋃₀ 𝒮) = ⋃ S ∈ 𝒮, R.comp S
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquivClass.toBialgHomClass : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] [inst_7 : EquivLike F A B] [BialgEquivClass F R A B], BialgHomClass F R A B
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_sliceTo_eq_false_iff : ∀ {s : String.Slice} {p : s.Pos}, (s.sliceTo p).isEmpty = false ↔ p ≠ s.startPos
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg : ∀ {α : Type u_1} [inst : Zero α] (p : Prop) [inst_1 : Decidable p] {a b : α} [inst_2 : Preorder α],
  0 < a → 0 ≤ b → 0 ≤ if p then a else b
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.hom_comp : ∀ {X Y Z : CpltSepUniformSpace} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g) =
    ⟨⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f), ⋯⟩
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j₁ j₂ j₃ : J}
  (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (iter₃ : Φ.Iteration j₃) {k₁ k₂ k₃ : J} (h₁₂ : k₁ ≤ k₂)
  (h₂₃ : k₂ ≤ k₃) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (h₃ : k₃ ≤ j₃) (h₁₂' : j₁ ≤ j₂) (h₂₃' : j₂ ≤ j₃),
  CategoryTheory.CategoryStruct.comp (iter₁.mapObj iter₂ h₁₂ h₁ h₂ h₁₂') (iter₂.mapObj iter₃ h₂₃ h₂ h₃ h₂₃') =
    iter₁.mapObj iter₃ ⋯ h₁ h₃ ⋯
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- A version of SGA3 XXI Lemma 1.2.1 (10), adapted to change of rings.  -/
RootPairing.rootFormIn_self_smul_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : Module S N] [IsScalarTower S R N] [inst_12 : P.IsValuedIn S]
  [inst_13 : Fintype ι] (i : ι),
  ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i = 2 • (P.PolarizationIn S) (P.rootSpanMem S i)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.foldl_eq : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {f : δ → (a : α) → β a → δ} {init : δ}
  {l : Std.DHashMap.Internal.AssocList α β},
  Std.DHashMap.Internal.AssocList.foldl f init l = List.foldl (fun d p => f d p.fst p.snd) init l.toList
-- Std.Internal.Do.ExceptPost
/-- Exception postcondition value notation: `epost⟨h₁, h₂⟩` for nested `EPost.Cons.mk`.  -/
Std.Internal.Do.«termEpost⟨_⟩» : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius_compl : ∀ {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.exradius signsᶜ = s.exradius signs
-- Lean.Setup
Lean.instToJsonImport : Lean.ToJson Lean.Import
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_inf_uniformSpace : ∀ {β : Type v} {u v : UniformSpace β} {F : Filter β}, Cauchy F ↔ Cauchy F ∧ Cauchy F
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.mul_mem_left_iff : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α} [I.IsTwoSided] [I.IsPrime] {x y : α}, x ∉ I → (x * y ∈ I ↔ y ∈ I)
-- Mathlib.RingTheory.PowerSeries.Inverse
/-- `Unit_of_divided_by_X_pow_order` is the unit power series obtained by dividing a non-zero
power series by the largest power of `X` that divides it.  -/
PowerSeries.Unit_of_divided_by_X_pow_order : {k : Type u_2} → [inst : Field k] → PowerSeries k → (PowerSeries k)ˣ
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsOpenEmbedding id
-- Lean.Data.Lsp.Internal
/-- Whether the module is being imported via `meta import`.  -/
Lean.Lsp.ImportInfo.isMeta : Lean.Lsp.ImportInfo → Bool
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0),
  (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.lift φ α β eq)).comp
      ↑(CochainComplex.mappingCone.fst φ) ⋯ =
    ↑α
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_mul`

---

The order is additive when multiplying meromorphic functions.  -/
fun_meromorphicOrderAt_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f g : 𝕜 → 𝕜'},
  MeromorphicAt f x →
    MeromorphicAt g x → meromorphicOrderAt (fun i => f i * g i) x = meromorphicOrderAt f x + meromorphicOrderAt g x
-- Mathlib.RingTheory.Extension.Generators
/-- If `P` is a family of generators of `S` over `R` and `T` is an `R`-algebra, we
obtain a natural family of generators of `T ⊗[R] S` over `T`.  -/
Algebra.Generators.baseChange : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            (T : Type u_2) →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] → Algebra.Generators R S ι → Algebra.Generators T (TensorProduct R T S) ι
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.ae_eq_zero_of_lintegral_rpow_eq_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ},
  0 ≤ p → ∀ {f : α → ENNReal}, AEMeasurable f μ → ∫⁻ (a : α), f a ^ p ∂μ = 0 → f =ᵐ[μ] 0
-- Mathlib.Analysis.Normed.Module.Dual
NormedSpace.closedBall_inv_subset_polar_closedBall : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {r : ℝ}, Metric.closedBall 0 r⁻¹ ⊆ StrongDual.polar 𝕜 (Metric.closedBall 0 r)
-- Init.Data.Option.Lemmas
Option.get_dite' : ∀ {β : Type u_1} {p : Prop} {x : Decidable p} (b : ¬p → β) (w : (if h : p then none else some (b h)).isSome = true),
  (if h : p then none else some (b h)).get w = b ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Compose a quadratic map with a linear function on the left.  -/
LinearMap.compQuadraticMap' : {S : Type u_1} →
  {R : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        {P : Type u_6} →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : Module R N] →
                    [inst_5 : AddCommMonoid P] →
                      [inst_6 : CommSemiring S] →
                        [inst_7 : Algebra S R] →
                          [inst_8 : Module S N] →
                            [inst_9 : Module S M] →
                              [IsScalarTower S R N] →
                                [IsScalarTower S R M] →
                                  [inst_12 : Module S P] → (N →ₗ[S] P) → QuadraticMap R M N → QuadraticMap S M P
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_iSup : ∀ {ι : Sort u_1} (a : ENNReal) (f : ι → ENNReal), a * ⨆ i, f i = ⨆ i, a * f i
-- Mathlib.Algebra.Group.Action.Defs
AddSemigroup.vaddAssocClass : ∀ {α : Type u_5} [inst : AddSemigroup α], VAddAssocClass α α α
-- Init.Data.Nat.Div.Basic
Nat.mul_div_mul_right : ∀ {m : ℕ} (n k : ℕ), 0 < m → n * m / (k * m) = n / k