mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- (Implementation): The covering object of `cylinder f g`.  -/
CategoryTheory.PreOneHypercover.cylinderX : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          [CategoryTheory.Limits.HasPullbacks C] → (f g : E.Hom F) → {i : E.I₀} → F.I₁ (f.s₀ i) (g.s₀ i) → C
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (f : (a : α) → β a → Bool)
  (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.filter f Std.DTreeMap.Internal.Impl.leaf hr_1 =
    { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add.eq_3 : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] (x₁ y₁ : F)
  (h₁ : W.Nonsingular x₁ y₁) (x₂ y₂ : F) (h₂ : W.Nonsingular x₂ y₂),
  (WeierstrassCurve.Affine.Point.some x₁ y₁ h₁).add (WeierstrassCurve.Affine.Point.some x₂ y₂ h₂) =
    if hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ then 0
    else
      WeierstrassCurve.Affine.Point.some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯
-- Mathlib.Topology.Order.Compact
/-- The **extreme value theorem**: if a continuous function `f` tends to negative infinity away from
compact sets, then it has a global maximum.  -/
Continuous.exists_forall_ge : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] [Nonempty β] {f : β → α},
  Continuous f → Filter.Tendsto f (Filter.cocompact β) Filter.atBot → ∃ x, ∀ (y : β), f y ≤ f x
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- A component of the natural transformation between right-derived functors can be computed
using a chosen injective resolution.  -/
CategoryTheory.InjectiveResolution.rightDerived_app_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  (α : F ⟶ G) {X : C} (P : CategoryTheory.InjectiveResolution X) (n : ℕ),
  (CategoryTheory.NatTrans.rightDerived α n).app X =
    CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom
      (CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex))
        (P.isoRightDerivedObj G n).inv)
-- Mathlib.Topology.Order.OrderClosed
Ioc_mem_nhdsGT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → Set.Ioc b a ∈ nhdsWithin b (Set.Ioi b)
-- Mathlib.Order.WithBot
WithBot.trichotomous.lt : ∀ {α : Type u_1} [inst : Preorder α] [Std.Trichotomous fun x1 x2 => x1 < x2], Std.Trichotomous fun x1 x2 => x1 < x2
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- `PiTensorProduct R s` with `R` a commutative semiring and `s : ι → Type*` is the tensor
product of all the `s i`'s. This is denoted by `⨂[R] i, s i`.  -/
PiTensorProduct : {ι : Type u_1} →
  (R : Type u_4) →
    [inst : CommSemiring R] →
      (s : ι → Type u_7) →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] → [(i : ι) → Module R (s i)] → Type (max (max u_1 u_4) u_7)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft'_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : C) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y z ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (CategoryTheory.inv f) z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z)
        h) =
    h
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
IsCompact.measure_lt_top_of_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  IsCompact s → (∀ x ∈ s, μ.FiniteAtFilter (nhdsWithin x s)) → μ s < ⊤
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_insertMany_list : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
        (∀ (a : α), m.contains a = true → (List.map Sigma.fst l).contains a = false) →
          (↑↑(m.insertMany l)).size = (↑m).size + l.length
-- Mathlib.CategoryTheory.Abelian.Basic
/-- Constructor for abelian categories. We assume that the category `C` is
preadditive, has finite products, and that any morphism `f : X ⟶ Y` has
a kernel `i : K ⟶ X`, a cokernel `p : Y ⟶ Q` such that `f` factors as `f = π ≫ ι`
where `π : X ⟶ I` is a cokernel of `i` and `ι : I ⟶ Y` is a kernel of `p`.
This assumption is packaged in a structure `AbelianStruct f`.  -/
CategoryTheory.Abelian.mk' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteProducts C] →
        (∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (CategoryTheory.Abelian.AbelianStruct f)) → CategoryTheory.Abelian C
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.piObjIso_inv_comp_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D) (s : α) {Z : C} (h : (f s).obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piObjIso f d).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Pi.π f s).app d) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun s => (f s).obj d) s) h
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
/-- Scalar multiplication in the colimit. See also `colimitSMulAux`.  -/
ModuleCat.FilteredColimits.colimitHasSMul : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) → SMul R ↑(ModuleCat.FilteredColimits.M F)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Fold a function from right to left (in decreasing order) across the tree.

