mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiable_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  Differentiable 𝕜 Φ ↔ ∀ (i : ι), Differentiable 𝕜 fun x => Φ x i
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_map_C : ∀ {R : Type u_1} [inst : CommSemiring R] (f : Polynomial R),
  Polynomial.Bivariate.swap (Polynomial.map Polynomial.C f) = Polynomial.C f
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_pow_id : ∀ {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {n : ℕ}, 1 < n → (fun x => x ^ n) =o[nhds 0] fun x => x
-- Init.Data.FloatArray.Basic
FloatArray.mk.injEq : ∀ (data data_1 : Array Float), ({ data := data } = { data := data_1 }) = (data = data_1)
-- Mathlib.Logic.Equiv.Set
Equiv.ofInjective.congr_simp : ∀ {α : Sort u_3} {β : Type u_4} (f : α → β) (hf : Function.Injective f), Equiv.ofInjective f hf = Equiv.ofInjective f hf
-- Mathlib.Algebra.Order.GroupWithZero.Finset
Finset.sup'_mul_le_mul_sup'_of_nonneg : ∀ {ι : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] {s : Finset ι} {a b : ι → M₀} [inst_1 : SemilatticeSup M₀]
  [PosMulMono M₀] [MulPosMono M₀],
  (∀ i ∈ s, 0 ≤ a i) → (∀ i ∈ s, 0 ≤ b i) → ∀ (hs : s.Nonempty), s.sup' hs (a * b) ≤ s.sup' hs a * s.sup' hs b
-- Init.Tactics
/-- `rename t => x` renames the most recent hypothesis whose type matches `t`
(which may contain placeholders) to `x`, or fails if no such hypothesis could be found.
 -/
Lean.Parser.Tactic.rename : Lean.ParserDescr
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendHomologyIso_hom_homologyι_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'] {Z : C} (h : K.opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom
      (CategoryTheory.CategoryStruct.comp (K.homologyι j) h) =
    CategoryTheory.CategoryStruct.comp ((K.extend e).homologyι j')
      (CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').hom h)
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Compare the values of `PolynomialLaw.toFun'` in a square diagram  -/
PolynomialLaw.toFun'_eq_of_diagram : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {S : Type v} [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  (f : M →ₚₗ[R] N) {A : Type u} [inst_7 : CommSemiring A] [inst_8 : Algebra R A] {φ : A →ₐ[R] S}
  (p : TensorProduct R A M) {T : Type w} [inst_9 : CommSemiring T] [inst_10 : Algebra R T] {B : Type u}
  [inst_11 : CommSemiring B] [inst_12 : Algebra R B] {ψ : B →ₐ[R] T} (q : TensorProduct R B M) (h : S →ₐ[R] T)
  (h' : ↥φ.range →ₐ[R] ↥ψ.range),
  ψ.range.val.comp h' = h.comp φ.range.val →
    (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p =
        (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q →
      (LinearMap.rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' B q)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_eq_sInf : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (f : ℝ →+*o K) (x : K),
  ArchimedeanClass.stdPart x = sInf {r | x < f r}
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted subtraction, over the image of an embedding, equals a
weighted subtraction with the same points and weights over the
original `Finset`.  -/
Finset.weightedVSub_map : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P),
  ((Finset.map e s₂).weightedVSub p) w = (s₂.weightedVSub (p ∘ ⇑e)) (w ∘ ⇑e)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instSeparableSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [TopologicalSpace.SeparableSpace M], TopologicalSpace.SeparableSpace Mᵈᵃᵃ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.monoFactorisationZero_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X Y : C), (CategoryTheory.Limits.monoFactorisationZero X Y).m = 0
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Adjunction.isCocontinuous_iff_coverPreserving : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G), F.IsCocontinuous J K ↔ CategoryTheory.CoverPreserving K J G
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.mkUnit : Lean.MacroM Lean.Syntax
-- Mathlib.GroupTheory.PushoutI
/-- For any word `w` in the coproduct,
if `w` is reduced (i.e none its letters are in the image of the base monoid), and nonempty, then
`w` itself is not in the image of the base group.  -/
Monoid.PushoutI.Reduced.eq_empty_of_mem_range : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i},
  (∀ (i : ι), Function.Injective ⇑(φ i)) →
    ∀ {w : Monoid.CoprodI.Word G},
      Monoid.PushoutI.Reduced φ w →
        Monoid.PushoutI.ofCoprodI w.prod ∈ (Monoid.PushoutI.base φ).range → w = Monoid.CoprodI.Word.empty
-- Init.Data.Float.Model.Float32
Float32.Model.instDecidableLT : DecidableLT Float32.Model
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_div_den : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ) (i : m) (j : n),
  ↑(A.num i j) / ↑A.den = A i j
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_addSubgroup_orbit_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : AddSubgroup G} {x : α}
  {a b : ↑(AddAction.orbit G x)}, a ∈ AddAction.orbit (↥H) b ↔ ↑a ∈ AddAction.orbit ↥H ↑b
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsRat.neg_to_eq : ∀ {α : Type u_1} [inst : DivisionRing α] {n d : ℕ} {a n' d' : α},
  Mathlib.Meta.NormNum.IsRat a (Int.negOfNat n) d → ↑n = n' → ↑d = d' → a = -(n' / d')
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.deg_eq_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (e : X ≅ Y), r.deg X = r.deg Y
-- Mathlib.Analysis.Complex.Polynomial.GaussLucas
/-- The sum of the weights `derivRootWeight P z w` of all the roots `w` of `P` is positive,
provided that `P` is not a constant polynomial.  -/
Polynomial.sum_derivRootWeight_pos : ∀ {P : Polynomial ℂ}, 0 < P.degree → ∀ (z : ℂ), 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_erase_le_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = false → ∀ {fallback : α}, (cmp ((t.erase k).maxD fallback) (t.maxD fallback)).isLE = true
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Pullback the coefficients of an element of `R[N]` under an injective `f : M → N`.

Coefficients not in the range of `f` are dropped.  -/
MonoidAlgebra.comapDomain : {R : Type u_3} →
  {M : Type u_6} →
    {N : Type u_7} → [inst : Semiring R] → (f : M → N) → Function.Injective f → MonoidAlgebra R N → MonoidAlgebra R M
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGE?ₘ'.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} [inst : Ord α] (k : α)
  (motive : Option ((a : α) × β a) → Std.DTreeMap.Internal.Impl.ExplorationStep α β (compare k) → Sort u_3)
  (x : Option ((a : α) × β a)) (k' : α) (a : compare k k' = Ordering.lt) (v : β k') (a_1 : List ((a : α) × β a))
  (h_1 :
    (x : Option ((a : α) × β a)) →
      (k' : α) →
        (a : compare k k' = Ordering.lt) →
          (v : β k') →
            (a_2 : List ((a : α) × β a)) → motive x (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_2))
  (h_2 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (r : List ((a : α) × β a)) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a c r))
  (h_3 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (a_2 : α) →
          (a_3 : compare k a_2 = Ordering.gt) →
            (a_4 : β a_2) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_2 a_3 a_4)),
  (match x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_1 with
    | x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_2 => h_1 x k' a v a_2
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a c r => h_2 base a c r
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_2 a_3 a_4 => h_3 base a a_2 a_3 a_4) =
    h_1 x k' a v a_1
-- Init.Data.Dyadic.Basic
Dyadic.instMul : Mul Dyadic
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_uIoc : ∀ {a b : ℝ}, MeasureTheory.volume (Set.uIoc a b) = ENNReal.ofReal |b - a|
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.normEq0.eq_1 : ∀ (c : ℕ) (k : ℤ),
  (Lean.Grind.CommRing.Poly.num k).normEq0 c =
    bif k % ↑c == 0 then Lean.Grind.CommRing.Poly.num 0 else Lean.Grind.CommRing.Poly.num k
-- Mathlib.Analysis.Normed.Group.Pointwise
inv_sphere : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), (Metric.sphere x δ)⁻¹ = Metric.sphere x⁻¹ δ
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Creates an E-matching theorem for `declName` with `numParams` parameters, and the given set of patterns.
Pattern variables are represented using de Bruijn indices.
 -/
Lean.Meta.Grind.mkEMatchTheorem : Lean.Name →
  ℕ →
    List Lean.Expr →
      Lean.Meta.Grind.EMatchTheoremKind →
        Bool → List Lean.Meta.Grind.EMatchTheoremConstraint → Lean.MetaM Lean.Meta.Grind.EMatchTheorem
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.label : Lean.Lsp.InlayHint → Lean.Lsp.InlayHintLabel
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_of_xn_modEq : ∀ {a : ℕ} (a1 : 1 < a) {i j n : ℕ},
  i ≤ 2 * n →
    j ≤ 2 * n →
      Pell.xn a1 i ≡ Pell.xn a1 j [MOD Pell.xn a1 n] → (a = 2 → n = 1 → (i = 0 → j ≠ 2) ∧ (i = 2 → j ≠ 0)) → i = j
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot_mem_affineSpan : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.altitudeFoot i ∈ affineSpan ℝ (Set.range s.points)
-- Mathlib.RingTheory.Polynomial.Radical
divRadical_dvd_wronskian_right : ∀ {k : Type u_1} [inst : Field k] [inst_1 : DecidableEq k] (a b : Polynomial k),
  EuclideanDomain.divRadical b ∣ a.wronskian b
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.ofOpSequence.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X (n + 1) ⟶ X n),
  CategoryTheory.Functor.ofOpSequence f = (CategoryTheory.Functor.ofSequence fun n => (f n).op).leftOp
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instVAdd' : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → {M : Type u_5} → [VAdd M β] → VAdd (l.Germ M) (l.Germ β)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.hasEqualizer_of_self : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y), CategoryTheory.Limits.HasEqualizer f f
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstHMulNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.SaddlePoint
/-- The pair `(a, b)` is a saddle point of `f` on `X × Y`
if `f a y ≤ f x b` for all `x ∈ X` and all `y` in `Y`.

Note: we do not require that `a ∈ X` and `b ∈ Y`.  -/
IsSaddlePointOn : {E : Type u_1} → {F : Type u_2} → {β : Type u_3} → Set E → Set F → (E → F → β) → [Preorder β] → E → F → Prop
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_injective : ∀ {α : Type u_1} [inst : PartialOrder α], Function.Injective UpperSet.Ici
-- Mathlib.RingTheory.Morita.Matrix
/-- An `R`-linear map between `Eᵢᵢ • M` and `Eᵢᵢ • N` induced by an `Mₙ(R)`-linear map
from `M` to `N`.  -/
MatrixModCat.fromMatrixLinear : {R : Type u} →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] →
          {M : Type u_1} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module (Matrix ι ι R) M] →
                [inst_5 : Module R M] →
                  [inst_6 : IsScalarTower R (Matrix ι ι R) M] →
                    {N : Type u_2} →
                      [inst_7 : AddCommGroup N] →
                        [inst_8 : Module (Matrix ι ι R) N] →
                          (i : ι) →
                            [inst_9 : Module R N] →
                              [inst_10 : IsScalarTower R (Matrix ι ι R) N] →
                                (M →ₗ[Matrix ι ι R] N) →
                                  ↥(MatrixModCat.toModuleCatObj R M i) →ₗ[R] ↥(MatrixModCat.toModuleCatObj R N i)
