mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.Bounded
TopHom.dual_symm_apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : OrderTop α] [inst_2 : LE β] [inst_3 : OrderTop β]
  (f : BotHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ), (TopHom.dual.symm f) a = f a
-- Init.Data.Vector.Basic
Vector.instNonemptyOfNatNat : ∀ {α : Type u_1}, Nonempty (Vector α 0)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
/-- The relation between the values of the quadratic character of one field `F` at the
cardinality of another field `F'` and of the quadratic character of `F'` at the cardinality
of `F`.  -/
quadraticChar_card_card : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 →
    ∀ {F' : Type u_2} [inst_3 : Field F'] [inst_4 : Fintype F'] [inst_5 : DecidableEq F'],
      ringChar F' ≠ 2 →
        ringChar F' ≠ ringChar F →
          (quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_refl_to_affineMap : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁], ↑(AffineEquiv.refl k P₁) = AffineMap.id k P₁
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_inv_hom_isIso_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) [inst_2 : CategoryTheory.IsIso η]
  {Z : F.obj a ⟶ F.obj b} (h : F.map g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) (CategoryTheory.CategoryStruct.comp (F.map₂ η) h) =
    h
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toComon_obj_comon_counit : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.Comon (CategoryTheory.Mon C)),
  CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit.hom
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_right_eq_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.deriv_arcsin_aux : ∀ {x : ℝ}, x ≠ -1 → x ≠ 1 → HasStrictDerivAt Real.arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ Real.arcsin x
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instCompleteLinearOrder : {α : Type u_1} → [inst : LinearOrder α] → CompleteLinearOrder (LowerSet α)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.revSkipWhile_prop_eq_self_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos},
  pos.revSkipWhile P = pos ↔ ∀ (h : pos ≠ s.startPos), ¬P ((pos.prev h).get ⋯)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) {Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CartesianMonoidalCategory.lift g h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z W).inv h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CartesianMonoidalCategory.lift f g) h) h_1
-- Init.Data.String.Basic
String.Slice.Pos.next.eq_1 : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.endPos),
  pos.next h = { offset := pos.offset.increaseBy ((pos.byte h).utf8ByteSize ⋯), isValidForSlice := ⋯ }
-- Mathlib.Algebra.Order.Group.Indicator
Function.mulSupport_max : ∀ {α : Type u_2} {M : Type u_3} [inst : One M] [inst_1 : LinearOrder M] (f g : α → M),
  (Function.mulSupport fun x => max (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
-- Mathlib.Order.LatticeIntervals
Set.Icc.codisjoint_iff : ∀ {α : Type u_1} {a b : α} [inst : SemilatticeSup α] [inst_1 : Fact (a ≤ b)] {x y : ↑(Set.Icc a b)},
  Codisjoint x y ↔ ↑x ⊔ ↑y = b
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.fieldNotation.generalized : Lean.Option Bool
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ),
  Int.fract ↑n = 0
-- Mathlib.Data.Nat.Pairing
Nat.pair_eq_of_unpair_eq : ∀ {n a b : ℕ}, Nat.unpair n = (a, b) → Nat.pair a b = n
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.subsingleton_coe_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] [Subsingleton G] (f : G →+ N),
  (↑f.range).Subsingleton
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- A continuous function on `ℝ` is `IntervalIntegrable` with respect to any locally finite measure
`ν` on ℝ.  -/
Continuous.intervalIntegrable : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  {u : ℝ → E}, Continuous u → ∀ (a b : ℝ), IntervalIntegrable u μ a b
-- Lean.Data.Lsp.Basic
/-- Notification to signal the start of progress reporting.  -/
Lean.Lsp.WorkDoneProgressBegin : Type
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.coprod_toFun : ∀ {A : Type u_2} {B : Type u_3} {E : Type u_6} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [inst_4 : CommMonoid E] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousMul E]
  (f : A →ₜ* E) (g : B →ₜ* E) (x : A × B), (f.coprod g) x = f x.1 * g x.2
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.mk.sizeOf_spec : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} [inst_1 : SizeOf J]
  (pt : Type w₁) (ι : (j : J) → F.obj j → pt)
  (ι_naturality :
    autoParam (∀ {j j' : J} (f : j ⟶ j'), ι j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = ι j)
      CategoryTheory.Functor.CoconeTypes.ι_naturality._autoParam),
  sizeOf { pt := pt, ι := ι, ι_naturality := ι_naturality } = 1 + sizeOf pt
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toContinuousLinearEquiv_one : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E], ↑1 = 1
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_eq_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : LawfulBEq α] [inst_1 : Inhabited α]
  {k : α}, k ∈ m → m.get! k = k
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_one : ∀ {R : Type u_1} [inst : Semiring R], ↑1 = 1
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.k_mul_k : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃), q.k * q.k = -((c₁ * c₃) • 1)
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_inter_self : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω},
  MeasurableSet s → ∀ (t : Set Ω) (μ : MeasureTheory.Measure Ω), μ[s ∩ t | s] = μ[t | s]
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.mk : {α : Type u} →
  {cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw._auto_1} → Std.TreeMap.Raw α Unit cmp → Std.TreeSet.Raw α cmp
