mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Basic
List.rotateLeft_nil : ∀ {α : Type u} {n : ℕ}, [].rotateLeft n = []
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.prod.eq_2 : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] (v : Fin 1 → α), FinVec.prod v = v 0
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets_inf : ∀ {α : Type u_1} (l₁ l₂ : Filter α), (l₁ ⊓ l₂).smallSets = l₁.smallSets ⊓ l₂.smallSets
-- Mathlib.Algebra.Order.ToIntervalMod
_private.Mathlib.Algebra.Order.ToIntervalMod.0.toIxxMod_total' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
-- Init.Data.Fin.Lemmas
Fin.zero_eq_one_iff : ∀ {n : ℕ} [inst : NeZero n], 0 = 1 ↔ n = 1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_eq_empty : ∀ {m n : ℤ}, n ≤ m → (m...n).toArray = #[]
-- Mathlib.Analysis.Normed.Module.Connected
/-- Let `E` be a linear subspace in a real vector space.
If `E` has codimension at least two, its complement is path-connected.  -/
isPathConnected_compl_of_one_lt_codim : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [ContinuousSMul ℝ F] {E : Submodule ℝ F}, 1 < Module.rank ℝ (F ⧸ E) → IsPathConnected (↑E)ᶜ
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_zero : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] [Nontrivial R],
  Matrix.rank 0 = 0
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- If a morphism `q : Z ⟶ X i` belongs to `sieve f f' i`, this is a choice of
a morphism `hom : Z ⟶ X' j` for some `j` such that `hom ≫ f' j = q ≫ f i`.  -/
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type t} →
      {S : C} →
        {X : ι → C} →
          {f : (i : ι) → X i ⟶ S} →
            {ι' : Type t'} →
              {X' : ι' → C} →
                {f' : (j : ι') → X' j ⟶ S} →
                  {i : ι} →
                    {Z : C} →
                      {q : Z ⟶ X i} →
                        (hq :
                            (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i).arrows
                              (CategoryTheory.Over.homMk q ⋯)) →
                          Z ⟶ X' (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.idx✝ hq)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- `toSimpleFunc f` satisfies the predicate `MemLp`.  -/
