mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of `fderiv_const_smul_field`.

---

Special case of `fderiv_const_smul_of_invertible` over a division semiring: any constant is
allowed.

TODO: This would work for scalars in a `GroupWithZero` if we had a `DistribMulActionWithZero`
typeclass.  -/
fderiv_const_smul_of_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {R : Type u_4} [inst_5 : DivisionSemiring R] [inst_6 : Module R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F] (c : R), fderiv 𝕜 (c • f) = c • fderiv 𝕜 f
-- Mathlib.GroupTheory.Index
Subgroup.index_top : ∀ {G : Type u_1} [inst : Group G], ⊤.index = 1
-- Init.Tactics
/-- * `generalize ([h :] e = x),+` replaces all occurrences `e`s in the main goal
  with a fresh hypothesis `x`s. If `h` is given, `h : e = x` is introduced as well.
* `generalize e = x at h₁ ... hₙ` also generalizes occurrences of `e`
  inside `h₁`, ..., `hₙ`.
* `generalize e = x at *` will generalize occurrences of `e` everywhere.
 -/
Lean.Parser.Tactic.generalize : Lean.ParserDescr
-- Init.Data.SInt.Lemmas
Int32.toNat_toBitVec : ∀ (x : Int32), x.toBitVec.toNat = x.toUInt32.toNat
-- Mathlib.Topology.Algebra.UniformField
/-- The pullback of a completable topological field along a uniform inducing
ring homomorphism is a completable topological field.  -/
IsUniformInducing.completableTopField : ∀ {α : Type u_3} {β : Type u_4} [inst : Field β] [b : UniformSpace β] [CompletableTopField β] [inst_2 : Field α]
  [inst_3 : UniformSpace α] [T0Space α] {f : α →+* β}, IsUniformInducing ⇑f → CompletableTopField α
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.ext_iff : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  {X Y : LeftInvariantDerivation I G}, X = Y ↔ ∀ (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤), X f = Y f
-- Mathlib.RingTheory.Trace.Defs
Algebra.traceForm_toMatrix : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R S) (i j : ι),
  (LinearMap.BilinForm.toMatrix b) (Algebra.traceForm R S) i j = (Algebra.trace R S) (b i * b j)
-- Mathlib.Order.Partition.Finpartition
/-- The finpartition in one part, aka indiscrete finpartition.  -/
Finpartition.indiscrete : {α : Type u_1} → [inst : Lattice α] → [inst_1 : OrderBot α] → {a : α} → a ≠ ⊥ → Finpartition a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.mk.sizeOf_spec : ∀ (label : String) (detail? : Option String) (documentation? : Option Lean.Lsp.MarkupContent)
  (kind? : Option Lean.Lsp.CompletionItemKind) (textEdit? : Option Lean.Lsp.InsertReplaceEdit)
  (sortText? : Option String) (data? : Option Lean.Lsp.ResolvableCompletionItemData)
  (tags? : Option (Array Lean.Lsp.CompletionItemTag)),
  sizeOf
      { label := label, detail? := detail?, documentation? := documentation?, kind? := kind?, textEdit? := textEdit?,
        sortText? := sortText?, data? := data?, tags? := tags? } =
    1 + sizeOf label + sizeOf detail? + sizeOf documentation? + sizeOf kind? + sizeOf textEdit? + sizeOf sortText? +
        sizeOf data? +
      sizeOf tags?
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.instSMulDomMulAct : {R : Type u_1} →
  {R' : Type u_2} →
    {M : Type u_4} →
      {M' : Type u_5} →
        [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'} →
                      {S' : Type u_6} →
                        [inst_6 : Monoid S'] →
                          [inst_7 : DistribMulAction S' M] → [SMulCommClass R S' M] → SMul S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).inv.app T))
      (CategoryTheory.ChosenPullbacksAlong.snd T.hom g) =
    CategoryTheory.Limits.pullback.snd T.hom g
-- Batteries.Data.BinomialHeap.Basic
/-- `O(1)`. Auxiliary for `Heap.merge`: combines two heap nodes of the same rank
into one with the next larger rank.
 -/
Batteries.BinomialHeap.Imp.combine : {α : Type u_1} →
  (α → α → Bool) →
    α →
      α →
        Batteries.BinomialHeap.Imp.HeapNode α →
          Batteries.BinomialHeap.Imp.HeapNode α → α × Batteries.BinomialHeap.Imp.HeapNode α
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.RootOrdered.eq_3 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : α) (c : RBTree.RBColor) (l : RBTree.RBNode α) (x_2 : α)
  (parent : RBTree.RBNode.Path α),
  RBTree.RBNode.Path.RootOrdered cmp (RBTree.RBNode.Path.right c l x_2 parent) x =
    (RBTree.RBNode.cmpLT cmp x_2 x ∧ RBTree.RBNode.Path.RootOrdered cmp parent x)
-- Mathlib.Logic.Basic
not_forall_not : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), ¬p x) ↔ ∃ x, p x
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (S : CategoryTheory.SplitEpi f.hom) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n)
      (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) 0) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) S.section_
