mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_neg_of_neg_of_neg_pi_lt : ∀ {x : ℝ}, x < 0 → -Real.pi < x → Real.sin x < 0
-- Mathlib.Analysis.Convex.Jensen
/-- A form of the **equality case of Jensen's equality** for the case of strict convex and
non-negative weights.  -/
StrictConvexOn.map_sum_eq_iff_of_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔
            ∀ ⦃j : ι⦄, j ∈ t → w j ≠ 0 → ∀ ⦃k : ι⦄, k ∈ t → w k ≠ 0 → p j = p k)
-- Mathlib.NumberTheory.FactorisationProperties
Nat.abundant_iff_two_lt_abundancyIndex : ∀ {n : ℕ}, n.Abundant ↔ 2 < n.abundancyIndex
-- Init.Data.Dyadic.Basic
Dyadic.neg.eq_2 : ∀ (n k : ℤ) (hn : n % 2 = 1), (Dyadic.ofOdd n k hn).neg = Dyadic.ofOdd (-n) k ⋯
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instOrdUnitVal : {x : ℚ} → Ord (Std.Time.Internal.UnitVal x)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- **Alias** of `SimpleGraph.not_cliqueFree_iff_top_isContained`. -/
SimpleGraph.not_cliqueFree_iff : ∀ {α : Type u_1} {G : SimpleGraph α} (n : ℕ), ¬G.CliqueFree n ↔ (SimpleGraph.completeGraph (Fin n)).IsContained G
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.hasSum_coe : ∀ {α : Type u_2} {L : SummationFilter α} {f : α → NNReal} {r : NNReal}, HasSum (fun a => ↑(f a)) (↑r) L ↔ HasSum f r L
-- Mathlib.CategoryTheory.Action.Concrete
TypeCat.endEquiv_symm_apply : ∀ (X : Type u) (f : CategoryTheory.End X) (a : X),
  (TypeCat.endEquiv X).symm f a = (CategoryTheory.ConcreteCategory.hom f) a
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_sub : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_1} [inst : Sub R] (A B : Matrix m n R), (A - B).vec = A.vec - B.vec
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuous_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  (UpperHemicontinuous fun x => {f x}) ↔ Continuous f
-- Mathlib.Algebra.Ring.Commute
eq_or_eq_neg_of_sq_eq_sq : ∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] (a b : R), a ^ 2 = b ^ 2 → a = b ∨ a = -b
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- An affine cover of `X` consists of a jointly surjective family of maps into `X` from
spectra of rings.

Note: The `map_prop` field is equipped with a default argument `by infer_instance`. In general
this causes worse error messages, but in practice `P` is mostly defined via `class`.
 -/
