mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.id_whiskerLeft_symm : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η)
        (CategoryTheory.Bicategory.leftUnitor g).hom)
-- Mathlib.CategoryTheory.Limits.MonoCoprod
_private.Mathlib.CategoryTheory.Limits.MonoCoprod.0.CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum.match_1.eq_2 : ∀ {I₁ : Type u_1} {I₂ : Type u_2} (motive : I₁ ⊕ I₂ → Sort u_3) (i₂ : I₂) (h_1 : (i₁ : I₁) → motive (Sum.inl i₁))
  (h_2 : (i₂ : I₂) → motive (Sum.inr i₂)),
  (match Sum.inr i₂ with
    | Sum.inl i₁ => h_1 i₁
    | Sum.inr i₂ => h_2 i₂) =
    h_2 i₂
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S' : Solution'`, the key factorization of `S'.a ^ 3 + S'.b ^ 3`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ),
  FermatLastTheoremForThreeGen.Solution'.a✝ S' ^ 3 + FermatLastTheoremForThreeGen.Solution'.b✝ S' ^ 3 =
    (FermatLastTheoremForThreeGen.Solution'.a✝ S' + FermatLastTheoremForThreeGen.Solution'.b✝ S') *
        (FermatLastTheoremForThreeGen.Solution'.a✝ S' + ↑⋯.unit * FermatLastTheoremForThreeGen.Solution'.b✝ S') *
      (FermatLastTheoremForThreeGen.Solution'.a✝ S' + ↑⋯.unit ^ 2 * FermatLastTheoremForThreeGen.Solution'.b✝ S')
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.le_valuation_add : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℤ_[p]}, x + y ≠ 0 → min x.valuation y.valuation ≤ (x + y).valuation
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_cast_iff : ∀ {s₁ s₂ : String.Slice} {h : s₁.copy = s₂.copy} {p : s₁.Pos} {t₁ t₂ : String}, (p.cast h).Splits t₁ t₂ ↔ p.Splits t₁ t₂
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_append : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote ctx (p₁.append p₂) =
    Int.Internal.Linear.Poly.denote ctx p₁ + Int.Internal.Linear.Poly.denote ctx p₂
-- Init.Data.BitVec.Basic
BitVec.instNeg : {n : ℕ} → Neg (BitVec n)
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  (h : d.mid ⟶ e.mid)
  (ι_h : autoParam (CategoryTheory.CategoryStruct.comp d.ι h = e.ι) CategoryTheory.Factorisation.Hom.ι_h._autoParam)
  (h_π : autoParam (CategoryTheory.CategoryStruct.comp h e.π = d.π) CategoryTheory.Factorisation.Hom.h_π._autoParam)
  (h_1 : d.mid ⟶ e.mid)
  (ι_h_1 : autoParam (CategoryTheory.CategoryStruct.comp d.ι h_1 = e.ι) CategoryTheory.Factorisation.Hom.ι_h._autoParam)
  (h_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h_1 e.π = d.π) CategoryTheory.Factorisation.Hom.h_π._autoParam),
  ({ h := h, ι_h := ι_h, h_π := h_π } = { h := h_1, ι_h := ι_h_1, h_π := h_π_1 }) = (h = h_1)
-- Mathlib.RingTheory.Trace.Defs
Algebra.traceForm_isSymm : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (Algebra.traceForm R S).IsSymm
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`.  -/
CategoryTheory.Center.tensorHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X₁ Y₁ X₂ Y₂ : CategoryTheory.Center C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (X₁.tensorObj X₂ ⟶ Y₁.tensorObj Y₂)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGED_eq_getD_getEntryGE? : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α} {fallback : α × β},
  Std.DTreeMap.Internal.Impl.Const.getEntryGED k t fallback =
    (Std.DTreeMap.Internal.Impl.Const.getEntryGE? k t).getD fallback
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.Sheaf.tensorProd_isSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  (X Y : CategoryTheory.Sheaf J A),
  CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.MonoidalCategoryStruct.tensorObj X.obj Y.obj)
-- Init.Data.String.Iterate
/-- Folds a function over a slice from the start, accumulating a value starting with `init`. The
accumulated value is combined with each character in order, using `f`.