-- Lean.Parser.Command
Lean.Parser.Command.derivingClasses : Lean.Parser.Parser
-- Mathlib.Tactic.DSimpPercent
/-- `dsimp% […] t` runs `dsimp […]` on term `t`.
If `t` is a proof, then it runs `dsimp […]` on the type of `t` instead.

For instance, instead of
```
have foo := ...
dsimp at foo
rw [foo]
```
one can write `rw [dsimp% foo]`.
 -/
Mathlib.Tactic.dsimpPercentElaborator : Lean.Elab.Term.TermElab
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
ZMod.χ₄_apply : ∀ (a : ZMod 4),
  ZMod.χ₄ a =
    match a with
    | 0 => 0
    | 2 => 0
    | 1 => 1
    | 3 => -1
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.index_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D)
  (I : S.shape.R), (S.index P).right I = P.obj (Opposite.op I.r.Z)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instSliceableImplRooSlice : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.Roo.Sliceable (Std.DTreeMap.Internal.Impl α β) α (Std.DTreeMap.Internal.RooSlice α β)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.IterM.step_flatMapAfterM.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (h : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.IterM m β) →
      (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => h_1 it₁' b h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_valEmbedding_Ico : ∀ {n : ℕ} (a b : Fin n), Finset.map Fin.valEmbedding (Finset.Ico a b) = Finset.Ico ↑a ↑b
-- Mathlib.Analysis.Convex.Caratheodory
/-- Given a point `x` in the convex hull of a set `s`, this is a finite subset of `s` of minimum
cardinality, whose convex hull contains `x`.  -/
Caratheodory.minCardFinsetOfMemConvexHull : {𝕜 : Type u_1} →
  {E : Type u} →
    [inst : Field 𝕜] →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] →
          [inst_3 : AddCommGroup E] → [inst_4 : Module 𝕜 E] → {s : Set E} → {x : E} → x ∈ (convexHull 𝕜) s → Finset E
-- Init.Data.Vector.MapIdx
Vector.mapIdx_mapIdx : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {f : ℕ → α → β} {g : ℕ → β → γ},
  Vector.mapIdx g (Vector.mapIdx f xs) = Vector.mapIdx (fun i => g i ∘ f i) xs
-- Mathlib.Control.Functor.Multivariate
/-- adapt `MvFunctor.LiftR` to accept relations as arrows  -/
MvFunctor.LiftR' : {n : ℕ} →
  {α : TypeVec.{u} n} →
    {F : TypeVec.{u} n → Type v} → [MvFunctor F] → (α.prod α).Arrow (TypeVec.repeat n Prop) → F α → F α → Prop
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_modEq_x2n_sub : ∀ {a : ℕ} (a1 : 1 < a) {n j : ℕ}, j ≤ 2 * n → Pell.xn a1 (2 * n - j) + Pell.xn a1 j ≡ 0 [MOD Pell.xn a1 n]
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
mulEquivOfPrimeCardEq.eq_1 : ∀ {G : Type u_2} {G' : Type u_3} {p : ℕ} [inst : Group G] [inst_1 : Group G'] [inst_2 : Fact (Nat.Prime p)]
  (hG : Nat.card G = p) (hH : Nat.card G' = p), mulEquivOfPrimeCardEq hG hH = mulEquivOfCyclicCardEq ⋯
-- Mathlib.CategoryTheory.Limits.Final
/-- If `Over j ⥤ J` is final, restricting a colimit cocone to the diagram below `j`,
preserves the limit.  -/
CategoryTheory.Limits.IsColimit.underPost : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {D : CategoryTheory.Functor J C} →
          {c : CategoryTheory.Limits.Cocone D} →
            CategoryTheory.Limits.IsColimit c →
              (j : J) → [(CategoryTheory.Under.forget j).Final] → CategoryTheory.Limits.IsColimit (c.underPost j)
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
/-- The discrete uniformity induces the discrete topology.  -/
DiscreteUniformity.instDiscreteTopology : ∀ (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X], DiscreteTopology X
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.Ordering.swap.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → motive x
-- Mathlib.Algebra.Group.Subgroup.Finsupp
AddSubgroup.mem_closure_iff_of_fintype : ∀ {M : Type u_1} [inst : AddCommGroup M] {x : M} {s : Set M} [inst_1 : Fintype ↑s],
  x ∈ AddSubgroup.closure s ↔ ∃ a, x = ∑ i, a i • ↑i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insert_ne_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.insert k v ≠ ∅
-- Mathlib.LinearAlgebra.Complex.Module
star_mul_self_add_self_mul_star : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [inst_1 : StarRing A] [inst_2 : Module ℂ A] [IsScalarTower ℂ A A]
  [SMulCommClass ℂ A A] [inst_5 : StarModule ℂ A] (a : A),
  star a * a + a * star a = 2 • (↑(realPart a) * ↑(realPart a) + ↑(imaginaryPart a) * ↑(imaginaryPart a))
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.apply_self_mul_coroot_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hx : B.IsReflective x) {y : M},
  (B x) x * (LinearMap.IsReflective.coroot B hx) y = 2 * (B x) y
