mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.IsDecompOn.eq_1 : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (f : X → X) (A : Set X) (S : Finset G),
  Equidecomp.IsDecompOn f A S = ∀ a ∈ A, ∃ g ∈ S, f a = g • a
-- Batteries.Recycling.RBTree.Basic
/-- A black node is balanced with black-height `n + 1`
if its children both have black-height `n`.  -/
RBTree.RBNode.Balanced.black : ∀ {α : Type u_1} {x : RBTree.RBNode α} {c₁ : RBTree.RBColor} {n : ℕ} {y : RBTree.RBNode α} {c₂ : RBTree.RBColor}
  {v : α},
  x.Balanced c₁ n →
    y.Balanced c₂ n → (RBTree.RBNode.node RBTree.RBColor.black x v y).Balanced RBTree.RBColor.black (n + 1)
-- Mathlib.Analysis.Convex.Strict
strictConvex_Icc : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β), StrictConvex 𝕜 (Set.Icc r s)
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitAnchorRefInfo.mk : ℕ → UInt64 → ℕ → Lean.Meta.Grind.SplitAnchorRefInfo
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.isSplitEpi_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting), CategoryTheory.IsSplitEpi S.g
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instCompleteLattice : {α : Type u_1} → {x : MeasurableSpace α} → CompleteLattice (MeasureTheory.Measure α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] {l : List α},
  (t.insertManyIfNewUnit l).isEmpty = (t.isEmpty && l.isEmpty)
-- Aesop.Rule
Aesop.instInhabitedNormSimpRule : Inhabited Aesop.NormSimpRule
-- Std.Http.Transport
/-- Creates a selector for receiving from a channel.
 -/
Std.Http.Internal.Mock.recvSelector : Std.CloseableChannel ByteArray → Std.Async.Selector (Option ByteArray)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- The (unique) isomorphism between the chosen terminal object and the chosen zero object.  -/
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → [inst_2 : CategoryTheory.Limits.HasTerminal C] → 0 ≅ ⊤_ C
-- Mathlib.LinearAlgebra.Charpoly.Basic
Algebra.aeval_self_charpoly_lmul : ∀ {R : Type u_2} {M : Type u_1} [inst : CommRing R] [inst_1 : Ring M] [inst_2 : Algebra R M]
  [inst_3 : Module.Finite R M] [inst_4 : Module.Free R M] (α : M),
  (Polynomial.aeval α) (LinearMap.charpoly ((Algebra.lmul R M) α)) = 0
-- Batteries.Data.String.Lemmas
String.instLawfulLTOrd : Std.LawfulLTOrd String
-- Init.Data.Nat.Basic
Nat.sub_one_lt : ∀ {n : ℕ}, n ≠ 0 → n - 1 < n
-- Mathlib.Data.Multiset.Functor
Multiset.traverse.eq_1 : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : CommApplicative F] {α' β' : Type u} (f : α' → F β'),
  Multiset.traverse f = Quotient.lift (Functor.map Multiset.ofList ∘ traverse f) ⋯
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.sigma_inj : ∀ {C : Type u} {F : C → Type v} (i : C) (x : F i), (CategoryTheory.Limits.CofanTypes.sigma F).inj i x = ⟨i, x⟩
-- Lean.Environment
Lean.Kernel.Exception.other : String → Lean.Kernel.Exception
-- Mathlib.RingTheory.FormalGroup.Basic
_private.Mathlib.RingTheory.FormalGroup.Basic.0.termY₂ : Lean.ParserDescr
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
lowerHemicontinuous_iff_isOpen_inter_nonempty : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} [inst_1 : TopologicalSpace β],
  LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen u → IsOpen {x | (f x ∩ u).Nonempty}
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C}
  {s : CategoryTheory.yoneda.obj X ⟶ A} {u v : CategoryTheory.OverPresheafAux.OverArrows η s}, u.val = v.val → u = v
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.add_neg_cancel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a : X ⟶ Y), a + -a = 0
-- Mathlib.Topology.Category.TopPair
/-- Given a morphism `f` of topological pairs, we can define a `Homotopy f f` by
`TopCat.Homotopy.refl` on the first and second components.
 -/
