mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.forall_mem_adjoin_smul_eq_self_iff : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E} {M : Type u_3}
  [inst_3 : Monoid M] [inst_4 : MulSemiringAction M E] [SMulCommClass M F E] (m : M),
  (∀ x ∈ IntermediateField.adjoin F S, m • x = x) ↔ ∀ x ∈ S, m • x = x
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.mkUnknownMonadResult : Lean.MetaM Lean.Elab.Term.ExtractMonadResult
-- Mathlib.Data.List.Basic
List.replicate_subset_singleton : ∀ {α : Type u} (n : ℕ) (a : α), List.replicate n a ⊆ [a]
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
lt_two_mul_self : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a : R} [ZeroLEOneClass R] [MulPosStrictMono R] [NeZero 1]
  [AddLeftStrictMono R], 0 < a → a < 2 * a
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns `true` if the tree is empty.  -/
Std.DTreeMap.Internal.Impl.isEmpty : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Bool
-- Mathlib.Condensed.Discrete.Colimit
/-- `lanPresheaf (locallyConstantPresheaf X)` as a condensed set.  -/
Condensed.lanCondensedSet : Type (u + 1) → CondensedSet
-- Mathlib.Topology.Category.Profinite.CofilteredLimit
/-- If `X` is a cofiltered limit of profinite sets, then any clopen subset of `X` arises from
a clopen set in one of the terms in the limit.
 -/
Profinite.exists_isClopen_of_cofiltered : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J]
  {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {U : Set ↑C.pt.toTop}
  (hC : CategoryTheory.Limits.IsLimit C),
  IsClopen U → ∃ j V, IsClopen V ∧ U = ⇑(CategoryTheory.ConcreteCategory.hom (C.π.app j)) ⁻¹' V
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associatorNatIsoRight_inv_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d),
  (CategoryTheory.Bicategory.associatorNatIsoRight f g d).inv.app X = (CategoryTheory.Bicategory.associator f g X).inv
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
/-- Club sets in regular cardinals correspond one to one with normal functions.

See also `Order.isNormal_enum_iff_isClub`.  -/
Order.isNormal_enum_iff_dirSupClosed : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] {s : Set α}
  {hs : IsCofinal s}, Order.IsNormal (Subtype.val ∘ ⇑(Order.enum s hs)) ↔ DirSupClosed s
-- Mathlib.Tactic.LinearCombinationPrime
/-- A value, equivalently a proof of `c = c`.  -/
Mathlib.Tactic.LinearCombinationPrime.Expanded.const : Lean.Term → Mathlib.Tactic.LinearCombinationPrime.Expanded
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonDiagnosticWith.toJson : {α : Type} → [Lean.ToJson α] → Lean.Lsp.DiagnosticWith α → Lean.Json
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.ofSubtype.match_1.eq_2 : ∀
  (motive :
    (n : ℕ) →
      (α : TypeVec.{u_1} n) → (p : α.Arrow (TypeVec.repeat n Prop)) → (x : Fin2 n) → TypeVec.Subtype_ p x → Sort u_2)
  (n : ℕ) (α : TypeVec.{u_1} (n + 1)) (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) (x : TypeVec.Subtype_ p Fin2.fz)
  (h_1 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) →
          (i : Fin2 n) → (x : TypeVec.Subtype_ p i.fs) → motive (n + 1) α p i.fs x)
  (h_2 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) → (x : TypeVec.Subtype_ p Fin2.fz) → motive (n + 1) α p Fin2.fz x),
  (match n + 1, α, p, Fin2.fz, x with
    | .(n + 1), α, p, i.fs, x => h_1 n α p i x
    | .(n + 1), α, p, Fin2.fz, x => h_2 n α p x) =
    h_2 n α p x
