mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableOn.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₁} {s : Set M}, MDiff[s] g → MDiff[s] f → MDiff[s] fun x => g x ∘SL f x
-- Mathlib.RingTheory.Ideal.Colon
/-- **Alias** of `Submodule.colon_univ`. -/
Submodule.colon_top : ∀ {R : Type u_1} [inst : Semiring R] {I : Ideal R} [I.IsTwoSided], Submodule.colon I Set.univ = I
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.neg_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 → W.neg P = P 2 • ![P 0 / P 2, W.toAffine.negY (P 0 / P 2) (P 1 / P 2), 1]
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∩ t₂).getKey! k = default
-- Mathlib.GroupTheory.Nilpotent
Group.IsNilpotent.isVirtuallyNilpotent : ∀ {G : Type u_1} [inst : Group G], Group.IsNilpotent G → Group.IsVirtuallyNilpotent G
-- Mathlib.CategoryTheory.GlueData
/-- For each `i j : J`, a monomorphism `f i j : V i j ⟶ U i`  -/
CategoryTheory.GlueData.f : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (self : CategoryTheory.GlueData C) → (i j : self.J) → self.V (i, j) ⟶ self.U i
-- Mathlib.Data.Finset.DenselyOrdered
Set.Finite.exists_between : ∀ {α : Type u_1} [inst : LinearOrder α] [DenselyOrdered α] {s t : Set α},
  s.Finite → s.Nonempty → t.Finite → t.Nonempty → (∀ x ∈ s, ∀ y ∈ t, x < y) → ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
-- Mathlib.Data.Set.Disjoint
Disjoint.inter_right : ∀ {α : Type u_1} {s t : Set α} (u : Set α), Disjoint s t → Disjoint s (t ∩ u)
-- Init.Data.Vector.Monadic
Vector.forM_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_4} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  {g : α → β} {f : β → m PUnit.{u_1 + 1}}, forM (Vector.map g xs) f = forM xs fun a => f (g a)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.guard.sizeOf_spec : ∀ (origin : Lean.Meta.Grind.Origin), sizeOf (Lean.Meta.Grind.SplitSource.guard origin) = 1 + sizeOf origin
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.isCondKernelCDF_condCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ],
  ProbabilityTheory.IsCondKernelCDF (fun p => ProbabilityTheory.condCDF ρ p.2) (ProbabilityTheory.Kernel.const Unit ρ)
    (ProbabilityTheory.Kernel.const Unit ρ.fst)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_atTop_sumTransform_le : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  ∃ c > 0,
    ∀ᶠ (n : ℕ) in Filter.atTop,
      ∀ (i : α), AkraBazziRecurrence.sumTransform (AkraBazziRecurrence.p a b) g (r i n) n ≤ c * g ↑n
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalExprOccurrences.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.Occurrences
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.nontrivial : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) [IsDomain R], f.degree ≠ 0 → Nontrivial (AdjoinRoot f)
-- Mathlib.Analysis.SpecificLimits.FloorPow
/-- If a monotone sequence `u` is such that `u ⌊c^n⌋₊ / ⌊c^n⌋₊` converges to a limit `l` for all
`c > 1`, then `u n / n` tends to `l`. It is even enough to have the assumption for a sequence of
`c`s converging to `1`.  -/
tendsto_div_of_monotone_of_tendsto_div_floor_pow : ∀ (u : ℕ → ℝ) (l : ℝ),
  Monotone u →
    ∀ (c : ℕ → ℝ),
      (∀ (k : ℕ), 1 < c k) →
        Filter.Tendsto c Filter.atTop (nhds 1) →
          (∀ (k : ℕ), Filter.Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) Filter.atTop (nhds l)) →
            Filter.Tendsto (fun n => u n / ↑n) Filter.atTop (nhds l)
