mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
HasFDerivAt.eventually_ne : ∀ {𝕜 : 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} {c : F},
  HasFDerivAt f f' x → (∃ C, AntilipschitzWith C ⇑f') → ∀ᶠ (z : E) in nhdsWithin x {x}ᶜ, f z ≠ c
-- Init.Data.Vector.Lemmas
Vector.mem_append : ∀ {α : Type u_1} {n m : ℕ} {a : α} {xs : Vector α n} {ys : Vector α m}, a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys
-- Batteries.Tactic.SqueezeScope
/-- The `squeeze_scope` tactic allows aggregating multiple calls to `simp` coming from the same syntax
but in different branches of execution, such as in `cases x <;> simp`.
The reported `simp` call covers all simp lemmas used by this syntax.
```
@[simp] def bar (z : Nat) := 1 + z
@[simp] def baz (z : Nat) := 1 + z

@[simp] def foo : Nat → Nat → Nat
  | 0, z => bar z
  | _+1, z => baz z

example : foo x y = 1 + y := by
  cases x <;> simp? -- two printouts:
  -- "Try this: simp only [foo, bar]"
  -- "Try this: simp only [foo, baz]"

example : foo x y = 1 + y := by
  squeeze_scope
    cases x <;> simp -- only one printout: "Try this: simp only [foo, baz, bar]"
```
 -/
Batteries.Tactic.squeezeScope : Lean.ParserDescr
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_8 : ∀ (motive : Lean.Expr → Sort u_1) (data : Lean.MData) (a : Lean.Expr)
  (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a)) (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.mdata data a with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_8 data a
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.scalarTensorEquiv_tmul : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] (a : A) (p : AddMonoidAlgebra R M),
  (AddMonoidAlgebra.scalarTensorEquiv R A) (a ⊗ₜ[R] p) = a • (AddMonoidAlgebra.mapAlgHom M (Algebra.ofId R A)) p
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopicMap_f_eq_zero : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₀ : ι},
  (∀ (l : ι), ¬c.Rel k₀ l) →
    (∀ (l : ι), ¬c.Rel l k₀) → ∀ (hom : (i j : ι) → C.X i ⟶ D.X j), (Homotopy.nullHomotopicMap hom).f k₀ = 0
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- Construct an isomorphism in `SingleFunctors C D A` by giving
level-wise isomorphisms and checking compatibility only in the forward direction.  -/
CategoryTheory.SingleFunctors.isoMk : {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] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              {F G : CategoryTheory.SingleFunctors C D A} →
                (iso : (a : A) → F.functor a ≅ G.functor a) →
                  (∀ (n a a' : A) (ha' : n + a = a'),
                      CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (iso a).hom =
                        CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Functor.whiskerRight (iso a').hom (CategoryTheory.shiftFunctor D n))
                          (G.shiftIso n a a' ha').hom) →
                    (F ≅ G)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.equivCongr_trans : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} {A₁' : Type uA₁'} {A₂' : Type uA₂'} {A₃' : Type uA₃'}
  [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Semiring A₁']
  [inst_5 : Semiring A₂'] [inst_6 : Semiring A₃'] [inst_7 : Algebra R A₁] [inst_8 : Algebra R A₂]
  [inst_9 : Algebra R A₃] [inst_10 : Algebra R A₁'] [inst_11 : Algebra R A₂'] [inst_12 : Algebra R A₃']
  (e₁₂ : A₁ ≃ₐ[R] A₂) (e₁₂' : A₁' ≃ₐ[R] A₂') (e₂₃ : A₂ ≃ₐ[R] A₃) (e₂₃' : A₂' ≃ₐ[R] A₃'),
  (e₁₂.equivCongr e₁₂').trans (e₂₃.equivCongr e₂₃') = (e₁₂.trans e₂₃).equivCongr (e₁₂'.trans e₂₃')
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_symm_toEquiv : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), ⇑e.symm = ⇑e.symm
-- Mathlib.Algebra.Torsor.Defs
vadd_eq_vadd_iff_neg_add_eq_vsub : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {v₁ v₂ : G} {p₁ p₂ : P},
  v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqResponse : {α : Type u_1} → [BEq α] → BEq (Lean.JsonRpc.Response α)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.IsClosed.harmonicContOnCl_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  IsClosed s → (InnerProductSpace.HarmonicContOnCl f s ↔ InnerProductSpace.HarmonicOnNhd f s)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.ennreal_toNNReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal}, Measurable f → Measurable fun x => (f x).toNNReal
-- Mathlib.Algebra.Category.CommAlgCat.Basic
_private.Mathlib.Algebra.Category.CommAlgCat.Basic.0.CommAlgCat.Hom.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (hom' hom'_1 : ↑A →ₐ[R] ↑B),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Init.Data.UInt.Lemmas
UInt64.sub_mul : ∀ {a b c : UInt64}, (a - b) * c = a * c - b * c
-- Lean.Meta.WHNF
/-- Auxiliary predicate for `whnfMatcher`.
See comment above.
 -/
Lean.Meta.canUnfoldAtMatcher : Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool
-- Mathlib.Computability.RE
Partrec.sumCasesOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ →. σ},
  Computable f → Partrec₂ g → Partrec₂ h → Partrec fun a => Sum.casesOn (f a) (g a) (h a)