-- Mathlib.Topology.QuasiSeparated
quasiSeparatedSpace_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (e : α ≃ₜ β),
  QuasiSeparatedSpace α ↔ QuasiSeparatedSpace β
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.Sign.instOrd : Ord Float.Model.UnpackedFloat.Sign
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.InteractiveMessage : Type
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instUniqueOfSubsingleton : {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] → [Subsingleton M] → Unique (LieSubmodule R L M)
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.prop_unit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [P.ContainsUnit], P (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinitary_E : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).E = E
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.Functor.IsPreFibered.exists_isCartesian' : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} [self : p.IsPreFibered] {a : 𝒳} {R : 𝒮} (f : R ⟶ p.obj a), ∃ b φ, p.IsCartesian f φ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.contains_alter_of_not_compare_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {f : Option β → Option β},
  ¬cmp k k' = Ordering.eq → (Std.ExtDTreeMap.Const.alter t k f).contains k' = t.contains k'
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.odd_of_ne_two : ∀ {p : ℕ}, Nat.Prime p → p ≠ 2 → Odd p
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.mul_op_ext_iff : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : AddZeroClass β] {f g : αᵐᵒᵖ →+ β},
  f = g ↔ f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {km : α}, t.minKey? = some km → t.getKey! km = km
-- Mathlib.NumberTheory.Divisors
Nat.sum_divisors_prime_pow : ∀ {α : Type u_1} [inst : AddCommMonoid α] {k p : ℕ} {f : ℕ → α},
  Nat.Prime p → ∑ x ∈ (p ^ k).divisors, f x = ∑ x ∈ Finset.range (k + 1), f (p ^ x)
-- Init.MetaTypes
Lean.Meta.instCoeListNatOccurrences : Coe (List ℕ) Lean.Meta.Occurrences
-- Init.Data.Iterators.Consumers.Loop
Std.instForMPartialOfIteratorLoopIdOfMonad : {m : Type x → Type x'} →
  {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → [Monad m] → ForM m (Std.Iter.Partial β) β
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariationFun.eq_1 : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) (s : Set X),
  MeasureTheory.preVariationFun f s = if h : MeasurableSet s then ⨆ P, ∑ p ∈ P.parts, f ↑p else 0
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.rnDeriv_conv : ∀ {G : Type u_3} [inst : AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] {ν₁ ν₂ : MeasureTheory.Measure G}
  [MeasureTheory.IsFiniteMeasure ν₁] [MeasureTheory.IsFiniteMeasure ν₂] [ν₁.HaveLebesgueDecomposition μ]
  [ν₂.HaveLebesgueDecomposition μ],
  ν₁.AbsolutelyContinuous μ →
    ν₂.AbsolutelyContinuous μ → (ν₁.conv ν₂).rnDeriv μ =ᵐ[μ] MeasureTheory.lconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ
-- Mathlib.Algebra.Order.Ring.Synonym
toDual_ofNat : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], OrderDual.toDual (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_imp_of_ae_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
  (∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ, x ∈ s → p x
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a : G), SkewMonoidAlgebra.single a 0 = 0
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_fixedBy : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α},
  a ∈ AddAction.fixedBy α m ↔ m +ᵥ a = a
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.sub_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m₁ m₂ : M) (n : N),
  (m₁ - m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n
-- Lean.Attributes
_private.Lean.Attributes.0.Lean.AttributeExtension.addImported : Array (Array Lean.AttributeExtensionOLeanEntry) → Lean.ImportM Lean.AttributeExtensionState
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- A `Submonoid` is either the trivial `Submonoid` or contains a nonzero element.  -/
Submonoid.bot_or_exists_ne_one : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), S = ⊥ ∨ ∃ x ∈ S, x ≠ 1
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.coe_zeroRootSubalgebra : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H],
  (LieAlgebra.zeroRootSubalgebra R L H).toSubmodule = ↑(LieAlgebra.rootSpace H 0)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The inf of an indexed family of orthogonal subspaces equals the
subspace orthogonal to the sup.  -/
Submodule.iInf_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} (K : ι → Submodule 𝕜 E), ⨅ i, (K i)ᗮ = (iSup K)ᗮ
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_zero : Real.sigmoid 0 = 2⁻¹
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalars_obj_carrier : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (A : AlgCat S),
  ↑((AlgCat.restrictScalars f).obj A) = ↑A