TopPair.Homotopy.refl : {X Y : TopPair} → (f : X ⟶ Y) → TopPair.Homotopy f f
-- Init.Data.List.Nat.Modify
List.modify_eq_take_drop : ∀ {α : Type u_1} (f : α → α) (l : List α) (i : ℕ), l.modify i f = List.take i l ++ List.modifyHead f (List.drop i l)
-- Mathlib.Data.DFinsupp.Module
DFinsupp.comapDomain_smul : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)]
  [inst_1 : (i : ι) → SMulZeroClass γ (β i)] (h : κ → ι) (hh : Function.Injective h) (r : γ) (f : Π₀ (i : ι), β i),
  DFinsupp.comapDomain h hh (r • f) = r • DFinsupp.comapDomain h hh f
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.classifier`.

---

Any representation `Ω` of `Subobject.presheaf C` gives a subobject classifier with truth values
object `Ω`.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy.classifier : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        CategoryTheory.SubobjectRepresentableBy Ω →
          [CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Subobject.Classifier C
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_apply : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r : k) (p : P1),
  (AffineMap.homothety c r) p = r • (p -ᵥ c) +ᵥ c
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.pi_eq_bot_iff : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] (S : (i : ι) → AddSubmonoid (M i)),
  AddSubmonoid.pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Functor C (CategoryTheory.Mon D)) (X_1 : C),
  ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso.inv.app X).app X_1).hom =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toArray_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  {f : α → β → Option γ},
  Std.DTreeMap.Const.toArray (Std.DTreeMap.filterMap (fun k v => f k v) t) =
    Array.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DTreeMap.Const.toArray t)
-- Mathlib.Util.WhatsNew
_private.Mathlib.Util.WhatsNew.0.Mathlib.WhatsNew.diffExtension.unsafe_4 : Lean.Environment →
  Lean.Environment →
    Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState →
      Lean.CoreM (Option Lean.MessageData)
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
Real.convergent.eq_2 : ∀ (x : ℝ) (n : ℕ), x.convergent n.succ = ↑⌊x⌋ + ((Int.fract x)⁻¹.convergent n)⁻¹
-- Mathlib.Data.Num.Bitwise
/-- Bitwise `fun a b ↦ a && !b` for `PosNum`. For example, `ldiff 5 9 = 4`:
```
 101
1001
----
 100
