mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.PersistentArray
Lean.PersistentArray.insertNewLeaf : {α : Type u} → Lean.PersistentArrayNode α → USize → USize → Array α → Lean.PersistentArrayNode α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∉ t₂ → (t₁ \ t₂).getKey! k = t₁.getKey! k
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.node.injEq : ∀ {α : Type u} (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (size_1 : ℕ) (l_1 : Ordnode α) (x_1 : α)
  (r_1 : Ordnode α),
  (Ordnode.node size l x r = Ordnode.node size_1 l_1 x_1 r_1) = (size = size_1 ∧ l = l_1 ∧ x = x_1 ∧ r = r_1)
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits : ∀ {p : ℕ} (n : ℕ), (p - 1) * ∑ i ∈ Finset.range (Nat.log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result.success.sizeOf_spec : sizeOf Std.Tactic.BVDecide.LRAT.Internal.Result.success = 1
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.mergeSort.match_1.splitter : {α : Type u_1} →
  (motive : List α → (α → α → Bool) → Sort u_2) →
    (x : List α) →
      (x_1 : α → α → Bool) →
        ((x : α → α → Bool) → motive [] x) →
          ((a : α) → (x : α → α → Bool) → motive [a] x) →
            ((a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le) → motive x x_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.throwUnexpected : {α : Type} → Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.GoalM α
-- Init.Data.List.TakeDrop
List.take_succ : ∀ {α : Type u_1} {l : List α} {i : ℕ}, List.take (i + 1) l = List.take i l ++ l[i]?.toList
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- The (bundled version of) coefficient of the limit `q` of the
inductively constructed sequence `qₖ` in the proof of Weierstrass division.  -/
PowerSeries.IsWeierstrassDivisorAt.divCoeff : {A : Type u_1} →
  [inst : CommRing A] →
    {g : PowerSeries A} →
      {I : Ideal A} →
        (H : g.IsWeierstrassDivisorAt I) →
          (f : PowerSeries A) →
            [IsPrecomplete I A] → (i : ℕ) → { x // ∀ (n : ℕ), (PowerSeries.coeff i) (H.seq f n) ≡ x [SMOD I ^ n • ⊤] }
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist.match_1.splitter : {X : Type u_1} →
  {Y : Type u_2} →
    (motive : X ⊕ Y → X ⊕ Y → Sort u_3) →
      (x x_1 : X ⊕ Y) →
        ((x y : X) → motive (Sum.inl x) (Sum.inl y)) →
          ((x y : Y) → motive (Sum.inr x) (Sum.inr y)) →
            ((x : X) → (y : Y) → motive (Sum.inl x) (Sum.inr y)) →
              ((x : Y) → (y : X) → motive (Sum.inr x) (Sum.inl y)) → motive x x_1
-- Mathlib.Algebra.Tropical.Basic
Tropical.inf_eq_add : ∀ {R : Type u} [inst : LinearOrder R], (fun x1 x2 => min x1 x2) = fun x1 x2 => x1 + x2
-- Mathlib.LinearAlgebra.RootSystem.Basic
RootPairing.isRootSystem_mk'' : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Finite ι]
  {k : Type u_5} [inst_3 : Field k] [inst_4 : CharZero k] [inst_5 : Module k M] [inst_6 : Module k N]
  {p : M →ₗ[k] N →ₗ[k] k} [inst_7 : p.IsPerfPair] {root : ι ↪ M} {coroot : ι ↪ N}
  {hp : ∀ (i : ι), (p (root i)) (coroot i) = 2}
  {hs :
    ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)}
  {hsp : Submodule.span k (Set.range ⇑root) = ⊤},
  (∀ (i j : ι), ∃ z, ↑z = (p (root i)) (coroot j)) → (RootPairing.mk'' p root coroot hp hs hsp).IsRootSystem
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_coe' : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f : NormedAddGroupHom G H) (g : G), UniformSpace.Completion.map ⇑f ↑g = ↑(f g)
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_lt_iff_lt_left : ∀ {a b c : ENNReal}, b ≠ ⊤ → b ≤ a → (a - b < c ↔ a < b + c)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isSome_maxKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {f : β → β}, t.WF → (Std.DTreeMap.Raw.Const.modify t k f).maxKey?.isSome = !t.isEmpty
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_dvd_of_mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G}, y ∈ AddSubgroup.zmultiples x → addOrderOf y ∣ addOrderOf x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.darts_ofDarts : ∀ {V : Type u} {G : SimpleGraph V} {l : List G.Dart} (hne : l ≠ []) (hchain : List.IsChain G.DartAdj l),
  (SimpleGraph.Walk.ofDarts l hne hchain).darts = l
-- Lean.Meta.Tactic.Apply
Lean.Meta.appendParentTag : Lean.MVarId → Array Lean.Expr → Array Lean.BinderInfo → Lean.MetaM Unit
-- Mathlib.Topology.UniformSpace.Basic
Uniform.tendsto_nhds_right : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {f : Filter β} {u : β → α} {a : α},
  Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (a, u x)) f (uniformity α)