-- Mathlib.Computability.TuringMachine.Tape
/-- The `cons` and `head`/`tail` functions are mutually inverse, unlike in the case of `List` where
this only holds for nonempty lists.  -/
Turing.ListBlank.cons_head_tail : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : Turing.ListBlank Γ), Turing.ListBlank.cons l.head l.tail = l
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S}, f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_piCurry_symm : ∀ {ι : Type u_6} {κ : ι → Type u_7} {X : (i : ι) → κ i → Type u_8}
  [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)], Measurable ⇑(Equiv.piCurry X).symm
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is `π`, the last two points are not equal.  -/
EuclideanGeometry.right_ne_of_oangle_eq_pi : ∀ {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}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi → p₃ ≠ p₂
-- Lean.Meta.FunInfo
Lean.Meta.FunInfo.getArity : Lean.Meta.FunInfo → ℕ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Adj B} {α α' : a ⟶ b}
  (x : α ⟶ α') (β : b ⟶ c),
  (CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight x β).τl = CategoryTheory.Bicategory.whiskerRight x.τl β.l
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
/-- On a space with a discrete uniformity, any function is uniformly continuous.  -/
DiscreteUniformity.uniformContinuous : ∀ (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] {Y : Type u_2} [inst : UniformSpace Y] (f : X → Y),
  UniformContinuous f
-- Mathlib.Order.Atoms
/-- **Alias** of `IsSimpleOrder.eq_top_of_lt`. -/
LT.lt.eq_top : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α] {a b : α}, a < b → b = ⊤
-- Init.Data.UInt.Lemmas
UInt8.ofNatClamp_eq_ofNat : ∀ n < UInt8.size, UInt8.ofNatClamp n = UInt8.ofNat n
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- The inclusion of a full subcategory is fully faithful.  -/
CategoryTheory.ObjectProperty.fullyFaithfulι : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (P : CategoryTheory.ObjectProperty C) → P.ι.FullyFaithful
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.updateCell.match_5.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (l : Std.DTreeMap.Internal.Impl α β) → l.Balanced → Sort u_3) (sz : ℕ)
  (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
  (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced)
  (h_1 : (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hl)
  (h_2 :
    (sz : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl),
  (match Std.DTreeMap.Internal.Impl.inner sz ky y l r, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl => h_1 hl
    | Std.DTreeMap.Internal.Impl.inner sz ky y l r, hl => h_2 sz ky y l r hl) =
    h_2 sz ky y l r hl
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isEmpty_filter_eq_true : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst p.snd) l).isEmpty = true ↔
      ∀ (k : α) (h : Std.Internal.List.containsKey k l = true),
        f (Std.Internal.List.getKey k l h) (Std.Internal.List.getValue k l h) = false)