MeasureTheory.Lp.simpleFunc.memLp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  MeasureTheory.MemLp (⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) p μ
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway : ∀ {R : Type u} [inst : CommRing R] {Rᵣ : Type u_2} [inst_1 : CommRing Rᵣ] [inst_2 : Algebra R Rᵣ] (r : R)
  [IsLocalization.Away r Rᵣ], RingHom.IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.tensorProduct_isLocalizedModule : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] {M : Type u_3} [inst_4 : AddCommMonoid M] [inst_5 : Module R M],
  IsLocalizedModule S ((TensorProduct.mk R A M) 1)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (m.insertMany l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_mul : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {p' : o → Type u_9} {α : Type u_12} [inst : DecidableEq o]
  [inst_1 : NonUnitalNonAssocSemiring α] [inst_2 : (i : o) → Fintype (n' i)] [inst_3 : Fintype o]
  (M : (i : o) → Matrix (m' i) (n' i) α) (N : (i : o) → Matrix (n' i) (p' i) α),
  (Matrix.blockDiagonal' fun k => M k * N k) = Matrix.blockDiagonal' M * Matrix.blockDiagonal' N
-- Lean.Elab.Util
Lean.Syntax.prettyPrint : Lean.Syntax → Std.Format
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_le_map₂_left : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [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 : M →ₗ[R] N →ₗ[R] P} {p₁ p₂ : Submodule R M} {q : Submodule R N},
  p₁ ≤ p₂ → Submodule.map₂ f p₁ q ≤ Submodule.map₂ f p₂ q
-- Init.Data.List.Lemmas
List.reverse_concat : ∀ {α : Type u_1} {l : List α} {a : α}, (l ++ [a]).reverse = a :: l.reverse
-- Mathlib.Data.ZMod.Basic
/-- This lemma works in the case in which `a ≠ 0`.  The version where
`ZMod n` is not infinite, i.e. `n ≠ 0`, is `addOrderOf_coe`.  -/
ZMod.addOrderOf_coe' : ∀ {a : ℕ} (n : ℕ), a ≠ 0 → addOrderOf ↑a = n / n.gcd a
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.mul_toMatrix₂'_mul : ∀ {n : Type u_11} {m : Type u_12} {n' : Type u_13} {m' : Type u_14} {R : Type u_16} [inst : CommSemiring R]
  [inst_1 : Fintype n] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] [inst_5 : Fintype n']
  [inst_6 : Fintype m'] [inst_7 : DecidableEq n'] [inst_8 : DecidableEq m'] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R)
  (M : Matrix n' n R) (N : Matrix m m' R),
  M * (LinearMap.toMatrix₂' R) B * N =
    (LinearMap.toMatrix₂' R) (B.compl₁₂ (Matrix.toLin' M.transpose) (Matrix.toLin' N))
-- Mathlib.Analysis.Convex.Jensen
/-- Canonical form of the **strict Jensen's inequality**.  -/
StrictConvexOn.map_sum_lt_iff_of_nonneg' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i) ↔ ∃ j ∈ t, w j ≠ 0 ∧ p j ≠ ∑ i ∈ t, w i • p i)
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.IsStableUnderComposition.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C},
  (∀ {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
      CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S →
        ∀ {σ : ι → Type (max u v)} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i),
          (∀ (i : ι), CategoryTheory.Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)) →
            (CategoryTheory.Presieve.ofArrows (fun p => Y p.fst p.snd) fun x =>
                CategoryTheory.CategoryStruct.comp (g x.fst x.snd) (f x.fst)) ∈
              J.coverings S) →
    J.IsStableUnderComposition
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A reversed telescoping sum along `{0, ..., n - 1}` of a function valued in a
commutative additive group reduces to the difference of the first and last terms.  -/
Finset.sum_range_sub' : ∀ {G : Type u_3} [inst : AddCommGroup G] (f : ℕ → G) (n : ℕ), ∑ i ∈ Finset.range n, (f i - f (i + 1)) = f 0 - f n
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.coe_toAlgEquiv : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Star A] [inst_6 : Star B] (f : A ≃⋆ₐ[R] B), ⇑f.toAlgEquiv = ⇑f
-- Mathlib.Data.List.Basic
List.erase_getElem : ∀ {ι : Type u_1} [inst : BEq ι] [LawfulBEq ι] {l : List ι} {i : ℕ} (hi : i < l.length),
  (l.erase l[i]).Perm (l.eraseIdx i)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.pow.congr_simp : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] {k : ℤ} (f f_1 : ModularForm Γ k),
  f = f_1 → ∀ (n : ℕ), f.pow n = f_1.pow n
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.IsMaximal.eq_of_le : ∀ {α : Type u} [inst : Semiring α] {I J : Ideal α}, I.IsMaximal → J ≠ ⊤ → I ≤ J → I = J
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.wr : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput old w → ℕ
-- Mathlib.Probability.Moments.Covariance
/-- The covariance of two real-valued random variables defined as
the integral of `(X - 𝔼[X])(Y - 𝔼[Y])`.  -/
ProbabilityTheory.«termCov[_,_;_]» : Lean.ParserDescr
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
  (insert t ↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
-- Mathlib.Algebra.Group.Subgroup.Defs
InvMemClass.inv.eq_1 : ∀ {G : Type u_5} {S : Type u_6} [inst : Inv G] [inst_1 : SetLike S G] [inst_2 : InvMemClass S G] {H : S},
  InvMemClass.inv = { inv := fun a => ⟨(↑a)⁻¹, ⋯⟩ }
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.isIso_toSheafify : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P : CategoryTheory.Functor Cᵒᵖ D},
  CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.IsIso (CategoryTheory.toSheafify J P)
-- Mathlib.Algebra.Group.Basic
sub_add_comm : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b + c = c - b + a
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.coe_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (g : N →ₙ+ P)
  (f : M →ₙ+ N), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.SubarrayIterator.count_eq : ∀ {α : Type u_1} {it : Std.Iter α}, it.length = it.internalState.xs.stop - it.internalState.xs.start
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.brecOn : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {motive : (a a_1 : M) → ConGen.Rel r a a_1 → Prop} {a a_1 : M}
  (t : ConGen.Rel r a a_1),
  (∀ (a a_2 : M) (t : ConGen.Rel r a a_2), ConGen.Rel.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.Tactic.Algebraize
/-- Given an expression `f` of type `RingHom A B` where `A` and `B` are commutative semirings,
this function adds the instance `Algebra A B` to the context (if it does not already exist).

This function also requires the type of `f`, given by the parameter `ft`. The reason this is done
(even though `ft` can be inferred from `f`) is to avoid recomputing `ft` in the `algebraize` tactic,
as when `algebraize` calls `addAlgebraInstanceFromRingHom` it has already computed `ft`.  -/
Mathlib.Tactic.Algebraize.addAlgebraInstanceFromRingHom : Lean.Expr → Lean.Expr → Lean.Elab.Tactic.TacticM Unit
-- Init.Meta
/-- `simp_all_arith!` has been deprecated. It was a shorthand for `simp_all! +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
 -/
Lean.Parser.Tactic.simpAllArithBang : Lean.ParserDescr
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.coe_ofLinearEquiv : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f : M ≃ₗ[R] M),
  ⇑↑(LinearMap.GeneralLinearGroup.ofLinearEquiv f) = ⇑f
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_orbit_of_mem_orbit_addSubmonoid : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] {S : AddSubmonoid M} {a b : α},
  a ∈ AddAction.orbit (↥S) b → a ∈ AddAction.orbit M b
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mem_carrier : ∀ {R : Type u} [inst : NonAssocRing R] {s : Subring R} {x : R}, x ∈ s.carrier ↔ x ∈ s
-- Init.Data.Nat.Coprime
Nat.Coprime.eq_one_of_dvd : ∀ {k m : ℕ}, k.Coprime m → k ∣ m → k = 1
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_zero : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.mirror 0 = 0
-- Mathlib.Order.Category.BddDistLat
BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat : (CategoryTheory.forget₂ BddDistLat BddLat).comp (CategoryTheory.forget₂ BddLat Lat) =
  (CategoryTheory.forget₂ BddDistLat DistLat).comp (CategoryTheory.forget₂ DistLat Lat)
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_same_eq_mul_div' : ∀ {R : Type u_1} {a b : R} [inst : Field R], a ≠ 1 → ∀ (n : ℕ), arithGeom a b b n = b * (1 - a ^ (n + 1)) / (1 - a)
-- Mathlib.Data.Real.Sign
Real.sign_of_pos : ∀ {r : ℝ}, 0 < r → r.sign = 1
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- Let `A` be an `R`-coalgebra and let `B` be an `R`-module with a `CoalgebraStruct`.
A linear equivalence `A ≃ₗ[R] B` that respects the `CoalgebraStruct`s defines an `R`-coalgebra
structure on `B`.  -/
CoalgEquiv.toCoalgebra : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] →
            [inst_3 : Coalgebra R A] →
              [inst_4 : AddCommMonoid B] →
                [inst_5 : Module R B] → [inst_6 : CoalgebraStruct R B] → (A ≃ₗc[R] B) → Coalgebra R B
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.instIsNilpotentSup : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M]
  (M₁ M₂ : LieSubmodule R L M) [LieModule.IsNilpotent L ↥M₁] [LieModule.IsNilpotent L ↥M₂],
  LieModule.IsNilpotent L ↥(M₁ ⊔ M₂)
-- Mathlib.Analysis.Normed.Group.Hom
/-- Homs between two given normed groups form a commutative additive group.  -/
NormedAddGroupHom.toAddCommGroup : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → AddCommGroup (NormedAddGroupHom V₁ V₂)
-- Init.Data.List.Sublist
List.IsInfix.filterMap : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) ⦃l₁ l₂ : List α⦄,
  l₁ <:+: l₂ → List.filterMap f l₁ <:+: List.filterMap f l₂
-- Mathlib.Data.QPF.Univariate.Basic
QPF.corecF.eq_1 : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (g : α → F α), QPF.corecF g = PFunctor.M.corec fun x => QPF.repr (g x)
-- Mathlib.Data.Fin.SuccPred
Fin.succ_zero_eq_one' : ∀ {n : ℕ} [inst : NeZero n], Fin.succ 0 = 1
-- Init.Data.BitVec.Bootstrap
BitVec.cons.eq_1 : ∀ {n : ℕ} (msb : Bool) (lsbs : BitVec n), BitVec.cons msb lsbs = BitVec.cast ⋯ (BitVec.ofBool msb ++ lsbs)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_eraseKey_eq_iff_beq_maxKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α}
  {he : (Std.Internal.List.eraseKey k l).isEmpty = false},
  Std.Internal.List.maxKey (Std.Internal.List.eraseKey k l) he = Std.Internal.List.maxKey l ⋯ ↔
    (k == Std.Internal.List.maxKey l ⋯) = false
-- Mathlib.CategoryTheory.GradedObject
/-- Constructor for `CofanMapObjFun X p j`.  -/
CategoryTheory.GradedObject.CofanMapObjFun.mk : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        (X : CategoryTheory.GradedObject I C) →
          (p : I → J) → (j : J) → (pt : C) → ((i : I) → p i = j → (X i ⟶ pt)) → X.CofanMapObjFun p j
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.coe_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R], ↑1 = 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_addHom : ∀ {α : Type u} [inst : AddMonoid α], ⇑WithTop.addHom = WithTop.some
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ico (f n) (f (Order.pred n))` are pairwise disjoint.  -/
Antitone.pairwise_disjoint_on_Ico_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Function.onFun Disjoint fun n => Set.Ico (f n) (f (Order.pred n)))
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.go.match_1.splitter : (motive : List String → Sort u_1) →
  (x : List String) → ((a : String) → (as : List String) → motive (a :: as)) → (Unit → motive []) → motive x
-- Lean.Meta.Tactic.Grind.EMatch
/-- Performs one round of E-matching, and returns `true` if new instances were generated.
Recall that the mapping is nonempty only if tracing or instance marking is enabled.
 -/
Lean.Meta.Grind.ematch' : optParam (Array Lean.Meta.Grind.EMatchTheorem) #[] → Lean.Meta.Grind.GoalM (Bool × Lean.Meta.Grind.EMatch.InstanceMap)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.keyAtIdx : {α : Type u} → {β : α → Type v} → (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → (n : ℕ) → n < t.size → α
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.tensorHom_id : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ : CategoryTheory.LocalizedMonoidal L W ε} (f : X₁ ⟶ X₂) (Y : CategoryTheory.LocalizedMonoidal L W ε),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.coassoc_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : A),
  (TensorProduct.assoc R A A A) ((LinearMap.rTensor A CoalgebraStruct.comul) (CoalgebraStruct.comul a)) =
    (LinearMap.lTensor A CoalgebraStruct.comul) (CoalgebraStruct.comul a)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.comp_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  {M N K : CategoryTheory.Mat_ C} (f : M ⟶ N) (g : N ⟶ K) (i : M.ι) (k : K.ι),
  CategoryTheory.CategoryStruct.comp f g i k = ∑ j, CategoryTheory.CategoryStruct.comp (f i j) (g j k)
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- Given sections over a family of open sets, extend it to include
sections over pairwise intersections of the open sets.  -/
TopCat.Presheaf.objPairwiseOfFamily : {X : TopCat} →
  {F : TopCat.Presheaf (Type u_4) X} →
    {ι : Type u_5} →
      {U : ι → TopologicalSpace.Opens ↑X} →
        ((i : ι) → F.obj (Opposite.op (U i))) →
          (i : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((CategoryTheory.Pairwise.diagram U).op.comp F).obj i
-- Init.Data.List.Basic
List.isPrefixOf.eq_1 : ∀ {α : Type u} [inst : BEq α] (x : List α), [].isPrefixOf x = true
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
/-- The parameters of a strongly regular graph with at least one vertex satisfy
`k * (k - ℓ - 1) = (n - k - 1) * μ`.  -/
SimpleGraph.IsSRGWith.param_eq : ∀ {n k ℓ μ : ℕ} {V : Type u} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],
  G.IsSRGWith n k ℓ μ → 0 < n → k * (k - ℓ - 1) = (n - k - 1) * μ
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit : ∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A]
  {a : A} (repr : Coalgebra.Repr R a ι),
  ∑ i ∈ repr.index, (HopfAlgebraStruct.antipode R) (repr.left i) * repr.right i =
    (algebraMap R A) (CoalgebraStruct.counit a)
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
continuous_polarCoord_symm : Continuous ↑polarCoord.symm
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The family of morphisms out of a universal arrow.  -/
CategoryTheory.StructuredArrow.IsUniversal.desc : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            {f : CategoryTheory.StructuredArrow S T} →
              f.IsUniversal → (g : CategoryTheory.StructuredArrow S T) → f.right ⟶ g.right
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.snd_app_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) (a : J.L) {Z : C}
  (h :
    ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingMultispan J)).obj K.pt).obj
        (CategoryTheory.Limits.WalkingMultispan.left a) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (I.snd a) (K.π (J.snd a))) h
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_sub : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : AddGroup α]
  (M N : Matrix ((i : o) × m' i) ((i : o) × n' i) α), (M - N).blockDiag' = M.blockDiag' - N.blockDiag'
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] [inst_9 : SizeOf 𝕜] [inst_10 : SizeOf V]
  [inst_11 : SizeOf V₂] [inst_12 : SizeOf P] [inst_13 : SizeOf P₂] (toAffineEquiv : P ≃ᵃ[𝕜] P₂)
  (norm_map : ∀ (x : V), ‖toAffineEquiv.linear x‖ = ‖x‖),
  sizeOf { toAffineEquiv := toAffineEquiv, norm_map := norm_map } = 1 + sizeOf toAffineEquiv
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.homeomorphCircle.congr_simp : ∀ {T : ℝ} (hT : T ≠ 0), AddCircle.homeomorphCircle hT = AddCircle.homeomorphCircle hT
-- Std.Async.Signal
/-- Hangup detected on controlling terminal or death of controlling process.

On Windows:
- SIGHUP is generated when the user closes the console window. The program is given ~10 seconds to
  perform cleanup before Windows unconditionally terminates it.
 -/
Std.Async.Signal.sighup : Std.Async.Signal
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.cotangentEquivProd.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) [inst_3 : Nontrivial S],
  Algebra.Generators.PresentationOfFreeCotangent.Aux.cotangentEquivProd✝ D =
    Algebra.Generators.PresentationOfFreeCotangent.Aux.cotangentEquivProd✝ D
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_disjoint_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {δ ε : ℝ},
  δ + ε ≤ dist x y → Disjoint (Metric.closedBall x δ) (Metric.ball y ε)