-- Mathlib.Data.PNat.Basic
PNat.mod_le : ∀ (m k : ℕ+), m.mod k ≤ m ∧ m.mod k ≤ k
-- Qq.Macro
Qq.Impl.unquoteLevelMVar : Lean.Expr → Qq.Impl.UnquoteM Lean.Level
-- Mathlib.Algebra.Ring.CentroidHom
/-- Negation of `CentroidHom`s as a `CentroidHom`.  -/
CentroidHom.instNeg : {α : Type u_5} → [inst : NonUnitalNonAssocRing α] → Neg (CentroidHom α)
-- Mathlib.Order.LiminfLimsup
Filter.liminf_le_liminf_of_le : ∀ {α : Type u_6} {β : Type u_7} [inst : ConditionallyCompleteLattice β] {f g : Filter α},
  g ≤ f →
    ∀ {u : α → β},
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_liminf_of_le._auto_1 →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) g u) Filter.liminf_le_liminf_of_le._auto_3 →
          Filter.liminf u f ≤ Filter.liminf u g
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instModuleComplex : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    [Γ.HasDetOne] →
      {α : Type u_2} →
        [inst : Semiring α] → [inst_1 : Module α ℂ] → [IsScalarTower α ℂ ℂ] → Module α (SlashInvariantForm Γ k)
