mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Sites.Representability
/-- The map from the glued scheme `(glueData hf).glued`, treated as a sheaf, to `F`.  -/
AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf : {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} →
  {ι : Type u} →
    {X : ι → AlgebraicGeometry.Scheme} →
      {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} →
        (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) →
          AlgebraicGeometry.Scheme.zariskiTopology.yoneda.obj
              (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).glued ⟶
            F
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Given two left-invariant measures which are finite on compacts,
`addHaarScalarFactor μ' μ` is a scalar such that `∫ f dμ' = (addHaarScalarFactor μ' μ) ∫ f dμ` for
any compactly supported continuous function `f`.

Note that there is a dissymmetry in the assumptions between `μ'` and `μ`: the measure `μ'` needs
only be finite on compact sets, while `μ` has to be finite on compact sets and positive on open
sets, i.e., an additive Haar measure, to exclude for instance the case where `μ = 0`, where the
definition doesn't make sense.  -/
MeasureTheory.Measure.addHaarScalarFactor : {G : Type u_1} →
  [inst : TopologicalSpace G] →
    [inst_1 : AddGroup G] →
      [IsTopologicalAddGroup G] →
        [inst_3 : MeasurableSpace G] →
          [BorelSpace G] →
            (μ' μ : MeasureTheory.Measure G) →
              [μ.IsAddHaarMeasure] → [MeasureTheory.IsFiniteMeasureOnCompacts μ'] → [μ'.IsAddLeftInvariant] → NNReal
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.isoInverseComp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E}
  {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D),
  i.isoInverseComp.hom.app X =
    CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj X))
