mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.TypeVec
TypeVec.subtypeVal.eq_def : ∀ (x : ℕ) (x_1 : TypeVec.{u} x) (x_2 : x_1.Arrow (TypeVec.repeat x Prop)) (x_3 : Fin2 x),
  TypeVec.subtypeVal x_2 x_3 =
    match (motive :=
      (x : ℕ) →
        (x_4 : TypeVec.{u} x) →
          (x_5 : x_4.Arrow (TypeVec.repeat x Prop)) → (x_6 : Fin2 x) → TypeVec.Subtype_ x_5 x_6 → x_4 x_6)
      x, x_1, x_2, x_3 with
    | n.succ, x, x_4, i.fs => TypeVec.subtypeVal (TypeVec.dropFun x_4) i
    | n.succ, x, x_4, Fin2.fz => Subtype.val
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.registerSolverExtension.unsafe_1 : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.SolverExtension Lean.Meta.Grind.SolverExtensionState
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.hom_ext_iff : ∀ {A B : ProfiniteAddGrp.{u}} {f g : A ⟶ B}, f = g ↔ ProfiniteAddGrp.Hom.hom f = ProfiniteAddGrp.Hom.hom g
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_inv_smul_symmDiff : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (symmDiff (c⁻¹ • s) t) = μ (symmDiff s (c • t))
-- Lean.Server.Rpc.Basic
Lean.Server.ReferencedObject.mk.injEq : ∀ (obj : Dynamic) (id : USize) (rc : ℕ) (obj_1 : Dynamic) (id_1 : USize) (rc_1 : ℕ),
  ({ obj := obj, id := id, rc := rc } = { obj := obj_1, id := id_1, rc := rc_1 }) =
    (obj = obj_1 ∧ id = id_1 ∧ rc = rc_1)
-- Std.Http.Data.Headers.Name
/-- A validated HTTP header name that ensures all characters conform to HTTP standards. Header names are
case-insensitive according to HTTP specifications.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-field-names
 -/
Std.Http.Header.Name : Type
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The colimit of `F ⋙ forget₂ GrpCat MonCat` in the category `MonCat`.
In the following, we will show that this has the structure of a group.
 -/
GrpCat.FilteredColimits.G : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J GrpCat → MonCat
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The second part of the third simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_σ_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 1)},
  CategoryTheory.CategoryStruct.comp (X.σ i) (X.δ i.succ) =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op { len := n }))
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The sieve generated by two morphisms.  -/
CategoryTheory.Sieve.ofTwoArrows : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {U V X : C} → (U ⟶ X) → (V ⟶ X) → CategoryTheory.Sieve X
-- Std.Http.Data.Status
/-- 400 Bad Request
 -/