```
 -/
PosNum.ldiff : PosNum → PosNum → Num
-- Mathlib.Algebra.Module.Rat
/-- `qsmul` is equal to any other module structure via a cast.  -/
Rat.cast_smul_eq_qsmul : ∀ {M : Type u_1} (R : Type u_3) [inst : DivisionRing R] [inst_1 : MulAction R M] [inst_2 : MulAction ℚ M]
  [IsScalarTower ℚ R M] (q : ℚ) (x : M), ↑q • x = q • x
-- Std.Time.DateTime
Std.Time.DateTime.instHSubOffset : HSub Std.Time.DateTime Std.Time.Day.Offset Std.Time.DateTime
-- Mathlib.SetTheory.ZFC.Class
/-- `A ∈ B` if `A` is a ZFC set which satisfies `B`  -/
Class.Mem : Class.{u} → Class.{u} → Prop
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.mk'_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsCofibrant Y]
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))),
  (HomotopicalAlgebra.CofibrantBrownFactorization.mk' f h).p = h.p
-- Mathlib.Topology.Gluing
TopCat.GlueData.ofOpenSubsets_toGlueData_J : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α),
  (TopCat.GlueData.ofOpenSubsets U).J = J
-- Mathlib.Algebra.Order.Pi
Pi.isOrderedRing : ∀ {I : Type u_1} {f : I → Type u_5} [inst : (i : I) → Semiring (f i)] [inst_1 : (i : I) → PartialOrder (f i)]
  [∀ (i : I), IsOrderedRing (f i)], IsOrderedRing ((i : I) → f i)
-- Mathlib.Algebra.Category.Grp.Ulift
AddCommGrpCat.instCreatesLimitsOfSizeUliftFunctor.eq_1 : AddCommGrpCat.instCreatesLimitsOfSizeUliftFunctor =
  {
    CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, u} J] =>
      { CreatesLimit := fun {x} => CategoryTheory.createsLimitOfFullyFaithfulOfPreserves } }
-- Mathlib.Order.BoundedOrder.Basic
/-- A type with a single element is a bounded order.  -/
BoundedOrder.ofUnique : (α : Type u_1) → [inst : Preorder α] → [Unique α] → BoundedOrder α
-- Mathlib.Data.Set.Monotone
Set.EqOn.congr_strictAntiOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  Set.EqOn f₁ f₂ s → (StrictAntiOn f₁ s ↔ StrictAntiOn f₂ s)
-- Mathlib.Combinatorics.Hindman
Hindman.FP.finsetProd : ∀ {M : Type u_1} [inst : CommMonoid M] (a : Stream' M) (s : Finset ℕ), s.Nonempty → ∏ i ∈ s, a.get i ∈ Hindman.FP a
-- Lean.Elab.InfoTree.Types
/-- Final environment at the end of `elabCommand`; empty for nested contexts. This environment can be
used to access information about the fully-elaborated current declaration such as declaration
ranges. It may not be a strict superset of `env` in case of backtracking, so `env` should be
preferred to access information about the elaboration context at the time this context object was
created.
 -/
Lean.Elab.CommandContextInfo.cmdEnv? : Lean.Elab.CommandContextInfo → Option Lean.Environment
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_antitone`. -/
lowerCentralSeries_antitone : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G), Antitone S.lowerCentralSeries
-- Mathlib.Data.Real.Basic
Real.ext_cauchy : ∀ {x y : ℝ}, x.cauchy = y.cauchy → x = y
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the day of the month to the given `days` value, with any
out-of-range days clipped to the nearest valid date.
 -/
Std.Time.DateTime.withDaysClip : Std.Time.DateTime → Std.Time.Day.Ordinal → Std.Time.DateTime
-- Mathlib.CategoryTheory.Category.KleisliCat
CategoryTheory.KleisliCat.category : {m : Type u → Type v} →
  [inst : Monad m] → [LawfulMonad m] → CategoryTheory.Category.{max u v, u + 1} (CategoryTheory.KleisliCat m)
-- Init.Data.Int.LemmasAux
Int.ble'.eq_1 : ∀ (a b : ℤ),
  a.ble' b =
    Int.rec (fun a => Int.rec (fun b => a.ble b) (fun x => false) b)
      (fun a => Int.rec (fun x => true) (fun b => b.ble a) b) a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.startsWith_prop_eq_false_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice},
  s.startsWith P = false ↔ ∀ (h : s.startPos ≠ s.endPos), ¬P (s.startPos.get h)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.eval.eq_1 : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L) (p : RatFunc K),
  RatFunc.eval f a p = Polynomial.eval₂ f a p.num / Polynomial.eval₂ f a p.denom
-- Mathlib.Data.PEquiv
PEquiv.mem_ofSet_iff : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {a b : α}, a ∈ (PEquiv.ofSet s) b ↔ a = b ∧ a ∈ s
-- Init.Data.Array.Erase
Array.eraseP_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  (Array.replicate n a).eraseP p = if p a = true then Array.replicate (n - 1) a else Array.replicate n a
-- Mathlib.CategoryTheory.Shift.Opposite
/-- The obvious isomorphism between the identity of `OppositeShift C A` and
`OppositeShift.functor (𝟙 C)`.
 -/
CategoryTheory.NatTrans.OppositeShift.natIsoId : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A : Type u_3) →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          CategoryTheory.Functor.id (CategoryTheory.OppositeShift C A) ≅
            CategoryTheory.OppositeShift.functor A (CategoryTheory.Functor.id C)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Another auxiliary equality related with the **Cauchy–Schwarz inequality**: the square of the
