mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
exists_nonneg_add_of_le : ∀ {α : Type u} [inst : AddZeroClass α] [inst_1 : Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftReflectLE α],
  a ≤ b → ∃ c, 0 ≤ c ∧ a + c = b
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.eq_false : ∀ (a : Bool), ((a = true) = False) = ((!a) = true)
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
Finset.smul_prod : ∀ {M : Type u_1} {N : Type u_2} {ι : Type u_4} [inst : CommMonoid N] [inst_1 : Monoid M] [inst_2 : MulAction M N]
  [IsScalarTower M N N] [SMulCommClass M N N] (s : Finset ι) (b : M) (f : ι → N),
  b ^ s.card • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x
-- Init.NotationExtra
Lean.calcFirstStep : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precompose_obj_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : G ⟶ F) (c : CategoryTheory.Limits.Cocone F),
  ((CategoryTheory.Limits.Cocone.precompose α).obj c).ι = CategoryTheory.CategoryStruct.comp α c.ι
-- Batteries.Data.DList.Lemmas
Batteries.DList.cons.eq_1 : ∀ {α : Type u} (x : α) (f : List α → List α) (h : ∀ (l : List α), f l = f [] ++ l),
  Batteries.DList.cons x { apply := f, invariant := h } = { apply := fun t => x :: f t, invariant := ⋯ }
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.st_mul : ∀ {x y : ℝ*}, ¬x.Infinite → ¬y.Infinite → (x * y).st = x.st * y.st
-- Mathlib.CategoryTheory.Discrete.Basic
/-- The discrete functor induced by a composition of maps can be written as a
composition of two discrete functors.
 -/
CategoryTheory.Discrete.functorComp : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {I : Type u₁} →
      {J : Type u₁'} →
        (f : J → C) →
          (g : I → J) →
            CategoryTheory.Discrete.functor (f ∘ g) ≅
              (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ g)).comp
                (CategoryTheory.Discrete.functor f)