Examples:

* `"coffee tea water".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2`

* `"coffee tea and water".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3`

* `"coffee tea water".toSlice.foldl (·.push ·) "" = "coffee tea water"`
 -/
String.Slice.foldl : {α : Type u} → (α → Char → α) → α → String.Slice → α
-- Mathlib.FieldTheory.Perfect
polynomial_expand_eq : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (f : Polynomial R),
  (Polynomial.expand R p) f = Polynomial.map (↑(frobeniusEquiv R p).symm) f ^ p
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rio.Internal.forIn'_eq_forIn'_iter : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  {r : Std.Rio α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.Rio.Internal.iter r) init fun a ha acc => f a ⋯ acc
-- Lean.Environment
Lean.Environment.toKernelEnv : Lean.Environment → Lean.Kernel.Environment
-- Init.Prelude
/-- Wraps a proof or value to increase its type's universe level by 1.  -/
PLift.up : {α : Sort u} → α → PLift α
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_neg : ∀ {R : Type u} {M : Type v} [inst : Neg R] [inst_1 : Neg M] (x : TrivSqZeroExt R M), (-x).snd = -x.snd
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Multiplication `y ↦ x * y` as an `IsometryEquiv`.  -/
IsometryEquiv.mulLeft : {G : Type v} → [inst : Group G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricSMul G G] → G → G ≃ᵢ G
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, a ∈ m.erase k → a ∈ m
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} [inst_1 : SizeOf C] (s₀ : E.I₀ → F.I₀) (h₀ : (i : E.I₀) → E.X i ⟶ F.X (s₀ i))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i) (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreZeroHypercover.Hom.w₀._autoParam),
  sizeOf { s₀ := s₀, h₀ := h₀, w₀ := w₀ } = 1
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_pageD : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r : ℤ) (hr : r₀ ≤ r) (pq pq' pq'' : κ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD X data r pq pq' hr)
      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD X data r pq' pq'' hr) =
    0
-- Mathlib.Data.Int.ModEq
Int.ModEq.mul_right : ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → a * c ≡ b * c [ZMOD n]
-- Mathlib.Algebra.Lie.Weights.Basic
/-- **Alias** of `zero_apply`. -/
LieModule.Weight.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.Order.CompleteLattice.Basic
sSup_Prop_eq : ∀ {s : Set Prop}, sSup s = ∃ p ∈ s, p
-- Mathlib.CategoryTheory.Subfunctor.Finite
/-- A choice of index type for the generating sections of a finitely generated subpresheaf.  -/
CategoryTheory.Subfunctor.IsFinite.Index : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} → (G : CategoryTheory.Subfunctor F) → [hG : G.IsFinite] → Type
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_sub_two_pi : ∀ (x : ℝ), Circle.exp (x - 2 * Real.pi) = Circle.exp x
-- Mathlib.GroupTheory.OrderOfElement
Nat.Coprime.addOrderOf_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] {y : G} {m : ℕ}, (addOrderOf y).Coprime m → addOrderOf (m • y) = addOrderOf y
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.orbit.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (x : MulAction.orbitRel.Quotient G α),
  x.orbit = Quotient.liftOn' x (MulAction.orbit G) ⋯
-- Mathlib.NumberTheory.FactorisationProperties
IsPrimePow.deficient : ∀ {n : ℕ}, IsPrimePow n → n.Deficient
-- Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
GenContFract.conts_recurrenceAux : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K] {gp ppred pred : GenContFract.Pair K},
  g.s.get? n = some gp →
    g.contsAux n = ppred →
      g.contsAux (n + 1) = pred →
        g.conts (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.WeierstrassCurve.Projective.toAffine_addX_of_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    ∀ {n d : F},
      d ≠ 0 →
        W.toAffine.addX (P 0 / P 2) (P 0 / P 2) (-n / P 2 / d) =
          (n ^ 2 - W.a₁ * n * P 2 * d - W.a₂ * P 2 ^ 2 * d ^ 2 - 2 * P 0 * P 2 * d ^ 2) * d / P 2 / (P 2 * d ^ 3)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.all_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {p : α → Bool},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.all p = t₂.all p
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableSub₂ : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Sub α] [DiscreteMeasurableSpace (α × α)], MeasurableSub₂ α
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.tendsto : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F} (x : E),
  IsBoundedLinearMap 𝕜 f → Filter.Tendsto f (nhds x) (nhds (f x))
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_union_Ioi_eq_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Icc a b ∪ Set.Ioi b = Set.Ici a
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isRevMatch_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch c pos ↔
    ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_self_add_left : ∀ {m n : ℕ}, (m + n).Coprime m ↔ n.Coprime m