-- Init.Data.Range.Polymorphic.Basic
Std.Rio.mem_iff : ∀ {α : Type u} {r : Std.Rio α} {a : α} [inst : LT α], a ∈ r ↔ a < r.upper
-- Mathlib.GroupTheory.Index
/-- Relative version of `AddSubgroup.index_eq_two_iff'`.  -/
AddSubgroup.relIindex_eq_two_iff' : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.relIndex K = 2 ↔ ∃ a ∈ K, ∀ b ∈ K, Xor (a + b ∈ H) (b ∈ H)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.divisionCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : DivisionCommMonoid α],
  Set.divisionCommMonoid = { toDivisionMonoid := Set.divisionMonoid, mul_comm := ⋯ }
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert!_snd_eq_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α)
  (b : β a), (Std.DTreeMap.Internal.Impl.containsThenInsert! a b t).2 = Std.DTreeMap.Internal.Impl.insertₘ a b t htb
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A fork `t` on the parallel pair `f g : X ⟶ Y` consists of two morphisms
`t.π.app zero : t.pt ⟶ X` and `t.π.app one : t.pt ⟶ Y`. Of these,
only the first one is interesting, and we give it the shorter name `Fork.ι t`.  -/
CategoryTheory.Limits.Fork.ι : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] → {f g : X ⟶ Y} → (t : CategoryTheory.Limits.Fork f g) → t.pt ⟶ X
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getKey?_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α},
  Std.DHashMap.Internal.AssocList.getKey? a l = Std.Internal.List.getKey? a l.toList
-- Mathlib.Topology.MetricSpace.Lipschitz
LocallyLipschitz.max_const : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : α → ℝ},
  LocallyLipschitz f → ∀ (a : ℝ), LocallyLipschitz fun x => max (f x) a
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
/-- The norm of `jacobiTheta τ - 1` decays exponentially as `im τ → ∞`.  -/
isBigO_at_im_infty_jacobiTheta_sub_one : (fun τ => jacobiTheta τ - 1) =O[Filter.comap Complex.im Filter.atTop] fun τ => Real.exp (-Real.pi * τ.im)
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_eq_iff_real : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, (starRingEnd K) z = z ↔ ∃ r, z = ↑r
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.div_lt_const_weak : ∀ {α : Type u_1} {b c : α} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α],
  b < c → ∀ {a : α}, 0 ≤ a → b / a ≤ c / a
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.mul_assoc : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : NonUnitalSemiring B] [inst_6 : Module R B]
  [inst_7 : SMulCommClass R B B] [inst_8 : IsScalarTower R B B] (x y z : TensorProduct R A B),
  (Algebra.TensorProduct.mul ((Algebra.TensorProduct.mul x) y)) z =
    (Algebra.TensorProduct.mul x) ((Algebra.TensorProduct.mul y) z)