-- Mathlib.Data.Set.Functor
Set.pure_def : ∀ {α : Type u} (a : α), pure a = {a}
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- Any linear equiv between `Rⁿ` and `Rᵐ` guarantees `m = n`.  -/
InvariantBasisNumber.eq_of_fin_equiv : ∀ {R : Type u} {inst : Semiring R} [self : InvariantBasisNumber R] {n m : ℕ} (a : (Fin n → R) ≃ₗ[R] Fin m → R), n = m
-- Mathlib.Analysis.Analytic.Composition
/-- Change of variables appearing to compute the composition of partial sums of formal
power series  -/
FormalMultilinearSeries.compChangeOfVariables : (m M N : ℕ) →
  (i : (n : ℕ) × (Fin n → ℕ)) → i ∈ FormalMultilinearSeries.compPartialSumSource m M N → (n : ℕ) × Composition n
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx?.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → Sort u_3) (x : ℕ)
  (h_1 : (x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) → (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n),
  (match Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.leaf, x => h_1 x
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n => h_2 size k v l r n) =
    h_1 x
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [inst_4 : CategoryTheory.Category.{v_7, u_7} E]
  (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (X_1 : C₁) (X_2 : C₂),
  (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X_1).obj X_2 =
    (X.obj (F₁.obj X_1)).obj (F₂.obj X_2)
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectSuccessorOf.below : {α β : Type w} →
  {m : Type w → Type w'} →
    [inst : Std.Iterator α m β] →
      {a : Std.IterM m β} →
        {motive : (a_1 : Std.IterM m β) → a.IsPlausibleIndirectSuccessorOf a_1 → Prop} →
          {a_1 : Std.IterM m β} → a.IsPlausibleIndirectSuccessorOf a_1 → Prop
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The universal property of the direct limit: maps from the components to another ring
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit.
 -/
DirectLimit.Ring.lift : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → NonAssocSemiring (G i)] →
                  [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] →
                    [inst_6 : Nonempty ι] →
                      (P : Type u_7) →
                        [inst_7 : NonAssocSemiring P] →
                          (g : (i : ι) → G i →+* P) →
                            (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) →
                              DirectLimit G f →+* P
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size_combine : ∀ {α : Type u_1} (le : α → α → Bool) (s : Batteries.PairingHeapImp.Heap α),
  (Batteries.PairingHeapImp.Heap.combine le s).size = s.size
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.not_dvd_of_natDegree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → q ≠ 0 → q.natDegree < p.natDegree → ¬p ∣ q
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.homMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (f : X.obj ⟶ Y.obj), (CategoryTheory.ObjectProperty.homMk f).hom = f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_addX : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P Q : Fin 3 → R), (W'.map f).addX (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₄.fun_cases_unfolding : ∀ (w x y z : UInt8) (motive : Option Char → Prop),
  ((ByteArray.utf8DecodeChar?.isInvalidContinuationByte x || ByteArray.utf8DecodeChar?.isInvalidContinuationByte y ||
          ByteArray.utf8DecodeChar?.isInvalidContinuationByte z) =
        true →
      motive none) →
    (¬(ByteArray.utf8DecodeChar?.isInvalidContinuationByte x || ByteArray.utf8DecodeChar?.isInvalidContinuationByte y ||
              ByteArray.utf8DecodeChar?.isInvalidContinuationByte z) =
            true →
        have r := ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z;
        r < 65536 → motive none) →
      (¬(ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
                  ByteArray.utf8DecodeChar?.isInvalidContinuationByte y ||
                ByteArray.utf8DecodeChar?.isInvalidContinuationByte z) =
              true →
          have r := ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z;
          ¬r < 65536 → 1114111 < r → motive none) →
        (¬(ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
                    ByteArray.utf8DecodeChar?.isInvalidContinuationByte y ||
                  ByteArray.utf8DecodeChar?.isInvalidContinuationByte z) =
                true →
            let r := ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z;
            ∀ (h : ¬r < 65536) (h_1 : ¬1114111 < r), motive (some { val := r, valid := ⋯ })) →
          motive (ByteArray.utf8DecodeChar?.assemble₄ w x y z)
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousSMul.exists_nhds_disjoint_image : ∀ (Γ : Type u_4) {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : SMul Γ T] [ProperlyDiscontinuousSMul Γ T]
  [T2Space T] [LocallyCompactSpace T] [ContinuousConstSMul Γ T] (x : T),
  ∃ U ∈ nhds x, ∀ (γ : Γ), γ • x ≠ x → Disjoint ((fun x => γ • x) '' U) U
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.edges_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.left.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : SizeOf J] (j : J),
  sizeOf (CategoryTheory.BiconeHom.left j) = 1 + sizeOf j
-- Mathlib.Order.Grade
CovBy.grade : ∀ (𝕆 : Type u_1) {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeOrder 𝕆 α] {a b : α},
  a ⋖ b → grade 𝕆 a ⋖ grade 𝕆 b
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.mk : {dir : Std.Http.Protocol.H1.Direction} →
  Array Std.Http.Chunk →
    Std.Http.Internal.ChunkedBuffer →
      Std.Http.Protocol.H1.Writer.State →
        Option Std.Http.Body.Length →
          Std.Http.Protocol.H1.Message.Head dir.swap → Bool → Bool → Bool → ℕ → Std.Http.Protocol.H1.Writer dir
-- Mathlib.Order.CompletePartialOrder
CompletePartialOrder.toPartialOrder : {α : Type u_4} → [self : CompletePartialOrder α] → PartialOrder α
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coreflection_sq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  P.coreflection i ^ 2 = 1
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_inj : ∀ {M : Type u_2} [inst : Mul M] {S T : Subsemigroup Mᵐᵒᵖ}, S.unop = T.unop ↔ S = T
-- Mathlib.RingTheory.Radical.Basic
/-- If `a` is a radical element, then `a` divides the radical of `b` if and only if it divides `b`.
Note the forward implication holds without the `b ≠ 0` assumption via `radical_dvd_self`.
 -/
UniqueFactorizationMonoid.dvd_radical_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M}, IsRadical a → b ≠ 0 → (a ∣ UniqueFactorizationMonoid.radical b ↔ a ∣ b)
-- Mathlib.Topology.Inseparable
IsClosed.stableUnderSpecialization : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → StableUnderSpecialization s
-- Mathlib.Algebra.Category.ModuleCat.Stalk
PresheafOfModules.germ_smul : ∀ {X : TopCat} {R : TopCat.Presheaf CommRingCat X}
  (M : PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat))) (x : ↑X)
  (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (r : ↑(R.obj (Opposite.op U))) (m : ↑(M.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf U x hx)) (r • m) =
    (CategoryTheory.ConcreteCategory.hom (R.germ U x hx)) r •
      (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf U x hx)) m
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.instIteratorLoopIdOfMonad : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      {pat : ρ} →
        [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ] →
          {n : Type u_1 → Type u_2} →
            [Monad n] → {s : String.Slice} → Std.IteratorLoop (String.Slice.SplitInclusiveIterator pat s) Id n
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLift_algebraMap_apply : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : IsFractionRing A K] [inst_10 : Algebra K L]
  [inst_11 : Algebra A L] [inst_12 : IsScalarTower A K L] [inst_13 : Algebra K L₂] [inst_14 : Algebra A L₂]
  [inst_15 : IsScalarTower A K L₂] [inst_16 : Algebra B L] [inst_17 : IsScalarTower A B L]
  [inst_18 : IsIntegralClosure B A L] [inst_19 : Algebra B₂ L₂] [inst_20 : IsScalarTower A B₂ L₂]
  [inst_21 : Algebra.IsAlgebraic K L] (σ : B →ₐ[A] B₂) (x : B),
  (galLift K L L₂ σ) ((algebraMap B L) x) = (algebraMap B₂ L₂) (σ x)
