mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_algebraMap_iff : ∀ {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] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [IsScalarTower R S A] {a : S},
  Function.Injective ⇑(algebraMap S A) → (IsAlgebraic R ((algebraMap S A) a) ↔ IsAlgebraic R a)
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.ξ.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {β : Type u_3} (x x_1 : β × (K →+* ℂ) → ℤ),
  x = x_1 → ∀ (a a_1 : β), a = a_1 → NumberField.house.ξ✝ K x a = NumberField.house.ξ✝ K x_1 a_1
-- Init.Data.List.Scan.Lemmas
List.tail_scanl : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} (h : 0 < l.length),
  (List.scanl f b l).tail = List.scanl f (f b (l.head ⋯)) l.tail
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.nonneg : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 ≤ p
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivAt_fst : ∀ {𝕜 : 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'] (x : M × M'),
  HasMFDerivAt% Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
-- Mathlib.Topology.Bornology.Hom
instCoeTCLocallyBoundedMapOfLocallyBoundedMapClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Bornology α] →
          [inst_2 : Bornology β] → [LocallyBoundedMapClass F α β] → CoeTC F (LocallyBoundedMap α β)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The measure of a closed ball can be expressed in terms of the measure of the closed unit ball.
Use instead `addHaar_closedBall`, which uses the measure of the open unit ball as a standard
form.  -/
MeasureTheory.Measure.addHaar_closedBall' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ},
  0 ≤ r → μ (Metric.closedBall x r) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.closedBall 0 1)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_le_of_eventually_le : ∀ {u v : ℕ → EReal} {b : EReal},
  b ≠ ⊤ → (∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ v n + b) → LinearGrowth.linearGrowthSup u ≤ LinearGrowth.linearGrowthSup v
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The fixed choice of a preimage.  -/
CategoryTheory.Presieve.getFunctorPushforwardStructure : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : C} →
          {F : CategoryTheory.Functor C D} →
            {S : CategoryTheory.Presieve X} →
              {Y : D} →
                {f : Y ⟶ F.obj X} →
                  CategoryTheory.Presieve.functorPushforward F S f →
                    CategoryTheory.Presieve.FunctorPushforwardStructure F S f
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.partDen_none_iff_s_none : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ}, g.partDens.get? n = none ↔ g.s.get? n = none
-- Lean.Level
Lean.Nat.imax : ℕ → ℕ → ℕ
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.surjective_of_dual_injective : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {A' : Type u_1} [inst_2 : AddCommGroup A']
  [inst_3 : Module R A] [inst_4 : Module R A'] (f : A →ₗ[R] A'),
  Function.Injective ⇑(CharacterModule.dual f) → Function.Surjective ⇑f
-- Mathlib.Data.Set.Disjoint
Set.disjoint_union_right : ∀ {α : Type u} {s t u : Set α}, Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
-- Mathlib.Topology.Order.OrderClosed
Filter.tendsto_nhds_max_right : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f : β → α}
  {l : Filter β} {a : α},
  Filter.Tendsto f l (nhdsWithin a (Set.Ioi a)) → Filter.Tendsto (fun i => max a (f i)) l (nhdsWithin a (Set.Ioi a))
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_one : Std.DTreeMap.Internal.Impl.BalancedAtRoot 0 1
-- Mathlib.Analysis.Complex.BranchLogRoot
/-- If `g : X → 𝔻` defined on a locally path connected space
is continuous on an open simply connected set `U` and `0 ∉ g '' U`,
then for any `n ≠ 0`, there exists a continuous branch of `ⁿ√g` on `U`.
More precisely, there exists a function `f : X → 𝔻` continuous on `U`
such that `(f x) ^ n = g x` for all `x`.  -/
Complex.UnitDisc.exists_continuousOn_pow_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X},
  IsSimplyConnected U →
    IsOpen U →
      ∀ {g : X → Complex.UnitDisc},
        ContinuousOn g U → 0 ∉ g '' U → ∀ (n : ℕ+), ∃ f, ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
