mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.NormTrace
ModularForm.eq_const_of_weight_zero : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] (f : ModularForm 𝒢 0), ∃ c, ⇑f = Function.const UpperHalfPlane c
-- Mathlib.Order.BoundedOrder.Basic
Ne.lt_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, a ≠ ⊤ → a < ⊤
-- Mathlib.Topology.Order.Lattice
ContinuousOn.finset_sup : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [inst_3 : OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (s.sup f) t
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.instCommMonoidWithConv : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring C] →
            [inst_3 : Bialgebra R A] →
              [inst_4 : Bialgebra R C] → [Coalgebra.IsCocomm R C] → CommMonoid (WithConv (C →ₐc[R] A))
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.changed.sizeOf_spec : ∀ (goal : Lean.MVarId) (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))),
  sizeOf (Aesop.NormSeqResult.changed goal script) = 1 + sizeOf goal + sizeOf script
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.iSupLift_mk : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B] {ι : Type u_1}
  [inst_7 : StarRing R] [inst_8 : IsScalarTower R A A] [inst_9 : SMulCommClass R A A] [inst_10 : StarModule R A]
  [inst_11 : Nonempty ι] {K : ι → NonUnitalStarSubalgebra R A} {dir : Directed (fun x1 x2 => x1 ≤ x2) K}
  {f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)}
  {T : NonUnitalStarSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (hx : ↑x ∈ T),
  (NonUnitalStarSubalgebra.iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x
-- Init.Data.Ord.Basic
instOrdFin : (n : ℕ) → Ord (Fin n)
-- Mathlib.Data.Finset.Sum
Finset.sumEquiv_symm_apply : ∀ {α : Type u_4} {β : Type u_5} (s : Finset α × Finset β), Finset.sumEquiv.symm s = s.1.disjSum s.2
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.brecOn.go : {motive : Mathlib.Tactic.ITauto.Proof → Sort u} →
  (t : Mathlib.Tactic.ITauto.Proof) →
    ((t : Mathlib.Tactic.ITauto.Proof) → Mathlib.Tactic.ITauto.Proof.below t → motive t) →
      motive t ×' Mathlib.Tactic.ITauto.Proof.below t
-- Init.Data.Array.Lemmas
Array.ne_and_not_mem_of_not_mem_push : ∀ {α : Type u_1} {a y : α} {xs : Array α}, a ∉ xs.push y → a ≠ y ∧ a ∉ xs
-- Lean.DocString.Types
Lean.Doc.Block.ol.inj : ∀ {i : Type u} {b : Type v} {start : ℤ} {items : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))} {start_1 : ℤ}
  {items_1 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))},
  Lean.Doc.Block.ol start items = Lean.Doc.Block.ol start_1 items_1 → start = start_1 ∧ items = items_1
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.zero_smul_const : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : Zero M] [inst_3 : Zero X] [inst_4 : SMulWithZero M X] [ContinuousSMul M X] {f : α → M} {l : Filter α},
  Filter.Tendsto f l (nhds 0) → ∀ (a : X), Filter.Tendsto (fun x => f x • a) l (nhds 0)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.restoreM_trans : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {o : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u}
  {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP o ps] [inst_1 : MonadControl n o] [inst_2 : MonadControlT m n]
  (x : stM m o α), ⦃(Std.Do.wp (MonadControl.restoreM (restoreM x))).apply Q⦄ restoreM x ⦃Q⦄
-- Lean.Parser.Extra
Lean.ppRealFill.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Data.ZMod.Basic
ZMod.val_one'' : ∀ {n : ℕ}, n ≠ 1 → ZMod.val 1 = 1
-- Mathlib.Tactic.CasesM
/-- Auxiliary for `constructorMatching`. Accumulates generated subgoals in `acc`.  -/
_private.Mathlib.Tactic.CasesM.0.Mathlib.Tactic.constructorMatching.go : (Lean.Expr → Lean.MetaM Bool) → Lean.MVarId → optParam (Array Lean.MVarId) #[] → Lean.MetaM (Array Lean.MVarId)
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.add_iff_right : ∀ {𝕜 : 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},
  Differentiable 𝕜 f → (Differentiable 𝕜 (f + g) ↔ Differentiable 𝕜 g)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.cast_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X),
  (F.cast h₀ h₁) a = F a
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiffOn_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [inst_5 : Fintype ι] (p : ENNReal) [inst_6 : Fact (1 ≤ p)] {n : WithTop ℕ∞}
  {f : H → PiLp p E} {t : Set H}, ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => (f x).ofLp i) t