seminorm of `⟪x, y⟫ • x - ⟪x, x⟫ • y` is equal to `‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2 - ‖⟪x, y⟫‖ ^ 2)`.
We use `InnerProductSpace.ofCore.normSq x` etc. (defeq to `is_R_or_C.re ⟪x, x⟫`) instead of
`‖x‖ ^ 2` etc. to avoid extra rewrites when applying it to an `InnerProductSpace`.  -/
InnerProductSpace.Core.cauchy_schwarz_aux : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F),
  InnerProductSpace.Core.normSq (inner 𝕜 x y • x - inner 𝕜 x x • y) =
    InnerProductSpace.Core.normSq x *
      (InnerProductSpace.Core.normSq x * InnerProductSpace.Core.normSq y - ‖inner 𝕜 x y‖ ^ 2)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instIsCentralScalar : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {S : Type u_5}
  [inst_6 : Monoid S] [inst_7 : DistribMulAction S M] [inst_8 : SMulCommClass R S M] [inst_9 : SMulCommClass S A M]
  [inst_10 : DistribMulAction Sᵐᵒᵖ M] [inst_11 : IsCentralScalar S M], IsCentralScalar S (Derivation R A M)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.coe_prodCongr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G] {G' : Type u_8}
  [inst_10 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H M] {M' : Type u_10} [inst_13 : TopologicalSpace M'] [inst_14 : ChartedSpace H' M']
  {N : Type u_11} [inst_15 : TopologicalSpace N] [inst_16 : ChartedSpace G N] {N' : Type u_12}
  [inst_17 : TopologicalSpace N'] [inst_18 : ChartedSpace G' N'] {n : WithTop ℕ∞} (h₁ : Diffeomorph I I' M M' n)
  (h₂ : Diffeomorph J J' N N' n), ⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂
-- Init.Data.Int.DivMod.Lemmas
Int.emod_sub_bmod : ∀ {y : ℤ} (x : ℤ) (n : ℕ), (x % ↑n - y).bmod n = (x - y).bmod n
-- Mathlib.Analysis.Seminorm
Seminorm.smul_le_smul : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p q : Seminorm 𝕜 E} {a b : NNReal}, p ≤ q → a ≤ b → a • p ≤ b • q
-- Mathlib.Algebra.Order.Ring.Archimedean
/-- See `mk_map_of_archimedean` for a version taking `M →+o R`.  -/
ArchimedeanClass.mk_map_of_archimedean' : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) {x : S},
  x ≠ 0 → ArchimedeanClass.mk (f x) = 0
-- Lean.Meta.LitValues
/-- Return `some (n, type)` if `e` is an `OfNat.ofNat`-application encoding `n` for a type with name `typeDeclName`.  -/
Lean.Meta.getOfNatValue? : Lean.Expr → Lean.Name → Lean.MetaM (Option (ℕ × Lean.Expr))
-- Mathlib.Logic.Nontrivial.Defs
subsingleton_iff : ∀ {α : Type u_1}, Subsingleton α ↔ ∀ (x y : α), x = y
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_succ_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ioo a (Order.succ b) = Set.Ioc a b
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertMany_nil : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β}, m.insertMany [] = m
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- For any path `p` from `x₀` to `x₁`, we have a homotopy from the constant path based at `x₁` to
`p.symm.trans p`.  -/
Path.Homotopy.reflSymmTrans : {X : Type u_1} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → (p : Path x₀ x₁) → (Path.refl x₁).Homotopy (p.symm.trans p)
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_sdiff_self_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s \ (s \ t) = s ∩ t
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- `finsetApprox` is a finite set such that each fractional ideal in the integral closure
contains an element close to `finsetApprox`.  -/
ClassGroup.finsetApprox : {R : Type u_1} →
  {S : Type u_2} →
    [inst : EuclideanDomain R] →
      [inst_1 : CommRing S] →
        [IsDomain S] →
          [inst_3 : Algebra R S] →
            {abv : AbsoluteValue R ℤ} →
              {ι : Type u_5} →
                [DecidableEq ι] →
                  [Fintype ι] → Module.Basis ι R S → abv.IsAdmissible → [Infinite R] → [DecidableEq R] → Finset R
-- Mathlib.GroupTheory.GroupExtension.Basic
SemidirectProduct.toGroupExtension.eq_1 : ∀ {N : Type u_1} {G : Type u_3} [inst : Group G] [inst_1 : Group N] (φ : G →* MulAut N),
  SemidirectProduct.toGroupExtension φ =
    { inl := SemidirectProduct.inl, rightHom := SemidirectProduct.rightHom, inl_injective := ⋯,
      range_inl_eq_ker_rightHom := ⋯, rightHom_surjective := ⋯ }
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_def : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P), LinearMap.lTensor M f = TensorProduct.map LinearMap.id f
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexFinsetRange_repr_self : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [inst_3 : Fintype ι] [inst_4 : DecidableEq M] (i : ι),
  b.reindexFinsetRange.repr (b i) = fun₀ | ⟨b i, ⋯⟩ => 1
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] (I : Ideal R),
  IsLocalRing.maximalIdeal R ∈ I.minimalPrimes → IsArtinianRing (R ⧸ I)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- If `s` is a measurable set, then `𝓝[s] a` is a measurably generated filter for