-- Mathlib.Topology.Order.HullKernel
/-- `T` order generates `α` if, for every `a` in `α`, there exists a subset of `T` such that `a` is
the `kernel` of `S`.  -/
PrimitiveSpectrum.OrderGenerates : {α : Type u_1} → [CompleteLattice α] → Set α → Prop
-- Mathlib.Order.IsNormal
Order.IsNormal.map_isSuccLimit : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [inst : LinearOrder α] [inst_1 : LinearOrder β],
  Order.IsNormal f → Order.IsSuccLimit a → Order.IsSuccLimit (f a)
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- If `X` is a completely regular T0 space with its Borel sigma algebra, then the mapping
that takes a point `x : X` to the delta-measure `diracProba x` is an embedding
`X → ProbabilityMeasure X`.  -/
MeasureTheory.isEmbedding_diracProba : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X] [T0Space X]
  [CompletelyRegularSpace X], Topology.IsEmbedding fun x => MeasureTheory.diracProba x
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {X Y : CategoryTheory.Center C} {x y : X.Hom Y}, x = y ↔ x.f = y.f
-- Init.Tactics
/-- Changes the goal to `False`, retaining as much information as possible:

* If the goal is `False`, do nothing.
* If the goal is an implication or a function type, introduce the argument and restart.
  (In particular, if the goal is `x ≠ y`, introduce `x = y`.)