-- Init.Data.BitVec.Bitblast
/-- The final carry bit when computing `x + y + c` is `true` iff `x.toNat + y.toNat + c.toNat ≥ 2^w`.  -/
BitVec.carry_width : ∀ {w : ℕ} {c : Bool} {x y : BitVec w}, BitVec.carry w x y c = decide (x.toNat + y.toNat + c.toNat ≥ 2 ^ w)
-- Mathlib.Analysis.Complex.Basic
RCLike.summable_conj : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜},
  Summable (fun x => (starRingEnd 𝕜) (f x)) L ↔ Summable f L
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Variant of `meromorphicTrailingCoeffAt_factorizedRational`: Compute the trailing coefficient of the
factorized rational function associated with `d : 𝕜 → ℤ` at points outside the support of `d`.
 -/
Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational_off_support : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} {x : 𝕜},
  Function.HasFiniteSupport d →
    x ∉ Function.support d →
      meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) x = ∏ᶠ (u : 𝕜), (x - u) ^ d u
-- Mathlib.ModelTheory.Syntax
/-- Take the conjunction of a finite set of formulas.

Note that this is an arbitrary formula defined using the axiom of choice. It is only well-defined up
to equivalence of formulas.  -/
FirstOrder.Language.BoundedFormula.iInf : {L : FirstOrder.Language} →
  {α : Type u'} → {β : Type v'} → {n : ℕ} → [Finite β] → (β → L.BoundedFormula α n) → L.BoundedFormula α n
-- Mathlib.Algebra.Order.Interval.Basic
instAddNonemptyInterval.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α],
  instAddNonemptyInterval = { add := fun s t => { toProd := s.toProd + t.toProd, fst_le_snd := ⋯ } }
-- Mathlib.Algebra.Order.Ring.Prod
instIsOrderedRingProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : Semiring β]
  [inst_4 : PartialOrder β] [IsOrderedRing β], IsOrderedRing (α × β)
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Extend `Set α → E →L[ℝ] F` to `(α →₁ₛ[μ] E) →L[𝕜] F`.  -/
MeasureTheory.L1.SimpleFunc.setToL1SCLM' : (α : Type u_1) →
  (E : Type u_2) →
    {F : Type u_3} →
      (𝕜 : Type u_6) →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : NormedAddCommGroup F] →
              [inst_3 : NormedSpace ℝ F] →
                {m : MeasurableSpace α} →
                  (μ : MeasureTheory.Measure α) →
                    [inst_4 : NormedRing 𝕜] →
                      [inst_5 : Module 𝕜 E] →
                        [inst_6 : IsBoundedSMul 𝕜 E] →
                          [inst_7 : Module 𝕜 F] →
                            {T : Set α → E →L[ℝ] F} →
                              {C : ℝ} →
                                MeasureTheory.DominatedFinMeasAdditive μ T C →
                                  (∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) → ↥(α →₁ₛ[μ] E) →L[𝕜] F
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.map_injective : ∀ {S : Type u_2} {T : Type u_3} [inst : Semiring S] [inst_1 : Semiring T] (f : S →+* T),
  Function.Injective ⇑f → Function.Injective ⇑(PowerSeries.map f)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for monotonicity of multiplication on the right,
