mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.instInhabited : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → [Inhabited β] → Inhabited (α →𝒄 β)
-- Mathlib.Topology.Separation.Basic
TopologicalSpace.IsTopologicalBasis.inseparable_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {b : Set (Set X)},
  TopologicalSpace.IsTopologicalBasis b → ∀ {x y : X}, Inseparable x y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.mem_normalizedFactors_iff' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {p x : α}, x ≠ 0 → (p ∈ UniqueFactorizationMonoid.normalizedFactors x ↔ Irreducible p ∧ normalize p = p ∧ p ∣ x)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
/-- The type `(shrinkYonedaGrp.obj M).obj Y` is equivalent to `Y.unop ⟶ M.X`.  -/
CategoryTheory.shrinkYonedaGrpObjObjEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        {M : CategoryTheory.Grp C} →
          {Y : Cᵒᵖ} → ↑((CategoryTheory.shrinkYonedaGrp.{w, v, u}.obj M).obj Y) ≃* (Opposite.unop Y ⟶ M.X)
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Change of variable formula for differentiable functions, set version: if a function `f` is
injective and differentiable on a null measurable set `s`, then the measure of `f '' s` is given
by the integral of `|(f' x).det|` on `s`.
Note that the null-measurability of `f '' s` is given by `nullMeasurable_image_of_fderivWithin`.  -/
MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasureTheory.NullMeasurableSet s μ →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s → ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = μ (f '' s)
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L → ∀ [Algebra.IsAlgebraic F ↥A], Module.rank L ↥(IntermediateField.adjoin L ↑A) = Module.rank F ↥A
-- Init.SimpLemmas
pi_congr : ∀ {α : Sort u} {β β' : α → Sort v}, (∀ (a : α), β a = β' a) → ((a : α) → β a) = ((a : α) → β' a)
-- Batteries.Recycling.RBTree.Alter
/-- Descend into the left subtree of a black node.  -/
RBTree.RBNode.Path.Balanced.blackL : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1} {y : RBTree.RBNode α} {c₂ : RBTree.RBColor} {n : ℕ}
  {parent : RBTree.RBNode.Path α} {v : α} {c₁ : RBTree.RBColor},
  y.Balanced c₂ n →
    RBTree.RBNode.Path.Balanced c₀ n₀ parent RBTree.RBColor.black (n + 1) →
      RBTree.RBNode.Path.Balanced c₀ n₀ (RBTree.RBNode.Path.left RBTree.RBColor.black parent v y) c₁ n
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.MarkdownM.State.mk.sizeOf_spec : ∀ (footnotes : Array (String × String)), sizeOf { footnotes := footnotes } = 1 + sizeOf footnotes
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG : ∀ (R : Type u) [inst : CommRing R], (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).Additive
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- An arbitrary choice of biproduct of a pair of objects.  -/
CategoryTheory.Limits.«term_⊞_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- A morphism `k : W ⟶ X` satisfying `k ≫ f = k ≫ g` induces a morphism
`l : W ⟶ weakEqualizer f g` satisfying `l ≫ weakEqualizer.ι f g = k`.  -/
CategoryTheory.Limits.weakEqualizer.lift' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g] →
          {W : C} →
            (k : W ⟶ X) →
              CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g →
                { l // CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.weakEqualizer.ι f g) = k }
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.Bool.cond_congr : ∀ (discr lhs rhs discr' lhs' rhs' : Bool),
  discr' = discr → lhs' = lhs → rhs' = rhs → (bif discr' then lhs' else rhs') = bif discr then lhs else rhs
-- Mathlib.Topology.DiscreteSubset
/-- The union of finitely many discrete closed subsets is discrete.  -/
IsDiscrete.biUnion : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {I : Set ι} {s : ι → Set X},
  I.Finite → (∀ i ∈ I, IsDiscrete (s i)) → (∀ i ∈ I, IsClosed (s i)) → IsDiscrete (⋃ i ∈ I, s i)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.instEnrichedCategoryTransportEnrichment : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [CategoryTheory.EnrichedCategory V C] →
          {W : Type v'} →
            [inst_3 : CategoryTheory.Category.{w', v'} W] →
              [inst_4 : CategoryTheory.MonoidalCategory W] →
                (F : CategoryTheory.Functor V W) →
                  [inst_5 : F.LaxMonoidal] → CategoryTheory.EnrichedCategory W (CategoryTheory.TransportEnrichment F C)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- Summable non-negative functions have countable support  -/
Summable.countable_support_nnreal : ∀ {α : Type u_1} (f : α → NNReal), Summable f → (Function.support f).Countable
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.SL_mulAction_ker : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_3} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  (MulAction.toPermHom (Matrix.SpecialLinearGroup ι K) (Projectivization K (ι → K))).ker =
    Subgroup.center (Matrix.SpecialLinearGroup ι K)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.instSubsingleton : ∀ {V : Type u} {G : SimpleGraph V} [Subsingleton V], Subsingleton G.ConnectedComponent
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.stRun.match_1.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_3} {k : K} (motive : Turing.TM2to1.StAct K Γ σ k → Sort u_4)
  (f : σ → Option (Γ k) → σ) (h_1 : (f : σ → Γ k) → motive (Turing.TM2to1.StAct.push f))
  (h_2 : (f : σ → Option (Γ k) → σ) → motive (Turing.TM2to1.StAct.peek f))
  (h_3 : (f : σ → Option (Γ k) → σ) → motive (Turing.TM2to1.StAct.pop f)),
  (match Turing.TM2to1.StAct.pop f with
    | Turing.TM2to1.StAct.push f => h_1 f
    | Turing.TM2to1.StAct.peek f => h_2 f
    | Turing.TM2to1.StAct.pop f => h_3 f) =
    h_3 f
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanFileProgressProcessingInfo : Lean.FromJson Lean.Lsp.LeanFileProgressProcessingInfo
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} {f g : X ⟶ Y},
  f = g ↔ f.left = g.left
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.mem_range : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {f : R →+* S} {y : S},
  y ∈ f.range ↔ ∃ x, f x = y
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.monoid.eq_1 : ∀ {α : Type u_2} [inst : Monoid α],
  Set.monoid =
    { toSemigroup := Set.semigroup, toOne := Set.mulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, toNPow := NPow.ofPow,
      npow_zero := ⋯, npow_succ := ⋯ }