AlgebraicGeometry.Scheme.AffineCover : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type (max (u + 1) (v + 1))
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : SeminormedAddGroup E]
  {ι : Type u_3} [Nonempty ι] [inst_2 : LinearOrder ι] {f : ι → α → E} {f_lim : α → E},
  (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
    MeasureTheory.eLpNorm f_lim ⊤ μ = essSup (fun x => Filter.liminf (fun m => ‖f m x‖ₑ) Filter.atTop) μ
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.homFromEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (f : X ⟶ Z),
  α.homFromEquiv f = CategoryTheory.CategoryStruct.comp α.inv f
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.recArgPos : Lean.Elab.Structural.EqnInfo → ℕ
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalTower_ofId : ∀ {S : Type v} {A' : Type u_1} [inst : CommSemiring A'] [inst_1 : CommSemiring S] [inst_2 : Algebra S A'],
  Polynomial.aevalTower (Algebra.ofId S A') = Polynomial.aeval
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul_nc.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (m₁ : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (pw : Lean.Grind.CommRing.Power) → motive (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit))
  (h_3 :
    (pw : Lean.Grind.CommRing.Power) → (m₁ : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult pw m₁))
  (pw : Lean.Grind.CommRing.Power),
  m₁ = Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit →
    (match m₁ with
      | Lean.Grind.CommRing.Mon.unit => h_1 ()
      | Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit => h_2 pw
      | Lean.Grind.CommRing.Mon.mult pw m₁ => h_3 pw m₁) ≍
      h_2 pw
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.basis_nhds : ∀ {X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X]
  {p : ι → Prop} {s : ι → Set Y},
  Topology.IsInducing f → ∀ {x : X}, (nhds (f x)).HasBasis p s → (nhds x).HasBasis p (Set.preimage f ∘ s)
-- Mathlib.Order.Category.BddLat
BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd : (CategoryTheory.forget₂ BddLat SemilatSupCat).comp (CategoryTheory.forget₂ SemilatSupCat PartOrd) =
  (CategoryTheory.forget₂ BddLat BddOrd).comp (CategoryTheory.forget₂ BddOrd PartOrd)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Let `V` be a vector bundle over a σ-compact Hausdorff finite-dimensional topological manifold
`M`. Let `t : M → Set (V x)` be a family of convex sets in the fibers of `V`.
Suppose that for each point `x₀ : M` there exists a neighborhood `U_x₀` of `x₀` and a local
section `s_loc : M → V x` such that `s_loc` is $C^n$ smooth on `U_x₀` (when viewed as a map to
the total space of the bundle) and `s_loc y ∈ t y` for all `y ∈ U_x₀`.
Then there exists a global $C^n$ smooth section `s : Cₛ^n⟮I_M; F_fiber, V⟯` such that
`s x ∈ t x` for all `x : M`.
 -/
exists_contMDiffSection_forall_mem_convex_of_local : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] [T2Space M] {n : ℕ∞} {F_fiber : Type u_1}
  [inst_9 : NormedAddCommGroup F_fiber] [inst_10 : NormedSpace ℝ F_fiber] (V : M → Type u_2)
  [inst_11 : (x : M) → AddCommGroup (V x)] [inst_12 : (x : M) → TopologicalSpace (V x)]
  [inst_13 : (x : M) → Module ℝ (V x)] [inst_14 : TopologicalSpace (Bundle.TotalSpace F_fiber V)]
  [inst_15 : FiberBundle F_fiber V] [VectorBundle ℝ F_fiber V] (t : (x : M) → Set (V x)),
  (∀ (x : M), Convex ℝ (t x)) →
    (∀ (x₀ : M),
        ∃ U_x₀ ∈ nhds x₀,
          ∃ s_loc,
            ContMDiffOn I (I.prod (modelWithCornersSelf ℝ F_fiber)) (↑n) (fun x => ⟨x, s_loc x⟩) U_x₀ ∧
              ∀ y ∈ U_x₀, s_loc y ∈ t y) →
      ∃ s, ∀ (x : M), s x ∈ t x
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- A function which is continuous on a set `s` is almost everywhere measurable with respect to
`μ.restrict s`.  -/
ContinuousOn.aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_2 : MeasurableSpace β] [inst_3 : TopologicalSpace β] [BorelSpace β] {f : α → β} {s : Set α}
  {μ : MeasureTheory.Measure α}, ContinuousOn f s → MeasurableSet s → AEMeasurable f (μ.restrict s)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.le_opNorm_mul_pow_of_le : ∀ {𝕜 : Type u} {G : Type wG} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] {n : ℕ} {Ei : Fin n → Type u_1} [inst_3 : (i : Fin n) → SeminormedAddCommGroup (Ei i)]
  [inst_4 : (i : Fin n) → NormedSpace 𝕜 (Ei i)] (f : ContinuousMultilinearMap 𝕜 Ei G) {m : (i : Fin n) → Ei i} {b : ℝ},
  ‖m‖ ≤ b → ‖f m‖ ≤ ‖f‖ * b ^ n
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `ColimitCocone F` contains a cocone over `F` together with the information that it is a
colimit.  -/
CategoryTheory.Limits.ColimitCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor J C → Type (max (max u u₁) v)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_maxKey?_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true → t.maxKey?.isSome = true
-- Mathlib.Topology.Algebra.Module.PerfectPairing
LinearMap.IsContPerfPair.mk : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : TopologicalSpace N] {p : M →ₗ[R] N →ₗ[R] R}
  (continuous_uncurry :
    Continuous fun x =>
      match x with
      | (x, y) => (p x) y),
  (Function.Bijective fun x => { toLinearMap := p x, cont := ⋯ }) →
    (Function.Bijective fun y => { toLinearMap := p.flip y, cont := ⋯ }) → p.IsContPerfPair
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.contains a = true → t.getKey? a = some (t.getKey! a)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_zero : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂},
  LinearMap.ker 0 = ⊤