-- Mathlib.Data.Sym.Sym2
Sym2.add.eq_1 : ∀ {M : Type u_4} [inst : AddCommMagma M], Sym2.add = Sym2.lift ⟨fun x1 x2 => x1 + x2, ⋯⟩
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.toPerfPair_apply : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [inst_5 : p.IsPerfPair] (x : M) (y : N),
  (p.toPerfPair x) y = (p x) y
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.continuousWithinAt : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : Set M₁} {x : M₁},
  ContinuousWithinAt (⇑e) s x
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
Continuous.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {X : Type u_5} [inst_5 : TopologicalSpace X] {f : X → E →L[𝕜] F} {g : X → E},
  Continuous f → Continuous g → Continuous fun x => (f x) (g x)
-- Lean.Environment
Lean.Kernel.Exception.interrupted.sizeOf_spec : sizeOf Lean.Kernel.Exception.interrupted = 1
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Commute.cfcAbs_mul_eq : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A},
  Commute a b → Commute a (star b) → CFC.abs (a * b) = CFC.abs a * CFC.abs b
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
HasEnoughRootsOfUnity.exists_primitiveRoot : ∀ (M : Type u_1) [inst : CommMonoid M] (n : ℕ) [HasEnoughRootsOfUnity M n], ∃ ζ, IsPrimitiveRoot ζ n
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
/-- Identity morphisms are right identities for composition.  -/
CategoryTheory.Bicategory.Strict.comp_id : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) = f
-- Mathlib.Algebra.Category.ModuleCat.Basic
CategoryTheory.Iso.toLinearEquiv_apply : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (i : X ≅ Y) (x : ↑X),
  i.toLinearEquiv x = (CategoryTheory.ConcreteCategory.hom i.hom) x
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Corollary of the Lebesgue dominated convergence theorem: If a sequence of functions `F n` is
(eventually) uniformly bounded by a constant and converges (eventually) pointwise to a
function `f`, then the integrals of `F n` with respect to a finite measure `μ` converge
to the integral of `f`.  -/
MeasureTheory.tendsto_integral_filter_of_norm_le_const : ∀ {α : Type u_1} {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_4} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → α → G}
  [MeasureTheory.IsFiniteMeasure μ] {f : α → G},
  (∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) μ) →
    (∃ C, ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ C) →
      (∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun n => F n ω) l (nhds (f ω))) →
        Filter.Tendsto (fun n => ∫ (ω : α), F n ω ∂μ) l (nhds (∫ (ω : α), f ω ∂μ))
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.splitter : {n : ℕ} →
  (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) →
    (step : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)) →
      (Unit → motive none) →
        ((id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints))) →
          ((id : ℕ) →
              (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
                (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints))) →
            ((id : ℕ) →
                (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
                  (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
                    (rupHints : Array ℕ) →
                      (ratHints : Array (ℕ × Array ℕ)) →
                        motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints))) →
              ((ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))) → motive step
-- Mathlib.Analysis.Calculus.TangentCone.Basic
UniqueDiffWithinAt.congr_pt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x y : E} {s : Set E}, UniqueDiffWithinAt 𝕜 s x → x = y → UniqueDiffWithinAt 𝕜 s y
-- Aesop.Forward.Match.Types
Aesop.ForwardRuleMatch.mk.sizeOf_spec : ∀ (rule : Aesop.ForwardRule) («match» : Aesop.CompleteMatch),
  sizeOf { rule := rule, «match» := «match» } = 1 + sizeOf rule + sizeOf «match»
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.ColimitOfShape.isCardinalPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : C} {J : Type w}
  [inst_1 : CategoryTheory.SmallCategory J] (p : P.ColimitOfShape J X) {κ : Cardinal.{w}} [inst_2 : Fact κ.IsRegular],
  P ≤ CategoryTheory.isCardinalPresentable C κ →
    ∀ [CategoryTheory.LocallySmall.{w, v, u} C] (κ' : Cardinal.{w}) [inst_4 : Fact κ'.IsRegular],
      κ ≤ κ' → HasCardinalLT (CategoryTheory.Arrow J) κ' → CategoryTheory.IsCardinalPresentable X κ'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {he : t ≠ ∅} {km : α}, t.minKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Algebra.Ring.Parity