namely `a₁ < a₂ → a₁ * b < a₂ * b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedMonoid`.  -/
MulRightStrictMono : (M : Type u_1) → [Mul M] → [LT M] → Prop
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_neg_comp_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj A] [inst_3 : CategoryTheory.AddGrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsAddMonHom f] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg f))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- `cofan 𝒜 f` is a coproduct of `f`.  -/
CategoryTheory.Limits.FormalCoproduct.isColimitCofan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (𝒜 : Type w) →
      (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_lt_tsub_left_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → c < b → a - b < a - c
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.not_hasDimensionLT : ∀ (n : ℕ),
  autoParam ((SSet.stdSimplex.obj { len := n }).HasDimensionLT n) SSet.stdSimplex.not_hasDimensionLT._auto_1 → False
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Remove a term from an element of the monoid algebra.  -/
MonoidAlgebra.erase : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → M → MonoidAlgebra R M → MonoidAlgebra R M
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- Generalization of `lintegral_eq_iSup_eapprox_lintegral` to ae-measurable functions.  -/
MeasureTheory.lintegral_eq_iSup_eapprox_lintegral' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ),
  ∫⁻ (a : α), f a ∂μ = ⨆ n, (MeasureTheory.SimpleFunc.eapprox (AEMeasurable.mk f hf) n).lintegral μ
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_add_lt_mk_right_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk (a + b) < ArchimedeanClass.mk b ↔ ArchimedeanClass.mk a < ArchimedeanClass.mk b
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsMultiplicativeTrivialCofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)],
  (HomotopicalAlgebra.trivialCofibrations C).IsMultiplicative
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_sdiff_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ici a \ Set.Ici b = Set.Ico a b
-- Init.Data.SInt.Lemmas
Int32.lt_or_le : ∀ (a b : Int32), a < b ∨ b ≤ a
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁),
  CategoryTheory.CategoryStruct.comp (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.contains a = false → t.getKeyD a fallback = fallback
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.Compatible.of_ge : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, G ≤ H → H.Compatible G
-- Mathlib.Analysis.Normed.Module.Basic
/-- A normed algebra `𝕜'` over `𝕜` is normed module that is also an algebra.

See the implementation notes for `Algebra` for a discussion about non-unital algebras. Following
the strategy there, a non-unital *normed* algebra can be written as:
```lean
variable [NormedField 𝕜] [NonUnitalSeminormedRing 𝕜']
variable [NormedSpace 𝕜 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']
```
 -/
NormedAlgebra.norm_smul_le : ∀ {𝕜 : Type u_6} {𝕜' : Type u_7} {inst : NormedField 𝕜} {inst_1 : SeminormedRing 𝕜'} [self : NormedAlgebra 𝕜 𝕜'] (r : 𝕜)
  (x : 𝕜'), ‖r • x‖ ≤ ‖r‖ * ‖x‖
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_Ioo_castLE : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.Ioo (Fin.castLE h i) (Fin.castLE h j) = Set.Ioo i j
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_alter_eq_sub_one : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∈ t → (f t[k]?).isNone = true → (t.alter k f).size = t.size - 1
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- Let `f : X → Y`. Suppose that to prove that `f` is continuous, it suffices to show that
for every compact Hausdorff space `K` and every continuous map `g : K → X`, `f ∘ g` is continuous.
Then `X` is compactly generated.  -/
uCompactlyGeneratedSpace_of_continuous_maps : ∀ {X : Type w} [t : TopologicalSpace X],
  (∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
      (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f) →
    UCompactlyGeneratedSpace X
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- **Alias** of `Metric.eball_top`. -/
Metric.emetric_ball_top : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), Metric.eball x ⊤ = Set.univ
-- Mathlib.Order.Lattice
SemilatticeSup.ext_sup : ∀ {α : Type u_1} {A B : SemilatticeSup α}, (∀ (x y : α), x ≤ y ↔ x ≤ y) → ∀ (x y : α), x ⊔ y = x ⊔ y
-- Std.Internal.UV.System
/-- Gets a subset of the password file entry for the current user.
 -/
Std.Internal.UV.System.osGetPasswd : IO Std.Internal.UV.System.PasswdInfo
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.pow.induct_unfolding : ∀ (p : Lean.Grind.CommRing.Poly) (motive : ℕ → Lean.Grind.CommRing.Poly → Prop),
  motive 0 (Lean.Grind.CommRing.Poly.num 1) →
    motive 1 p →
      (∀ (k : ℕ), (k = 0 → False) → motive k (p.pow k) → motive k.succ (p.mul (p.pow k))) →
        ∀ (k : ℕ), motive k (p.pow k)
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.sigma_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] [inst_1 : UnivLE.{v, u}]
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) (x : PUnit.{v + 1}),
  𝒰.sigma.f x = CategoryTheory.Limits.Sigma.desc 𝒰.f
-- Mathlib.Data.Finset.Image
Finset.coe_map : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α), ↑(Finset.map f s) = ⇑f '' ↑s
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.lift.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f f_1 : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (e_f : f = f_1)
  (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) [inst_5 : IsAdicComplete I N],
  IsAdicComplete.StrictMono.lift I ha f hf = IsAdicComplete.StrictMono.lift I ha f_1 ⋯
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.getCaseGoals.getUserName : Lean.MVarId → Lean.Elab.Tactic.TacticM Lean.Name
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Poly.denote.match_1.splitter : (motive : Lean.Grind.Linarith.Poly → Sort u_1) →
  (p : Lean.Grind.Linarith.Poly) →
    (Unit → motive Lean.Grind.Linarith.Poly.nil) →
      ((k : ℤ) →
          (v : Lean.Grind.Linarith.Var) →
            (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)) →
        motive p
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.eq_affineLocally' : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : outParam ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop)}
  [self : AlgebraicGeometry.HasRingHomProperty P Q],
  P = AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => Q
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.free_δ_freeMk : ∀ (R : Type u) [inst : CommRing R] {X Y : Type u} (z : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.OplaxMonoidal.δ (ModuleCat.free R) X Y))
      (ModuleCat.freeMk z) =
    ModuleCat.freeMk z.1 ⊗ₜ[R] ModuleCat.freeMk z.2