-- Mathlib.Data.Finset.Pairwise
Set.PairwiseDisjoint.attach : ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  (↑s).PairwiseDisjoint f → (↑s.attach).PairwiseDisjoint (f ∘ Subtype.val)
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.mk.inj : ∀ {X : Type u_2} {inst : TopologicalSpace X} {P : Set X → Set X → Prop} {C U : Set X} {P_C_U : P C U}
  {closed_C : IsClosed C} {open_U : IsOpen U} {subset : C ⊆ U}
  {hP :
    ∀ {c u : Set X},
      IsClosed c → P c u → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P c v ∧ P (closure v) u}
  {C_1 U_1 : Set X} {P_C_U_1 : P C_1 U_1} {closed_C_1 : IsClosed C_1} {open_U_1 : IsOpen U_1} {subset_1 : C_1 ⊆ U_1}
  {hP_1 :
    ∀ {c u : Set X},
      IsClosed c → P c u → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P c v ∧ P (closure v) u},
  { C := C, U := U, P_C_U := P_C_U, closed_C := closed_C, open_U := open_U, subset := subset, hP := hP } =
      { C := C_1, U := U_1, P_C_U := P_C_U_1, closed_C := closed_C_1, open_U := open_U_1, subset := subset_1,
        hP := hP_1 } →
    C = C_1 ∧ U = U_1
-- Mathlib.Algebra.Group.AddChar
AddChar.toMonoidHomEquiv_zero : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M], AddChar.toMonoidHomEquiv 0 = 1
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombinationOn_range : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} (s : Set α), (Finsupp.linearCombinationOn α M R v s).range = ⊤
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart.eq_1 : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A],
  imaginaryPart = skewAdjoint.negISMul ∘ₗ skewAdjointPart ℝ
-- Mathlib.Analysis.Calculus.FDeriv.Norm
norm_fderiv_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x : E} [Nontrivial E],
  DifferentiableAt ℝ (fun x => ‖x‖) x → ‖fderiv ℝ (fun x => ‖x‖) x‖ = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- For all `m ≤ n`, `truncation m` factors through `SSet.Truncated n`.  -/
SSet.truncationCompTrunc : {n m : ℕ} → (h : m ≤ n) → (SSet.truncation n).comp (SSet.Truncated.trunc n m ⋯) ≅ SSet.truncation m
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : P.IsMultiplicative] [inst_2 : P.RespectsIso],
  AlgebraicGeometry.Scheme.overGrothendieckTopology P S = (AlgebraicGeometry.Scheme.overPretopology P S).toGrothendieck
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The equivariant map between `SubMulAction.ofStabilizer M a`
and `ofFixingSubgroup M {a}`.  -/
SubMulAction.ofFixingSubgroup_of_singleton : (M : Type u_1) →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        (a : α) →
          have φ := fun x =>
            match x with
            | ⟨m, hm⟩ => ⟨m, ⋯⟩;
          ↥(SubMulAction.ofFixingSubgroup M {a}) →ₑ[φ] ↥(SubMulAction.ofStabilizer M a)