-- Init.Data.List.Find
List.findIdx?_eq_findSome?_zipIdx : ∀ {α : Type u_1} {xs : List α} {p : α → Bool},
  List.findIdx? p xs =
    List.findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.convolution_zero : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : Monoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E), DiscreteConvolution.convolution L f 0 = 0
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ico : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α},
  Filter.Tendsto a l Filter.atBot →
    Filter.Tendsto b l Filter.atTop → ∀ [NoMaxOrder α], MeasureTheory.AECover μ l fun i => Set.Ico (a i) (b i)
-- Mathlib.Topology.Order.Lattice
ContinuousInf.mk : ∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : Min L], (Continuous fun p => p.1 ⊓ p.2) → ContinuousInf L
-- Mathlib.Data.Set.Image
Function.Surjective.preimage_subset_preimage_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β}, Function.Surjective f → (f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The atomic Grothendieck topology: a sieve is covering iff it is nonempty.
For the pullback stability condition, we need the right Ore condition to hold.

See https://ncatlab.org/nlab/show/atomic+site, or [MM92] Chapter III, Section 2, example (f).
 -/
CategoryTheory.GrothendieckTopology.atomic : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology.RightOreCondition C → CategoryTheory.GrothendieckTopology C
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.fderiv_fourierChar_neg_bilinear_left_apply : ∀ {V : Type u_1} {W : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : NormedAddCommGroup W]
  [inst_3 : NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (v y : V) (w : W),
  (fderiv ℝ (fun v => ↑(Real.fourierChar (-(L v) w))) v) y =
    -2 * ↑Real.pi * Complex.I * ↑((L y) w) * ↑(Real.fourierChar (-(L v) w))
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.backward.grind.inferPattern : Lean.Option Bool
-- Init.Data.List.Nat.Range
List.pairwise_le_range' : ∀ {s n : ℕ} (step : optParam ℕ 1), List.Pairwise (fun x1 x2 => x1 ≤ x2) (List.range' s n step)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.isProbabilityMeasure : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.iIndep m μ → MeasureTheory.IsProbabilityMeasure μ
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.le_inf_support_coeff_mul`. -/
AddMonoidAlgebra.le_inf_support_mul : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : SemilatticeInf T] [inst_1 : OrderTop T] [inst_2 : Semiring R]
  [inst_3 : Add A] [inst_4 : Add T] [AddLeftMono T] [AddRightMono T] {degt : A → T},
  (∀ (a b : A), degt a + degt b ≤ degt (a + b)) →
    ∀ (f g : AddMonoidAlgebra R A), f.coeff.support.inf degt + g.coeff.support.inf degt ≤ (f * g).coeff.support.inf degt
-- Std.Time.Format.Basic
/-- Parses a short month name using the given locale symbols and returns the corresponding `Month.Ordinal`.
 -/
Std.Time.parseMonthShort : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Month.Ordinal
-- Mathlib.Order.Defs.Unbundled
irrefl : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Irrefl r] (a : α), ¬r a a
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is nonpositive on
`Ioo a b` and nonnegative on `Ioo b c`. Then `f` attains its minimum on `Ioc a c` at `b`.  -/
isMinOn_Ioc_of_deriv : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  ContinuousAt f b →
    ContinuousAt f c →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        DifferentiableOn ℝ f (Set.Ioo b c) →
          (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) → IsMinOn f (Set.Ioc a c) b
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.Equiv.mk : ∀ {α : Type u} {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.Topology.Semicontinuity.Defs
Semicontinuous.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : β → Prop}, Semicontinuous fun _x => f
-- Lean.Util.MonadCache
Lean.MonadCacheT.run : {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [inst_1 : BEq α] →
        [inst_2 : Hashable α] → [MonadLiftT (ST ω) m] → [Monad m] → {σ : Type} → Lean.MonadCacheT α β m σ → m σ
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.instSemigroupWithZero : {𝕜 : Type u_1} → [inst : NonUnitalSeminormedRing 𝕜] → SemigroupWithZero ↑(Metric.closedBall 0 1)
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.weakFEPair_k : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k], (ModularForm.weakFEPair hk f).k = ↑k
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Eta-expanded form of `differentiable_id` -/
differentiable_fun_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E], Differentiable 𝕜 fun x => x
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex)
  (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1))
  (w :
    f.f (n + 1) =
      CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' +
        CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1))),
  CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 2) (n + 3))
      (CategoryTheory.InjectiveResolution.descHomotopyZeroSucc f n g g' w) =
    f.f (n + 2) - CategoryTheory.CategoryStruct.comp g' (J.cocomplex.d (n + 1) (n + 2))
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.transEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (f' : β ≃ γ) (a : α),
  ↑(e.transEquiv f') a = f' (↑e a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter!_eq_sub_one : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∈ t →
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone = true →
          (Std.DTreeMap.Internal.Impl.Const.alter! k f t).size = t.size - 1
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.isClosed_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubmonoid M), IsClosed ↑s.topologicalClosure
-- Init.System.IO
/-- Creates a stream from a mutable reference to a buffer.

The resulting stream simulates a file, mutating the contents of the reference in response to writes
and reading from it in response to reads. These streams can be used with `IO.withStdin`,
`IO.setStdin`, and the corresponding operators for standard output and standard error to redirect
input and output.
 -/
IO.FS.Stream.ofBuffer : IO.Ref IO.FS.Stream.Buffer → IO.FS.Stream
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.instHasFiniteCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] [CategoryTheory.HasWeakSheafify J D]
  [CategoryTheory.Limits.HasFiniteCoproducts D], CategoryTheory.Limits.HasFiniteCoproducts (CategoryTheory.Sheaf J D)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractRight_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (d : Module.Dual R M) (x : M),
  (CliffordAlgebra.contractRight ((CliffordAlgebra.ι Q) x)) d = (algebraMap R (CliffordAlgebra Q)) (d x)
-- Mathlib.Algebra.Category.Ring.Topology
/-- `Hom(A[Xᵢ], R)` is homeomorphic to `Hom(A, R) × Rⁱ`.  -/
CommRingCat.HomTopology.mvPolynomialHomeomorph : (σ : Type v) →
  (R A : CommRingCat) →
    [inst : TopologicalSpace ↑R] →
      [IsTopologicalRing ↑R] → (CommRingCat.of (MvPolynomial σ ↑A) ⟶ R) ≃ₜ (A ⟶ R) × (σ → ↑R)
-- Aesop.Forward.State
Aesop.InstMap.instToMessageData : Lean.ToMessageData Aesop.InstMap
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- The differentials `s.d i j : s.N i ⟶ s.N j` on nondegenerate simplices of a split
simplicial object are induced by the differentials on the alternating face map complex.  -/
CategoryTheory.SimplicialObject.Splitting.d : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) → [CategoryTheory.Preadditive C] → (i j : ℕ) → s.N i ⟶ s.N j
-- Init.Data.UInt.Lemmas
UInt16.toUSize_ofNatClamp_of_le : ∀ {n : ℕ}, UInt16.size ≤ n → (UInt16.ofNatClamp n).toUSize = USize.ofNatLT (UInt16.size - 1) ⋯
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WPMonad.mk : {m : Type u → Type v} →
  {Pred : outParam (Type w)} →
    {EPred : outParam (Type w')} →
      [inst : Monad m] →
        [inst_1 : Std.Internal.Do.Assertion Pred] →
          [inst_2 : Std.Internal.Do.Assertion EPred] →
            [toLawfulMonad : LawfulMonad m] →
              (toWP : (α : Type u) → Std.Internal.Do.WP (m α) α Pred EPred) →
                (∀ {α : Type u} (x : α) (post : α → Pred) (epost : EPred),
                    Lean.Order.PartialOrder.rel (post x) (Std.Internal.Do.wp (pure x) post epost)) →
                  (∀ {α β : Type u} (x : m α) (f : α → m β) (post : β → Pred) (epost : EPred),
                      Lean.Order.PartialOrder.rel
                        (Std.Internal.Do.wp x (fun a => Std.Internal.Do.wp (f a) post epost) epost)
                        (Std.Internal.Do.wp (x >>= f) post epost)) →
                    Std.Internal.Do.WPMonad m Pred EPred
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `f a ≤ B a`;
* `B` has right derivative `B'` at every point of `[a, b)`;
* `f` has right derivative `f'` at every point of `[a, b)`;
* we have `f' x ≤ B' x` on `[a, b)`.

Then `f x ≤ B x` everywhere on `[a, b]`.  -/
image_le_of_deriv_right_le_deriv_boundary : ∀ {f f' : ℝ → ℝ} {a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      ∀ {B B' : ℝ → ℝ},
        f a ≤ B a →
          ContinuousOn B (Set.Icc a b) →
            (∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
              (∀ x ∈ Set.Ico a b, f' x ≤ B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (h : CategoryTheory.CategoryStruct.comp f g = fg),
  F.mapComp' f g fg h = F.map₂Iso (CategoryTheory.eqToIso ⋯) ≪≫ F.mapComp f g
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
CategoryTheory.Sheaf.ab5ofSize : ∀ {C : Type u} {A : Type u₁} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasFiniteLimits A]
  [inst_3 : CategoryTheory.HasSheafify J A]
  [inst_4 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A]
  [CategoryTheory.AB5OfSize.{v₂, u₂, v₁, u₁} A],
  CategoryTheory.AB5OfSize.{v₂, u₂, max u v₁, max (max (max u₁ u) v₁) v} (CategoryTheory.Sheaf J A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.map_fst_toList_eq_keys : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  List.map Prod.fst (Std.DTreeMap.Internal.Impl.Const.toList t) = t.keys
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.CompactOpens α), IsCompact ↑s
-- Mathlib.Analysis.Calculus.FDeriv.Defs
fderivWithin_zero_of_not_differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  ¬DifferentiableWithinAt 𝕜 f s x → fderivWithin 𝕜 f s x = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.facePairComplIso_hom_ι'_assoc : ∀ {n : ℕ} (i j : Fin (n + 3)) (h : i < j) {Z : SSet} (h_1 : SSet.stdSimplex.obj { len := n + 2 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.facePairComplIso i j h).hom
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.face {i, j}ᶜ).ι h_1) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (j.pred ⋯))
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i) h_1)
-- Aesop.Tree.Data.ForwardRuleMatches
Aesop.ForwardRuleMatches.mk.inj : ∀
  {normMatches safeMatches unsafeMatches normMatches_1 safeMatches_1 unsafeMatches_1 :
    Lean.PHashSet Aesop.ForwardRuleMatch},
  { normMatches := normMatches, safeMatches := safeMatches, unsafeMatches := unsafeMatches } =
      { normMatches := normMatches_1, safeMatches := safeMatches_1, unsafeMatches := unsafeMatches_1 } →
    normMatches = normMatches_1 ∧ safeMatches = safeMatches_1 ∧ unsafeMatches = unsafeMatches_1
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_mul : ∀ {K : Type u_1} [inst : RCLike K] (z w : K), RCLike.normSq (z * w) = RCLike.normSq z * RCLike.normSq w
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A map is a homeomorphism iff it is the map underlying a bundled homeomorphism `h : X ≃ₜ Y`.  -/
isHomeomorph_iff_exists_homeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f ↔ ∃ h, ⇑h = f
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.stronglyMeasurable_integral_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.next_prev : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.startPos}, (p.prev h).next ⋯ = p
-- Mathlib.Topology.LocalAtTarget
GeneralizingMap.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  GeneralizingMap f → ∀ (s : Set β), GeneralizingMap (s.restrictPreimage f)
-- Mathlib.Tactic.NormNum.Core
/-- Elaborates a call to `norm_num only? [args]` or `norm_num1`.
* `args`: the `(simpArgs)?` syntax for simp arguments
* `loc`: the `(location)?` syntax for the optional location argument
* `simpOnly`: true if `only` was used in `norm_num`
* `useSimp`: false if `norm_num1` was used, in which case only the structural parts
  of `simp` will be used, not any of the post-processing that `simp only` does without lemmas
 -/
