mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.IsLocalSourceTargetProperty.mono_source : ∀ {H : Type u_6} {G : Type u_8} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace G] {M : Type u_10}
  {N : Type u_12} [inst_2 : TopologicalSpace M] [inst_3 : TopologicalSpace N]
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop},
  Manifold.IsLocalSourceTargetProperty P →
    ∀ {f : M → N} {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G} {s : Set M},
      IsOpen s → P f φ ψ → P f (φ.restr s) ψ
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Corecursor for M-type of `P`  -/
MvPFunctor.M.corec : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → {α : TypeVec.{u} n} → {β : Type u} → (β → ↑P (α ::: β)) → β → P.M α
-- Mathlib.Data.Real.Basic
Real.instMin : Min ℝ
-- Mathlib.RingTheory.DedekindDomain.Basic
IsDedekindDomain.toIsDomain : ∀ {A : Type u_2} {inst : CommRing A} [self : IsDedekindDomain A], IsDomain A
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_pow : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] {k : ℤ} (f : ModularForm Γ k) (n : ℕ), ⇑(f.pow n) = ⇑f ^ n
-- Lean.Elab.Tactic.Basic
/-- Execute an action while suppressing any new messages it generates.
Restores the original message log after the action completes.
Useful for trying tactics without polluting the message log with errors from failed attempts.  -/
Lean.Elab.Tactic.withSuppressedMessages : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM α
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.Cycle.decidableNontrivialCoe.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x y : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (x : α) → motive [x]) (h_3 : (x y : α) → (l : List α) → motive (x :: y :: l)),
  (match x :: y :: l with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: l => h_3 x y l) =
    h_3 x y l
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the second quadrant. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open second quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open second quadrant
  for some `A`, `B`, and `c < 2`;
* `f` is equal to zero on the boundary of the second quadrant.

Then `f` is equal to zero on the closed second quadrant.  -/
PhragmenLindelof.eq_zero_on_quadrant_II : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
  DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (∀ x ≤ 0, f ↑x = 0) → (∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = 0) → Set.EqOn f 0 {z | z.re ≤ 0 ∧ 0 ≤ z.im}
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.pure_pow : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α] (a : α)
  (n : ℕ), NonemptyInterval.pure a ^ n = NonemptyInterval.pure (a ^ n)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.card_toFinset : ∀ {α : Type u} {s : Set α} [inst : Fintype ↑s] (h : s.Finite), h.toFinset.card = Fintype.card ↑s
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Standard formula, computing the Laplacian from any orthonormal basis.
 -/
InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f : E → F) {s : Set E} {ι : Type u_5}
  [inst_5 : Fintype ι] {e : E},
  UniqueDiffOn ℝ s →
    e ∈ s →
      ∀ (v : OrthonormalBasis ι ℝ E),
        InnerProductSpace.laplacianWithin f s e = ∑ i, (iteratedFDerivWithin ℝ 2 f s e) ![v i, v i]
-- Mathlib.Analysis.Normed.Module.Basic
/-- The product of two normed algebras is a normed algebra, with the sup norm.  -/
Prod.normedAlgebra : (𝕜 : Type u_1) →
  [inst : NormedField 𝕜] →
    {E : Type u_6} →
      {F : Type u_7} →
        [inst_1 : SeminormedRing E] →
          [inst_2 : SeminormedRing F] → [NormedAlgebra 𝕜 E] → [NormedAlgebra 𝕜 F] → NormedAlgebra 𝕜 (E × F)