-- Std.Http.Protocol.H1.Reader
/-- The body-framing sub-state of the `Reader` state machine.
 -/
Std.Http.Protocol.H1.Reader.BodyState : Type
-- Mathlib.Analysis.Matrix.PosDef
/-- The pre-inner product space structure implementation. Only an auxiliary for
`Matrix.toSeminormedAddCommGroup`, `Matrix.toNormedAddCommGroup`,
and `Matrix.toInnerProductSpace`.  -/
_private.Mathlib.Analysis.Matrix.PosDef.0.Matrix.PosSemidef.preInnerProductSpace : {n : Type u_2} →
  {𝕜 : Type u_3} →
    [Fintype n] → [inst : RCLike 𝕜] → {M : Matrix n n 𝕜} → M.PosSemidef → PreInnerProductSpace.Core 𝕜 (n → 𝕜)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeletonLT_mono : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  {n m : ℕ∞}, m ≤ n → ↑(Topology.RelCWComplex.skeletonLT C m) ⊆ ↑(Topology.RelCWComplex.skeletonLT C n)
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast.match_1.eq_2 : ∀ {α : Type u_1} (motive : (x : List α) → x ≠ [] → Sort u_2) (a : α) (x : [a] ≠ []) (h_1 : (h : [] ≠ []) → motive [] h)
  (h_2 : (a : α) → (x : [a] ≠ []) → motive [a] x)
  (h_3 : (head b : α) → (as : List α) → (x : head :: b :: as ≠ []) → motive (head :: b :: as) x),
  (match [a], x with
    | [], h => h_1 h
    | [a], x => h_2 a x
    | head :: b :: as, x => h_3 head b as x) =
    h_2 a x
-- Mathlib.Data.Fin.SuccPred
Fin.exists_succAbove_eq_iff : ∀ {n : ℕ} {x y : Fin (n + 1)}, (∃ z, x.succAbove z = y) ↔ y ≠ x
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesFiniteProducts.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (n : ℕ), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin n)) F) →
    CategoryTheory.Limits.PreservesFiniteProducts F