Mathlib.Meta.NormNum.elabNormNum : Lean.Syntax → Lean.Syntax → Lean.Syntax → optParam Bool false → optParam Bool true → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomWhiskerLeft_comp_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X : C)
  {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y'') {Z : V} (h : (X ⟶[V] Y'') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V X (CategoryTheory.CategoryStruct.comp g g')) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V X g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V X g') h)
-- Init.Data.ToString.Basic
instToStringBool : ToString Bool
-- Mathlib.Topology.Connected.Clopen
/-- If every map to `Bool` (a discrete two-element space), that is
continuous on a set `s`, is constant on s, then s is preconnected  -/
isPreconnected_of_forall_constant : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  (∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y) → IsPreconnected s
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.MLListImpl.cons : {m : Type u → Type u} → {α : Type u} → α → MLList.MLListImpl✝ m α → MLList.MLListImpl✝ m α
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Makes a continuous additive isomorphism from
a homeomorphism which preserves addition.  -/
ContinuousAddEquiv.mk' : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] →
        [inst_2 : Add M] → [inst_3 : Add N] → (f : M ≃ₜ N) → (∀ (x y : M), f (x + y) = f x + f y) → M ≃ₜ+ N
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsArtinianScheme.toCompactSpace : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsArtinianScheme X], CompactSpace ↥X
-- Mathlib.Order.Monotone.Basic
/-- If a monotone function is equal at two points, it is equal between all of them  -/
Monotone.eq_of_ge_of_le : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β} {a₁ a₂ : α},
  Monotone f → f a₁ = f a₂ → ∀ {i : α}, a₁ ≤ i → i ≤ a₂ → f i = f a₁
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.Quotient.OfSurjective.dpow.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [inst_1 : CommRing B]
  (f : A →+* B) (n : ℕ),
  DividedPowers.Quotient.OfSurjective.dpow hI f n = Function.extend (fun a => f ↑a) (fun a => f (hI.dpow n ↑a)) 0