-- Std.Time.Format.Modifier
Std.Time.ZoneName.full.sizeOf_spec : sizeOf Std.Time.ZoneName.full = 1
-- Mathlib.RingTheory.Localization.NormTrace
/-- The norm of `a : S` in `R` can be computed in `Sₘ`.  -/
Algebra.norm_eq_iff : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
  {Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] [inst_5 : CommRing Sₘ] [inst_6 : Algebra S Sₘ]
  {M : Submonoid R} [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_9 : Algebra Rₘ Sₘ]
  [inst_10 : Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [Module.Free R S] [Module.Finite R S] {a : S}
  {b : R},
  M ≤ nonZeroDivisors R → ((Algebra.norm R) a = b ↔ (Algebra.norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) b)
-- Lean.Elab.Tactic.Omega.OmegaM
/-- The atoms up-to-defeq encountered so far.  -/
Lean.Elab.Tactic.Omega.State.atoms : Lean.Elab.Tactic.Omega.State → Std.HashMap Lean.Expr ℕ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.self_le_maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k} {fallback : α}, (cmp k ((t.insert k v).maxKeyD fallback)).isLE = true
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α}, ∅[a]? = none
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insertMany_append : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {l₁ l₂ : List (α × β)},
  t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitCoyonedaHomIsoLimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor Iᵒᵖ C) (F : CategoryTheory.Functor C (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.rightOp.comp CategoryTheory.coyoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))],
  CategoryTheory.Limits.colimitCoyonedaHomIsoLimit D F =
    CategoryTheory.Limits.colimitHomIsoLimitYoneda (D.rightOp.comp CategoryTheory.coyoneda) F ≪≫
      CategoryTheory.Limits.HasLimit.isoOfNatIso
        ((D.comp (CategoryTheory.Prod.sectL C F)).isoWhiskerLeft (CategoryTheory.coyonedaLemma C))
-- Lean.Message
Lean.toMessageList : Array Lean.MessageData → Lean.MessageData
-- Mathlib.Data.Int.Init
Int.gcd_ofNat_negSucc : ∀ (m n : ℕ), (↑m).gcd (Int.negSucc n) = m.gcd (n + 1)
-- Mathlib.Topology.EMetricSpace.Defs
/-- Triangle inequality for the extended distance  -/
edist_triangle_left : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y z : α), edist x y ≤ edist z x + edist z y
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x y : β),
  CauSeq.const abv (x + y) = CauSeq.const abv x + CauSeq.const abv y
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.coe_sumMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α ↪ β) (e₂ : γ ↪ δ),
  ⇑(e₁.sumMap e₂) = Sum.map ⇑e₁ ⇑e₂
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The unit rank of the number field `K`, it is equal to `card (InfinitePlace K) - 1`.  -/
NumberField.Units.rank : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℕ
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α →ₘ[μ] E}, f ∈ MeasureTheory.Lp E p μ ↔ MeasureTheory.eLpNorm (↑f) p μ < ⊤
-- Init.Grind.Lemmas
Lean.Grind.ne_of_ne_of_eq_left : ∀ {α : Sort u} {a b c : α}, a = b → b ≠ c → a ≠ c
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.circleTransformDeriv_periodic : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (R : ℝ) (z w : ℂ) (f : ℂ → E),
  Function.Periodic (Complex.circleTransformDeriv R z w f) (2 * Real.pi)
-- Init.Data.Iterators.Lemmas.Combinators.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.ULift.0.Std.Iter.step_uLift.match_1.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2)
  (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety.eq_1 : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r : k),
  AffineMap.homothety c r = r • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.const k P1 c
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_sInf : ∀ {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph) (v : V),
  (sInf s).neighborSet v = (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v
-- Mathlib.RingTheory.Ideal.Over
/-- Consider the following commutative diagram of ring maps
```
A → B
↓   ↓
C → D
```
and let `P` be an ideal of `B`. Assume that the image in `C` of the ideal of `A` under `P`
is maximal and that the image of `P` in `D` is not equal to `D`, then the image in `C` of the
ideal of `A` under `P` is equal to the ideal of `C` under the image of `P` in `D`.
 -/
Ideal.under_map_eq_map_under : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : CommSemiring B] [inst_2 : Algebra A B] (P : Ideal B)
  {C : Type u_5} {D : Type u_6} [inst_3 : CommSemiring C] [inst_4 : Semiring D] [inst_5 : Algebra A C]
  [inst_6 : Algebra C D] [inst_7 : Algebra A D] [inst_8 : Algebra B D] [IsScalarTower A C D] [IsScalarTower A B D],
  (Ideal.map (algebraMap A C) (Ideal.under A P)).IsMaximal →
    Ideal.map (algebraMap B D) P ≠ ⊤ →
      Ideal.under C (Ideal.map (algebraMap B D) P) = Ideal.map (algebraMap A C) (Ideal.under A P)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.instMax : {α : Type u_1} → [inst : TopologicalSpace α] → Max (TopologicalSpace.PositiveCompacts α)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- **Alias** of `CategoryTheory.Functor.map_isPushout`. -/