-- Lean.Meta.Tactic.Backtrack
/-- An arbitrary procedure which can be used to modify the list of goals
before each attempt to generate alternatives.
Called as `proc goals curr`, where `goals` are the original goals for `backtracking`,
and `curr` are the current goals.
Returning `some l` will replace the current goals with `l` and recurse
(consuming one step of maximum depth).
Returning `none` will proceed to generating alternative without changing goals.
Failure will cause backtracking.
(defaults to `none`)  -/
Lean.Meta.Tactic.Backtrack.BacktrackConfig.proc : Lean.Meta.Tactic.Backtrack.BacktrackConfig →
  List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.IterM.step_take.match_1.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.abs_density_star_sub_density_le_eps : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α},
  100 ≤ 4 ^ P.parts.card * ε ^ 5 →
    ε ≤ 1 →
      ∀ {hU : U ∈ P.parts} {hV : V ∈ P.parts},
        U ≠ V →
          ¬G.IsUniform ε U V →
            |↑(G.edgeDensity ((SzemerediRegularity.star hP G ε hU V).biUnion id)
                      ((SzemerediRegularity.star hP G ε hV U).biUnion id)) -
                  ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))| ≤
              ε / 5
-- Mathlib.Algebra.Order.Hom.Basic
GroupSeminormClass.toMulLEAddHomClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Group α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : GroupSeminormClass F α β], MulLEAddHomClass F α β
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.toList_roo : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Roo.Sliceable.mkSlice t lowerBound<...upperBound) =
        List.filter (fun e => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLT = true))
          t.toList
-- Std.Http.Data.Extensions
/-- Inserts a value into the extensions, keyed by its type name. If a value of the same type already
exists, it is replaced.
 -/
Std.Http.Extensions.insert : {α : Type u_1} → Std.Http.Extensions → [TypeName α] → α → Std.Http.Extensions
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.opOp_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.opOp C).obj X = Opposite.op (Opposite.op X)
-- Mathlib.Data.List.Basic
/-- `eq_nil_or_concat` in simp normal form  -/
List.eq_nil_or_concat' : ∀ {α : Type u} (l : List α), l = [] ∨ ∃ L b, l = L ++ [b]
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- the category of additive functors is denoted `C ⥤+ D`  -/
CategoryTheory.«term_⥤+_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.mem_centralizer_iff_addCommutator_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] {g : G} {s : Set G}, g ∈ AddSubgroup.centralizer s ↔ ∀ h ∈ s, ⁅h, g⁆ = 0
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.instDecidableRelAdjAddCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet.eq_1 : ∀ {M : Type u_1} (s : Set M) [inst : Add M] [inst_1 : Fintype M] [inst_2 : DecidableEq M]
  [inst_3 : DecidablePred fun x => x ∈ s] (u v : M),
  SimpleGraph.instDecidableRelAdjAddCayleyOfFintypeOfDecidableEqOfDecidablePredMemSet s u v =
    decidable_of_iff (u ≠ v ∧ ∃ g ∈ s, u + g = v ∨ u = v + g) ⋯
-- Mathlib.Geometry.Manifold.DerivationBundle
fdifferential_apply : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ↑⊤) {x : M}
  (v : PointDerivation I x) (g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 ↑⊤),
  ((fdifferential f x) v) g = v (g.comp f)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.shiftRight.injEq : ∀ {m n : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr m) (rhs : Std.Tactic.BVDecide.BVExpr n) (n_1 : ℕ)
  (lhs_1 : Std.Tactic.BVDecide.BVExpr m) (rhs_1 : Std.Tactic.BVDecide.BVExpr n_1),
  (lhs.shiftRight rhs = lhs_1.shiftRight rhs_1) = (n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1)
-- Mathlib.Tactic.MoveAdd
/-- `prepareOp sum` takes an `Expr`ession as input.  It assumes that `sum` is a well-formed
term representing a repeated application of a binary operation and that the summands are the
last two arguments passed to the operation.
It returns the expression consisting of the operation with all its arguments already applied,
except for the last two.
This is similar to `Lean.Meta.mkAdd, Lean.Meta.mkMul`, except that the resulting operation is
primed to work with operands of the same type as the ones already appearing in `sum`.

This is useful to rearrange the operands.
 -/
Mathlib.MoveAdd.prepareOp : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic
Preorder.instHasLimitsOfShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : Preorder J] [OrderBot J],
  CategoryTheory.Limits.HasLimitsOfShape J C
-- Init.Internal.Order.Basic
Lean.Order.admissible_and : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] (P Q : α → Prop),
  Lean.Order.admissible P → Lean.Order.admissible Q → Lean.Order.admissible fun x => P x ∧ Q x