```
foldr f {1, 2, 4} z = f 1 (f 2 (f 4 z))
```  -/
Ordnode.foldr : {α : Type u_1} → {β : Sort u_2} → (α → β → β) → Ordnode α → β → β
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.mk.sizeOf_spec : ∀ (G : Option Std.Time.Year.Era) (y u Y : Option Std.Time.Year.Offset) (D : Option (Sigma Std.Time.Day.Ordinal.OfYear))
  (M L : Option Std.Time.Month.Ordinal) (d : Option Std.Time.Day.Ordinal) (Q q : Option Std.Time.Month.Quarter)
  (w : Option Std.Time.Week.OfYear.Ordinal) (W : Option Std.Time.Week.Ordinal) (E e c : Option Std.Time.Weekday)
  (F : Option (Std.Time.Internal.Bounded.LE 1 5)) (a : Option Std.Time.HourMarker) (b : Option Std.Time.DayPeriod)
  (B : Option Std.Time.ExtendedDayPeriod) (h : Option (Std.Time.Internal.Bounded.LE 1 12))
  (K : Option (Std.Time.Internal.Bounded.LE 0 11)) (k : Option (Std.Time.Internal.Bounded.LE 1 24))
  (H : Option Std.Time.Hour.Ordinal) (m : Option Std.Time.Minute.Ordinal) (s : Option (Std.Time.Second.Ordinal true))
  (S : Option Std.Time.Nanosecond.Ordinal) (A : Option Std.Time.Millisecond.Offset)
  (n : Option Std.Time.Nanosecond.Ordinal) (N : Option Std.Time.Nanosecond.Offset) (V z zabbrev v : Option String)
  (O X x Z : Option Std.Time.TimeZone.Offset),
  sizeOf
      { G := G, y := y, u := u, Y := Y, D := D, M := M, L := L, d := d, Q := Q, q := q, w := w, W := W, E := E, e := e,
        c := c, F := F, a := a, b := b, B := B, h := h, K := K, k := k, H := H, m := m, s := s, S := S, A := A, n := n,
        N := N, V := V, z := z, zabbrev := zabbrev, v := v, O := O, X := X, x := x, Z := Z } =
    ⋯ + sizeOf E + sizeOf e + sizeOf c + sizeOf F + sizeOf a + sizeOf b + sizeOf B + sizeOf h + sizeOf K + sizeOf k +
                                  sizeOf H +
                                sizeOf m +
                              sizeOf s +
                            sizeOf S +
                          sizeOf A +
                        sizeOf n +
                      sizeOf N +
                    sizeOf V +
                  sizeOf z +
                sizeOf zabbrev +
              sizeOf v +
            sizeOf O +
          sizeOf X +
        sizeOf x +
      sizeOf Z
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.forget₂_algebra_obj : ∀ {R : Type u} [inst : CommRing R] (X : BialgCat R),
  (CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).obj X = AlgCat.of R X.carrier
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_cast_Iic : ∀ {n m : ℕ} (h : n = m) (i : Fin n), Finset.image (Fin.cast h) (Finset.Iic i) = Finset.Iic (Fin.cast h i)
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUTimes.mk.sizeOf_spec : ∀ (user nice sys idle irq : UInt64),
  sizeOf { user := user, nice := nice, sys := sys, idle := idle, irq := irq } =
    1 + sizeOf user + sizeOf nice + sizeOf sys + sizeOf idle + sizeOf irq
-- Mathlib.Algebra.CharP.MixedCharZero
/-- A ring of characteristic zero is not a `ℚ`-algebra iff it has mixed characteristic for some `p`.
 -/
isEmpty_algebraRat_iff_mixedCharZero : ∀ (R : Type u_1) [inst : CommRing R] [CharZero R], IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The cofork `biprod.inlCokernelFork` is indeed a colimit.  -/
CategoryTheory.Limits.biprod.isCokernelInlCokernelFork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.biprod.inlCokernelCofork X Y)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
fderivWithin_congr : ∀ {𝕜 : 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 f₁ : E → F} {x : E} {s : Set E},
  Set.EqOn f₁ f s → f₁ x = f x → fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePoint_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂), (s.map f.toAffineMap ⋯).mongePoint = f s.mongePoint
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Product of elements of a submonoid of a `CommMonoid` indexed by a `Finset` is in the
submonoid.  -/
prod_mem : ∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : CommMonoid M] [inst_1 : SetLike B M] [SubmonoidClass B M] {ι : Type u_5}
  {t : Finset ι} {f : ι → M}, (∀ c ∈ t, f c ∈ S) → ∏ c ∈ t, f c ∈ S
-- Batteries.Data.Fin.Lemmas
Fin.findRev?_one : ∀ {p : Fin 1 → Bool}, Fin.findRev? p = if p 0 = true then some 0 else none
-- Mathlib.GroupTheory.Finiteness
Group.closure_finset_fg : ∀ {G : Type u_3} [inst : Group G] (s : Finset G), Group.FG ↥(Subgroup.closure ↑s)
-- Std.Async.Basic
Std.Async.instMonadAsyncStateRefT' : {t m : Type → Type} → {s n : Type} → [Std.Async.MonadAsync t m] → Std.Async.MonadAsync t (StateRefT' s n m)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.restr_coe_symm : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α), ↑(e.restr s).symm = ↑e.symm
-- Init.Data.RArray
Lean.RArray.branch.inj : ∀ {α : Type u} {a : ℕ} {a_1 a_2 : Lean.RArray α} {a_3 : ℕ} {a_4 a_5 : Lean.RArray α},
  Lean.RArray.branch a a_1 a_2 = Lean.RArray.branch a_3 a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.Algebra.Module.RingHom