CategoryTheory.IsPushout.map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F],
  CategoryTheory.IsPushout f g h i → CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- A submodule `S` is a core of `f` if the closure of the restriction of `f` to `S` is `f`.  -/
LinearPMap.HasCore : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] →
                    [ContinuousAdd E] →
                      [ContinuousAdd F] →
                        [inst_9 : TopologicalSpace R] →
                          [ContinuousSMul R E] → [ContinuousSMul R F] → (E →ₗ.[R] F) → Submodule R E → Prop
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.map_roots_comp_C_mul_X_add_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R) (a b : R),
  IsUnit a → Multiset.map (fun x => a * x + b) (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)).roots = p.roots
-- Init.Data.List.Lemmas
List.head!_of_head? : ∀ {α : Type u_1} {a : α} [inst : Inhabited α] {l : List α}, l.head? = some a → l.head! = a
-- Mathlib.Topology.Order
generateFrom_iInter : ∀ {α : Type u} {ι : Sort v} (f : ι → TopologicalSpace α), TopologicalSpace.generateFrom (⋂ i, {s | IsOpen s}) = ⨆ i, f i
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_iff_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∈ m ↔ m.contains a = true
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of a strictly monotone function and a monotone function is
strictly monotone.  -/
StrictMonoOn.add_monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [AddLeftMono α] [AddRightStrictMono α], StrictMonoOn f s → MonotoneOn g s → StrictMonoOn (fun x => f x + g x) s
-- Mathlib.Algebra.Group.ULift
ULift.zero : {α : Type u} → [Zero α] → Zero (ULift.{u_1, u} α)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.LHom.onTheory_model : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] [inst_1 : L'.Structure M]
  (φ : L →ᴸ L') [φ.IsExpansionOn M] (T : L.Theory), M ⊨ φ.onTheory T ↔ M ⊨ T
-- Init.Data.Array.Lemmas
Array.size_append : ∀ {α : Type u_1} {xs ys : Array α}, (xs ++ ys).size = xs.size + ys.size
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra)
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (X : J),
  (CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone D c).ι.app X =
    CategoryTheory.CategoryStruct.comp (D.obj X).a (T.map (c.ι.app X))
-- Mathlib.RepresentationTheory.Coinduced
Representation.coindMap_coe_apply_apply : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  {A : Type u_4} {B : Type u_5} [inst_3 : AddCommMonoid A] [inst_4 : Module k A] [inst_5 : AddCommMonoid B]
  [inst_6 : Module k B] (σ : Representation k G A) (ρ : Representation k G B) (f : σ.IntertwiningMap ρ)
  (x : ↥(Representation.coindV φ σ)) (h : H), ↑((Representation.coindMap φ f) x) h = f (↑x h)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instOrderTop.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenSubgroup.instOrderTop = { toTop := OpenSubgroup.instTop, le_top := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- If `D` is an injection into a linear order `B`, the leading coefficient of `f : R[A]` is the
nonzero coefficient of highest degree according to `D`, or 0 if `f = 0`. In general, it is defined
to be the coefficient at an inverse image of `supDegree f` (if such exists).  -/
AddMonoidAlgebra.leadingCoeff : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_5} →
      [inst : Semiring R] → [inst_1 : LinearOrder B] → [OrderBot B] → (A → B) → [Nonempty A] → AddMonoidAlgebra R A → R
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α},
  m.WF → (Array.find? (fun x => x.1 == k) (Std.DHashMap.Raw.Const.toArray m) = none ↔ m.contains k = false)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq_id : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantTo i₀) [inst_2 : CategoryTheory.IsCofiltered J],
  h.coneπApp i₀ = CategoryTheory.CategoryStruct.id (F.obj i₀)
-- Mathlib.NumberTheory.Multiplicity
sq_dvd_add_pow_sub_sub : ∀ {R : Type u_1} [inst : CommRing R] (p x : R) (n : ℕ), p ^ 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * ↑n - x ^ n
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- Show that if the two given cofans in `extendCofan` are colimits,
then the constructed cofan is also a colimit.
 -/
CategoryTheory.extendCofanIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      (f : Fin (n + 1) → C) →
        {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} →
          {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} →
            CategoryTheory.Limits.IsColimit c₁ →
              CategoryTheory.Limits.IsColimit c₂ → CategoryTheory.Limits.IsColimit (CategoryTheory.extendCofan c₁ c₂)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → β → γ} {k : α},
  (Std.ExtHashMap.map f m).getKey! k = m.getKey! k