-- Mathlib.RingTheory.Finiteness.Nilpotent
Matrix.isNilpotent_iff_forall_row : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {A : Matrix ι ι R}, IsNilpotent A ↔ ∀ (i : ι), ∃ n, (A ^ n).row i = 0
-- Lean.Elab.Syntax
Lean.Elab.Command.inferMacroRulesAltKind : Lean.TSyntax `Lean.Parser.Term.matchAlt → Lean.Elab.Command.CommandElabM Lean.SyntaxNodeKind
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.sSupFun_strictMono : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} [IsOrderedAddMonoid R]
  {c : Set (HahnEmbedding.Partial seed)},
  c.Nonempty → ∀ (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c), StrictMono ↑(HahnEmbedding.Partial.sSupFun hc)
-- Mathlib.Algebra.Group.Basic
eq_sub_iff_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a = b - c ↔ a + c = b
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyonedaForget_hom_app_app_hom_apply_hom : ∀ (X : CommMonCatᵒᵖ) (X_1 : CommMonCat) (f : ↑(Opposite.unop X) →* ↑X_1),
  CommMonCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((CommMonCat.coyonedaForget.hom.app X).app X_1)) f) = f
-- Init.Data.SInt.Lemmas
UInt32.toInt32_neg : ∀ (a : UInt32), (-a).toInt32 = -a.toInt32
-- Mathlib.Analysis.Convex.Deriv
StrictMonoOn.exists_slope_lt_deriv_aux : ∀ {x y : ℝ} {f : ℝ → ℝ},
  ContinuousOn f (Set.Icc x y) →
    x < y →
      StrictMonoOn (deriv f) (Set.Ioo x y) →
        (∀ w ∈ Set.Ioo x y, deriv f w ≠ 0) → ∃ a ∈ Set.Ioo x y, (f y - f x) / (y - x) < deriv f a
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.resolveLValAux.throwInvalidFieldAt : Lean.Expr →
  Lean.Expr →
    {α : Type} → Lean.Syntax → String → Lean.Name → optParam Lean.Name Lean.Name.anonymous → Lean.Elab.TermElabM α
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.pi_injective : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {γ : Type w} [Nonempty I] [inst_2 : Mul γ]
  (g : (i : I) → γ →ₙ* f i), (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(MulHom.pi g)
-- Lean.Server.Requests
_private.Lean.Server.Requests.0.Lean.Server.RequestM.findCmdParsedSnap.isAfterHoverPos : String.Pos.Raw → Lean.Language.Lean.CommandParsedSnapshot → Bool
-- Mathlib.Data.DFinsupp.Defs
/-- Equality of sigma types is sufficient (but not necessary) to show equality of `DFinsupp`s.  -/
DFinsupp.single_eq_of_sigma_eq : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i j : ι} {xi : β i} {xj : β j},
  ⟨i, xi⟩ = ⟨j, xj⟩ → (fun₀ | i => xi) = fun₀ | j => xj
-- Batteries.Data.Fin.Lemmas
Fin.eq_false_of_isNone_find? : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, (Fin.find? p).isNone = true → p i = false
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that `|v - Aₙ / Bₙ| ≤ 1 / (bₙ * Bₙ * Bₙ)`. This bound is worse than the one shown in
`GenContFract.abs_sub_convs_le`, but sometimes it is easier to apply and
sufficient for one's use case.
 -/
GenContFract.abs_sub_convergents_le' : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {b : K},
  (GenContFract.of v).partDens.get? n = some b →
    |v - (GenContFract.of v).convs n| ≤ 1 / (b * (GenContFract.of v).dens n * (GenContFract.of v).dens n)
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.le_infsep : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} {d : ℝ},
  s.Nontrivial → (∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y) → d ≤ s.infsep
-- Mathlib.LinearAlgebra.Matrix.FiniteDimensional
Matrix.finiteDimensional : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} [inst : Field R] [Finite m] [Finite n], FiniteDimensional R (Matrix m n R)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.shrink.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → Array α → Sort u_2) →
    (x : ℕ) →
      (x_1 : Array α) → ((xs : Array α) → motive 0 xs) → ((n : ℕ) → (xs : Array α) → motive n.succ xs) → motive x x_1
-- Init.Prelude
/-- A byte array is valid UTF-8 if it is of the form `List.Internal.utf8Encode m` for some `m`.

Note that in order for this definition to be well-behaved it is necessary to know that this `m`
is unique. To show this, one defines UTF-8 decoding and shows that encoding and decoding are
mutually inverse.  -/
ByteArray.IsValidUTF8 : ByteArray → Prop
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ext_of_isAffine : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] {I J : X.IdealSheafData},
  I.ideal ⟨⊤, ⋯⟩ = J.ideal ⟨⊤, ⋯⟩ → I = J
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_cast_Ioc : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.image (Fin.cast h) (Finset.Ioc i j) = Finset.Ioc (Fin.cast h i) (Fin.cast h j)
-- Std.Http.Protocol.H1.Writer
/-- The message head has been provided; waiting for `shouldFlush` to become true before
serializing headers to output.
 -/
Std.Http.Protocol.H1.Writer.State.waitingForFlush : Std.Http.Protocol.H1.Writer.State
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_hom_right_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ)
  (X_1 : SimplexCategory), X.leftOpRightOpIso.hom.right.app X_1 = CategoryTheory.CategoryStruct.id (X.right.obj X_1)
-- Init.Data.List.Scan.Basic
/-- Fold a function `f` over the list from the left, returning the list of partial results.
```
scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]
```
 -/
List.scanl : {β : Type u_1} → {α : Type u_2} → (β → α → β) → β → List α → List β
-- Mathlib.Topology.Germ
Filter.Germ.isConstant_comp_subtype : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {s : Set X} {f : X → Y} {x : ↑s},
  (↑f).IsConstant → (↑(f ∘ Subtype.val)).IsConstant
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimInfo.mk.inj : ∀ {elimExpr elimType : Lean.Expr} {motivePos : ℕ} {targetsPos : Array ℕ} {altsInfo : Array Lean.Meta.ElimAltInfo}
  {numComplexMotiveArgs : ℕ} {elimExpr_1 elimType_1 : Lean.Expr} {motivePos_1 : ℕ} {targetsPos_1 : Array ℕ}
  {altsInfo_1 : Array Lean.Meta.ElimAltInfo} {numComplexMotiveArgs_1 : ℕ},
  { elimExpr := elimExpr, elimType := elimType, motivePos := motivePos, targetsPos := targetsPos, altsInfo := altsInfo,
        numComplexMotiveArgs := numComplexMotiveArgs } =
      { elimExpr := elimExpr_1, elimType := elimType_1, motivePos := motivePos_1, targetsPos := targetsPos_1,
        altsInfo := altsInfo_1, numComplexMotiveArgs := numComplexMotiveArgs_1 } →
    elimExpr = elimExpr_1 ∧
      elimType = elimType_1 ∧
        motivePos = motivePos_1 ∧
          targetsPos = targetsPos_1 ∧ altsInfo = altsInfo_1 ∧ numComplexMotiveArgs = numComplexMotiveArgs_1
-- Mathlib.Algebra.Regular.Basic
/-- An element admitting a left additive opposite is add-left-regular.  -/
isAddLeftRegular_of_add_eq_zero : ∀ {R : Type u_1} [inst : AddMonoid R] {a b : R}, b + a = 0 → IsAddLeftRegular a
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.isType2Type : Lean.Expr → Lean.MetaM Bool
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.mk.inj : ∀ {description : Unit → Lean.MessageData} {m : Lean.Elab.Do.DoElabM Lean.Expr}
  {stM runInBase : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr}
  {restoreCont : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont}
  {description_1 : Unit → Lean.MessageData} {m_1 : Lean.Elab.Do.DoElabM Lean.Expr}
  {stM_1 runInBase_1 : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr}
  {restoreCont_1 : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont},
  { description := description, m := m, stM := stM, runInBase := runInBase, restoreCont := restoreCont } =
      { description := description_1, m := m_1, stM := stM_1, runInBase := runInBase_1, restoreCont := restoreCont_1 } →
    description = description_1 ∧ m = m_1 ∧ stM = stM_1 ∧ runInBase = runInBase_1 ∧ restoreCont = restoreCont_1
-- Init.Data.BitVec.Lemmas
BitVec.toInt_le : ∀ {w : ℕ} {x : BitVec w}, x.toInt ≤ 2 ^ (w - 1) - 1
-- Mathlib.MeasureTheory.Measure.Map
/-- If `map f μ = μ`, then the measure of the preimage of any null measurable set `s`
is equal to the measure of `s`.
Note that this lemma does not assume (a.e.) measurability of `f`.  -/
MeasureTheory.Measure.measure_preimage_of_map_eq_self : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → α},
  MeasureTheory.Measure.map f μ = μ → ∀ {s : Set α}, MeasureTheory.NullMeasurableSet s μ → μ (f ⁻¹' s) = μ s
-- Mathlib.Analysis.Convex.Gauge
gauge_le_one_of_mem : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E}, x ∈ s → gauge s x ≤ 1
-- Init.Data.Array.Lemmas
Array.self_eq_append_left : ∀ {α : Type u_1} {xs ys : Array α}, ys = xs ++ ys ↔ xs = #[]
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rcc_eq_none_iff : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toList[i]? = none ↔ (n + 1 - m).toNat ≤ i
-- Mathlib.Logic.Equiv.Defs
Equiv.permCongr_apply : ∀ {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Equiv.Perm α') (x : β'), (e.permCongr p) x = e (p (e.symm x))
-- Mathlib.Order.SuccPred.Limit
/-- A successor pre-limit is a value that doesn't cover any other.

It's so named because in a successor order, a successor pre-limit can't be the successor of anything
smaller.

Use `IsSuccLimit` if you want to exclude the case of a minimal element.  -/
Order.IsSuccPrelimit : {α : Type u_1} → [LT α] → α → Prop