mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.mapInvariantsOfRes_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {H : Type u_6} [inst_10 : Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R H W} (φ : H →* G)
  (f : ContIntertwiningMap (π.restrict φ) π') (v : ↥π.invariants),
  ↑((ContIntertwiningMap.mapInvariantsOfRes φ f) v) = f ↑v
-- Mathlib.Data.List.Flatten
List.Sublist.flatMap : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α},
  l₁.Sublist l₂ → ∀ (f : α → List β), (List.flatMap f l₁).Sublist (List.flatMap f l₂)
-- Mathlib.Data.PNat.Defs
PNat.natPred_eq_pred : ∀ {n : ℕ} (h : 0 < n), PNat.natPred ⟨n, h⟩ = n.pred
-- Init.Data.List.Nat.Modify
List.modify_succ_cons : ∀ {α : Type u_1} (f : α → α) (a : α) (l : List α) (i : ℕ), (a :: l).modify (i + 1) f = a :: l.modify i f
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous`.

---

A continuous and strongly adapted process is strongly progressive.  -/
MeasureTheory.StronglyAdapted.progMeasurable_of_continuous : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : TopologicalSpace ι]
  [TopologicalSpace.MetrizableSpace ι] [SecondCountableTopology ι] [inst_5 : MeasurableSpace ι] [OpensMeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.StronglyAdapted f u → (∀ (ω : Ω), Continuous fun i => u i ω) → MeasureTheory.IsStronglyProgressive f u
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Equivalent types have equivalent simple graphs.  -/
Equiv.simpleGraph : {V : Type u_1} → {W : Type u_2} → V ≃ W → SimpleGraph V ≃ SimpleGraph W
-- Mathlib.Data.Finset.Max
/-- If finsets `s` and `t` are interleaved, then `Finset.card s ≤ Finset.card t + 1`.  -/
Finset.card_le_of_interleaved : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α},
  (∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y) → s.card ≤ t.card + 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_insertEntryIfNew_le_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α} {v : β k},
        (compare (Std.Internal.List.minKey! (Std.Internal.List.insertEntryIfNew k v l))
              (Std.Internal.List.minKey! l)).isLE =
          true
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Convert a Dyck word to a binary rooted tree.

`f(0) = nil`. For a nonzero word find the `D` that matches the initial `U`,
which has index `p.firstReturn`, then let `x` be everything strictly between said `U` and `D`,
and `y` be everything strictly after said `D`. `p = x.nest + y` with `x, y` (possibly empty)
Dyck words. `f(p) = f(x) △ f(y)`, where △ (defined in `Mathlib/Data/Tree/Basic.lean`) joins two
subtrees to a new root node.  -/
DyckWord.toTree : DyckWord → BinaryTree Unit
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instNonUnitalNonAssocSemiring : {R : Type u_1} → {a b : R} → [NonUnitalNonAssocSemiring R] → NonUnitalNonAssocSemiring (QuadraticAlgebra R a b)
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Two additive isomorphisms agree if they are defined by the same underlying function.  -/
AddEquiv.ext : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f g : M ≃+ N}, (∀ (x : M), f x = g x) → f = g
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.smulc_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Zero β] [inst_3 : TopologicalSpace γ] [inst_4 : SMulZeroClass γ β] [inst_5 : ContinuousSMul γ β]
  {F : Type u_5} [inst_6 : FunLike F α γ] [inst_7 : ContinuousMapClass F α γ] (f : F)
  (g : CompactlySupportedContinuousMap α β) (x : α), (f • g) x = f x • g x
-- Lean.Meta.Tactic.Grind.Types
/-- Given applications `a` and `b`, case-split on whether the corresponding
`i`-th arguments are equal or not. The split is only performed if all other
arguments are already known to be equal or are also tagged as split candidates.
 -/
Lean.Meta.Grind.SplitInfo.arg : Lean.Expr → Lean.Expr → ℕ → Lean.Expr → Lean.Meta.Grind.SplitSource → Lean.Meta.Grind.SplitInfo
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- The constructed `pullbackConeOfLeft` is indeed limiting.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit : {X Y Z : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] →
        CategoryTheory.Limits.IsLimit (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeft f g)
-- Init.Data.List.TakeDrop
List.dropWhile.eq_def : ∀ {α : Type u} (p : α → Bool) (x : List α),
  List.dropWhile p x =
    match x with
    | [] => []
    | a :: l =>
      match p a with
      | true => List.dropWhile p l
      | false => a :: l
-- Mathlib.Analysis.Normed.Module.Extr
/-- If `f : α → E` is a function such that `norm ∘ f` has a local maximum at a point `c`, then the
function `fun x => ‖f x + f c‖` has a local maximum at `c`.  -/
IsLocalMax.norm_add_self : ∀ {X : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] [inst_2 : TopologicalSpace X]
  {f : X → E} {c : X}, IsLocalMax (norm ∘ f) c → IsLocalMax (fun x => ‖f x + f c‖) c
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.mem_submodule_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  (S : α → Submodule R M) (x : α →₀ M), x ∈ Finsupp.submodule S ↔ ∀ (i : α), x i ∈ S i
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.val_mem_of_mem_units : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x : Mˣ}, x ∈ S.units → ↑x ∈ S
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueue.instEmptyCollection : EmptyCollection Aesop.UnsafeQueue
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.mem_neLocus : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] {f g : α →₀ N}
  {a : α}, a ∈ f.neLocus g ↔ f a ≠ g a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_minKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → t.minKey?.isSome = true
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁ : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive] (n : ℤ)
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCommShiftIso n).inv.app X).hom₁ = (CategoryTheory.Functor.commShiftIso F n).inv.app X.obj₁
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.ofNatCode.eq_4 : Nat.Partrec.Code.ofNatCode 3 = Nat.Partrec.Code.right
-- Init.Data.List.MapIdx
_private.Init.Data.List.MapIdx.0.Option.getD.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (opt : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive opt
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that the region between the position `startPos` and the end of the slice
`s` matches the pattern `pat`. Note that there might be a longer match.
 -/
String.Slice.Pattern.Model.IsRevMatch : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → Prop
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) {x : R}
  {r s : S}, f r ≤ x → x ≤ f s → 0 ≤ ArchimedeanClass.mk x
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.Acyclic.truncGE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : HomologicalComplex C c'} [inst_2 : ∀ (i' : ι'), K.HasHomology i']
  [inst_3 : CategoryTheory.Limits.HasZeroObject C],
  K.Acyclic → ∀ (e : c.Embedding c') [inst_4 : e.IsTruncGE], (K.truncGE e).Acyclic
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget₂CommMon_map_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommGrp C} (f : A ⟶ B),
  ((CategoryTheory.CommGrp.forget₂CommMon C).map f).hom = f.hom.hom
-- Init.Data.UInt.Bitwise
UInt64.toUInt8_or : ∀ (a b : UInt64), (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_star : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (star a).imJ = -a.imJ
-- Mathlib.Tactic.Ring.Basic
/-- This is a routine which is used to clean up the unsolved subgoal
of a failed `ring1` application. It is overridden in `Mathlib/Tactic/Ring/RingNF.lean`
to apply the `ring_nf` simp set to the goal.
 -/
Mathlib.Tactic.Ring.ringCleanupRef : IO.Ref (Lean.Expr → Lean.MetaM Lean.Expr)
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- Given `h : v.FineSubfamilyOn f s`, then `h.index` is a set parametrizing a disjoint
covering of almost every `s`.  -/
VitaliFamily.FineSubfamilyOn.index : {X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m0 : MeasurableSpace X} →
      {μ : MeasureTheory.Measure X} →
        {v : VitaliFamily μ} → {f : X → Set (Set X)} → {s : Set X} → v.FineSubfamilyOn f s → Set (X × Set X)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.elementsFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Functor C (Type w)} (n : X ⟶ Y),
  CategoryTheory.Functor.elementsFunctor.map n = (CategoryTheory.NatTrans.mapElements n).toCatHom
-- Mathlib.Data.Int.WithZero
WithZeroMulInt.toNNReal_le_one_iff : ∀ {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : 1 < e), (WithZeroMulInt.toNNReal ⋯) m ≤ 1 ↔ m ≤ 1
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.transcendental_ringHom_iff_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : EquivLike FRS R S] [inst_7 : RingEquivClass FRS R S] [inst_8 : EquivLike FAB A B]
  [inst_9 : RingEquivClass FAB A B] (f : FRS) (g : FAB),
  (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → (Algebra.Transcendental S B ↔ Algebra.Transcendental R A)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The `p`-adic value of an integer `z ≠ 0` is its `p`-adic value as a rational.  -/
padicValRat.of_int : ∀ {p : ℕ} {z : ℤ}, padicValRat p ↑z = ↑(padicValInt p z)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.rupAdd_sound : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ) (c : β) (rupHints : Array ℕ) (f' : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints = (f', true) →
      Std.Tactic.BVDecide.LRAT.Internal.Liff α f f'
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.symm_invLHom : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (e : L ≃ᴸ L'), e.symm.invLHom = e.toLHom
-- Mathlib.Algebra.Order.Group.Lattice
CommGroup.toDistribLattice.eq_1 : ∀ (α : Type u_2) [inst : Lattice α] [inst_1 : CommGroup α] [inst_2 : MulLeftMono α],
  CommGroup.toDistribLattice α = { toLattice := inst, le_sup_inf := ⋯ }
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.ae_compProd_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} {p : β × γ → Prop},
  MeasurableSet {x | p x} →
    ((∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc) ↔ ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c))
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
max_mul_mul_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α] [MulLeftMono α] (a b c : α), max (a * b) (a * c) = a * max b c
-- Mathlib.Logic.Equiv.Defs
Equiv.forall_congr' : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β),
  (∀ (b : β), p (e.symm b) ↔ q b) → ((∀ (a : α), p a) ↔ ∀ (b : β), q b)
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.congr_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {α β : CategoryTheory.NatTrans F G}, α = β → ∀ (X : C), α.app X = β.app X
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
Fintype.linearIndependent_iffₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Fintype ι],
  LinearIndependent R v ↔ ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i
-- Mathlib.GroupTheory.Nilpotent
Group.nilpotencyClass_of_not_nilpotent : ∀ {G : Type u_1} [inst : Group G], ¬Group.IsNilpotent G → Group.nilpotencyClass G = 0
-- Init.Data.Vector.Find
Vector.finRev?_push : ∀ {α : Type} {n : ℕ} {p : α → Bool} {a : α} {xs : Vector α n},
  Vector.findRev? p (xs.push a) = (Option.guard p a).or (Vector.findRev? p xs)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.finrank_eq : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℤ (Additive (NumberField.RingOfIntegers K)ˣ) = NumberField.Units.rank K
-- Mathlib.Data.Finset.Lattice.Prod
Finset.sup_inf_sup : ∀ {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [inst : DistribLattice α] [inst_1 : OrderBot α] (s : Finset ι)
  (t : Finset κ) (f : ι → α) (g : κ → α), s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i => f i.1 ⊓ g i.2
-- Init.Data.List.Sublist
List.cons_sublist_iff : ∀ {α : Type u_1} {a : α} {l l' : List α}, (a :: l).Sublist l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l.Sublist r₂
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) (a : J) {Z : P.Over ⊤ (𝒰.X j)}
  (h : (d.cocone j).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.map ⊤ ⋯).map ((d.cocone i).ι.app a))
      (CategoryTheory.CategoryStruct.comp (d.transitionMap hij) h) =
    CategoryTheory.CategoryStruct.comp ((d.trans hij).app a)
      (CategoryTheory.CategoryStruct.comp ((d.cocone j).ι.app a) h)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.expPartialHomeomorph_target : Real.expPartialHomeomorph.target = Set.Ioi 0
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a ring inherits a ring structure  -/
Subring.toRing : {R : Type u_1} → [inst : Ring R] → (s : Subring R) → Ring ↥s
-- Mathlib.Order.BooleanAlgebra.Basic
IsCompl.compl_eq_iff : ∀ {α : Type u} {x y z : α} [inst : BooleanAlgebra α], IsCompl x y → (zᶜ = y ↔ z = x)
-- Mathlib.Algebra.Polynomial.Basic
/-- Monomials generate the additive monoid of polynomials.  -/
Polynomial.addSubmonoid_closure_setOfPred_eq_monomial : ∀ {R : Type u} [inst : Semiring R], AddSubmonoid.closure {p | ∃ n a, p = (Polynomial.monomial n) a} = ⊤
-- Init.Data.Array.Lemmas
Array.all_iff_forall : ∀ {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : ℕ},
  as.all p start stop = true ↔ ∀ (i : ℕ) (x : i < as.size), start ≤ i ∧ i < stop → p as[i] = true
-- Lean.Meta.KAbstract
/-- Abstract occurrences of `p` in `e`. We detect subterms equivalent to `p` using key-matching.
That is, only perform `isDefEq` tests when the head symbol of subterm is equivalent to head symbol of `p`.

By default, all occurrences are abstracted,
but this behavior can be controlled using the `occs` parameter.

All matches of `p` in `e` are considered for occurrences,
but for each match that is included by the `occs` parameter,
metavariables appearing in `p` (or `e`) may become instantiated,
affecting the possibility of subsequent matches.
For matches that are not included in the `occs` parameter, the metavariable context is rolled back
to prevent blocking subsequent matches which require different instantiations.
 -/
Lean.Meta.kabstract : Lean.Expr → Lean.Expr → optParam Lean.Meta.Occurrences Lean.Meta.Occurrences.all → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInType : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ) →
          AddCommGroup ((AlgebraicGeometry.structureSheafInType R M).obj.obj U)
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.LocallyOfFiniteType.isLocallyNoetherian : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f]
  [AlgebraicGeometry.IsLocallyNoetherian Y], AlgebraicGeometry.IsLocallyNoetherian X
-- Mathlib.RingTheory.HahnSeries.Summable
/-- Make an element of `orderTopSubOnePos`  -/
HahnSeries.toOrderTopSubOnePos : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : LinearOrder Γ] →
        [inst_2 : IsOrderedCancelAddMonoid Γ] →
          [inst_3 : CommRing R] → {x : HahnSeries Γ R} → 0 < (x - 1).orderTop → ↥(HahnSeries.orderTopSubOnePos Γ R)
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a base map `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is differentiable.