-- Lean.DocString.Extension
Lean.ElabBlock.custom.inj : ∀ {val val_1 : Dynamic}, Lean.ElabBlock.custom val = Lean.ElabBlock.custom val_1 → val = val_1
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquiv_comp : ∀ {A : Type u_8} (K : Type u_9) {B : Type u_10} (L : Type u_11) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] {C : Type u_12} (M : Type u_13) [inst_8 : CommRing C]
  [inst_9 : CommRing M] [inst_10 : Algebra C M] [inst_11 : IsFractionRing C M] (f : A ≃+* B) (g : B ≃+* C),
  IsFractionRing.ringEquivOfRingEquiv (f.trans g) =
    (IsFractionRing.ringEquivOfRingEquiv f).trans (IsFractionRing.ringEquivOfRingEquiv g)
-- Lean.Server.CodeActions.Attr
/-- The command kinds that this extension supports.
If empty it is called on all command kinds.  -/
Lean.CodeAction.CommandCodeActionEntry.cmdKinds : Lean.CodeAction.CommandCodeActionEntry → Array Lean.Name
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- The parts are disjoint  -/
OrderedFinpartition.disjoint : ∀ {n : ℕ} (self : OrderedFinpartition n), Set.univ.PairwiseDisjoint fun m => Set.range (self.emb m)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.comp_id : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →⋆ₐ[R] B),
  f.comp (StarAlgHom.id R A) = f
-- Init.Data.Int.DivMod.Lemmas
Int.add_emod_right : ∀ (a b : ℤ), (a + b) % b = a % b
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_insert_intCast : ∀ {R : Type uR} {A : Type uA} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (n : ℤ) (s : Set A),
  Algebra.adjoin R (insert (↑n) s) = Algebra.adjoin R s
-- Init.Data.Array.Range
_private.Init.Data.Array.Range.0.Array.ofFn.go.match_1.eq_2 : ∀ {n : ℕ} (motive : (x : ℕ) → x ≤ n → Sort u_1) (x : 0 ≤ n) (h_1 : (i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h)
  (h_2 : (x : 0 ≤ n) → motive 0 x),
  (match 0, x with
    | i.succ, h => h_1 i h
    | 0, x => h_2 x) =
    h_2 x
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.CategoryStruct.id.hcongr_3 : ∀ (obj obj' : Type u),
  obj = obj' →
    ∀ (self : CategoryTheory.CategoryStruct.{v, u} obj) (self' : CategoryTheory.CategoryStruct.{v, u} obj'),
      self ≍ self' →
        ∀ (X : obj) (X' : obj'), X ≍ X' → CategoryTheory.CategoryStruct.id X ≍ CategoryTheory.CategoryStruct.id X'
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
/-- A category `C` induces a functor from `Cat` to itself defined
by forming the category of functors out of `C`.  -/
CategoryTheory.Cat.exp : (C : Type u) → [CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Cat
-- Init.Data.Ord.Basic
List.compare_cons_nil : ∀ {α : Type u_1} [inst : Ord α] {x : α} {xs : List α}, compare (x :: xs) [] = Ordering.gt
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
_private.Std.Tactic.BVDecide.LRAT.Internal.Clause.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_6.eq_1 : ∀ {n : ℕ} (motive : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → Sort u_1)
  (h_1 : Unit → motive none)
  (h_2 : (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → motive (some map)),
  (match none with
    | none => h_1 ()
    | some map => h_2 map) =
    h_1 ()
-- Mathlib.Data.Matrix.Basic
Matrix.mulVec_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {ι : Type u_14} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : Fintype n] (x : Matrix m n α) (s : Finset ι) (y : ι → n → α),
  x.mulVec (∑ i ∈ s, y i) = ∑ i ∈ s, x.mulVec (y i)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.anyTR.loop.eq_1 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (h : 0 ≤ n), Nat.anyTR.loop✝ n f 0 h = false
-- Mathlib.Topology.Sober
genericPoint.congr_simp : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : QuasiSober α] [inst_2 : IrreducibleSpace α],
  genericPoint α = genericPoint α
-- Mathlib.ModelTheory.Syntax
/-- Relabels a term's variables along a particular function.  -/
FirstOrder.Language.Term.relabel : {L : FirstOrder.Language} → {α : Type u'} → {β : Type v'} → (α → β) → L.Term α → L.Term β
-- Mathlib.Topology.Closure
closure_empty : ∀ {X : Type u} [inst : TopologicalSpace X], closure ∅ = ∅
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : N ≃+ P},
  (f.ofAddEquivOfLocalizations k).toAddMonoidHom = k.toAddMonoidHom.comp f.toAddMonoidHom
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_multiset_prod_X_sub_C_eq_card : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] (s : Multiset R),
  (Multiset.map (fun x => Polynomial.X - Polynomial.C x) s).prod.natDegree = s.card
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.utf8Len.match_1.eq_2 : ∀ (motive : List Char → Sort u_1) (c : Char) (cs : List Char) (h_1 : Unit → motive [])
  (h_2 : (c : Char) → (cs : List Char) → motive (c :: cs)),
  (match c :: cs with
    | [] => h_1 ()
    | c :: cs => h_2 c cs) =
    h_2 c cs