-- Mathlib.Order.PFilter
Order.PFilter.mk : {P : Type u_1} → [inst : Preorder P] → Order.Ideal Pᵒᵈ → Order.PFilter P
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.map_div_atTop_eq_nat : ∀ (k : ℕ), 0 < k → Filter.map (fun a => a / k) Filter.atTop = Filter.atTop
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.Flat f], AlgebraicGeometry.Flat (f ∣_ V)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
  AlgebraicGeometry.Scheme.Spec
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.semiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Monoid M],
  MonoidAlgebra.semiring =
    { toAddCommMonoid := MonoidAlgebra.instAddCommMonoid, toMul := MonoidAlgebra.nonUnitalSemiring.toMul,
      mul_assoc := ⋯, toOne := MonoidAlgebra.nonAssocSemiring.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto,
      npow_zero := ⋯, npow_succ := ⋯, zero_mul := ⋯, mul_zero := ⋯, left_distrib := ⋯, right_distrib := ⋯,
      toNatCast := MonoidAlgebra.nonAssocSemiring.toNatCast, natCast_zero := ⋯, natCast_succ := ⋯ }
-- Mathlib.Algebra.Group.Defs
AddRightCancelSemigroup.ext_iff : ∀ {G : Type u} {x y : AddRightCancelSemigroup G}, x = y ↔ Add.add = Add.add
-- Mathlib.Algebra.Notation.Lemmas
one_lt_dite : ∀ {α : Type u_1} [inst : One α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α} [inst_2 : LT α],
  (∀ (h : p), 1 < a h) → (∀ (h : ¬p), 1 < b h) → 1 < dite p a b
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- The clifford algebra over `CliffordAlgebraQuaternion.Q c₁ c₂` is isomorphic as an `R`-algebra
to `ℍ[R,c₁,c₂]`.  -/
CliffordAlgebraQuaternion.equiv : {R : Type u_1} →
  [inst : CommRing R] →
    {c₁ c₂ : R} → CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂) ≃ₐ[R] QuaternionAlgebra R c₁ 0 c₂
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_restrict : ∀ {α : Type u} (M : Matroid α) (X Y : Set α), (M.restrict X).cRk Y = M.cRk (X ∩ Y)
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAtFilter.mono : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L₁ L₂ : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L₂ → L₁ ≤ L₂ → HasDerivAtFilter f f' L₁
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {U : CategoryTheory.Comonad C}
  {c c' : CategoryTheory.Cokleisli U} {of of_1 : U.obj c.of ⟶ c'.of}, { of := of } = { of := of_1 } → of = of_1
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.singletonFinsubgraph_le_adj_left : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {e : G.Adj u v},
  SimpleGraph.singletonFinsubgraph u ≤ SimpleGraph.finsubgraphOfAdj e
-- Std.Http.Data.Status
Std.Http.Status.uriTooLong.sizeOf_spec : sizeOf Std.Http.Status.uriTooLong = 1
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalClosure_union : ∀ {G : Type u_5} [inst : AddGroup G] (s t : Set G),
  AddSubgroup.normalClosure (s ∪ t) = AddSubgroup.normalClosure s ⊔ AddSubgroup.normalClosure t
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_not_contains_of_containsKey_eq_false_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = false →
      Std.Internal.List.getValueD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback =
        Std.Internal.List.getValueD k l₁ fallback