-- Std.Data.HashMap.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.HashMap.insertIfNew : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → Std.HashMap α β
-- Init.Data.SInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toInt8 : Bool → Int8
-- Init.Data.Array.MinMax
Array.min?_mem : ∀ {α : Type u_1} {a : α} [inst : Min α] [Std.MinEqOr α] (xs : Array α), xs.min? = some a → a ∈ xs
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
Echelon.Decomposition.mk.sizeOf_spec : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : LinearOrder m] {n : Type u_2} [inst_2 : LinearOrder n] {R : Type u_3}
  [inst_3 : CommRing R] {A : Matrix m n R} [inst_4 : SizeOf m] [inst_5 : SizeOf n] [inst_6 : SizeOf R]
  (L : Matrix m m R) (σ : Equiv.Perm m) (pivot : m → WithTop n)
  (isPivotedBy : (L * A.submatrix (⇑σ) id).IsPivotedBy pivot) (L_lowerTriangular : L.IsLowerTriangular)
  (L_diag_ne_zero : ∀ (i : m), L.diag i ≠ 0),
  sizeOf
      { L := L, σ := σ, pivot := pivot, isPivotedBy := isPivotedBy, L_lowerTriangular := L_lowerTriangular,
        L_diag_ne_zero := L_diag_ne_zero } =
    1 + sizeOf σ + sizeOf isPivotedBy
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S)
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w :
    ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) e.hom)
  {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)}
  (w' :
    ∀ (i : ι), CategoryTheory.CategoryStruct.comp (q' i) (f' (β i)) = CategoryTheory.CategoryStruct.comp (f i) e.inv),
  (CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence F e w w').inverse =
    CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.eval_polynomialZ : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  (MvPolynomial.eval P) W'.polynomialZ =
    W'.a₁ * P 0 * P 1 + 3 * W'.a₃ * P 1 * P 2 ^ 2 -
      (2 * W'.a₂ * P 0 ^ 2 * P 2 + 4 * W'.a₄ * P 0 * P 2 ^ 3 + 6 * W'.a₆ * P 2 ^ 5)
-- Mathlib.Data.Bool.Basic
Bool.eq_true_eq_not_eq_false : ∀ (b : Bool), (¬b = false) = (b = true)
-- Init.Data.List.BasicAux
/-- Auxiliary for `partitionMap`:
`partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right)`
if `partitionMap f l = (left, right)`.  -/
_private.Init.Data.List.BasicAux.0.List.partitionMap.go : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β ⊕ γ) → List α → Array β → Array γ → List β × List γ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.fold_filterWithPostcondition : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [LawfulMonad n] [inst_6 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n]
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {g : δ → β → δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.filterWithPostcondition f it) =
    Std.IterM.foldM
      (fun d b => do
        let __do_lift ← (f b).run
        pure (if __do_lift.down = true then g d b else d))
      init it
-- Mathlib.MeasureTheory.PiSystem
mem_piiUnionInter_of_measurableSet : ∀ {α : Type u_3} {ι : Type u_4} (m : ι → MeasurableSpace α) {S : Set ι} {i : ι},
  i ∈ S → ∀ (s : Set α), MeasurableSet s → s ∈ piiUnionInter (fun n => {s | MeasurableSet s}) S
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.zero_def : ∀ {ι : 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 : Nonempty ι]
  [inst_5 : (i : ι) → Zero (G i)] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] (i : ι), 0 = ⟦⟨i, 0⟩⟧
-- Mathlib.Topology.Constructions
Continuous.codRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Continuous f → ∀ (hs : ∀ (a : X), f a ∈ s), Continuous (Set.codRestrict f s hs)
-- Mathlib.Data.Finset.Card
Finset.one_le_card : ∀ {α : Type u_1} {s : Finset α}, 1 ≤ s.card ↔ s.Nonempty
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.sup_apply : ∀ {E : Type u_3} [inst : AddGroup E] (p q : NonarchAddGroupNorm E) (x : E), (p ⊔ q) x = max (p x) (q x)
-- Std.Time.Date.Unit.Month
/-- Creates an `Ordinal` from an integer, ensuring the value is within bounds.
 -/
Std.Time.Month.Ordinal.ofInt : (data : ℤ) → 1 ≤ data ∧ data ≤ 12 → Std.Time.Month.Ordinal
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_apply_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x (f y) ↔ f.SameCycle x y
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Node.measure.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_3) →
      (x : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
        (x = Lean.PersistentHashMap.Entry.null → motive Lean.PersistentHashMap.Entry.null) →
          ((key : α) →
              (val : β) →
                x = Lean.PersistentHashMap.Entry.entry key val → motive (Lean.PersistentHashMap.Entry.entry key val)) →
            ((node : Lean.PersistentHashMap.Node α β) →
                x = Lean.PersistentHashMap.Entry.ref node → motive (Lean.PersistentHashMap.Entry.ref node)) →
              motive x
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.instFaithfulSMulProjectiveSpecialLinearGroupForall : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_3} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  FaithfulSMul (Matrix.ProjectiveSpecialLinearGroup ι K) (Projectivization K (ι → K))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.ExprPair.rhs : (self : Std.Tactic.BVDecide.BVPred.ExprPair) → Std.Tactic.BVDecide.BVExpr self.w
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.concat_isPath_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (h : G.Adj v w),
  (p.concat h).IsPath ↔ p.IsPath ∧ w ∉ p.support