each `a`. This cannot be an `instance` because it depends on a non-instance `hs : MeasurableSet s`.
 -/
MeasurableSet.nhdsWithin_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α},
  MeasurableSet s → ∀ (a : α), (nhdsWithin a s).IsMeasurablyGenerated
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.verifyCert_correct : ∀ (cnf : Std.Sat.CNF ℕ) (cert : String), Std.Tactic.BVDecide.Reflect.verifyCert cnf cert = true → cnf.Unsat
-- Mathlib.Analysis.Convex.Strict
StrictConvex.convex : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : Module 𝕜 E] {s : Set E}, StrictConvex 𝕜 s → Convex 𝕜 s
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
HasOuterApproxClosed.tendsto_apprSeq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F),
  Filter.Tendsto (fun n x => (hF.apprSeq n) x) Filter.atTop (nhds (F.indicator fun x => 1))
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- A helper to construct a `GradedAlgebra` when the `SetLike.GradedMonoid` structure is already
available. This makes the `left_inv` condition easier to prove, and phrases the `right_inv`
condition in a way that allows custom `@[ext]` lemmas to apply.

See note [reducible non-instances].  -/
GradedAlgebra.ofAlgHom : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                (𝒜 : ι → Submodule R A) →
                  [inst_5 : SetLike.GradedMonoid 𝒜] →
                    (decompose : A →ₐ[R] DirectSum ι fun i => ↥(𝒜 i)) →
                      (DirectSum.coeAlgHom 𝒜).comp decompose = AlgHom.id R A →
                        (∀ (i : ι) (x : ↥(𝒜 i)), decompose ↑x = (DirectSum.of (fun i => ↥(𝒜 i)) i) x) → GradedAlgebra 𝒜
-- Std.Async.Process
Std.IO.Process.PId.mk.injEq : ∀ (toUInt64 toUInt64_1 : UInt64), ({ toUInt64 := toUInt64 } = { toUInt64 := toUInt64_1 }) = (toUInt64 = toUInt64_1)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSet_empty_right : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] (s : Set Ω), ProbabilityTheory.CondIndepSet m' hm' s ∅ μ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- For any morphism `f : U ⟶ V` in `FormalCoproduct C` and a type `α`,
this is the induced map `U.power α ⟶ V.power α`.  -/
CategoryTheory.Limits.FormalCoproduct.powerMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {U V : CategoryTheory.Limits.FormalCoproduct C} →
      (U ⟶ V) → (α : Type t) → [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] → U.power α ⟶ V.power α
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.simple_mul_simple_pow' : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B),
  (cs.simple i' * cs.simple i) ^ M.M i i' = 1
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.topologicalClosure_minimal : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] (s : Subgroup G)
  {t : Subgroup G}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.Topology.Perfect
IsPreconnected.preperfect_of_nontrivial : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T1Space α] {U : Set α}, U.Nontrivial → IsPreconnected U → Preperfect U