-- Mathlib.Algebra.Group.Defs
isRightCancelAdd_iff : ∀ (G : Type u) [inst : Add G], IsRightCancelAdd G ↔ ∀ (a : G), IsAddRightRegular a
-- Mathlib.Algebra.Polynomial.RuleOfSigns
_private.Mathlib.Algebra.Polynomial.RuleOfSigns.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.le_of_opNorm_le_of_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  {x : E} {a b : ℝ}, ‖f‖ ≤ a → ‖x‖ ≤ b → ‖f x‖ ≤ a * b
-- Mathlib.Order.Basic
Pi.instSDiff : {ι : Type u_1} → {π : ι → Type u_4} → [(i : ι) → SDiff (π i)] → SDiff ((i : ι) → π i)
-- Mathlib.Topology.Constructions
/-- **Alias** of `IsClosedMap.domRestrict`. -/
IsClosedMap.restrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsClosedMap f → ∀ {s : Set X}, IsClosed s → IsClosedMap (s.domRestrict f)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The `MulHom` from a subsemigroup to its image.
See `MulEquiv.subsemigroupMap` for a variant for `MulEquiv`s.  -/
MulHom.subsemigroupMap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] → [inst_1 : Mul N] → (f : M →ₙ* N) → (M' : Subsemigroup M) → ↥M' →ₙ* ↥(Subsemigroup.map f M')
-- Init.SimpLemmas
ite_true : ∀ {α : Sort u_1} (a b : α), (if True then a else b) = a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} (not_mem : k ∉ t₂)
  {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₁.get k ⋯
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Ioc_eq_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Iic a ∪ Set.Ioc a b = Set.Iic b
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.toDual_eq_bot : ∀ (α : Type u) [inst : Top α] {a : α}, OrderDual.toDual a = ⊥ ↔ a = ⊤
-- Mathlib.Topology.Order.OrderClosed
disjoint_nhds_atTop_iff : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {a : α},
  Disjoint (nhds a) Filter.atTop ↔ ¬IsTop a
-- Aesop.Search.RuleSelection
Aesop.selectUnsafeRules : {Q : Type} → [inst : Aesop.Queue Q] → Array Aesop.PostponedSafeRule → Aesop.GoalRef → Aesop.SearchM Q Aesop.UnsafeQueue
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.instIsSplitMonoI : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y),
  CategoryTheory.IsSplitMono h.i
-- Mathlib.CategoryTheory.GradedObject
/-- The canonical inclusion `X i ⟶ X.mapObj p j` when `p i = j`, the zero morphism otherwise.  -/
CategoryTheory.GradedObject.ιMapObjOrZero : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        (X : CategoryTheory.GradedObject I C) →
          (p : I → J) →
            [inst_1 : X.HasMap p] →
              [CategoryTheory.Limits.HasZeroMorphisms C] → [DecidableEq J] → (i : I) → (j : J) → X i ⟶ X.mapObj p j
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.C.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonAssocSemiring R],
  HahnSeries.C = { toFun := ⇑(HahnSeries.single 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Data.Finset.Card
/-- `s.card` is the number of elements of `s`, aka its cardinality.

The notation `#s` can be accessed in the `Finset` locale.  -/
Finset.card : {α : Type u_1} → Finset α → ℕ
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Relations.directSum_G : ∀ {A : Type u} [inst : Ring A] {ι : Type w} (relations : ι → Module.Relations A),
  (Module.Relations.directSum relations).G = ((i : ι) × (relations i).G)
-- Mathlib.RingTheory.Localization.Away.Basic
Localization.awayMap_injective_of_dvd : ∀ {S : Type u_2} [inst : CommSemiring S] {R : Type u_4} [inst_1 : CommRing R] (f : R →+* S) {a b : R},
  a ∣ b → Function.Injective ⇑(Localization.awayMap f a) → Function.Injective ⇑(Localization.awayMap f b)
-- Init.Data.Repr
Prod.repr : {α : Type u_1} → {β : Type u_2} → [Repr α] → [ReprTuple β] → α × β → ℕ → Std.Format
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instVAdd.eq_1 : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → VAdd R (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)],
  DirectLimit.instVAdd = { vadd := fun r => DirectLimit.map f f (fun x x_1 => r +ᵥ x_1) ⋯ }
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The forgetful map from `NonUnitalSubalgebra` to `NonUnitalSubsemiring` as an
`OrderEmbedding`  -/
NonUnitalSubalgebra.toNonUnitalSubsemiring' : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → NonUnitalSubalgebra R A ↪o NonUnitalSubsemiring A
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instMonoid : Monoid ℕ
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.isoInv_pullback_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (Z : CategoryTheory.Over Y),
  ((CategoryTheory.ChosenPullbacksAlong.pullback f.inv).obj Z).hom = CategoryTheory.CategoryStruct.comp Z.hom f.hom
-- Mathlib.ModelTheory.Substructures
/-- The restriction of a first-order embedding to a substructure `s ⊆ M` gives an embedding `s → N`.
 -/
FirstOrder.Language.Embedding.domRestrict : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Embedding M N → (p : L.Substructure M) → L.Embedding (↥p) N
-- Lean.Util.FindExpr
Lean.Expr.findExtImpl? : (Lean.Expr → Lean.Expr.FindStep) → Lean.Expr → Option Lean.Expr
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.indicator : ∀ {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {l : Filter ι} {F : Type u_5}
  [inst : PseudoEMetricSpace F] [inst_1 : Zero F] {f : ι → α → F} {g : α → F},
  MeasureTheory.TendstoInMeasure μ f l g →
    ∀ (s : Set α), MeasureTheory.TendstoInMeasure μ (fun i => s.indicator (f i)) l (s.indicator g)
-- Mathlib.Topology.UnitInterval
/-- The coercion from `I` to `ℝ≥0`.  -/
unitInterval.toNNReal : ↑unitInterval → NNReal
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instBEqDatabase : BEq Mathlib.CrossRef.Database
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal],
  F.mapMon =
    { obj := fun A => { X := F.obj A.X, mon := CategoryTheory.Functor.monObjObj A.X },
      map := fun {X Y} f => { hom := F.map f.hom, isMonHom_hom := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The identity sequence is an EDS.  -/
IsEllipticDvdSequence.id : IsEllipticDvdSequence id
-- Mathlib.Tactic.Polynomial.Core
_private.Mathlib.Tactic.Polynomial.Core.0.Mathlib.Tactic.Polynomial.mkPolynomialExt.unsafe_impl_2 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Tactic.Polynomial.PolynomialExt
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mrange_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange (AddMonoidHom.snd M N) = ⊤
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- The natural equivalence between continuous linear maps from `M` to `N`
and continuous 1-multilinear alternating maps from `M` to `N`.  -/
ContinuousAlternatingMap.ofSubsingleton : (R : Type u_1) →
  (M : Type u_2) →
    (N : Type u_4) →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] → [Subsingleton ι] → ι → (M →L[R] N) ≃ M [⋀^ι]→L[R] N
-- Mathlib.Combinatorics.Additive.Dissociation
mulDissociated_empty : ∀ {α : Type u_1} [inst : CommGroup α], MulDissociated ∅
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_eq_false_of_assemble₃_eq_some_right : ∀ {w x y : UInt8} {c : Char},
  ByteArray.utf8DecodeChar?.assemble₃ w x y = some c → ByteArray.utf8DecodeChar?.isInvalidContinuationByte y = false
-- Lean.ReducibilityAttrs
Lean.reducibilityExtraExt : Lean.SimpleScopedEnvExtension (Lean.Name × Lean.ReducibilityStatus) (Lean.SMap Lean.Name Lean.ReducibilityStatus)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.reuse.injEq : ∀ (x : Lean.IR.VarId) (i : Lean.IR.CtorInfo) (updtHeader : Bool) (ys : Array Lean.IR.Arg) (x_1 : Lean.IR.VarId)
  (i_1 : Lean.IR.CtorInfo) (updtHeader_1 : Bool) (ys_1 : Array Lean.IR.Arg),
  (Lean.IR.Expr.reuse x i updtHeader ys = Lean.IR.Expr.reuse x_1 i_1 updtHeader_1 ys_1) =
    (x = x_1 ∧ i = i_1 ∧ updtHeader = updtHeader_1 ∧ ys = ys_1)
-- Qq.Macro
Qq.Impl.MVarSynth.type : Lean.MVarId → Qq.Impl.MVarSynth
-- Init.Sym.Lemmas
Lean.Sym.UInt16.le_eq_false : ∀ (a b : UInt16), decide (a ≤ b) = false → (a ≤ b) = False
-- Aesop.Saturate
Aesop.saturateCore : Aesop.LocalRuleSet → Lean.MVarId → Aesop.SaturateM Lean.MVarId
-- Mathlib.Analysis.Complex.Exponential
Complex.ofReal_exp_ofReal_re : ∀ (x : ℝ), ↑(Complex.exp ↑x).re = Complex.exp ↑x
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.angle_le_angle_add_angle_aux : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  ‖x‖ = 1 →
    ‖y‖ = 1 →
      x =
        Real.cos (InnerProductGeometry.angle x y) • y +
          Real.sin (InnerProductGeometry.angle x y) • NormedSpace.normalize (InnerProductGeometry.ortho✝ y x)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.snd_op_opIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd.op (CategoryTheory.Limits.biprod.opIso P Q).hom =
    CategoryTheory.Limits.biprod.inr
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- When given a basis, `gramSchmidt` produces a basis.  -/
InnerProductSpace.gramSchmidtBasis : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_3} →
            [inst_3 : LinearOrder ι] →
              [LocallyFiniteOrderBot ι] → [WellFoundedLT ι] → Module.Basis ι 𝕜 E → Module.Basis ι 𝕜 E
-- Mathlib.Order.Hom.Basic
OrderHom.mono : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), Monotone ⇑f
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.cons_mk : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (a : Γ) (l : List Γ),
  Turing.ListBlank.cons a (Turing.ListBlank.mk l) = Turing.ListBlank.mk (a :: l)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_4.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) (x_1 : Lean.Grind.CommRing.Var),
  x = Lean.Grind.CommRing.Expr.var x_1 →
    (match x with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | a.add b => h_3 a b
      | a.mul b => h_4 a b
      | a.pow k => h_5 a k
      | Lean.Grind.CommRing.Expr.natCast n => h_6 n
      | a.sub b => h_7 a b
      | a.neg => h_8 a
      | Lean.Grind.CommRing.Expr.intCast k => h_9 k) ≍
      h_2 x_1
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.instOfIsSepClosedOfEssFiniteTypeOfFormallyEtale : ∀ {k : Type u_1} {R : Type u_2} [inst : Field k] [inst_1 : CommRing R] [inst_2 : Algebra k R] [IsSepClosed k]
  [Algebra.EssFiniteType k R] [Algebra.FormallyEtale k R], Algebra.IsFiniteSplit k R