* Otherwise, for a propositional goal `P`, replace it with `¬ ¬ P`
  (attempting to find a `Decidable` instance, but otherwise falling back to working classically)
  and introduce `¬ P`.
* For a non-propositional goal use `False.elim`.
 -/
Lean.Parser.Tactic.falseOrByContra : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] (c : F) {x : M}, (d% fun x => c) x = 0
-- Mathlib.CategoryTheory.Sites.Point.Map
/-- Given a cocontinuous functor `F : C ⥤ D` between sites `(C, J)` and `(D, K)`,
`P` a presheaf on `D`, then `(Φ.map F K).presheafFiber.obj P` is a colimit
of `P.obj (op (F.obj X))` for `X : C`, `x : Φ.fiber.obj X`.  -/
CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberMapCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          (Φ : J.Point) →
            (F : CategoryTheory.Functor C D) →
              (K : CategoryTheory.GrothendieckTopology D) →
                [inst_2 : F.IsCocontinuous J K] →
                  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] →
                    {A : Type u''} →
                      [inst_4 : CategoryTheory.Category.{v'', u''} A] →
                        [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] →
                          (P : CategoryTheory.Functor Dᵒᵖ A) →
                            CategoryTheory.Limits.IsColimit (Φ.presheafFiberMapCocone F K P)
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- The induced property by a local property `P`: it is satisfied for `f` at `x` iff there exist
charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively, such that `f` satisfies `P`
w.r.t. `φ` and `ψ`.

The motivating examples are smooth immersions and submersions: the corresponding condition is that
`f` look like the inclusion `u ↦ (u, 0)` (resp. a projection `(u, v) ↦ u`)
in the charts `φ` and `ψ`.
 -/