-- Mathlib.Order.RelClasses
/-- Induction on a well-founded relation.  -/
IsWellFounded.induction : ∀ {α : Type u} (r : α → α → Prop) [IsWellFounded α r] {motive : α → Prop} (a : α),
  (∀ (x : α), (∀ (y : α), r y x → motive y) → motive x) → motive a
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.iterFromIdxM_equiv_iterM_drop_toList : ∀ {α : Type w} {array : Array α} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] {pos : ℕ},
  (array.iterFromIdxM m pos).Equiv ((List.drop pos array.toList).iterM m)
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
Mathlib.Tactic.BicategoryLike.Normalize.instInhabitedResult.default : Mathlib.Tactic.BicategoryLike.Normalize.Result
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α]
  [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ {f : α → E} {t : Set α},
      MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ (g +ᵥ s), f x ∂μ
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of the reverse direction of `Sym2.fromRel_mono_iff`. -/
Sym2.fromRel_mono : ∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} (sym₁ : Std.Symm r₁) (sym₂ : Std.Symm r₂),
  r₁ ≤ r₂ → Sym2.fromRel sym₁ ⊆ Sym2.fromRel sym₂
-- Mathlib.Analysis.Normed.Affine.AddTorsor
antilipschitzWith_lineMap : ∀ {W : Type u_3} {Q : Type u_4} [inst : NormedAddCommGroup W] [inst_1 : MetricSpace Q] [inst_2 : NormedAddTorsor W Q]
  {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 W] {p₁ p₂ : Q},
  p₁ ≠ p₂ → AntilipschitzWith (nndist p₁ p₂)⁻¹ ⇑(AffineMap.lineMap p₁ p₂)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points not equal to `p`, the angle between the second and the third at `p` plus
the angle between the first and the second equals the angle between the first and the third.  -/
EuclideanGeometry.oangle_add_swap : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  p₁ ≠ p →
    p₂ ≠ p →
      p₃ ≠ p → EuclideanGeometry.oangle p₂ p p₃ + EuclideanGeometry.oangle p₁ p p₂ = EuclideanGeometry.oangle p₁ p p₃
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tmod_right : ∀ (a b : ℤ), (a * b).tmod a = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Connected
CategoryTheory.instIsConnectedWidePushoutShape : ∀ {J : Type u_1}, CategoryTheory.IsConnected (CategoryTheory.Limits.WidePushoutShape J)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_sSup : ∀ {α : Type u_1} {ms : Set (MeasurableSpace α)} {s : Set α},
  MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable {s | ∃ m ∈ ms, MeasurableSet s} s
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) {P Q : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} (f : P ⟶ Q) (E : ℰ)
  (g : Q ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E)
  (p : CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P) {Z : ℰ}
  (h :
    ((CategoryTheory.Functor.const
                (CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P)).obj
            E).obj
        p ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A P E).symm
            (CategoryTheory.CategoryStruct.comp f g)).app
        p)
      h =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A Q E).symm g).app
        ((CategoryTheory.CostructuredArrow.map f).obj p))
      h