RingHom.toModule_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : R) (y : S), x • y = f x * y
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_homothetyUnitsMulHom_apply : ∀ {R : Type u_10} {V : Type u_11} {P : Type u_12} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] (p : P) (t : Rˣ), ⇑((AffineEquiv.homothetyUnitsMulHom p) t) = ⇑(AffineMap.homothety p ↑t)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_toList : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.toList.isEmpty = m.isEmpty
-- Init.Prelude
Nat.eq_of_beq_eq_true : ∀ {n m : ℕ}, n.beq m = true → n = m
-- Lean.Elab.Tactic.Simp
/-- Implement a `simp` discharge function using the given tactic syntax code.
Recall that `simp` dischargers are in `SimpM` which does not have access to `Term.State`.
We need access to `Term.State` to store messages and update the info tree.
Thus, we create an `IO.ref` to track these changes at `Term.State` when we execute `tacticCode`.
We must set this reference with the current `Term.State` before we execute `simp` using the
generated `Simp.Discharge`.  -/
Lean.Elab.Tactic.tacticToDischarge : Lean.Syntax → Lean.Elab.Tactic.TacticM (IO.Ref Lean.Elab.Term.State × Lean.Meta.Simp.Discharge)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finrank_eq_one_iff_eq_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : IntermediateField F E},
  Module.finrank (↥K) E = 1 ↔ K = ⊤
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∈ m₂ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.isLocalHomeomorphOn : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X},
  IsCoveringMapOn f s → IsLocalHomeomorphOn f (f ⁻¹' s)
-- Mathlib.Data.Fintype.Sets
Set.toFinset_inter : ∀ {α : Type u_1} (s t : Set α) [inst : DecidableEq α] [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t]
  [inst_3 : Fintype ↑(s ∩ t)], (s ∩ t).toFinset = s.toFinset ∩ t.toFinset
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [inst : Inhabited α] [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get! k = m₂.get! k
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
HomotopyEquiv.isKInjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {L₁ L₂ : CochainComplex C ℤ} (e : HomotopyEquiv L₁ L₂) [L₁.IsKInjective], L₂.IsKInjective
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- **Alias** of `ZetaAsymptotics.termSum_of_lt`. -/
ZetaAsymptotics.term_sum_of_lt : ∀ (N : ℕ) {s : ℝ},
  1 < s →
    ZetaAsymptotics.termSum s N =
      1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- `Matrix.conjTranspose` as a `StarAlgEquiv` to the opposite ring  -/
Matrix.conjTransposeAlgEquiv : (n : Type u_3) →
  {R : Type u_7} →
    (α : Type v) →
      [inst : Fintype n] →
        [inst_1 : CommSemiring R] →
          [inst_2 : StarRing R] →
            [TrivialStar R] →
              [inst_4 : Semiring α] →
                [inst_5 : StarRing α] →
                  [inst_6 : Algebra R α] → [StarModule R α] → Matrix n n α ≃⋆ₐ[R] (Matrix n n α)ᵐᵒᵖ
-- Mathlib.Logic.Small.Set
small_sUnion : ∀ {α : Type u1} (s : Set (Set α)) [Small.{u, u1} ↑s] [∀ (t : ↑s), Small.{u, u1} ↑↑t], Small.{u, u1} ↑(⋃₀ s)
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_Ioc : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ),
  Rat.cast ⁻¹' Set.Ioc ↑p ↑q = Set.Ioc p q
-- Lean.MetavarContext
/-- Similar to `findExprDependsOn`, but checks the expressions in the given local declaration
depends on a free variable `x` s.t. `pf x` is `true` or an unassigned metavariable `?m` s.t. `pm ?m` is true.
- When `generalizeNondepLet := true` (the default), then values of nondependent lets are ignored,
  for computing dependencies from "within" a telescope.
 -/
Lean.findLocalDeclDependsOn : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadMCtx m] →
      Lean.LocalDecl →
        (optParam (Lean.FVarId → Bool) fun x => false) →
          (optParam (Lean.MVarId → Bool) fun x => false) → optParam Bool true → m Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- For `I : MultispanIndex J C`, we say that it has a multicoequalizer if