-- Init.Data.UInt.Lemmas
UInt64.toUSize_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n →
    (UInt64.ofNatClamp n).toUSize = USize.ofNatLT (USize.size - 1) UInt64.toUSize_ofNatClamp_of_le._proof_1
-- Batteries.Data.Fin.Basic
/-- Heterogeneous fold over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`, where
`f 2 : α 3 → α 2`, `f 1 : α 2 → α 1`, etc.

This is the dependent version of `Fin.foldr`.  -/
Fin.dfoldr : (n : ℕ) → (α : Fin (n + 1) → Type u_1) → ((i : Fin n) → α i.succ → α i.castSucc) → α (Fin.last n) → α 0
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestSeqCore : Array Lean.Syntax → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertMany_append : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {l₁ l₂ : List (α × β)},
  m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
-- Lean.Linter.Init
Lean.Linter.LinterOptions.toOptions : Lean.Linter.LinterOptions → Lean.Options
-- Mathlib.Order.Hom.Basic
le_map_inv_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : EquivLike F α β]
  [OrderIsoClass F α β] (f : F) {a : α} {b : β}, a ≤ EquivLike.inv f b ↔ f a ≤ b
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The unit incidence algebra is the delta function, whose entries are `0` except on the diagonal
where they are `1`.  -/
IncidenceAlgebra.instOne : {𝕜 : Type u_2} →
  {α : Type u_5} → [inst : Preorder α] → [DecidableEq α] → [inst_2 : Zero 𝕜] → [One 𝕜] → One (IncidenceAlgebra 𝕜 α)
-- Qq.Match
_private.Qq.Match.0.Qq.buildPatternTerm : Lean.Term → Lean.Term → Lean.Term → Lean.MacroM Lean.Term
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.instMonoHomOfLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (N₁ N₂ : M.Submodule) (hle : N₁ ≤ N₂),
  CategoryTheory.Mono (PresheafOfModules.Submodule.homOfLE hle)
-- Mathlib.Combinatorics.Additive.FreimanHom
AddHomClass.isAddFreimanHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α}
  {B : Set β} {n : ℕ} [inst_2 : FunLike F α β] [AddHomClass F α β] (f : F),
  Set.MapsTo (⇑f) A B → IsAddFreimanHom n A B ⇑f
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_himp : ∀ {V : Type u} {G : SimpleGraph V} [inst : Finite V] (G₁ G₂ : G.Finsubgraph), ↑(G₁ ⇨ G₂) = ↑G₁ ⇨ ↑G₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {fallback : α} {hc : t.minKeyD fallback ∈ t}, t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Push forward the multiplication of `R` on `M` along a compatible surjective map `f : R → S`.

See also `Function.Surjective.distribMulActionLeft`.
 -/
Function.Surjective.distribSMulLeft : {R : Type u_12} →
  {S : Type u_13} →
    {M : Type u_14} →
      [inst : AddZeroClass M] →
        [inst_1 : DistribSMul R M] →
          [inst_2 : SMul S M] →
            (f : R → S) → Function.Surjective f → (∀ (c : R) (x : M), f c • x = c • x) → DistribSMul S M
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.height_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)), (s.reindex e).height = s.height ∘ ⇑e.symm
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.add_iff_left : ∀ {𝕜 : 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 g : E → F}
  {x : E}, DifferentiableAt 𝕜 g x → (DifferentiableAt 𝕜 (f + g) x ↔ DifferentiableAt 𝕜 f x)
-- Mathlib.Order.Notation
Bot.ext_iff : ∀ {α : Type u_1} {x y : Bot α}, x = y ↔ ⊥ = ⊥
-- Mathlib.Order.MinMax
max_lt_max : ∀ {α : Type u} [inst : LinearOrder α] {a b c d : α}, a < c → b < d → max a b < max c d
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquiv_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {Q : Type u_4} [inst_4 : CommSemiring Q] [inst_5 : Algebra R Q]
  [inst_6 : IsLocalization M Q] (x : R) (y : ↥M),
  (IsLocalization.algEquiv M S Q) (IsLocalization.mk' S x y) = IsLocalization.mk' Q x y
-- Mathlib.MeasureTheory.Measure.Hausdorff
Isometry.hausdorffMeasure_image : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {f : X → Y} {d : ℝ},
  Isometry f →
    0 ≤ d ∨ Function.Surjective f →
      ∀ (s : Set X), (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) = (MeasureTheory.Measure.hausdorffMeasure d) s
-- Mathlib.RingTheory.HahnSeries.Summable
/-- **Alias** of `HahnSeries.SummableFamily.embDomain_of_notMem_range`. -/
HahnSeries.SummableFamily.embDomain_notin_range : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {b : β}, b ∉ Set.range ⇑f → (s.embDomain f) b = 0
-- Init.Data.List.Lemmas
List.map_eq_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {b : β}, List.map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integrable_bilin : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁] [inst_5 : NormedSpace 𝕜 F₁]
  [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {μ : MeasureTheory.Measure E}
  {φ : E → F₂},
  MeasureTheory.IntegrableOn φ (↑K) μ →
    ∀ (f : ContDiffMapSupportedIn E F₁ n K), MeasureTheory.Integrable (fun x => (B (f x)) (φ x)) μ
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.det_ne_zero_of_right_inverse : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α}
  [Nontrivial α], A * B = 1 → A.det ≠ 0
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snocEquiv_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) (f : α (Fin.last n) × ((i : Fin n) → α i.castSucc)) (x : Fin (n + 1)),
  (Fin.snocEquiv α) f x = Fin.snoc f.2 f.1 x
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- This is a variant of integer exponentiation, defined for internal use in the `field_simp` tactic
implementation. It differs from the usual integer exponentiation in that `0 ^ 0` is `0`, not `1`.
With this choice, the function `n ↦ a ^ n` is always a homomorphism (`a ^ (n + m) = a ^ n * a ^ m`),
even if `a` is zero.  -/
Mathlib.Tactic.FieldSimp.zpow' : {α : Type u_1} → [GroupWithZero α] → α → ℤ → α
-- Lean.Declaration
Lean.InductiveVal.isUnsafeEx : Lean.InductiveVal → Bool
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeOp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F),
  CategoryTheory.Functor.mapConeOp G t =
    CategoryTheory.Limits.Cocone.ext (CategoryTheory.Iso.refl (G.mapCone t).op.pt) ⋯
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.map_ne : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) {x y : E}, x ≠ y → e x ≠ e y
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
BitVec.reduceShiftRightShiftRight : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.Analytic.Constructions
Units.ofNearby.congr_simp : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (x x_1 : Rˣ) (e_x : x = x_1) (y y_1 : R)
  (e_y : y = y_1) (h : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹), x.ofNearby y h = x_1.ofNearby y_1 ⋯
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.uncurry_pullbackArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (s : CategoryTheory.Presieve X)
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] {B : C} (b : B ⟶ X),
  (CategoryTheory.Presieve.pullbackArrows b s).uncurry =
    (fun f => ⟨CategoryTheory.Limits.pullback f.snd b, CategoryTheory.Limits.pullback.snd f.snd b⟩) '' s.uncurry
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] (X : C₁),
  CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app X)
      (F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) =
    DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app X)
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_lt_iff_lt : ∀ {a b : ℕ} (ha : a < UInt32.size) (hb : b < UInt32.size), UInt32.ofNatLT a ha < UInt32.ofNatLT b hb ↔ a < b
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.latticeBasis.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.latticeBasis K = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₁ = f.f₀.τ₃
-- Mathlib.GroupTheory.OrderOfElement
RightCancelMonoid.injective_pow_iff_not_isOfFinOrder : ∀ {G : Type u_1} [inst : RightCancelMonoid G] {x : G}, (Function.Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_sub_int : ∀ (f : CircleDeg1Lift) (x : ℝ) (n : ℤ), f (x - ↑n) = f x - ↑n
-- Mathlib.Order.KrullDimension
/-- The elements of height zero are the minimal elements.  -/
Order.height_eq_zero : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.height x = 0 ↔ IsMin x
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.getSimpTheorems : Lean.Meta.SimpM Lean.Meta.SimpTheoremsArray
-- Mathlib.Algebra.Order.Group.Cone
instPartialOrderAddGroupCone : (G : Type u_1) → [inst : AddCommGroup G] → PartialOrder (AddGroupCone G)
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varsToConstants.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} {γ : Type u_4} (motive : L.Term (γ ⊕ α) → Sort u_5) (a : α)
  (h_1 : (a : α) → motive (FirstOrder.Language.var (Sum.inr a)))
  (h_2 : (c : γ) → motive (FirstOrder.Language.var (Sum.inl c)))
  (h_3 : (l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term (γ ⊕ α)) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.var (Sum.inr a) with
    | FirstOrder.Language.var (Sum.inr a) => h_1 a
    | FirstOrder.Language.var (Sum.inl c) => h_2 c
    | FirstOrder.Language.func f ts => h_3 l f ts) =
    h_1 a
-- Mathlib.Analysis.SpecificLimits.Normed
instHasSummableGeomSeriesOfCompleteSpace : ∀ {R : Type u_4} [inst : NormedRing R] [CompleteSpace R], HasSummableGeomSeries R
-- Mathlib.Data.List.Chain
List.IsChain.drop : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.IsChain R l → ∀ (n : ℕ), List.IsChain R (List.drop n l)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.inv.eq_1 : ∀ (m : Tactic.ComputeAsymptotics.UnitMonomial), m.inv = List.map (fun x => -x) m
-- Mathlib.Analysis.Convex.EGauge
div_le_egauge_ball : ∀ (𝕜 : Type u_1) [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (r : NNReal) (x : E), ‖x‖ₑ / ↑r ≤ egauge 𝕜 (Metric.ball 0 ↑r) x
-- Mathlib.FieldTheory.Separable
/-- If a non-zero polynomial over `F` splits in `K`, then it has no repeated roots on `K`
if and only if it is separable.  -/
Polynomial.nodup_aroots_iff_of_splits : ∀ {F : Type u} [inst : Field F] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra F K] {f : Polynomial F},
  f ≠ 0 → (Polynomial.map (algebraMap F K) f).Splits → ((f.aroots K).Nodup ↔ f.Separable)
-- Mathlib.MeasureTheory.Integral.MeanInequalities
/-- Hölder's inequality in case of finite non-zero integrals  -/
ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → ENNReal},
      AEMeasurable f μ →
        ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤ →
          ∫⁻ (a : α), g a ^ q ∂μ ≠ ⊤ →
            ∫⁻ (a : α), f a ^ p ∂μ ≠ 0 →
              ∫⁻ (a : α), g a ^ q ∂μ ≠ 0 →
                ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
-- Lean.Compiler.InitAttr
Lean.getInitFnNameForCore? : Lean.Environment → Lean.ParametricAttribute Lean.Name → Lean.Name → Option Lean.Name
-- Mathlib.Order.Filter.Prod
Filter.coprod_neBot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β},
  (f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.map.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasCokernel f'] (p p_1 : X ⟶ X') (e_p : p = p_1) (q q_1 : Y ⟶ Y') (e_q : q = q_1)
  (w : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f'),
  CategoryTheory.Limits.cokernel.map f f' p q w = CategoryTheory.Limits.cokernel.map f f' p_1 q_1 ⋯
-- Mathlib.Data.Multiset.Fintype
Multiset.mem_of_mem_toEnumFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {p : α × ℕ}, p ∈ m.toEnumFinset → p.1 ∈ m
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C), S.Exact ↔ CategoryTheory.IsIso (imageToKernel' S.f S.g ⋯)
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.ringEquiv.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : (i : ι) → CommRing (G i)]
  (f' : (i j : ι) → i ≤ j → G i →+* G j) [inst_2 : DirectedSystem G fun i j h => ⇑(f' i j h)]
  [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι], Ring.DirectLimit.ringEquiv G f' = Ring.DirectLimit.ringEquiv G f'
-- Mathlib.Order.SuccPred.InitialSeg
PrincipalSeg.apply_covBy_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {a b : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α <i β),
  f.toRelEmbedding a ⋖ f.toRelEmbedding b ↔ a ⋖ b
-- Init.Data.SInt.Lemmas
Int64.toInt_maxValue_add_one : Int64.maxValue.toInt + 1 = 2 ^ 63
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rcc : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toArray[i]? = if i < (n + 1 - m).toNat then some (m + ↑i) else none
-- Mathlib.RingTheory.SimpleModule.Isotypic
mem_fullyInvariantSubmodule_iff : ∀ {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {m : Submodule R M}, m ∈ fullyInvariantSubmodule R M ↔ m.IsFullyInvariant
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.constantBaseRingEquiv_tprod : ∀ {ι : Type u_1} {R : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype ι] (x : ι → R),
  (PiTensorProduct.constantBaseRingEquiv ι R) ((PiTensorProduct.tprod R) x) = ∏ i, x i
-- Mathlib.CategoryTheory.Bicategory.Coherence
_private.Mathlib.CategoryTheory.Bicategory.Coherence.0.CategoryTheory.FreeBicategory.inclusionPathAux.match_1.splitter : {B : Type u_2} →
  [inst : Quiver B] →
    {a : B} →
      (motive : (x : B) → Quiver.Path a x → Sort u_3) →
        (x : B) →
          (x_1 : Quiver.Path a x) →
            (Unit → motive a Quiver.Path.nil) →
              ((x b : B) → (p : Quiver.Path a b) → (f : b ⟶ x) → motive x (p.cons f)) → motive x x_1
-- Init.Core
UInt64.ofBitVec.inj : ∀ {toBitVec toBitVec_1 : BitVec 64}, { toBitVec := toBitVec } = { toBitVec := toBitVec_1 } → toBitVec = toBitVec_1
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_npow' : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a : ℚ},
  ↑a.den ≠ 0 → ∀ (n : ℕ), Lean.Grind.Field.NormNum.ofRat (a ^ n) = Lean.Grind.Field.NormNum.ofRat a ^ n
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- **Alias** of `MeasureTheory.eLpNorm_mono_enorm_ae`. -/
MeasureTheory.eLpNorm_mono_ae' : ∀ {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : ENorm ε] [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
-- Mathlib.Geometry.Manifold.Immersion
/-- A function `f : M → N` between `C^n` manifolds is `C^n` if and only if it is continuous
and its composition `φ ∘ f` with a `C^n` immersion `φ : N → N'` is `C^n`.  -/
ContMDiff.iff_comp_isImmersion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E''' : Type u_4} {E'' : Type u}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup E'''] [inst_6 : NormedSpace 𝕜 E'''] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {G' : Type u_10}
  [inst_9 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G}
  {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M]
  {N : Type u_13} [inst_12 : TopologicalSpace N] [inst_13 : ChartedSpace G N] {N' : Type u_14}
  [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N} {φ : N → N'},
  Manifold.IsImmersion J J' n φ → (ContMDiff I J n f ↔ Continuous f ∧ ContMDiff I J' n (φ ∘ f))