-- Mathlib.Topology.Category.CompHaus.Limits
/-- The isomorphism from an arbitrary terminal object of `CompHaus` to a one-element space.  -/
CompHaus.terminalIsoPUnit : ⊤_ CompHaus ≅ CompHaus.of PUnit.{u + 1}
-- Init.Data.SInt.Lemmas
Int16.zero_lt_one : 0 < 1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_1.eq : ∀ {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_2 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Sort u}
  {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  (t : Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot))
  (F_1 : (t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t :
        Lean.Language.TransformedSnap
          (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t)
  (F_5 :
    (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t)
  (F_6 :
    (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t)
  (F_7 :
    (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t)
  (F_8 :
    (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t),
  Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_1 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 =
    F_2 t (Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_1.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8).2
-- Lean.Meta.Match.MatcherApp.Transform
Lean.Meta.MatcherApp.TransformAltFVars.mk.sizeOf_spec : ∀ (args fields overlaps discrEqs extraEqs : Array Lean.Expr),
  sizeOf { args := args, fields := fields, overlaps := overlaps, discrEqs := discrEqs, extraEqs := extraEqs } =
    1 + sizeOf args + sizeOf fields + sizeOf overlaps + sizeOf discrEqs + sizeOf extraEqs
-- Mathlib.Data.List.FinRange
List.ofFn_id : ∀ (n : ℕ), List.ofFn id = List.finRange n
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
CategoryTheory.Sheaf.hasExactColimitsOfShape : ∀ {C : Type u} {A : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Category.{v₁, u₁} A] [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasFiniteLimits A]
  [inst_4 : CategoryTheory.HasSheafify J A] [inst_5 : CategoryTheory.Limits.HasColimitsOfShape K A]
  [CategoryTheory.HasExactColimitsOfShape K A], CategoryTheory.HasExactColimitsOfShape K (CategoryTheory.Sheaf J A)
-- Lean.EnvExtension
Lean.MapDeclarationExtension.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α]
  (toPersistentEnvExtension : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)),
  sizeOf { toPersistentEnvExtension := toPersistentEnvExtension } = 1 + sizeOf toPersistentEnvExtension
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisors_le_comap_nonZeroDivisors_of_injective : ∀ {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [inst : MonoidWithZero M₀] [inst_1 : MonoidWithZero M₀']
  [inst_2 : FunLike F M₀ M₀'] [NoZeroDivisors M₀'] [inst_4 : MonoidWithZeroHomClass F M₀ M₀'] (f : F),
  Function.Injective ⇑f → nonZeroDivisors M₀ ≤ Submonoid.comap f (nonZeroDivisors M₀')
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
  (h₁₂ : p₁ = p₂) (h₂₃ : p₂ = p₃),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom
-- Init.Data.SInt.Lemmas
Int8.toBitVec_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toBitVec = OfNat.ofNat n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.inter_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.inter t₂ = t₁ ∩ t₂
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- Evidence that `h` commutes with the left Kan extension `f⁺ g`.  -/
CategoryTheory.Bicategory.Lan.CommuteWith.isKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : a ⟶ c) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] →
            {x : B} →
              (h : c ⟶ x) →
                [CategoryTheory.Bicategory.Lan.CommuteWith f g h] →
                  ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h).IsKan
-- Mathlib.Order.Bounded
Set.bounded_ge_Ioc : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 ≥ x2) (Set.Ioc a b)
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- The symbol vanishes when both entries are even (and `b / 2 ≠ 0`).  -/
Mathlib.Meta.NormNum.jacobiSymNat.even_even : ∀ (a b : ℕ), (b / 2).beq 0 = false → a % 2 = 0 → b % 2 = 0 → Mathlib.Meta.NormNum.jacobiSymNat a b = 0
-- Mathlib.Algebra.Lie.UniversalEnveloping
instRingUniversalEnvelopingAlgebra : (R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Ring (UniversalEnvelopingAlgebra R L)
-- Mathlib.Tactic.Linter.MinImports
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.ImportState.mk : Option (Lean.NameMap Lean.NameSet) → Lean.NameSet → ℕ → Mathlib.Linter.ImportState✝
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- `MeasureTheory.SignedMeasure.toJordanDecomposition` and
`MeasureTheory.JordanDecomposition.toSignedMeasure` form an `Equiv`.  -/
MeasureTheory.SignedMeasure.toJordanDecompositionEquiv : (α : Type u_2) → [inst : MeasurableSpace α] → MeasureTheory.SignedMeasure α ≃ MeasureTheory.JordanDecomposition α
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.equivalenceMonoOver_functor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  (A : CategoryTheory.Subfunctor F),
  (CategoryTheory.Subfunctor.equivalenceMonoOver F).functor.obj A = CategoryTheory.MonoOver.mk A.ι
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.exact_cotangentComplex_toKaehler : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Function.Exact ⇑P.cotangentComplex ⇑P.toKaehler
-- Init.Grind.Order
Lean.Grind.Order.lt_trans : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α},
  a < b → b < c → a < c
-- Init.Data.UInt.Lemmas
UInt64.ofNatClamp.eq_1 : ∀ (n : ℕ),
  UInt64.ofNatClamp n =
    if h : n < UInt64.size then UInt64.ofNatLT n h else UInt64.ofNatLT (UInt64.size - 1) UInt64.ofNatClamp._proof_1
-- Init.Data.Nat.Lemmas
Nat.exists_eq_add_of_le' : ∀ {m n : ℕ}, m ≤ n → ∃ k, n = k + m
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.involute_comp_involute : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, CliffordAlgebra.involute.comp CliffordAlgebra.involute = AlgHom.id R (CliffordAlgebra Q)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonHighlightMatchesOptions : Lean.FromJson Lean.Lsp.HighlightMatchesOptions
-- Std.Data.ByteSlice
/-- The starting index of the region of interest (inclusive).
 -/
Std.Slice.Internal.ByteSliceData.start : Std.Slice.Internal.ByteSliceData → ℕ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.hasRightHomology_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasRightHomology], S₂.HasRightHomology
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- A structure on a lax functor that promotes a lax functor to a pseudofunctor.

See `Pseudofunctor.mkOfLax`.  -/
CategoryTheory.LaxFunctor.PseudoCore : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.LaxFunctor B C → Type (max (max u₁ v₁) w₂)
-- Lean.Compiler.IR.Basic
Lean.IR.Arg.var.injEq : ∀ (id id_1 : Lean.IR.VarId), (Lean.IR.Arg.var id = Lean.IR.Arg.var id_1) = (id = id_1)
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
tsum_dirichletSummand : ∀ {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re),
  ∑' (n : ℕ), (dirichletSummandHom χ ⋯) n = LSeries (fun n => χ ↑n) s
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonDiagnosticTag : Lean.ToJson Lean.Lsp.DiagnosticTag
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (t : Set α), μ t = ∑' (g : G), μ ((g +ᵥ t) ∩ s)
-- Mathlib.Data.Finsupp.Multiset
Finsupp.sum_id_lt_of_lt : ∀ {ι : Type u_3} (m n : ι →₀ ℕ), m < n → (m.sum fun x => id) < n.sum fun x => id
-- Init.Data.List.Monadic
List.mapM.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m β) (as : List α),
  List.mapM f as = List.mapM.loop f as []
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 0 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂₃ f₄).obj 0)
-- Lean.Language.Basic
Lean.Language.instInhabitedSnapshotTask.default : {α : Type} → [Inhabited α] → Lean.Language.SnapshotTask α
-- Mathlib.Computability.Primrec.Basic
Primrec₂.left : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec₂ fun a x => a
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.decidableLE : {α : Type u_1} → [inst : Preorder α] → [DecidableLE α] → DecidableLE (WithZero α)
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.map_P : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (G : CategoryTheory.Functor C D) [G.Additive] (X : CategoryTheory.SimplicialObject C) (q n : ℕ),
  G.map ((AlgebraicTopology.DoldKan.P q).f n) = (AlgebraicTopology.DoldKan.P q).f n
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.neg : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f : α → β} {a : α} {s : Set α}, IsLocalExtrOn f s a → IsLocalExtrOn (fun x => -f x) s a
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D},
  autoParam (G.IsCoverDense K) CategoryTheory.Functor.IsDenseSubsite.isCoverDense'._autoParam →
    autoParam (G.IsLocallyFull K) CategoryTheory.Functor.IsDenseSubsite.isLocallyFull'._autoParam →
      autoParam (G.IsLocallyFaithful K) CategoryTheory.Functor.IsDenseSubsite.isLocallyFaithful'._autoParam →
        (∀ {X : C} {S : CategoryTheory.Sieve X}, CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj X) ↔ S ∈ J X) →
          CategoryTheory.Functor.IsDenseSubsite J K G
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rio_eq_some_iff : ∀ {k n i : ℕ}, (*...n).toList[i]? = some k ↔ i < n ∧ i = k
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
tprod_def : ∀ {α : Type u_4} {β : Type u_5} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) (L : SummationFilter β),
  tprod f L =
    if h : Multipliable f L then
      if L.HasSupport ∧ (Function.mulSupport f ∩ L.support).Finite then finprod (L.support.mulIndicator f)
      else if HasProd f 1 L then 1 else Exists.choose h
    else 1