Std.Http.Status.badRequest : Std.Http.Status
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_inv : ∀ {X Y : SSet} (A : Y.Subcomplex) (f : X ⟶ Y) [inst : CategoryTheory.IsIso f],
  A.image (CategoryTheory.inv f) = A.preimage f
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.mk.sizeOf_spec : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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] [inst_6 : LieModule R L M]
  [inst_7 : SizeOf R] [inst_8 : SizeOf L] [inst_9 : SizeOf M] (toLinearMap : L →ₗ[R] M)
  (leibniz' : ∀ (a b : L), toLinearMap ⁅a, b⁆ = ⁅a, toLinearMap b⁆ - ⁅b, toLinearMap a⁆),
  sizeOf { toLinearMap := toLinearMap, leibniz' := leibniz' } = 1 + sizeOf toLinearMap
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instIsIsoOverInferInstanceOverClass : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C), CategoryTheory.IsIso (S ↘ S)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.instCoeLinearMap : {R : Type u_1} →
  {S : Type u_6} →
    {M : Type u_7} →
      {M₂ : Type u_9} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {modM : Module R M} →
                  {modM₂ : Module S M₂} →
                    {σ : R →+* S} →
                      {σ' : S →+* R} →
                        [inst_4 : RingHomInvPair σ σ'] →
                          [inst_5 : RingHomInvPair σ' σ] → Coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂)
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithBot.some ⁻¹' Set.Ico ↑b ↑a = Set.Ico b a
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.map' : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing A'] [inst_3 : Algebra R A] [inst_4 : Algebra R A'],
  AlgebraicIndependent R x → ∀ {f : A →ₐ[R] A'}, Function.Injective ⇑f → AlgebraicIndependent R (⇑f ∘ x)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNonAssocRing : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [NonAssocRing β] → NonAssocRing (MeasureTheory.SimpleFunc α β)
-- Init.Data.Order.LemmasExtra
_private.Init.Data.Order.LemmasExtra.0.Std.min_le_min : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Min α] [Std.LawfulOrderLeftLeaningMin α] [Std.IsLinearOrder α] (a b : α),
  a ⊓ b ≤ b ⊓ a
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The counit of an adjunction  -/
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.counit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G → (G.comp F ⟶ CategoryTheory.Functor.id D)
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.objDown_objUp : ∀ {C : Type u_1} (A : C), (CategoryTheory.ULiftHom.objUp A).objDown = A
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.mk_out : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (a : Associates α), Associates.mk a.out = a
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Quiver.Hom.comp_toLoc : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {a b c : C} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.CategoryStruct.comp f g).toLoc = CategoryTheory.CategoryStruct.comp f.toLoc g.toLoc
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isInt_zpow_neg : ∀ {α : Type u_1} [inst : DivisionRing α] {a : α} {b : ℤ} {nb ne : ℕ},
  Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb) →
    Mathlib.Meta.NormNum.IsInt (a ^ nb)⁻¹ (Int.negOfNat ne) → Mathlib.Meta.NormNum.IsInt (a ^ b) (Int.negOfNat ne)
-- Mathlib.RingTheory.WittVector.Basic
WittVector.map_id : ∀ {p : ℕ} (R : Type u_1) [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)],
  WittVector.map (RingHom.id R) = RingHom.id (WittVector p R)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.isZero_H_obj_of_isIso : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j),
  CategoryTheory.IsIso f → ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.ιChainComplex_toNormalizedChainComplex_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : C}
  (h : (X.normalizedChainComplex R).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιChainComplex x)
      (CategoryTheory.CategoryStruct.comp ((X.toNormalizedChainComplex R).f n) h) =
    CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x) h
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.toTop_obj : ∀ (X : SimplexCategory),
  SimplexCategory.toTop.{u}.obj X = TopCat.uliftFunctor.obj (TopCat.of ↑(stdSimplex ℝ (Fin (X.len + 1))))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_sub_int_mul_pi : ∀ (x : ℝ) (n : ℤ), Real.tan (x - ↑n * Real.pi) = Real.tan x