-- Init.Data.String.Defs
String.Slice.offset_startPos : ∀ {s : String.Slice}, s.startPos.offset = 0
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.norm_toCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x : v.Completion), ‖x.toCompletion‖ = ‖x‖
-- Mathlib.LinearAlgebra.Dimension.Free
/-- A free module with rank 1 has a basis with one element.  -/
Module.basisUnique : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [Module.Free R M] →
            [StrongRankCondition R] → (ι : Type u_2) → [Unique ι] → Module.finrank R M = 1 → Module.Basis ι R M
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a meromorphic function `f` at a `z₀` is infinity iff `f` vanishes locally around
`z₀`.  -/
meromorphicOrderAt_eq_top_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = 0
-- Init.Data.Bool
Bool.and_self_right : ∀ (a b : Bool), (a && b && b) = (a && b)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The middle left map in the oplax associativity hexagon.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPre F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPostPre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPrePre F)
-- Lean.Meta.Tactic.Simp.Attr
Lean.Meta.getSimpTheorems : Lean.CoreM Lean.Meta.SimpTheorems
-- Init.Data.List.Lemmas
List.contains_insert : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {l : List α} {a x : α},
  (List.insert a l).contains x = (x == a || l.contains x)
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.splitAndAssumption : Lean.MVarId → Lean.Name → Lean.MetaM Unit
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.m : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Minute.Ordinal
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.neg_def : ∀ {K : Type u_1} [inst : CommRing K] (x : RatFunc K),
  x.neg =
    match x with
    | { toFractionRing := p } => { toFractionRing := -p }
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_addNatEmb_Ioi : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.map (Fin.addNatEmb m) (Finset.Ioi i) = Finset.Ioi (i.addNat m)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {f : Option β → Option β},
      (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).isEmpty =
        ((↑(m.erase k)).isEmpty && (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isNone)
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Modifies the delaborator so that it ensures resulting term is annotated using `annotateTermInfoUnlessAnnotated`.
 -/
Lean.PrettyPrinter.Delaborator.withAnnotateTermInfoUnlessAnnotated : Lean.PrettyPrinter.Delaborator.Delab → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instTop.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M],
  Submonoid.instTop = { top := { carrier := Set.univ, mul_mem' := ⋯, one_mem' := ⋯ } }
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmooth.trans : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_1)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [Algebra.IsStandardSmooth R S] [Algebra.IsStandardSmooth S T], Algebra.IsStandardSmooth R T
-- Lean.Util.Trace
Lean.instMonadTraceOfMonadLift : (m n : Type → Type) → [MonadLift m n] → [Lean.MonadTrace m] → Lean.MonadTrace n
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_union_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Ici a ∪ Set.Iio a = Set.univ
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.toList'_think : ∀ {α : Type u} (l : List α) (s : Stream'.WSeq α),
  Computation.corec
      (fun x =>
        match x with
        | (l, s) =>
          match Stream'.Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l, s.think) =
    (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Stream'.Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, s)).think
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.cons.injEq : ∀ {V : Type u} [inst : Quiver V] {a b c : V} (a_1 : Quiver.Path a b) (a_2 : b ⟶ c) (b_1 : V) (a_3 : Quiver.Path a b_1)
  (a_4 : b_1 ⟶ c), (a_1.cons a_2 = a_3.cons a_4) = (b = b_1 ∧ a_1 ≍ a_3 ∧ a_2 ≍ a_4)
-- Std.Data.HashSet.Raw
/-- Monadically computes a value by folding the given function over the elements in the hash set in some
order.
 -/
Std.HashSet.Raw.foldM : {α : Type u} → {m : Type v → Type w} → [Monad m] → {β : Type v} → (β → α → m β) → β → Std.HashSet.Raw α → m β
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.mul_zeta_apply : ∀ {f : ArithmeticFunction ℕ} {x : ℕ}, (f * ArithmeticFunction.zeta) x = ∑ i ∈ x.divisors, f i
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.Offset.add : Lean.Expr → ℕ → Lean.Meta.Sym.Offset
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Composition of refinement morphisms of pre-`1`-hypercovers.  -/
CategoryTheory.PreOneHypercover.Hom.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} → {G : CategoryTheory.PreOneHypercover S} → E.Hom F → F.Hom G → E.Hom G
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- `arcosh` is defined using a logarithm, `arcosh x = log (x + √(x ^ 2 - 1))`.  -/
Real.arcosh : ℝ → ℝ
-- Lean.Elab.MutualInductive
/-- Whether the command should allow indices (like `inductive`) or not (like `structure`).  -/
Lean.Elab.Command.InductiveView.allowIndices : Lean.Elab.Command.InductiveView → Bool
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ihom_obj_ρ_apply : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] {A : Rep.{u_1, u, v} k G} {B : Rep.{u_2, u, v} k G}
  (g : G) (x : ↑A →ₗ[k] ↑B), ((A.ihom.obj B).ρ g) x = B.ρ g ∘ₗ x ∘ₗ A.ρ g⁻¹
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- `SlashInvariantFormClass F Γ k` asserts `F` is a type of bundled functions that are invariant
under the `SlashAction`.  -/
SlashInvariantFormClass : (F : Type u_1) → outParam (Subgroup (GL (Fin 2) ℝ)) → outParam ℤ → [FunLike F UpperHalfPlane ℂ] → Prop
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instRing : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] → [inst_1 : PartialOrder S] → [inst_2 : Ring R] → (v : AbsoluteValue R S) → Ring (WithAbs v)
-- Mathlib.GroupTheory.Index
Subgroup.mul_self_mem_of_index_two : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 → ∀ (a : G), a * a ∈ H
-- Init.Data.String.Subslice
String.Slice.Subslice.startInclusive_ofSliceFrom : ∀ {s : String.Slice} {p : s.Pos} {sl : (s.sliceFrom p).Subslice},
  sl.ofSliceFrom.startInclusive = String.Slice.Pos.ofSliceFrom sl.startInclusive
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The condition that `h : A.PairingCore` is proper, i.e. for each `s : h.ι`,
the type (II) simplex `h.type₂ s` is uniquely a `1`-codimensional
face of the type (I) simplex `h.type₁ s`.  -/
SSet.Subcomplex.PairingCore.IsProper : {X : SSet} → {A : X.Subcomplex} → A.PairingCore → Prop
-- Mathlib.Logic.Function.Basic
Function.update_ne_self_iff : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a},
  Function.update f a b ≠ f ↔ b ≠ f a
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.ext_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} ⦃α β : X ≅ Y⦄, α.inv = β.inv → α = β
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.sup_normal : ∀ {G : Type u_2} [inst : Group G] (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal], (H ⊔ K).Normal
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.mk_one : ∀ {M : Type u_1} [inst : One M], DomMulAct.mk 1 = 1
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.inv_hom_id_apply : ∀ {X Y : FintypeCat} (f : X ≅ Y) (y : Y.obj),
  (CategoryTheory.ConcreteCategory.hom f.hom) ((CategoryTheory.ConcreteCategory.hom f.inv) y) = y