-- Mathlib.Order.Basic
Function.const_lt_const : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [Nonempty β] {a b : α},
  Function.const β a < Function.const β b ↔ a < b
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_clm_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {x : 𝕜} {s : Set 𝕜}
  {G : Type u_2} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {c : 𝕜 → F →L[𝕜] G} {d : 𝕜 → E →L[𝕜] F},
  DifferentiableWithinAt 𝕜 c s x →
    DifferentiableWithinAt 𝕜 d s x →
      derivWithin (fun y => c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x
-- Mathlib.Analysis.Complex.AbsMax
Complex.norm_max_aux₃ : ∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {f : ℂ → F} {z w : ℂ} {r : ℝ},
  dist w z = r → DiffContOnCl ℂ f (Metric.ball z r) → IsMaxOn (norm ∘ f) (Metric.ball z r) z → ‖f w‖ = ‖f z‖
-- Mathlib.Data.Nat.Log
Nat.clog_pow : ∀ (b x : ℕ), 1 < b → Nat.clog b (b ^ x) = x
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.AEEqFun.integrable_mk : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε} (hf : MeasureTheory.AEStronglyMeasurable f μ),
  (MeasureTheory.AEEqFun.mk f hf).Integrable ↔ MeasureTheory.Integrable f μ
-- Mathlib.Topology.MetricSpace.Infsep
Finset.coe_infsep_of_offDiag_nonempty : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Finset α} (hs : s.offDiag.Nonempty),
  (↑s).infsep = s.offDiag.inf' hs (Function.uncurry dist)
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.instIsMultiplicativeQuasiIso : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.CategoryWithHomology C], (HomologicalComplex.quasiIso C c).IsMultiplicative
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₂.getKey k ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
zsmul_pos : ∀ {G : Type u_2} [inst : SubNegMonoid G] [inst_1 : Preorder G] [AddLeftMono G] {x : G},
  0 < x → ∀ {n : ℤ}, 0 < n → 0 < n • x
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.inverse_map_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  {X Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} (f : X ⟶ Y),
  ((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).map f).f = f.f.f
-- Mathlib.Topology.MetricSpace.Algebra
LipschitzAdd.C.eq_1 : ∀ (β : Type u_2) [inst : PseudoMetricSpace β] [inst_1 : AddMonoid β] [_i : LipschitzAdd β],
  LipschitzAdd.C β = Classical.choose ⋯
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
contMDiff_tangentBundleModelSpaceHomeomorph_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H},
  ContMDiff I.tangent I.tangent n ⇑(tangentBundleModelSpaceHomeomorph I).symm
-- Lean.Server.References
/-- Content of individual `.ilean` files  -/
Lean.Server.Ilean : Type
-- Mathlib.Algebra.AffineMonoid.Embedding
AffineAddMonoid.embedding_injective : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] [inst_1 : AddMonoid.FG M] [inst_2 : IsAddTorsionFree M],
  Function.Injective ⇑(AffineAddMonoid.embedding M)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Construct a morphism in `P.Under Q X` from a morphism in `Under X`.  -/