-- Init.Prelude
/-- Retrieve the left-most node or leaf's info in the Syntax tree.  -/
Lean.Syntax.getHeadInfo? : Lean.Syntax → Option Lean.SourceInfo
-- Init.Grind.AC
Lean.Grind.AC.superpose_tail_idempotent_cert.eq_1 : ∀ (x : Lean.Grind.AC.Var) (lhs₁ rhs₁ rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_tail_idempotent_cert x lhs₁ rhs₁ rhs =
    (lhs₁.endsWithVar_k x).and' (rhs.beq' (rhs₁.concat (Lean.Grind.AC.Seq.var x)))
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_self : ∀ (a b : ℤ), b * a.tdiv b = a - a.tmod b
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.mem_pullSub_self : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} {x : List A}, x ∈ Descriptive.Tree.pullSub T x ↔ [] ∈ T
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- A category `HasPushouts` if it has all colimits of shape `WalkingSpan`, i.e. if it has a
pushout for every pair of morphisms with the same domain.  -/
CategoryTheory.Limits.HasPushouts : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Data.Multiset.Bind
Multiset.mem_join : ∀ {α : Type u_1} {a : α} {S : Multiset (Multiset α)}, a ∈ S.join ↔ ∃ s ∈ S, a ∈ s
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.mkConst.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool),
  aig.mkConst val =
    {
      aig :=
        { decls := aig.decls.push Std.Sat.AIG.Decl.false, cache := aig.cache.noUpdate, hdag := ⋯, hzero := ⋯,
          hconst := ⋯ },
      ref := { gate := aig.decls.size, invert := val, hgate := ⋯ } }
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.asNatTrans_mkHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f : C ≌ D} (η : e ⟶ f), CategoryTheory.Equivalence.asNatTrans (CategoryTheory.Equivalence.mkHom η) = η
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.instSetLike : {G : Type u_1} → [inst : Group G] → SetLike (Subgroup G) G
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_involutive : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B], Function.Involutive (FractionalIdeal.dual A K)
-- Mathlib.Order.Fin.Basic
Fin.OrderEmbedding.instInhabitedOrderEmbeddingNat : {n : ℕ} → Inhabited (Fin n ↪o ℕ)
-- Std.Http.Data.Body.Stream
Std.Http.Body.instForInAsyncStreamChunk : ForIn Std.Async.Async Std.Http.Body.Stream Std.Http.Chunk
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instCompleteLattice : (M : Type u_1) → [inst : AddZeroClass M] → CompleteLattice (SaturatedAddSubmonoid M)
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableWithinAt.fun_sum : ∀ {𝕜 : 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] {x : E}
  {s : Set E} {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) → DifferentiableWithinAt 𝕜 (fun y => ∑ i ∈ u, A i y) s x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {he : t ≠ ∅}, t.getKey! (t.maxKey he) = t.maxKey he
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.copy_dropSuffix?_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice},
  Option.map String.Slice.copy (s.copy.dropSuffix? pat) = Option.map String.Slice.copy (s.dropSuffix? pat)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.ι_evalHom_assoc : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ) {Z : CommRingCat} (h : CommRingCat.of R ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)
      (CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.evalHom IM I M R x) h) =
    CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.evalAt IM I M R x (Opposite.unop U)) h
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterMatrix.reindexGroupEquiv_symm_apply_simple : ∀ {B : Type u_1} {B' : Type u_2} (M : CoxeterMatrix B) (e : B ≃ B') (i : B),
  (M.reindexGroupEquiv e).symm (M.simple i) = (CoxeterMatrix.reindex e M).simple (e i)