-- Mathlib.Data.Nat.Nth
Nat.nth.eq_1 : ∀ (p : ℕ → Prop) (n : ℕ),
  Nat.nth p n =
    if h : (Set.ofPred p).Finite then (h.toFinset.sort fun a b => a ≤ b).getD n 0
    else ↑((Nat.Subtype.orderIsoOfNat (Set.ofPred p)) n)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_sup : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M) (x : M),
  x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x
-- Mathlib.Topology.Inseparable
Inseparable.map_of_continuousAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
  Inseparable x y → ContinuousAt f x → ContinuousAt f y → Inseparable (f x) (f y)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instDecompositionMonoid : ∀ {M : Type u_1} [inst : CommMonoid M] [DecompositionMonoid M], DecompositionMonoid (Associates M)
-- Mathlib.Topology.Sheaves.Skyscraper
/-- The cocone at `*` for the stalk functor of `skyscraperPresheaf p₀ A` when `y ∉ closure {p₀}` is a
colimit
 -/
skyscraperPresheafCoconeIsColimitOfNotSpecializes : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          (A : C) →
            [inst_2 : CategoryTheory.Limits.HasTerminal C] →
              {y : ↑X} → ¬p₀ ⤳ y → CategoryTheory.Limits.IsColimit (skyscraperPresheafCocone p₀ A y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α} {k : α},
  Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.unitOfList l) k = ()
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α} {v : β k}, (t.insertIfNew k v).getKey? a = if cmp k a = Ordering.eq ∧ k ∉ t then some k else t.getKey? a
-- Init.Data.BitVec.Lemmas
BitVec.xor_self : ∀ {w : ℕ} {x : BitVec w}, x ^^^ x = 0#w
-- Mathlib.Algebra.Category.MonCat.Basic
AddEquiv.toAddCommMonCatIso_inv : ∀ {X Y : Type u} [inst : AddCommMonoid X] [inst_1 : AddCommMonoid Y] (e : X ≃+ Y),
  e.toAddCommMonCatIso.inv = AddCommMonCat.ofHom e.symm.toAddMonoidHom
-- Init.Data.RArray
_private.Init.Data.RArray.0.Lean.RArray.get_eq_def.match_1.eq_2 : ∀ {α : Type u_1} (motive : Lean.RArray α → Sort u_2) (p : ℕ) (l r : Lean.RArray α)
  (h_1 : (x : α) → motive (Lean.RArray.leaf x))
  (h_2 : (p : ℕ) → (l r : Lean.RArray α) → motive (Lean.RArray.branch p l r)),
  (match Lean.RArray.branch p l r with
    | Lean.RArray.leaf x => h_1 x
    | Lean.RArray.branch p l r => h_2 p l r) =
    h_2 p l r
-- Mathlib.Data.Set.NAry
Set.image2_inter_union_subset_union : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β},
  Set.image2 f (s ∩ s') (t ∪ t') ⊆ Set.image2 f s t ∪ Set.image2 f s' t'
-- Mathlib.Topology.UniformSpace.Defs
uniformity_le_symm : ∀ {α : Type ua} [inst : UniformSpace α], uniformity α ≤ Filter.map Prod.swap (uniformity α)
-- Init.Data.UInt.Lemmas
UInt8.neg_mul_comm : ∀ (a b : UInt8), -a * b = a * -b
-- Lean.Parser.Types
Lean.Parser.Error.merge : Lean.Parser.Error → Lean.Parser.Error → Lean.Parser.Error
-- Lean.Parser.Command
Lean.Parser.Command.init_quot : Lean.Parser.Parser
-- Std.Time.Internal.Bounded
_private.Std.Time.Internal.Bounded.0.Int.tdiv.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.ofNat n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_3 m n
-- Mathlib.Analysis.Meromorphic.Basic
/-- Iterated derivatives of meromorphic functions are meromorphic.
 -/
MeromorphicAt.iterated_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {n : ℕ} {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → MeromorphicAt (deriv^[n] f) x