-- Mathlib.Logic.Small.Defs
Shrink.rec : {α : Type u_1} →
  [inst : Small.{w, u_1} α] →
    {F : Shrink.{w, u_1} α → Sort v} → ((X : α) → F ((equivShrink α) X)) → (X : Shrink.{w, u_1} α) → F X
-- Mathlib.Probability.Density
MeasureTheory.withDensity_pdf_le_map : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} (X : Ω → E)
  (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) MeasureTheory.withDensity_pdf_le_map._auto_1),
  μ.withDensity (MeasureTheory.pdf X ℙ μ) ≤ MeasureTheory.Measure.map X ℙ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_ofList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α}, (Std.ExtHashMap.ofList l).contains k = (List.map Prod.fst l).contains k
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.Ordered.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering), RBTree.RBNode.Ordered cmp RBTree.RBNode.nil = True
-- Lean.Meta.Tactic.Grind.Simp
/-- Infers the type of the proof, preprocess it, and adds it to todo list.  -/
Lean.Meta.Grind.pushNewFact : Lean.Expr → optParam ℕ 0 → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a left extension from a 1-morphism and a 2-morphism.  -/
CategoryTheory.Bicategory.LeftExtension.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          (h : b ⟶ c) → (g ⟶ CategoryTheory.CategoryStruct.comp f h) → CategoryTheory.Bicategory.LeftExtension f g
-- Init.Data.Array.Find
Array.findIdx?_eq_some_iff_getElem : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool} {i : ℕ},
  Array.findIdx? p xs = some i ↔ ∃ (h : i < xs.size), p xs[i] = true ∧ ∀ (j : ℕ) (hji : j < i), ¬p xs[j] = true
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
/-- The obvious morphism `colimit (kernel (g y)) ⟶ X` (which is an epimorphism
if `J` is filtered, see `epi_f`).  -/
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
        {X : C} →
          {J : Type w} →
            [inst_3 : CategoryTheory.SmallCategory J] →
              {Y : CategoryTheory.Functor J C} →
                {j₀ : J} →
                  (y : X ⟶ Y.obj j₀) →
                    CategoryTheory.Limits.colimit
                        (CategoryTheory.Limits.kernel
                          (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)) ⟶
                      X
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_add_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [i : AddRightMono α] {b c : α}, b ≤ c → ∀ (a : α), b + a ≤ c + a
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.ins.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_bot_of_isReduced : ∀ {R : Type u} [inst : CommSemiring R] [IsReduced R], ⊥.radical = ⊥
-- Mathlib.Data.ENat.Basic
instLTENat : LT ℕ∞
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- An equivalent formulation of the sheaf condition
(which we prove equivalent to the usual one below as
`isSheaf_iff_isSheafOpensLeCover`).

A presheaf is a sheaf if `F` sends the cone `(opensLeCoverCocone U).op` to a limit cone.
(Recall `opensLeCoverCocone U`, has cone point `iSup U`,
mapping down to any `V` which is contained in some `U i`.)
 -/