CategoryTheory.MorphismProperty.Under.Hom.mk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      {X : T} →
        [inst_1 : Q.IsMultiplicative] →
          {A B : P.Under Q X} →
            (f :
                (CategoryTheory.MorphismProperty.Under.forget P Q X).obj A ⟶
                  (CategoryTheory.MorphismProperty.Under.forget P Q X).obj B) →
              Q (CategoryTheory.Under.Hom.right f) → (A ⟶ B)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] (t t_1 : Std.DTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (f f_1 : Option (β a) → Option (β a)), f = f_1 → t.alter a f = t_1.alter a f_1
-- Mathlib.Data.Set.Monotone
Monotone.rangeFactorization : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Monotone (Set.rangeFactorization f)
-- Init.Data.Int.Basic
/-- Decides whether `a < b`.

```
#eval `¬ ( (7 : Int) < 0 )` -- true
#eval `¬ ( (0 : Int) < 0 )` -- true
#eval `(7 : Int) < 10` -- true
```

Implemented by efficient native code.  -/
Int.decLt : (a b : ℤ) → Decidable (a < b)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry : Type u → Type v → Type w → Type (max (max u v) w)
-- Init.Data.Array.Mem
/-- This tactic, added to the `decreasing_trivial` toolbox, proves that
`sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions
over a nested inductive like `inductive T | mk : Array T → T`.  -/
Array.tacticArray_get_dec : Lean.ParserDescr
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.negate_eq : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), c.negate = List.map Std.Sat.Literal.negate c.toList
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Fold over the elements of a heap in increasing order,
by repeatedly pulling the minimum element out of the heap.
 -/
Batteries.BinomialHeap.fold : {α : Type u} → {le : α → α → Bool} → {β : Type u_1} → Batteries.BinomialHeap α le → β → (β → α → β) → β
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.instIsLocallySurjectiveFunMapTypeSheafComposeForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) [inst_4 : J.HasSheafCompose (CategoryTheory.forget A)]
  [CategoryTheory.Sheaf.IsLocallySurjective φ],
  CategoryTheory.Sheaf.IsLocallySurjective ((CategoryTheory.sheafCompose J (CategoryTheory.forget A)).map φ)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_cons : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} (h : t.WF) {l : List α} {k : α},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t (k :: l) ⋯) =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit (Std.DTreeMap.Internal.Impl.insertIfNew k () t ⋯).impl l ⋯)
-- Init.Data.Array.Basic
Array.size_set : ∀ {α : Type u} {xs : Array α} {i : ℕ} {v : α} (h : i < xs.size), (xs.set i v h).size = xs.size
-- Mathlib.GroupTheory.Solvable
Group.isSolvable_of_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
  Function.Surjective ⇑f → ∀ [Group.IsSolvable G], Group.IsSolvable G'
-- Init.Data.List.Find
List.idxOf?_singleton : ∀ {α : Type u_1} [inst : BEq α] {a b : α}, List.idxOf? b [a] = if (a == b) = true then some 0 else none
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.toList_filterMap : ∀ {β : Type v} {γ : Type w} {α : Type u} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {f : α → β → Option γ},
  (Std.DHashMap.Raw.Const.toList ↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).Perm
    (List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DHashMap.Raw.Const.toList ↑m))
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_two_iff : ∀ {α : Type u_1}, Nat.card α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = Set.univ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.mem_darts_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {d : G.Dart} {p : G.Walk u v}, d ∈ p.reverse.darts ↔ d.symm ∈ p.darts
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.range_subtype : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R), (NonUnitalSubringClass.subtype s).range = s
-- Init.Meta.Defs
/-- Creates an optional node.

Optional nodes consist of null nodes that contain either zero or one element.
 -/
Lean.mkOptionalNode : Option Lean.Syntax → Lean.Syntax
-- Mathlib.NumberTheory.FermatPsp
/-- **Alias** of `Nat.infinite_setOfPred_pseudoprimes`.

---

Infinite set variant of `Nat.exists_infinite_pseudoprimes`
 -/
Nat.infinite_setOf_pseudoprimes : ∀ {b : ℕ}, 1 ≤ b → {n | n.FermatPsp b}.Infinite
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] {ι : Type u_4} {fi : Filter ι} [inst_1 : Fact (1 ≤ p)]
  (f : ι → ↥(MeasureTheory.Lp E p μ)) (f_lim : α → E) (f_lim_ℒp : MeasureTheory.MemLp f_lim p μ),
  Filter.Tendsto f fi (nhds (MeasureTheory.MemLp.toLp f_lim f_lim_ℒp)) ↔
    Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑↑(f n) - f_lim) p μ) fi (nhds 0)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {h' : k ∈ m.erase a}, (m.erase a).getKey k h' = m.getKey k ⋯
-- Mathlib.CategoryTheory.Yoneda
/-- A variant of the curried version of the Coyoneda lemma with a raise in the universe level.  -/
CategoryTheory.uliftCoyonedaRightOpCompCoyoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.rightOp.comp CategoryTheory.coyoneda ≅
      (CategoryTheory.evaluation C (Type (max v₁ w))).comp
        ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor C (Type (max v₁ w))) (Type (max v₁ w))
              (Type (max (max w u₁) v₁))).obj
          CategoryTheory.uliftFunctor.{u₁, max v₁ w})
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.negate_eq : ∀ {α : outParam (Type u)} {β : Type v} [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (c : β),
  Std.Tactic.BVDecide.LRAT.Internal.Clause.negate c =
    List.map Std.Sat.Literal.negate (Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c)
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α]
  {f : β → α} [inst_2 : DecidableEq β] {g : γ → β} (s : Finset γ), (Finset.image g s).lcm f = s.lcm (f ∘ g)
-- Init.Data.Vector.Lemmas
/-- `Vector.ext` is an extensionality theorem.
Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
 -/
Vector.ext : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n}, (∀ (i : ℕ) (x : i < n), xs[i] = ys[i]) → xs = ys
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.cotangentSpaceBasis_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  (P : Algebra.Generators R S ι) (i : ι),
  P.cotangentSpaceBasis i = 1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) (MvPolynomial.X i)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] (f : ι → β → α) [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], SummableLocallyUniformly f = ∃ g, HasSumLocallyUniformly f g
-- Mathlib.Algebra.Order.CompleteField
LinearOrderedField.cutMap_nonempty : ∀ {α : Type u_2} (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [Archimedean α] (a : α), (LinearOrderedField.cutMap β a).Nonempty
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_add_pi : ∀ (θ : Real.Angle), (θ + ↑Real.pi).sign = -θ.sign
-- Mathlib.Algebra.Order.Field.Pi
Pi.exists_forall_pos_add_lt : ∀ {α : Type u_1} {ι : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedCancelAddMonoid α]
  [Nontrivial α] [DenselyOrdered α] [ExistsAddOfLE α] [Finite ι] {x y : ι → α},
  (∀ (i : ι), x i < y i) → ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomLeft : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' : Dᵒᵖ} (f : c ⟶ c') (d : Cᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f d =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.unop (Opposite.unop d)).op