Manifold.LiftSourceTargetPropertyAt : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_4} →
      {H : Type u_6} →
        {G : Type u_8} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 F G →
                            {M : Type u_10} →
                              {N : Type u_12} →
                                [inst : TopologicalSpace M] →
                                  [ChartedSpace H M] →
                                    [inst_8 : TopologicalSpace N] →
                                      [ChartedSpace G N] →
                                        WithTop ℕ∞ →
                                          (M → N) →
                                            M →
                                              ((M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop) →
                                                Prop
-- Mathlib.Data.Rel
SetRel.image_empty_left : ∀ {α : Type u_1} {β : Type u_2} (s : Set α), ∅.image s = ∅
-- Init.Data.Int.Order
Int.sign_trichotomy : ∀ (a : ℤ), a.sign = 1 ∨ a.sign = 0 ∨ a.sign = -1
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- Every subgroups basis on a ring leads to a ring filter basis.  -/
RingSubgroupsBasis.toRingFilterBasis : {A : Type u_1} →
  {ι : Type u_2} → [inst : Ring A] → [Nonempty ι] → {B : ι → AddSubgroup A} → RingSubgroupsBasis B → RingFilterBasis A
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- **Alias** of `IntermediateField.restrictAlgEquiv`.

---

`F` is equivalent to `F` as an intermediate field of `E / K`.
 -/
IntermediateField.restrict_algEquiv : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → {F E : IntermediateField K L} → (h : F ≤ E) → ↥F ≃ₐ[K] ↥(IntermediateField.restrict h)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_uIoc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m '' Set.uIoc i j = Set.uIoc (Fin.castAdd m i) (Fin.castAdd m j)
-- Init.Grind.FieldNormNum
_private.Init.Grind.FieldNormNum.0.Lean.Grind.Field.NormNum.dvd_helper₂ : ∀ {z : ℤ} {n : ℕ}, z.natAbs.gcd n ∣ n
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddCommMonCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddCommMonCat)
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.comp_zsmul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) (n : ℤ), CategoryTheory.CategoryStruct.comp f (n • g) = n • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas.0.RootPairing.chainBotCoeff_mul_chainTopCoeff.aux_2 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : CharZero R]
  [inst_2 : IsDomain R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [inst_7 : Finite ι] [inst_8 : P.IsCrystallographic] {b : P.Base} {i j k l m : ι}
  [P.IsReduced] [P.IsIrreducible],
  i ∈ b.support →
    j ∈ b.support →
      i ≠ j →
        P.root k + P.root i = P.root l →
          P.root k - P.root j = P.root m →
            P.root k + P.root i - P.root j ∈ Set.range ⇑P.root →
              P.pairingIn ℤ k i < 0 →
                0 < P.pairingIn ℤ k j →
                  have this := ⋯;
                  P.root i + P.root m ∈ Set.range ⇑P.root →
                    P.root j + P.root (-l) ∈ Set.range ⇑P.root →
                      P.root j + P.root (-k) ∈ Set.range ⇑P.root →
                        ¬(RootPairing.chainBotCoeff i m = 1 ∧ RootPairing.chainBotCoeff j (-l) = 0)
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Multiset.range_succ' : ∀ {n nn n' : ℕ}, Mathlib.Meta.NormNum.IsNat n nn → nn = n'.succ → Multiset.range n = n' ::ₘ Multiset.range n'
-- Mathlib.LinearAlgebra.Dimension.Constructions
linearIndepOn_union_iff_quotient : ∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s t : Set ι}
  {f : ι → M},
  Disjoint s t →
    (LinearIndepOn R f (s ∪ t) ↔ LinearIndepOn R f s ∧ LinearIndepOn R (⇑(Submodule.span R (f '' s)).mkQ ∘ f) t)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_sub_left : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {f : ℝ → E},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ (c : ℝ),
      autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_sub_left._auto_1 →
        IntervalIntegrable (fun x => f (c - x)) MeasureTheory.volume (c - a) (c - b)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor set of `w` is a subset of `s`.  -/
SimpleGraph.isBipartiteWith_neighborSet_subset' : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → w ∈ t → G.neighborSet w ⊆ s