mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.lineDerivOp_left_neg : ∀ {V : Type u_5} {E : Type u_6} {F : Type u_7} [inst : AddCommGroup V] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : LineDeriv V E F] [LineDerivAdd V E F] (v : V) (x : E),
  LineDeriv.lineDerivOp (-v) x = -LineDeriv.lineDerivOp v x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.foldM_eq_foldlM_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  Std.DHashMap.foldM (fun d a x => f d a) init m = List.foldlM f init m.keys
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangle_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Pretriangulated.contractibleTriangle X).obj₃ = 0
-- Lean.Parser.Extra
Lean.Parser.ppGroup.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.Types.instIsStableUnderSupJointlySurjectivePrecoverage : CategoryTheory.Types.jointlySurjectivePrecoverage.IsStableUnderSup
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_X_one : ∀ {R : Type u_1} [inst : Semiring R], SkewPolynomial.X.coeff 1 = 1
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  {X Y : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))} (f : X ⟶ Y) (X_1 : C₁)
  (X_2 : C₂) (X_3 : C₃),
  (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).map f).app X_1).app X_2).app X_3 =
    ((f.app (F₁.obj X_1)).app (F₂.obj X_2)).app (F₃.obj X_3)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_inj : ∀ {z w : Complex.UnitClosedDisc}, ↑z = ↑w ↔ z = w
-- Init.Tactics
/-- `rotate_left n` rotates goals to the left by `n`. That is, `rotate_left 1`
takes the main goal and puts it to the back of the subgoal list.
If `n` is omitted, it defaults to `1`.
 -/
Lean.Parser.Tactic.rotateLeft : Lean.ParserDescr
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsPosSemidef.mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : LE R]
  {B : LinearMap.BilinForm R M}, B.IsSymm → B.IsNonneg → B.IsPosSemidef
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.  -/
MonoidHom.eqOn_closureM : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {f g : M →* N} {s : Set M},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Submonoid.closure s)
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.instInhabited : (G : Type u) → [inst : Group G] → Inhabited (Abelianization G)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_add : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {g₁ g₂ : Π₀ (i : ι), β i},
  (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If the limit of `F` exists and `G` preserves it, then if `G` reflects isomorphisms then it
reflects the limit of `F` (see also `JointlyReflectIsomorphisms.jointlyReflectsColimit` in
the file `CategoryTheory/Functor/ReflectsIso/Limits.lean` for the corresponding result
for a family of functors which joinly reflect isomorphisms).
 -/
CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasLimit F]
  [CategoryTheory.Limits.PreservesLimit F G], CategoryTheory.Limits.ReflectsLimit F G