-- Mathlib.Data.List.Rotate
List.rotate_singleton : ∀ {α : Type u} (x : α) (n : ℕ), [x].rotate n = [x]
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instBot : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [Bot β] → Bot (l.Germ β)
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- Continuously polynomial everywhere implies continuous  -/
CPolynomialOn.continuous : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  CPolynomialOn 𝕜 f Set.univ → Continuous f
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.proj_eq_self : ∀ {I : Type u} (J : I → Prop) [inst : (i : I) → Decidable (J i)] {x : I → Bool},
  (∀ (i : I), x i ≠ false → J i) → Profinite.NobelingProof.Proj J x = x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.type : Lean.Meta.Grind.Arith.Linear.NatStruct → Lean.Expr
-- Mathlib.Data.Sym.Sym2
Sym2.lift₂_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3}
  (f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) (a₁ a₂ : α)
  (b₁ b₂ : β), Sym2.lift₂ f s(a₁, a₂) s(b₁, b₂) = ↑f a₁ a₂ b₁ b₂
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.brecOn.eq : ∀ {α : Type} {motive_1 : Lean.Meta.DiscrTree.Trie α → Sort u}
  {motive_2 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u}
  {motive_3 : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u}
  {motive_4 : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α → Sort u} (t : Lean.Meta.DiscrTree.Trie α)
  (F_1 : (t : Lean.Meta.DiscrTree.Trie α) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
      Lean.Meta.DiscrTree.Trie.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) → Lean.Meta.DiscrTree.Trie.below_2 t → motive_3 t)
  (F_4 : (t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Lean.Meta.DiscrTree.Trie.below_3 t → motive_4 t),
  t.brecOn F_1 F_2 F_3 F_4 = F_1 t (Lean.Meta.DiscrTree.Trie.brecOn.go t F_1 F_2 F_3 F_4).2
-- Batteries.Data.List.Lemmas
List.Disjoint.eq_1 : ∀ {α : Type u_1} (l₁ l₂ : List α), l₁.Disjoint l₂ = ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ → False
-- Mathlib.Order.GameAdd
Prod.gameAdd_swap_swap_mk : ∀ {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) (a₁ a₂ : α) (b₁ b₂ : β),
  Prod.GameAdd rα rβ (a₁, b₁) (a₂, b₂) ↔ Prod.GameAdd rβ rα (b₁, a₁) (b₂, a₂)
-- Mathlib.MeasureTheory.Function.EssSup
essSup_mono_measure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f : α → β},
  ν.AbsolutelyContinuous μ →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae ν) f) essSup_mono_measure._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f) essSup_mono_measure._auto_3 →
        essSup f ν ≤ essSup f μ