TopCat.Presheaf.IsSheafOpensLeCover : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : TopCat} → TopCat.Presheaf C X → Prop
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.instInhabitedSearchState.default : Lean.Meta.Grind.EMatch.SearchState
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_add_pi : ∀ (x : ℂ), Complex.cos (x + ↑Real.pi) = -Complex.cos x
-- Mathlib.Data.Semiquot
Semiquot.exists_mem : ∀ {α : Type u_1} (q : Semiquot α), ∃ a, a ∈ q
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
_private.Std.Tactic.BVDecide.LRAT.Internal.Clause.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_1.splitter : (motive : Option Bool → Sort u_1) →
  (val? : Option Bool) →
    ((val' : Bool) → motive (some val')) →
      ((x : Option Bool) → (∀ (val' : Bool), x = some val' → False) → motive x) → motive val?
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_ne_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {x : ↑(Set.Icc 0 1)},
  ↑x ≠ 1 ↔ x ≠ 1
-- Mathlib.Lean.Expr.Basic
/-- Update the last component of a name.  -/
Lean.Name.updateLast : (String → String) → Lean.Name → Lean.Name
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagSource.ematch.inj : ∀ {origin : Lean.Meta.Grind.Origin} {inst : Lean.Expr} {origin_1 : Lean.Meta.Grind.Origin} {inst_1 : Lean.Expr},
  Lean.Meta.Grind.EMatchDiagSource.ematch origin inst = Lean.Meta.Grind.EMatchDiagSource.ematch origin_1 inst_1 →
    origin = origin_1 ∧ inst = inst_1
-- Init.Data.Vector.Lemmas
Vector.flatMap_toArray : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m},
  Array.flatMap (fun a => (f a).toArray) xs.toArray = (xs.flatMap f).toArray
-- Mathlib.RingTheory.DividedPowers.DPMorphism
/-- The identity map as a `DPMorphism`.  -/
DividedPowers.DPMorphism.id : {A : Type u_3} → [inst : CommSemiring A] → {I : Ideal A} → (hI : DividedPowers I) → hI.DPMorphism hI
-- Init.Data.SInt.Lemmas
Int64.ofInt_sub : ∀ (a b : ℤ), Int64.ofInt (a - b) = Int64.ofInt a - Int64.ofInt b
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Apollonius's Theorem**.  -/
EuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (a b c : P),
  dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.ExtDTreeMap.keyAtIdx? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → ℕ → Option α
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- **Alias** of `isOpen_setOfPred_nat_le_rank`. -/
isOpen_setOf_nat_le_rank : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  (n : ℕ), IsOpen {f | ↑n ≤ (↑f).rank}
-- Mathlib.NumberTheory.Chebyshev
/-- Integrability for the integral in `Chebyshev.primeCounting_eq_theta_div_log_add_integral`.  -/
Chebyshev.integrableOn_theta_div_id_mul_log_sq : ∀ (x : ℝ),
  MeasureTheory.IntegrableOn (fun t => Chebyshev.theta t / (t * Real.log t ^ 2)) (Set.Icc 2 x) MeasureTheory.volume
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.smooth_def : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.Smooth ↔ f.FormallySmooth ∧ f.FinitePresentation
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- the morphism from the zeroth row to the first row  -/
CategoryTheory.ShortComplex.SnakeInput.v₀₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (self : CategoryTheory.ShortComplex.SnakeInput C) → self.L₀ ⟶ self.L₁
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.uniformBell_zero_right : ∀ (m : ℕ), m.uniformBell 0 = 1
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- The element `h i`, as a term of the Cartan subalgebra `cartanSubalgebra' b`.  -/
RootPairing.GeckConstruction.h' : {ι : 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} →
                    [inst_5 : P.IsCrystallographic] →
                      {b : P.Base} →
                        [inst_6 : Finite ι] →
                          [inst_7 : IsDomain R] →
                            [inst_8 : CharZero R] →
                              [inst_9 : Fintype ι] →
                                [inst_10 : DecidableEq ι] →
                                  ↥b.support → ↥(RootPairing.GeckConstruction.cartanSubalgebra' b)
-- Mathlib.Algebra.Order.Module.Field
PosSMulStrictMono.toPosSMulReflectLT : ∀ {𝕜 : Type u_1} {G : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup G] [inst_4 : PartialOrder G] [inst_5 : MulActionWithZero 𝕜 G] [PosSMulStrictMono 𝕜 G],
  PosSMulReflectLT 𝕜 G
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Multipliable.hasProd : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α},
  Multipliable f L → HasProd f (∏'[L] (b : β), f b) L
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_subset_Ico_right : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₂ ≤ a₁ → Set.Ico b a₂ ⊆ Set.Ico b a₁
-- Lean.DocString.Extension
Lean.ElabInline.custom.injEq : ∀ (val val_1 : Dynamic), (Lean.ElabInline.custom val = Lean.ElabInline.custom val_1) = (val = val_1)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.forget_obj : ∀ {W : Type v'} [inst : CategoryTheory.Category.{w', v'} W] [inst_1 : CategoryTheory.MonoidalCategory W] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory W C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory W D]
  (F : CategoryTheory.EnrichedFunctor W C D) (X : CategoryTheory.ForgetEnrichment W C),
  F.forget.obj X = CategoryTheory.ForgetEnrichment.of W (F.obj (CategoryTheory.ForgetEnrichment.to W X))
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.IsEquivalence],
  CategoryTheory.IsIso h.unit