We give here a version of this statement within a set at a point.  -/
MDifferentiableWithinAt.clm_bundle_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_6} [inst : NontriviallyNormedField 𝕜]
  {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_10}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_12}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M} {x : M}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)}, MDiffAt[s] (T% ϕ) x → MDiffAt[s] (T% v) x → (MDiffAt[s] fun m => ⋯) x
-- Mathlib.Analysis.Normed.Group.Pointwise
infEDist_inv : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (x : E) (s : Set E), Metric.infEDist x⁻¹ s = Metric.infEDist x s⁻¹
-- Init.Data.Char.Basic
/-- One character is less than another if its code point is strictly less than the other's.
 -/
Char.lt : Char → Char → Prop
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.div_cert.eq_1 : ∀ (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.div_cert p₁ k p = (!k.beq' 0).and' ((Lean.Grind.CommRing.Poly.mulConst_k k p).beq' p₁)
-- Init.Data.UInt.Bitwise
UInt64.ofFin_shiftLeft : ∀ (a b : Fin UInt64.size), ↑b < 64 → UInt64.ofFin (a <<< b) = UInt64.ofFin a <<< UInt64.ofFin b
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.socket : {α β : Type} → Std.Http.Server.Connection.PollSources✝ α β → Option α
-- Mathlib.Data.Vector.Basic
_private.Mathlib.Data.Vector.Basic.0.List.Vector.mOfFn.match_1.eq_1 : ∀ {m : Type u_3 → Type u_2} {α : Type u_3} (motive : (x : ℕ) → (Fin x → m α) → Sort u_1) (x : Fin 0 → m α)
  (h_1 : (x : Fin 0 → m α) → motive 0 x) (h_2 : (n : ℕ) → (f : Fin (n + 1) → m α) → motive n.succ f),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, f => h_2 n f) =
    h_1 x
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The `𝟙_ V`-shaped generalized element giving the identity in a `V`-enriched category.
 -/
CategoryTheory.eId : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          (X : C) → CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] X
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.instIsDenseFunctorOppositeTypeYoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.yoneda.IsDense
-- Init.Data.Array.Basic
/-- Reference implementation for `forIn'`  -/
Array.forIn' : {α : Type u} →
  {β : Type v} → {m : Type v → Type w} → [Monad m] → (as : Array α) → β → ((a : α) → a ∈ as → β → m (ForInStep β)) → m β
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι) {Z : C}
  (h : P.X.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.p.f n) (CategoryTheory.CategoryStruct.comp (P.p.f n) h) =
    CategoryTheory.CategoryStruct.comp (P.p.f n) h
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.instDistribMulAction : {R : Type u_1} →
  {R₂ : Type u_3} →
    {S : Type u_5} →
      {M : Type u_8} →
        {M₂ : Type u_10} →
          [inst : Semiring R] →
            [inst_1 : Semiring R₂] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module R₂ M₂] →
                      {σ₁₂ : R →+* R₂} →
                        [inst_6 : Monoid S] →
                          [inst_7 : DistribMulAction S M₂] →
                            [SMulCommClass R₂ S M₂] → DistribMulAction S (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_neg_of_base_lt_one : ∀ {b x : ℝ}, 0 < b → b < 1 → 1 < x → Real.logb b x < 0