-- Mathlib.Order.Interval.Finset.Defs
/-- `x ∈ finsetIoi a ↔ a < x`  -/
LocallyFiniteOrderTop.finset_mem_Ioi : ∀ {α : Type u_1} {inst : Preorder α} [self : LocallyFiniteOrderTop α] (a x : α),
  x ∈ LocallyFiniteOrderTop.finsetIoi a ↔ a < x
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
/-- We say that two formal morphisms in the free monoidal category are equivalent if they become
equal if we apply the relations that are true in a monoidal category. Note that we will prove
that there is only one equivalence class -- this is the monoidal coherence theorem.  -/
CategoryTheory.FreeMonoidalCategory.setoidHom : {C : Type u} → (X Y : CategoryTheory.FreeMonoidalCategory C) → Setoid (X.Hom Y)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Auxiliary construction for `CliffordAlgebra.contractLeft`  -/
CliffordAlgebra.contractLeftAux : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) →
            Module.Dual R M → M →ₗ[R] CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedCosZeta_residue_zero : ∀ (a : UnitAddCircle), Filter.Tendsto (fun s => s * HurwitzZeta.completedCosZeta a s) (nhdsWithin 0 {0}ᶜ) (nhds (-1))
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_div : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedAddCommGroupWithTop Γ₀]
  (v : AddValuation K Γ₀) {x y : K}, v (x / y) = v x - v y
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g * f` is
circle integrable.
 -/
CircleIntegrable.continuousOn_mul : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [inst : NormedRing 𝕜] {f g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (g * f) c R
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.mclosure_preimage_le : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (s : Set N),
  Subsemigroup.closure (⇑f ⁻¹' s) ≤ Subsemigroup.comap f (Subsemigroup.closure s)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.module' : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (S : IntermediateField K L) →
            {R : Type u_4} →
              [inst_3 : Semiring R] → [inst_4 : SMul R K] → [inst_5 : Module R L] → [IsScalarTower R K L] → Module R ↥S
-- Mathlib.Topology.Connected.PathComponentOne
/-- The path component of the identity in a locally path connected additive topological group,
as an open normal additive subgroup. It is, in fact, clopen.  -/
OpenNormalAddSubgroup.pathComponentZero : (G : Type u_1) →
  [inst : TopologicalSpace G] →
    [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → [LocallyPathConnectedSpace G] → OpenNormalAddSubgroup G
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_pi_congr_lift : ∀ {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.lift.{w', w} (Cardinal.mk (f i)) = Cardinal.lift.{w, w'} (Cardinal.mk (g (e i)))) →
    Cardinal.lift.{max v' w', max v w} (Cardinal.mk ((i : ι) → f i)) =
      Cardinal.lift.{max v w, max v' w'} (Cardinal.mk ((i : ι') → g i))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l → (Std.DTreeMap.ofList l cmp).size = l.length
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isOpen_setOfPred_disjoint : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], IsOpen {p | Disjoint p.1 p.2}
-- Init.Data.SInt.Lemmas
ISize.toInt_le : ∀ (x : ISize), x.toInt ≤ ISize.maxValue.toInt
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_inv_whiskerRight_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) g ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv h)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, List.find? (fun x_2 => x_2.fst == k) m.toList = none ↔ k ∉ m
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.restrictPreimage_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty),
  (e.restrictPreimage hs).baseSet = Subtype.val ⁻¹' e.toPretrivialization.baseSet