-- Mathlib.Data.Sym.Sym2
Sym2.pmap_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {P : α → Prop} {Q : β → Prop} (f : (a : α) → P a → β)
  (g : (b : β) → Q b → γ) (z : Sym2 α) (h : ∀ a ∈ z, P a) (h' : ∀ b ∈ Sym2.pmap f z h, Q b),
  Sym2.pmap g (Sym2.pmap f z h) h' = Sym2.pmap (fun a ha => g (f a ⋯) ⋯) z ⋯
-- Mathlib.Analysis.Complex.Schwarz
/-- The **Schwarz Lemma**. Let `f : E → F` be a complex analytic function
on an open ball with center `c` and radius `R₁`.
If `f` sends this ball to a closed ball with center `f c` and radius `R₂`,
then for any `z` in the former ball we have `dist (f z) (f c) ≤ (R₂ / R₁) * dist z c`.
 -/
Complex.dist_le_div_mul_dist_of_mapsTo_ball : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {R₁ R₂ : ℝ} {f : E → F} {c z : E},
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) →
      z ∈ Metric.ball c R₁ → dist (f z) (f c) ≤ R₂ / R₁ * dist z c
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_C_mul_X : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a * Polynomial.X).leadingCoeff = a
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_int : Cardinal.mk ℤ = Cardinal.aleph0
-- Init.Data.Int.Cooper
_private.Init.Data.Int.Cooper.0.Int.Cooper.resolve_left'.eq_1 : ∀ (a c d p x : ℤ) (h₁ : p ≤ a * x),
  Int.Cooper.resolve_left' a c d p x h₁ = ↑(Int.add_of_le h₁) % a.lcm (a * d / ↑((a * d).gcd c))
-- Batteries.Data.List.Count
List.fst_idxToSigmaCount : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs : List α} {i : Fin xs.length},
  (xs.idxToSigmaCount i).fst = xs[↑i]
-- Mathlib.Topology.Instances.ENat
ContinuousOn.enatSub : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f g : X → ℕ∞} {s : Set X},
  ContinuousOn f s → ContinuousOn g s → (∀ x ∈ s, f x ≠ ⊤ ∨ g x ≠ ⊤) → ContinuousOn (fun x => f x - g x) s
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
/-- Universally injective satisfies fpqc descent.  -/
AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact : CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.UniversallyInjective)
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.Topology.Bases
TopologicalSpace.isSeparable_iUnion : ∀ {α : Type u} [t : TopologicalSpace α] {ι : Sort u_2} [Countable ι] {s : ι → Set α},
  TopologicalSpace.IsSeparable (⋃ i, s i) ↔ ∀ (i : ι), TopologicalSpace.IsSeparable (s i)
-- Init.Data.Queue
/-- `O(n)`. Applies the monadic predicate `p` to every element in the queue, and returns the queue
of elements for which `p` returns `true`. Note that there are currently no guarantees for the order
that `p` is applied in.
 -/
Std.Queue.filterM : {m : Type → Type v} → [Monad m] → {α : Type} → (α → m Bool) → Std.Queue α → m (Std.Queue α)
-- Mathlib.Algebra.Group.Graph
AddMonoidHom.coe_mgraph : ∀ {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] [inst_1 : AddMonoid H] (f : G →+ H), ↑f.mgraph = {x | f x.1 = x.2}
-- Mathlib.Algebra.Group.Equiv.Defs
MulHom.toMulEquiv.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (g : N →ₙ* M)
  (h₁ : g.comp f = MulHom.id M) (h₂ : f.comp g = MulHom.id N),
  f.toMulEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous iff the
family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is equicontinuous.  -/
IsUniformInducing.equicontinuous_iff : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} {β : Type u_8} [tX : TopologicalSpace X] [uα : UniformSpace α]
  [uβ : UniformSpace β] {F : ι → X → α} {u : α → β},
  IsUniformInducing u → (Equicontinuous F ↔ Equicontinuous ((fun x => u ∘ x) ∘ F))
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.Core.nhds_toTopologicalSpace : ∀ {α : Type u} (u : UniformSpace.Core α) (x : α), nhds x = Filter.comap (Prod.mk x) u.uniformity
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.instInhabitedAction : {a : Type u_1} → {a_1 : Type u_2} → Inhabited (Std.Tactic.BVDecide.LRAT.Action a a_1)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.eq_2 : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (s : Set E) (x : E) (n_2 : ℕ∞),
  ContDiffWithinAt 𝕜 (some n_2) f s x =
    ∀ (m : ℕ), ↑m ≤ n_2 → ∃ u ∈ nhdsWithin x (insert x s), ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u