-- Init.Data.List.Basic
List.drop_eq_nil_of_le : ∀ {α : Type u} {as : List α} {i : ℕ}, as.length ≤ i → List.drop i as = []
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.mk.inj : ∀ {Ω : Type w} {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {obj : Set Ω} {hom : ↑obj → ↑obj → Set Ω}
  {objEquiv : ↑obj ≃ C} {homEquiv : {X Y : ↑obj} → ↑(hom X Y) ≃ (objEquiv X ⟶ objEquiv Y)} {obj_1 : Set Ω}
  {hom_1 : ↑obj_1 → ↑obj_1 → Set Ω} {objEquiv_1 : ↑obj_1 ≃ C}
  {homEquiv_1 : {X Y : ↑obj_1} → ↑(hom_1 X Y) ≃ (objEquiv_1 X ⟶ objEquiv_1 Y)},
  { obj := obj, hom := hom, objEquiv := objEquiv, homEquiv := homEquiv } =
      { obj := obj_1, hom := hom_1, objEquiv := objEquiv_1, homEquiv := homEquiv_1 } →
    obj = obj_1 ∧ hom ≍ hom_1 ∧ objEquiv ≍ objEquiv_1 ∧ homEquiv ≍ homEquiv_1
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toCommSemiring : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → CommSemiring ↥S
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_bitwise : ∀ {f : Bool → Bool → Bool},
  f false false = false → ∀ (x y i : ℕ), (Nat.bitwise f x y).testBit i = f (x.testBit i) (y.testBit i)
-- Init.Prelude
/-- Get the context name used in Note `Macro Scope Representation`.  -/
Lean.MonadQuotation.getContext : {m : Type → Type} → [self : Lean.MonadQuotation m] → m Lean.Name
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.mono_of_cofibration : ∀ {X Y : SSet} (f : X ⟶ Y) [HomotopicalAlgebra.Cofibration f], CategoryTheory.Mono f
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- The point given by `secondInter` lies on the sphere.  -/
EuclideanGeometry.Sphere.secondInter_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P} (v : V), s.secondInter p v ∈ s ↔ p ∈ s
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Std.HashMap α Unit} (l : List α),
  m₁.Equiv m₂ → (m₁.insertManyIfNewUnit l).Equiv (m₂.insertManyIfNewUnit l)
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.eraseCasesAttr : Lean.Meta.Grind.Extension → Lean.Name → Lean.CoreM Unit
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- Choice of tagged point of each box in this prepartition:
we extend this to a total function, on all boxes in `ι → ℝ`.  -/
BoxIntegral.TaggedPrepartition.tag : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.TaggedPrepartition I → BoxIntegral.Box ι → ι → ℝ
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mod_eq_sub_mul_div : ∀ {R : Type u_1} [inst : EuclideanDomain R] (a b : R), a % b = a - b * (a / b)
-- Mathlib.RingTheory.NormalClosure
_private.Mathlib.RingTheory.NormalClosure.0.Ring.termL : Lean.ParserDescr
-- Mathlib.Topology.Algebra.ProperConstSMul
instProperConstSMulForall : ∀ {M : Type u_1} {ι : Type u_2} {X : ι → Type u_3} [inst : (i : ι) → SMul M (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), ProperConstSMul M (X i)], ProperConstSMul M ((i : ι) → X i)
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.topologicalClosure_map_le : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A]
  [inst_6 : StarModule R A] [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A]
  [inst_9 : TopologicalSpace B] [inst_10 : Semiring B] [inst_11 : Algebra R B] [inst_12 : StarRing B]
  [inst_13 : StarModule R B] [inst_14 : IsSemitopologicalSemiring B] [inst_15 : ContinuousStar B]
  (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B),
  IsClosedMap ⇑φ → (StarSubalgebra.map φ s).topologicalClosure ≤ StarSubalgebra.map φ s.topologicalClosure
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  {Y : CategoryTheory.Functor C V} (β : CategoryTheory.MonoidalCategory.DayConvolution.convolution F G ⟶ Y) (X : C × C),
  ((CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy F G).homEquiv β).app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app X)
      (β.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X.1 X.2))
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instSMul : {R : Type uR} →
  {S : Type uS} →
    {ι : Type uι} →
      {M₁ : ι → Type v₁} →
        {M₂ : Type v₂} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : (i : ι) → Module R (M₁ i)] →
                  [inst_4 : Module R M₂] →
                    [inst_5 : DistribSMul S M₂] → [SMulCommClass R S M₂] → SMul S (MultilinearMap R M₁ M₂)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_div_div_cancel_left' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {c : G₀} (a b : G₀), c ≠ 0 → c / a / (c / b) = b / a