-- Mathlib.Algebra.CubicDiscriminant
Cubic.of_b_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R],
  P.a = 0 → P.b = 0 → P.toPoly = Polynomial.C P.c * Polynomial.X + Polynomial.C P.d
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.match_4.eq_2 : ∀ (s : String) (motive : Char → Option (s.Pos × ℕ) → Sort u_1) (x : Char) (x_1 : Option (s.Pos × ℕ))
  (h_1 : (q : s.Pos) → (v : ℕ) → x_1 = some (q, v) → motive 'u' (some (q, v)))
  (h_2 : (x : Char) → (x_2 : Option (s.Pos × ℕ)) → x_1 = x_2 → motive x x_2),
  (∀ (q : s.Pos) (v : ℕ), x = 'u' → x_1 = some (q, v) → False) →
    (match x, h₂ : x_1 with
      | 'u', some (q, v) => h_1 q v h₂
      | x, x_3 => h_2 x x_3 h₂) =
      h_2 x x_1 ⋯
-- Mathlib.Order.Completion
DedekindCut.instCompleteLinearOrder : {α : Type u_1} → [inst : LinearOrder α] → CompleteLinearOrder (DedekindCut α)
-- Mathlib.Tactic.NormNum.Result
/-- Returns the rational number that is the result of `norm_num` evaluation.  -/
Mathlib.Meta.NormNum.Result.toRat : {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«$α»)} → Mathlib.Meta.NormNum.Result e → Option ℚ
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.error.parenthesizer : String → Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.projIdx.injEq : ∀ (structName : Lean.Name) (idx : ℕ) (structName_1 : Lean.Name) (idx_1 : ℕ),
  (Lean.Elab.Term.LValResolution.projIdx structName idx = Lean.Elab.Term.LValResolution.projIdx structName_1 idx_1) =
    (structName = structName_1 ∧ idx = idx_1)
-- Mathlib.Algebra.Group.Defs
SubNegMonoid.zsmul_zero' : ∀ {G : Type u} [self : SubNegMonoid G] (a : G), 0 • a = 0
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableAt.norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {x : G}, DifferentiableAt ℝ f x → f x ≠ 0 → DifferentiableAt ℝ (fun y => ‖f y‖) x
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.sub : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} {f g : X → E},
  MeasureTheory.LocallyIntegrableOn f s μ →
    MeasureTheory.LocallyIntegrableOn g s μ → MeasureTheory.LocallyIntegrableOn (f - g) s μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : β k → β k}
  {he : (Std.DTreeMap.Internal.Impl.modify k f t).isEmpty = false},
  (Std.DTreeMap.Internal.Impl.modify k f t).maxKey he = t.maxKey ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_7 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.cpop with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_7 ()