the associated multicospan has a limit.  -/
CategoryTheory.Limits.HasMulticoequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} → CategoryTheory.Limits.MultispanIndex J C → Prop
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- A sufficient condition for the set of roots of a nonzero polynomial `f` to be a subset of the
set of roots of `g` is that `f` divides `f.derivative * g`. Over an algebraically closed field of
characteristic zero, this is also a necessary condition.
See `isRoot_of_isRoot_iff_dvd_derivative_mul`  -/
Polynomial.isRoot_of_isRoot_of_dvd_derivative_mul : ∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] {f g : Polynomial R},
  f ≠ 0 → f ∣ Polynomial.derivative f * g → ∀ {a : R}, f.IsRoot a → g.IsRoot a
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.biInf_le_nhds : ∀ (x : ENNReal), ⨅ ε, ⨅ (_ : ε > 0), Filter.principal (Set.Icc (x - ε) (x + ε)) ≤ nhds x
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- An extension `E / F` is purely inseparable if and only there is at most one
embedding `E →ₐ[F] AlgebraicClosure E`  -/
isPurelyInseparable_iff_subsingleton_emb : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IsPurelyInseparable F E ↔ Subsingleton (Field.Emb F E)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.le_restrict_empty : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v w : MeasureTheory.VectorMeasure α M), v.restrict ∅ ≤ w.restrict ∅
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.frequently_atBot' : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] {p : α → Prop} [Nonempty α] [NoMinOrder α],
  (∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b, a > b ∧ p b
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.lt_neg_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommGroup M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {a b : M}, a < -b ↔ b < -a
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_Ioi_eq_Ici : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (x : ℝ),
  derivWithin f (Set.Ioi x) x = derivWithin f (Set.Ici x) x
-- Mathlib.RingTheory.Valuation.Basic
/-- The `AddValuation` associated to a `Valuation`.
 -/
AddValuation.ofValuation : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] → Valuation R (Multiplicative Γ₀ᵒᵈ) ≃ AddValuation R Γ₀
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.free.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (I I_1 : Type u),
  I = I_1 → SheafOfModules.free I = SheafOfModules.free I_1
-- Mathlib.Analysis.Complex.ReImTopology
Complex.isOpenMap_re : IsOpenMap Complex.re
-- Init.Data.List.Basic
List.instReflBEq : ∀ {α : Type u} [inst : BEq α] [ReflBEq α], ReflBEq (List α)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_preimage_of_injective_of_subset_range : ∀ {α β : Type u} (f : α → β) (s : Set β),
  Function.Injective f → s ⊆ Set.range f → Cardinal.mk ↑(f ⁻¹' s) = Cardinal.mk ↑s
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_neg : ∀ (ctx : Int.Internal.Linear.Context) (p p' : Int.Internal.Linear.Poly),
  p'.beq' (p.mul (-1)) = true → Int.Internal.Linear.Poly.denote' ctx p ≠ 0 → Int.Internal.Linear.Poly.denote' ctx p' ≠ 0
-- Init.Data.List.Control
/-- Returns the first element of the list for which the monadic predicate `p` returns `true`, or `none`
if no such element is found. Elements of the list are checked in order.

`O(|l|)`.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
 -/
List.findM? : {m : Type → Type u} → [Monad m] → {α : Type} → (α → m Bool) → List α → m (Option α)
-- Mathlib.Algebra.Lie.Semisimple.Basic
/-- A semisimple Lie algebra has trivial radical.  -/
LieAlgebra.IsSemisimple.instHasTrivialRadical : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSemisimple R L], LieAlgebra.HasTrivialRadical R L
-- Init.Core
/-- `Trichotomous r` says that `r` is trichotomous, that is, `¬ r a b → ¬ r b a → a = b`.  -/
Std.Trichotomous : {α : Sort u} → (α → α → Prop) → Prop
-- Mathlib.Analysis.Normed.Lp.ProdLp
_private.Mathlib.Analysis.Normed.Lp.ProdLp.0.WithLp.edist_proj_le_edist_aux : ∀ (p : ENNReal) {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] (x y : WithLp p (α × β)),
  edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `left` co(ntra)variant.  -/
Left.one_lt_inv_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a : α}, 1 < a⁻¹ ↔ a < 1
-- Mathlib.Topology.Connected.Clopen
preimage_connectedComponent_connected : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  (∀ (t : β), IsConnected (f ⁻¹' {t})) → Topology.IsCoinducing f → ∀ (t : β), IsConnected (f ⁻¹' connectedComponent t)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.π_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g), c.π.app CategoryTheory.Limits.WalkingCospan.left = c.fst
-- Std.Internal.Do.WP.Lemmas
StateT.pure.eq_1 : ∀ {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (a : α) (s : σ), StateT.pure a s = pure (a, s)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.OuterRegular.outerRegular : ∀ {α : Type u_1} {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : μ.OuterRegular] ⦃A : Set α⦄, MeasurableSet A → ∀ r > μ A, ∃ U ⊇ A, IsOpen U ∧ μ U < r
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add_lt : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R} {g : Γ₀}, v x < g → v y < g → v (x + y) < g