-- Init.Data.Array.MapIdx
Array.mapFinIdx_induction : ∀ {α : Type u_1} {β : Type u_2} (xs : Array α) (f : (i : ℕ) → α → i < xs.size → β) (motive : ℕ → Prop),
  motive 0 →
    ∀ (p : (i : ℕ) → β → i < xs.size → Prop),
      (∀ (i : ℕ) (h : i < xs.size), motive i → p i (f i xs[i] h) h ∧ motive (i + 1)) →
        motive xs.size ∧
          ∃ (eq : (xs.mapFinIdx f).size = xs.size), ∀ (i : ℕ) (h : i < xs.size), p i (xs.mapFinIdx f)[i] h
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.insert.induct_unfolding : ∀ (k : ℤ) (v : Lean.Grind.Linarith.Var) (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Prop),
  motive Lean.Grind.Linarith.Poly.nil (Lean.Grind.Linarith.Poly.add k v Lean.Grind.Linarith.Poly.nil) →
    (∀ (k_1 : ℤ) (v_1 : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
        Nat.blt v_1 v = true →
          motive (Lean.Grind.Linarith.Poly.add k_1 v_1 p)
            (Lean.Grind.Linarith.Poly.add k v (Lean.Grind.Linarith.Poly.add k_1 v_1 p))) →
      (∀ (k_1 : ℤ) (v_1 : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
          Nat.blt v_1 v = false →
            Nat.beq v v_1 = true → (k.add k_1 == 0) = true → motive (Lean.Grind.Linarith.Poly.add k_1 v_1 p) p) →
        (∀ (k_1 : ℤ) (v_1 : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
            Nat.blt v_1 v = false →
              Nat.beq v v_1 = true →
                ¬(k.add k_1 == 0) = true →
                  motive (Lean.Grind.Linarith.Poly.add k_1 v_1 p) (Lean.Grind.Linarith.Poly.add (k.add k_1) v_1 p)) →
          (∀ (k_1 : ℤ) (v_1 : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
              Nat.blt v_1 v = false →
                Nat.beq v v_1 = false →
                  motive p (Lean.Grind.Linarith.Poly.insert k v p) →
                    motive (Lean.Grind.Linarith.Poly.add k_1 v_1 p)
                      (Lean.Grind.Linarith.Poly.add k_1 v_1 (Lean.Grind.Linarith.Poly.insert k v p))) →
            ∀ (p : Lean.Grind.Linarith.Poly), motive p (Lean.Grind.Linarith.Poly.insert k v p)
-- Aesop.Tree.RunMetaM
Aesop.Rapp.runMetaM' : {m : Type → Type u_1} → [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.Rapp → m α
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.nonuniformWitness_mem_nonuniformWitnesses : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [inst_4 : DecidableRel G.Adj] {ε : 𝕜}
  {s t : Finset α}, ¬G.IsUniform ε s t → t ∈ P.parts → s ≠ t → G.nonuniformWitness ε s t ∈ P.nonuniformWitnesses G ε s
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toAlternatingMap_add : ∀ {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] [inst_7 : ContinuousAdd N] (f g : M [⋀^ι]→L[R] N),
  (f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.singleton_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {t : Finset β} (a : α), {a} • t = a • t
-- Init.Data.List.Lemmas
List.filterMap_eq_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, List.filterMap (some ∘ f) = List.map f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isSome_getKey?_eq_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, (m.getKey? a).isSome = m.contains a
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.Dep.eRk_lt_encard : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite], M.Dep X → M.eRk X < X.encard
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.instQuasiIsoIntι' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (R : CategoryTheory.InjectiveResolution X), QuasiIso R.ι'
-- Mathlib.Util.TermReduce
/-- `beta% t` elaborates `t` and then if the result is in the form
`f x1 ... xn` where `f` is a (nested) lambda expression,
it will substitute all of its arguments by beta reduction.
This does not recursively do beta reduction, nor will it do
beta reduction of subexpressions.

In particular, `t` is elaborated, its metavariables are instantiated,
and then `Lean.Expr.headBeta` is applied.  -/
Mathlib.Util.TermReduce.elabBeta : Lean.Elab.Term.TermElab
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- Functors out of `WalkingIso` define isomorphisms in the target category.  -/
CategoryTheory.WalkingIso.toIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.WalkingIso C) →
      F.obj CategoryTheory.WalkingIso.zero ≅ F.obj CategoryTheory.WalkingIso.one
-- Mathlib.Order.Filter.Pointwise
Filter.smul_filter.instNeBot : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {a : α} [f.NeBot], (a • f).NeBot
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- A collection of bases with the exchange property and at least one finite member is a matroid  -/
Matroid.ofExistsFiniteIsBase : {α : Type u_1} →
  (E : Set α) →
    (IsBase : Set α → Prop) →
      (∃ B, IsBase B ∧ B.Finite) → Matroid.ExchangeProperty IsBase → (∀ (B : Set α), IsBase B → B ⊆ E) → Matroid α
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.FormallyUnramified.stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.FormallyUnramified f] (x : ↥X),
  (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).FormallyUnramified
-- Lean.DocString.Parser
/-- Items like -  -/
Lean.Doc.Parser.UnorderedListType.dash : Lean.Doc.Parser.UnorderedListType
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.range_val : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] (S : NonUnitalStarSubalgebra R A),
  NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subtype S) = S
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.map.eq_1 : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition]
  {f : X ⟶ Y} (hPf : P f),
  CategoryTheory.MorphismProperty.Under.map Q hPf =
    CategoryTheory.MorphismProperty.Comma.mapLeft (CategoryTheory.Functor.id T)
      (CategoryTheory.Discrete.natTrans fun x => f) ⋯
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions : ∀ {P : TopCat → Prop} [inst : CompHausLike.HasExplicitFiniteCoproducts P]
  [CompHausLike.HasExplicitPullbacksOfInclusions P], CategoryTheory.HasPullbacksOfInclusions (CompHausLike P)
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with
an index set which is a countable set in any type.  -/
dense_biInter_of_isOpen : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [BaireSpace X] {S : Set α} {f : α → Set X},
  (∀ s ∈ S, IsOpen (f s)) → S.Countable → (∀ s ∈ S, Dense (f s)) → Dense (⋂ s ∈ S, f s)
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findM?.eq_def : ∀ {m : Type → Type u} [inst : Monad m] {α : Type} (p : α → m Bool) (x : List α),
  List.findM? p x =
    match x with
    | [] => pure none
    | a :: as => do
      let __do_lift ← p a
      match __do_lift with
        | true => pure (some a)
        | false => List.findM? p as