Function.Involutive.iterate_eq_id : ∀ {α : Type u_4} {f : α → α} {n : ℕ}, Function.Involutive f → f ≠ id → (f^[n] = id ↔ Even n)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The range of a morphism of semirings is a fintype, if the domain is a fintype.
Note: this instance can form a diamond with `Subtype.fintype` in the
  presence of `Fintype S`.  -/
RingHom.fintypeRangeS : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] → [Fintype R] → [DecidableEq S] → (f : R →+* S) → Fintype ↥f.rangeS
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
/-- Chooses an exiting variable: the variable imposing the strictest limit on the increase of the
entering variable, breaking ties by choosing the variable with smallest index.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.chooseExitingVar : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    ℕ → Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmM matType ℕ
-- Lean.Elab.Binders
/-- For `let x := v; b`, adds `eq : x = v` to the context.  -/
Lean.Elab.Term.LetConfig.eq? : Lean.Elab.Term.LetConfig → Option Lean.Ident
-- Lean.Meta.Transform
/-- Removes all `patternWithRef` annotations from `e`.  -/
Lean.Meta.erasePatternRefAnnotations : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.instNormedAddCommGroupComplement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              (h : Manifold.IsSubmersionAt I J n f x) → NormedAddCommGroup h.complement
-- Init.Data.Array.Lemmas
Array.setIfInBounds_eq_empty_iff : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α}, xs.setIfInBounds i a = #[] ↔ xs = #[]
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_erase_eq_of_not_compare_minD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k fallback : α},
      (t.erase k).isEmpty = false → ¬cmp k (t.minD fallback) = Ordering.eq → (t.erase k).minD fallback = t.minD fallback
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_update_of_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∈ s → ∀ (f : ι → M) (b : M), ∑ x ∈ s, Function.update f i b x = b + ∑ x ∈ s \ {i}, f x
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.RigidCategory.toRightRigidCategory : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.RigidCategory C] → CategoryTheory.RightRigidCategory C
-- Mathlib.GroupTheory.Divisible
Prod.divisibleBy : {β : Type u_3} →
  {B : Type u_4} →
    {B' : Type u_5} →
      [inst : SMul β B] →
        [inst_1 : SMul β B'] →
          [inst_2 : Zero β] →
            [inst_3 : AddMonoid B] →
              [inst_4 : AddMonoid B'] → [DivisibleBy B β] → [DivisibleBy B' β] → DivisibleBy (B × B') β
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
SpectrumRestricts.of_subset_range_algebraMap : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a : A} {f : S → R},
  Function.LeftInverse f ⇑(algebraMap R S) → spectrum S a ⊆ Set.range ⇑(algebraMap R S) → SpectrumRestricts a f
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.of_order_le : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k l : ℕ} {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → l ≤ k → ContDiffPointwiseHolderAt l α f a
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.subtypeVal : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α},
  IsLowerSet s → ∀ {a : ↑s}, Order.IsSuccPrelimit a → Order.IsSuccPrelimit ↑a
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- We can always derive `PreservesFiniteLimits C` by showing that we are preserving limits at an
arbitrary universe.  -/
CategoryTheory.Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  (∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J} (x : CategoryTheory.FinCategory J),
      CategoryTheory.Limits.PreservesLimitsOfShape J F) →
    CategoryTheory.Limits.PreservesFiniteLimits F
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_erase_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], (m.erase k).get! k = default
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.isUniformInducing_pureCauchy : ∀ {α : Type u} [inst : UniformSpace α], IsUniformInducing CauchyFilter.pureCauchy