-- Mathlib.LinearAlgebra.Center
/-- Over a commutative domain, an endomorphism `f` of a free module `V`
such that `f v` and `v` are collinear, for all `v : V`,
consists of homotheties.  -/
LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  [Module.Free R V] {f : V →ₗ[R] V}, (∀ (v : V), ¬LinearIndependent R ![v, f v]) → ∃ a, f = a • 1
-- Mathlib.Logic.Basic
forall_or_of_or_forall : ∀ {α : Sort u_3} {p : α → Prop} {b : Prop}, (b ∨ ∀ (x : α), p x) → ∀ (x : α), b ∨ p x
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `Nat.succ a`,
such that `norm_num` successfully recognises `a`.  -/
Mathlib.Meta.NormNum.evalNatSucc : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Order.Hom.Basic
OrderEmbedding.coe_subtype : ∀ {α : Type u_2} [inst : Preorder α] (p : α → Prop), ⇑(OrderEmbedding.subtype p) = Subtype.val
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_trunc_mul_trunc : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (f g : PowerSeries R),
  (PowerSeries.trunc n) (↑((PowerSeries.trunc n) f) * ↑((PowerSeries.trunc n) g)) = (PowerSeries.trunc n) (f * g)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.endPos_matched : ∀ {s : String.Slice} {p q : s.Pos}, (String.Slice.Pattern.SearchStep.matched p q).endPos = q
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left : ∀ {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] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  {𝒢 : CategoryTheory.Functor Dᵒᵖ A} (f : 𝒢 ⟶ ℱ) (g : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj),
  CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom (CategoryTheory.CategoryStruct.comp (G.op.whiskerLeft f) g) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom g)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.one_lt_prod' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {f : ι → M}
  {s : Finset ι} [MulLeftStrictMono M], (∀ i ∈ s, 1 ≤ f i) → (∃ i ∈ s, 1 < f i) → 1 < ∏ i ∈ s, f i
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableAt.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸},
  DifferentiableAt 𝕜 a x → DifferentiableAt 𝕜 b x → DifferentiableAt 𝕜 (a * b) x
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.State.resumeStack : Lean.Meta.SynthInstance.State → Array (Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.instVAddOfVAddCommClass.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : VAdd M X]
  [inst_1 : VAdd N Y] [inst_2 : VAdd R Y] [inst_3 : VAddCommClass N R Y],
  AddActionHom.instVAddOfVAddCommClass = { vadd := fun h f => { toFun := h +ᵥ ⇑f, map_vadd' := ⋯ } }
-- Mathlib.Topology.Separation.CompletelyRegular
completelyRegularSpace_iff : ∀ (X : Type u) [inst : TopologicalSpace X],
  CompletelyRegularSpace X ↔ ∀ (x : X) (K : Set X), IsClosed K → x ∉ K → ∃ f, Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).isEmpty = ((m.erase k).isEmpty && (f (Std.DHashMap.Const.get? m k)).isNone)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.reportMissingToIntAdapter : Lean.Expr → Lean.Expr → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.reindex_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι) (i : ι'), (s.reindex e).π i = s.π (e i)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.dirac_apply_of_mem : ∀ {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [inst_2 : MeasurableSpace β]
  {x : β} {v : M} {s : Set β}, MeasurableSet s → x ∈ s → (MeasureTheory.VectorMeasure.dirac x v) s = v
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_setOfPred : ∀ {α : Type u_1}, Measurable fun p => {a | p a}
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `L / K` is a field extension, `S` is a finite subset of `L`, such that every element of `S`
is integral (= algebraic) over `K`, then `K(S) / K` is a finite extension.
A direct corollary of `finiteDimensional_iSup_of_finite`.  -/
IntermediateField.finiteDimensional_adjoin : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {S : Set L} [Finite ↑S],
  (∀ x ∈ S, IsIntegral K x) → FiniteDimensional K ↥(IntermediateField.adjoin K S)
-- Mathlib.NumberTheory.Bernoulli
bernoulli'.eq_1 : ∀ (n : ℕ), bernoulli' n = 1 - ∑ k, ↑(n.choose ↑k) / (↑n - ↑↑k + 1) * bernoulli' ↑k
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Result.mk : Lean.Expr → Mathlib.Meta.FunProp.Result
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_finset_eq_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (s : Finset α),
  ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ s, f i
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- A dense open set `U : Opens X` of a scheme `X` over `S` is `S`-birational to `X`.  -/
AlgebraicGeometry.Scheme.Opens.birationalOver_of_dense : ∀ {X S : AlgebraicGeometry.Scheme} (U : X.Opens) (sX : X ⟶ S),
  Dense ↑U → AlgebraicGeometry.Scheme.BirationalOver (CategoryTheory.CategoryStruct.comp U.ι sX) sX
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true → (k == a) = false → Std.Internal.List.containsKey a l = true
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.MeasurePreserving.vaddInvariantMeasure_iterateAddAct : ∀ {α : Type w} {f : α → α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.MeasurePreserving f μ μ → MeasureTheory.VAddInvariantMeasure (IterateAddAct f) α μ
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.preimage_bot : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), (TopologicalSpace.Opens.map f.base).obj ⊥ = ⊥
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
WfDvdMonoid.wfDvdMonoid_associates : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α], WfDvdMonoid (Associates α)
-- Init.Data.SInt.Bitwise
instIdempotentOpInt16HAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightComp_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ R₃ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (hr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r'.app X.right)))
  (hrr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom ((CategoryTheory.CategoryStruct.comp r r').app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightComp L r r' hr hr' hrr').hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a `NormedGroup` from a `SeminormedGroup` satisfying `∀ x, ‖x‖ = 0 → x = 1`. This
avoids having to go back to the `(Pseudo)MetricSpace` level when declaring a `NormedGroup`
instance as a special case of a more general `SeminormedGroup` instance.  -/
NormedGroup.ofSeparation : {E : Type u_5} → [inst : SeminormedGroup E] → (∀ (x : E), ‖x‖ = 0 → x = 1) → NormedGroup E
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.map_inv_of_isCocycle₁ : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : MulAction G A] {f : G → A},
  groupCohomology.IsCocycle₁ f → ∀ (g : G), g • f g⁻¹ = -f g
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullback_obj_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : P.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] (A : P.Over Q Y),
  ((CategoryTheory.MorphismProperty.Over.pullback P Q f).obj A).left = CategoryTheory.Limits.pullback A.hom f
-- Std.Data.DHashMap.Raw
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DHashMap.Raw.getKey! : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → [Inhabited α] → Std.DHashMap.Raw α β → α → α