-- Mathlib.Algebra.Field.Defs
/-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`  -/
Field.zpow_neg' : ∀ {K : Type u} [self : Field K] (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G],
  ContMDiff (I.prod I) I n fun p => p.1 + p.2
-- Mathlib.Algebra.Module.Hom
ZeroHom.instModule : {R : Type u_1} →
  {A : Type u_4} →
    {B : Type u_5} →
      [inst : Semiring R] → [inst_1 : AddMonoid A] → [inst_2 : AddCommMonoid B] → [Module R B] → Module R (ZeroHom A B)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.TransferEncoding.inst : Std.Http.Header Std.Http.Header.TransferEncoding
-- Aesop.Forward.Match.Types
Aesop.instHashableCompleteMatch : Hashable Aesop.CompleteMatch
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
CategoryTheory.zeroMul_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {A : C}
  [inst_2 : CategoryTheory.Closed A] {I : C} (t : CategoryTheory.Limits.IsInitial I),
  (CategoryTheory.zeroMul t).inv = t.to (CategoryTheory.MonoidalCategoryStruct.tensorObj A I)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.ext : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} {F G : f₀.HomotopyWith f₁ P}, (∀ (x : ↑unitInterval × X), F x = G x) → F = G
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.eq_jacobson_iff_sInf_maximal' : ∀ {R : Type u} [inst : Ring R] {I : Ideal R},
  I.jacobson = I ↔ ∃ M, (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M
-- Std.Data.TreeMap.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.
 -/
Std.TreeMap.insert : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → β → Std.TreeMap α β cmp
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.insertMany_list_singleton : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α}, m.insertMany [k] = m.insert k
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.inclusion_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖)
  {x : RestrictedProduct (fun i => R i) (fun i => A i) 𝓖} (i : ι), (RestrictedProduct.inclusion R A h x) i = x i
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.compMultilinearMap_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (g : M₂ →ₗ[R] M₃)
  (f : MultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i), (g.compMultilinearMap f) m = g (f m)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_extend_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_8} {ι' : Type u_9} {f : ι → ι'},
  Function.Injective f →
    ∀ (m : ι → MeasureTheory.Measure α), MeasureTheory.Measure.sum (Function.extend f m 0) = MeasureTheory.Measure.sum m
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_iInter_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β},
  (∀ (i : ι), Set.MapsTo f (s i) (t i)) → Set.MapsTo f (⋂ i, s i) (⋂ i, t i)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_eq_of_equiv : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      (↑m₁).Equiv ↑m₂ →
        ∀ {k : α} {fallback : β},
          Std.DHashMap.Internal.Raw₀.Const.getD m₁ k fallback = Std.DHashMap.Internal.Raw₀.Const.getD m₂ k fallback
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.instMulActionProjGenLinGroupForall : {K : Type u_1} →
  [inst : Field K] →
    {ι : Type u_3} →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] → MulAction (Matrix.ProjGenLinGroup ι K) (Projectivization K (ι → K))
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.eq_neg_one : ∀ {G : Type u_1} [inst : Ring G] [inst_1 : LinearOrder G] [IsStrictOrderedRing G] {a : G},
  a ≤ 0 → IsOfFinOrder a → a = -1
-- Mathlib.CategoryTheory.Localization.Trifunctor
/-- Given localization functor `L₁ : C₁ ⥤ D₁`, `L₂ : C₂ ⥤ D₂` and `L₃ : C₃ ⥤ D₃`
with respect to `W₁ : MorphismProperty C₁`, `W₂ : MorphismProperty C₂` and
`W₃ : MorphismProperty C₃` respectively, and a trifunctor `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E`
which inverts `W₁`, `W₂` and `W₃`, this is the induced localized
trifunctor `D₁ ⥤ D₂ ⥤ D₃ ⥤ E`.  -/
CategoryTheory.Localization.lift₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_6} →
        {D₂ : Type u_7} →
          {D₃ : Type u_8} →
            {E : Type u_13} →
              [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
                [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                    [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁] →
                      [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] →
                        [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃] →
                          [inst_6 : CategoryTheory.Category.{v_13, u_13} E] →
                            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) →
                              {W₁ : CategoryTheory.MorphismProperty C₁} →
                                {W₂ : CategoryTheory.MorphismProperty C₂} →
                                  {W₃ : CategoryTheory.MorphismProperty C₃} →
                                    W₁.IsInvertedBy₃ W₂ W₃ F →
                                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                                        (L₂ : CategoryTheory.Functor C₂ D₂) →
                                          (L₃ : CategoryTheory.Functor C₃ D₃) →
                                            [L₁.IsLocalization W₁] →
                                              [L₂.IsLocalization W₂] →
                                                [L₃.IsLocalization W₃] →
                                                  [W₁.ContainsIdentities] →
                                                    [W₂.ContainsIdentities] →
                                                      [W₃.ContainsIdentities] →
                                                        CategoryTheory.Functor D₁
                                                          (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.instRepr : Repr GaussianInt
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousAt_finite : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [Finite ι]
  {F : ι → X → α} {x₀ : X}, EquicontinuousAt F x₀ ↔ ∀ (i : ι), ContinuousAt (F i) x₀
-- Std.Time.Format.Modifier
Std.Time.Modifier.O.inj : ∀ {presentation presentation_1 : Std.Time.OffsetO},
  Std.Time.Modifier.O presentation = Std.Time.Modifier.O presentation_1 → presentation = presentation_1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendIso_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : s.pt ≅ X),
  (s.extendIso f).inv.hom = f.inv
-- Mathlib.NumberTheory.Padics.Complex
PadicComplex.instIsScalarTowerPadicPadicAlgCl : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], IsScalarTower ℚ_[p] (PadicAlgCl p) ℂ_[p]
-- Mathlib.Data.ENat.Lattice
ENat.le_iInf_add_iInf : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} {κ : Sort u_4} {g : κ → ℕ∞},
  (∀ (i : ι) (j : κ), a ≤ f i + g j) → a ≤ iInf f + iInf g
-- Mathlib.Analysis.Convex.Body
ConvexBody.nonempty : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] (K : ConvexBody V),
  (↑K).Nonempty
-- Lean.Meta.SizeOf
/-- Create `SizeOf` local instances for applicable parameters, and execute `k` using them.  -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.mkLocalInstances : {α : Type} → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_of_le_ge_cert.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly), Int.Internal.Linear.eq_of_le_ge_cert p₁ p₂ = p₂.beq' (p₁.mul_k (-1))
-- Init.Control.StateRef
StateRefT'.instMonad : {ω σ : Type} → {m : Type → Type} → [Monad m] → Monad (StateRefT' ω σ m)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
/-- `natTrailingDegree p` forces `trailingDegree p` to `ℕ`, by defining
`natTrailingDegree ⊤ = 0`.  -/
Polynomial.natTrailingDegree : {R : Type u} → [inst : Semiring R] → Polynomial R → ℕ
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_mapsTo : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α),
  Set.MapsTo (fun j => ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (Set.Iio k) ↑F
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.Rewrite.mk.injEq : ∀ (symm : Bool) (proof replacement : Lean.Expr) (stringLength : ℕ) (extraGoals : Array (Lean.MVarId × Lean.BinderInfo))
  (makesNewMVars symm_1 : Bool) (proof_1 replacement_1 : Lean.Expr) (stringLength_1 : ℕ)
  (extraGoals_1 : Array (Lean.MVarId × Lean.BinderInfo)) (makesNewMVars_1 : Bool),
  ({ symm := symm, proof := proof, replacement := replacement, stringLength := stringLength, extraGoals := extraGoals,
        makesNewMVars := makesNewMVars } =
      { symm := symm_1, proof := proof_1, replacement := replacement_1, stringLength := stringLength_1,
        extraGoals := extraGoals_1, makesNewMVars := makesNewMVars_1 }) =
    (symm = symm_1 ∧
      proof = proof_1 ∧
        replacement = replacement_1 ∧
          stringLength = stringLength_1 ∧ extraGoals = extraGoals_1 ∧ makesNewMVars = makesNewMVars_1)
-- Mathlib.InformationTheory.Coding.UniquelyDecodable
InformationTheory.UniquelyDecodable.flatten_injective : ∀ {α : Type u_1} {S : Set (List α)}, InformationTheory.UniquelyDecodable S → Function.Injective fun L => (↑L).flatten
-- Mathlib.ModelTheory.Bundled
/-- The equivalence relation on bundled `L.Structure`s indicating that they are isomorphic.  -/
FirstOrder.Language.equivSetoid : {L : FirstOrder.Language} → Setoid (CategoryTheory.Bundled L.Structure)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited β] {a : α}, ∅[a]! = default
-- Mathlib.Topology.UrysohnsLemma
/-- Continuity of `Urysohns.CU.lim`. See module docstring for a sketch of the proofs.  -/
Urysohns.CU.continuous_lim : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P), Continuous c.lim
-- Init.Data.String.Basic
String.decidableLT : (s₁ s₂ : String) → Decidable (s₁ < s₂)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A morphism of functors `WithInitial C ⥤ D` gives a morphism between the associated comma
objects.  -/
CategoryTheory.WithInitial.mkCommaMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {F G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D} →
          (F ⟶ G) → (CategoryTheory.WithInitial.mkCommaObject F ⟶ CategoryTheory.WithInitial.mkCommaObject G)
-- Mathlib.Algebra.Group.Invertible.Defs
/-- The inverse of an `Invertible` element  -/
Invertible.invOf : {α : Type u} → {inst : Mul α} → {inst_1 : One α} → (a : α) → [self : Invertible a] → α
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- A weighted homogeneous polynomial of degree `n` whose support degrees are all equal to a
fixed `d₀` is a single monomial.  -/
MvPolynomial.IsWeightedHomogeneous.eq_monomial_of_unique_weight : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {φ : MvPolynomial σ R}
  {n : M} {w : σ → M} {d₀ : σ →₀ ℕ},
  MvPolynomial.IsWeightedHomogeneous w φ n →
    (∀ (d : σ →₀ ℕ), (Finsupp.weight w) d = n → d = d₀) → φ = (MvPolynomial.monomial d₀) (MvPolynomial.coeff d₀ φ)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.mem_stabilizer_set_iff_subset_vadd_set : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {s : Set α},
  s.Finite → (a ∈ AddAction.stabilizer G s ↔ s ⊆ a +ᵥ s)
-- Mathlib.Algebra.Lie.OfAssociative
AlgHom.toLieHom_injective : ∀ {A : Type v} [inst : Ring A] {R : Type u} [inst_1 : CommRing R] [inst_2 : Algebra R A] {B : Type w} [inst_3 : Ring B]
  [inst_4 : Algebra R B] {f g : A →ₐ[R] B}, f.toLieHom = g.toLieHom → f = g
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Alt.mk.sizeOf_spec : ∀ {σ : Type} [inst : SizeOf σ] (ref : Lean.Syntax) (vars : Array Lean.Elab.Term.Do.Var) (patterns : Lean.Syntax)
  (rhs : σ),
  sizeOf { ref := ref, vars := vars, patterns := patterns, rhs := rhs } =
    1 + sizeOf ref + sizeOf vars + sizeOf patterns + sizeOf rhs
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.toAddHom_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N), f.toAddHom = ↑f
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftRight_add : ∀ (i : ℤ) (m n : ℕ), i >>> (m + n) = i >>> m >>> n
-- Mathlib.Data.ENNReal.Inv
ENNReal.iSup_div : ∀ {ι : Sort u_1} (f : ι → ENNReal) (a : ENNReal), iSup f / a = ⨆ i, f i / a
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabVersion : Lean.Elab.Command.CommandElab
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement'.symm : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → K.IsComplement' H
-- Mathlib.Order.WithBot
WithTop.coe_eq_bot : ∀ {α : Type u_1} [inst : Bot α] {a : α}, ↑a = ⊥ ↔ a = ⊥
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield contains `1`, products and inverses.

Be assured that we're not actually proving that subfields are subgroups:
`SubgroupClass` is really an abbreviation of `SubgroupWithOrWithoutZeroClass`.
 -/
SubfieldClass.toSubgroupClass : ∀ {K : Type u} [inst : DivisionRing K] (S : Type u_1) [inst_1 : SetLike S K] [h : SubfieldClass S K], SubgroupClass S K
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The morphism `(cokernel f).truncGE n ⟶ S f n` which in degree `n` is
given by `Injective.ι _`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.p : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            (n : ℤ) →
              (CategoryTheory.Limits.cokernel f).truncGE n ⟶
                CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.S✝ f n
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a product is the max of the nilpotency classes of the factors.  -/
Group.nilpotencyClass_prod : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] [Group.IsNilpotent G₁] [Group.IsNilpotent G₂],
  Group.nilpotencyClass (G₁ × G₂) = max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂)
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.ncard_inter_orthRadius_le_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hf2 : Fact (Module.finrank ℝ V = 2)] {s : EuclideanGeometry.Sphere P} {p : P},
  p ≠ s.center → (Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)).ncard ≤ 2
-- Mathlib.MeasureTheory.Group.Measure
/-- In an abelian group every left invariant measure is also right-invariant.
We don't declare the converse as an instance, since that would loop type-class inference, and
we use `IsMulLeftInvariant` as the default hypothesis in abelian groups.  -/
MeasureTheory.IsMulLeftInvariant.isMulRightInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : CommSemigroup G] {μ : MeasureTheory.Measure G}
  [μ.IsMulLeftInvariant], μ.IsMulRightInvariant
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
/-- A normed additive commutative group structure on `C⋆ᵐᵒᵈ(A, Π i, E i)` with the wrong topology,
uniformity and bornology. This is only used to build the instance with the correct forgetful
inheritance data.  -/
WithCStarModule.normedAddCommGroupPiAux : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {ι : Type u_2} →
        {E : ι → Type u_3} →
          [Fintype ι] →
            [inst_3 : (i : ι) → NormedAddCommGroup (E i)] →
              [inst_4 : (i : ι) → Module ℂ (E i)] →
                [inst_5 : (i : ι) → SMul A (E i)] →
                  [(i : ι) → CStarModule A (E i)] →
                    [StarOrderedRing A] → NormedAddCommGroup (WithCStarModule A ((i : ι) → E i))
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.iSup.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} [inst : Finite β] (f : β → L.BoundedFormula α n),
  FirstOrder.Language.BoundedFormula.iSup f = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map f Finset.univ.toList)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF → (m.alter k f)[k']? = if (k == k') = true then f m[k]? else m[k']?
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.instCoeFunForall : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → CoeFun (ContinuousMap.HomotopyEquiv X Y) fun x => X → Y
-- Init.Tactics
/-- `bv_omega` is `omega` with an additional preprocessor that turns statements about `BitVec` into statements about `Nat`.
Currently the preprocessor is implemented as `try simp only [bitvec_to_nat] at *`.
`bitvec_to_nat` is a `@[simp]` attribute that you can (cautiously) add to more theorems.
 -/
Lean.Parser.Tactic.tacticBv_omega : Lean.ParserDescr
-- Mathlib.Analysis.Asymptotics.Lemmas
ContinuousAt.isBigO : ∀ {F : Type u_4} [inst : Norm F] {α : Type u_17} {E : Type u_18} [inst_1 : NormedRing E] [inst_2 : One F]
  [NormOneClass F] [inst_4 : TopologicalSpace α] {f : α → E} {x : α}, ContinuousAt f x → f =O[nhds x] fun x => 1
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.instHasColimitGrothendieckFunctorCompGrothendieckProj : ∀ {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) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension G]
  [CategoryTheory.Limits.HasColimitsOfShape D H],
  CategoryTheory.Limits.HasColimit ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G)
-- Mathlib.Data.Fintype.BigOperators
Finset.prod_fin_eq_prod_range : ∀ {β : Type u_2} [inst : CommMonoid β] {n : ℕ} (c : Fin n → β),
  ∏ i, c i = ∏ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 1
-- Lean.CoreM
Lean.Core.Context.maxHeartbeats : Lean.Core.Context → ℕ