-- Mathlib.Data.Multiset.Fintype
/-- One of the possible equivalences from `Multiset.mapEquivAux`, selected using choice.
 -/
Multiset.mapEquiv : {α : Type u_1} →
  {β : Type u_2} →
    [inst : DecidableEq α] →
      [inst_1 : DecidableEq β] → (s : Multiset α) → (f : α → β) → s.ToType ≃ (Multiset.map f s).ToType
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote.match_1.congr_eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (p : Int.Internal.Linear.Poly)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add k v p))
  (k : ℤ) (v : Int.Internal.Linear.Var) (p_1 : Int.Internal.Linear.Poly),
  p = Int.Internal.Linear.Poly.add k v p_1 →
    (match p with
      | Int.Internal.Linear.Poly.num k => h_1 k
      | Int.Internal.Linear.Poly.add k v p => h_2 k v p) ≍
      h_2 k v p_1
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_conj : ∀ (x : ℂ), Complex.sinh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.sinh x)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- If `H` is a characteristic additive subgroup of `G`, then every automorphism of `G` induces an
automorphism of `H`.  -/
AddAut.characteristic : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → [H.Characteristic] → AddAut G →+ AddAut ↥H
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.min : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMaxOn f s a → IsLocalMaxOn g s a → IsLocalMaxOn (fun x => min (f x) (g x)) s a
-- Mathlib.Analysis.Complex.Circle
Circle.neg_ne_self : ∀ (x : Circle), -x ≠ x
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- How many new goals are generated.  -/
Mathlib.Tactic.ClickSuggestions.ApplyKey.numGoals : Mathlib.Tactic.ClickSuggestions.ApplyKey → ℕ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_diff_eq_false_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true → Std.DTreeMap.Internal.Impl.contains k (m₁.diff m₂ ⋯) = false
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_eq_some_getElem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  (h : a ∈ t), t[a]? = some t[a]
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.prod_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : 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]
  [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) (x : A),
  (f.prod g) x = (f x, g x)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} →
        (f₀ : S₁.L₀ ⟶ S₂.L₀) →
          (f₁ : S₁.L₁ ⟶ S₂.L₁) →
            (f₂ : S₁.L₂ ⟶ S₂.L₂) →
              (f₃ : S₁.L₃ ⟶ S₂.L₃) →
                autoParam (CategoryTheory.CategoryStruct.comp f₀ S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ f₁)
                    CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁._autoParam →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp f₁ S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ f₂)
                      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂._autoParam →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp f₂ S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ f₃)
                        CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃._autoParam →
                      S₁.Hom S₂
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_finVal : ∀ {w : ℕ} (n : Fin (2 ^ w)), BitVec.ofNat w ↑n = { toFin := n }
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point}
  {x y : Φ₁.Hom Φ₂}, x.hom = y.hom → x = y
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.unwantedUnicode.injEq : ∀ (c c_1 : Char),
  (Mathlib.Linter.TextBased.StyleError.unwantedUnicode✝ c = Mathlib.Linter.TextBased.StyleError.unwantedUnicode✝ c_1) =
    (c = c_1)
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_inter : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} [inst_2 : (a : α) → DecidableEq (δ a)]
  (s t : (a : α) → Finset (δ a)), (Fintype.piFinset fun i => s i ∩ t i) = Fintype.piFinset s ∩ Fintype.piFinset t
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_succ_left : ∀ (n k : ℕ), k ≠ 0 → (n + 1).stirlingFirst k = n * n.stirlingFirst k + n.stirlingFirst (k - 1)
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.whiskerRight_def : ∀ (R : Type u) [inst : CommRing R] {X₁ X₂ : HopfAlgCat R} (f : X₁ ⟶ X₂) (X : HopfAlgCat R),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = HopfAlgCat.ofHom (BialgHom.rTensor X.carrier f.toBialgHom')
-- Lean.Data.Position
Lean.instReprPosition : Repr Lean.Position
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_lift_fst_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c}
  (α : M ⟶ K) (β : M ⟶ L) (i : ι),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i)
      (CategoryTheory.Limits.biprod.fst.f i) =
    α.f i
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_succ`. -/
lowerCentralSeries_succ : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) (n : ℕ), S.lowerCentralSeries (n + 1) = ⁅S.lowerCentralSeries n, S⁆
-- Init.Data.String.Termination
String.Slice.Pos.lt_iff_remainingBytes_lt : ∀ {s : String.Slice} (p q : s.Pos), p < q ↔ q.remainingBytes < p.remainingBytes
-- Mathlib.Algebra.Category.Grp.Basic
CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply : ∀ {X Y : AddCommGrpCat} (i : X ≅ Y) (a : ↑X), i.addCommGroupIsoToAddEquiv a = (AddCommGrpCat.Hom.hom i.hom) a
-- Mathlib.CategoryTheory.Filtered.Basic
/-- for every pair of objects there exists another object "to the left"  -/
CategoryTheory.IsCofilteredOrEmpty.cone_objs : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsCofilteredOrEmpty C] (X Y : C),
  ∃ W x x, True
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- The sheaf condition in terms of an equalizer diagram is equivalent
to the default sheaf condition.
 -/
TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X), F.IsSheaf ↔ F.IsSheafEqualizerProducts
-- Lean.Meta.Tactic.Grind.Arith.Simproc
_private.Lean.Meta.Tactic.Grind.Arith.Simproc.0.Lean.Meta.Grind.Arith.isNotFieldQuick : Lean.Expr → Bool
-- Mathlib.Algebra.Order.Ring.Abs
abs_eq_iff_mul_self_eq : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α}, |a| = |b| ↔ a * a = b * b
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv (CategoryTheory.CategoryStruct.comp S.homologyπ h) =
    CategoryTheory.CategoryStruct.comp S.moduleCatLeftHomologyData.π
      (CategoryTheory.CategoryStruct.comp S.moduleCatHomologyIso.inv h)
-- Mathlib.Algebra.Lie.Solvable
/-- Given a solvable Lie ideal `I` with derived series `I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥`, this is the
natural number `k` (the number of inclusions).

For a non-solvable ideal, the value is 0.  -/
LieAlgebra.derivedLengthOfIdeal : (R : Type u) → (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieIdeal R L → ℕ
-- Mathlib.Data.List.Fold
/-- **First Bird–Wadler duality theorem**.  -/
List.foldl_eq_foldr_of_commute : ∀ {α : Type u_1} {l : List α} {a : α} {f : α → α → α} [Std.Associative f],
  (∀ (x : α), f a x = f x a) → List.foldl f a l = List.foldr f a l