mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Closure
interior_iInter₂_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort v} (p : ι → Sort u_1) (s : (i : ι) → p i → Set X),
  interior (⋂ i, ⋂ j, s i j) ⊆ ⋂ i, ⋂ j, interior (s i j)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Given a local frame `s i` on open set `u` containing `x`, if a section `t`
has differentiable coefficients at `x ∈ u` w.r.t. `s i`, then `t` is differentiable at `x`.  -/
IsLocalFrameOn.mdifferentiableAt_of_coeff_aux : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {x : M} {t : (x : M) → V x} [VectorBundle 𝕜 F V] (hs : IsLocalFrameOn I F 1 s u) [FiniteDimensional 𝕜 F],
  (∀ (i : ι), MDiffAt ((LinearMap.piApply (hs.coeff i)) t) x) → IsOpen u → x ∈ u → MDiffAt (T% t) x
-- Batteries.Data.UnionFind.Basic
Batteries.UFNode.mk.inj : ∀ {parent rank parent_1 rank_1 : ℕ},
  { parent := parent, rank := rank } = { parent := parent_1, rank := rank_1 } → parent = parent_1 ∧ rank = rank_1
-- Init.Prelude
/-- Congruence in the function part of an application: If `f = g` then `f a = g a`.  -/
congrFun : ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The field `ι` interprets an element of `D` as a functor `C ⥤ V`.  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.faithful_ι : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {V : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} V}
  {inst_2 : CategoryTheory.MonoidalCategory C} {inst_3 : CategoryTheory.MonoidalCategory V} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D} {inst_5 : CategoryTheory.MonoidalCategoryStruct D}
  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D],
  (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).Faithful
-- Init.Data.Nat.Lemmas
Nat.div_pow_of_pos : ∀ (a n : ℕ), n > 0 → a ∣ a ^ n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.BVVar.mk.inj : ∀ {width ident ident_1 : ℕ}, { ident := ident } = { ident := ident_1 } → ident = ident_1
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.exists_pos_measure_of_cover : ∀ {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {U : ι → Set α},
  ⋃ i, U i = Set.univ → μ ≠ 0 → ∃ i, 0 < μ (U i)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.coe_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (K : AddSubgroup N) (f : G →+ N),
  ↑(AddSubgroup.comap f K) = ⇑f ⁻¹' ↑K
-- Mathlib.Algebra.Star.Unitary
/-- In a \*-monoid, `unitary R` is the submonoid consisting of all the elements `U` of
`R` such that `star U * U = 1` and `U * star U = 1`.
 -/
unitary : (R : Type u_1) → [inst : Monoid R] → [StarMul R] → Submonoid R
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The coweight space representation of endomorphisms  -/
RootPairing.Hom.coweightHom : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → P.End →* (N →ₗ[R] N)ᵐᵒᵖ
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_unitor : ∀ (C : Type u) (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.FreeMonoidalCategory C)) n =
    CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as })
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Do not use this. Use `_root_.mul_lt_mul_of_pos_right` instead.  -/
MulPosStrictMono.mul_lt_mul_of_pos_right : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : Zero α} {inst_2 : Preorder α} [self : MulPosStrictMono α] ⦃c : α⦄,
  0 < c → ∀ ⦃a b : α⦄, a < b → a * c < b * c
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.and_self_right : ∀ (a b : ℕ), a &&& b &&& b = a &&& b
-- Mathlib.Topology.Category.Sequential
Sequential.isoOfHomeo_hom : ∀ {X Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop),
  (Sequential.isoOfHomeo f).hom =
    CategoryTheory.InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f, continuous_toFun := ⋯ })
-- Init.Data.Vector.Lex
Vector.le_trans' : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  [Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2] {xs ys zs : Vector α n},
  xs ≤ ys → ys ≤ zs → xs ≤ zs
-- Mathlib.Algebra.Homology.Localization
HomotopyCategory.quotient_map_mem_quasiIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  {K L : HomologicalComplex C c} (f : K ⟶ L),
  HomotopyCategory.quasiIso C c ((HomotopyCategory.quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- If `G₀` is a group with zero with measurable multiplication, then left multiplication by a
nonzero element `g : G₀` is a measurable automorphism of `G₀`.  -/
MeasurableEquiv.mulLeft₀ : {G₀ : Type u_2} →
  [inst : GroupWithZero G₀] → [inst_1 : MeasurableSpace G₀] → [MeasurableMul G₀] → (g : G₀) → g ≠ 0 → G₀ ≃ᵐ G₀
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_balanceL : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α},
  l.Balanced →
    r.Balanced →
      l.Sized →
        r.Sized →
          ((∃ l', Ordnode.Raised l' l.size ∧ Ordnode.BalancedSz l' r.size) ∨
              ∃ r', Ordnode.Raised r.size r' ∧ Ordnode.BalancedSz l.size r') →
            (Ordnode.All P (l.balanceL x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r)
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.mem_nsmul : ∀ {α : Type u_1} {a : α} {s : Multiset α} {n : ℕ}, a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.postcomposing_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b c : B) (f : b ⟶ c),
  (CategoryTheory.Bicategory.postcomposing a b c).obj f = CategoryTheory.Bicategory.postcomp a f
-- Mathlib.CategoryTheory.Functor.Currying
/-- `F.flip` is isomorphic to uncurrying `F`, swapping the variables, and currying.  -/
CategoryTheory.Functor.flipIsoCurrySwapUncurry : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} E] →
            (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) →
              F.flip ≅
                CategoryTheory.Functor.curry.obj
                  ((CategoryTheory.Prod.swap D C).comp (CategoryTheory.Functor.uncurry.obj F))
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
_private.Mathlib.CategoryTheory.Triangulated.SpectralObject.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_4 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (i : ℕ) (hi : i + 1 < n + 1 + 1) (j : ℕ)
  (hj : j + 1 < n + 1 + 1) (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩)
  (h_1 : (isLt isLt_1 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_1 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij with
    | ⟨0, isLt⟩, ⟨0, isLt_1⟩, x => h_1 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨1, isLt_1⟩, x => h_2 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_4 i hi j hj hij
-- Init.Data.String.Basic
String.Slice.Pos.offset_sliceTo : ∀ {s : String.Slice} {p₀ pos : s.Pos} {h : pos ≤ p₀}, (p₀.sliceTo pos h).offset = pos.offset
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_toArray_iff_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {k : α} {v : β},
  (k, v) ∈ m.toArray ↔ m[k]? = some v
-- Mathlib.Topology.Algebra.UniformField
UniformSpace.Completion.continuous_hatInv : ∀ {K : Type u_1} [inst : Field K] [inst_1 : UniformSpace K] [CompletableTopField K] {x : UniformSpace.Completion K},
  x ≠ 0 → ContinuousAt UniformSpace.Completion.hatInv x
-- Init.Data.SInt.Lemmas
ISize.toBitVec_toInt32 : ∀ (x : ISize), x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_eq_false_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = true → t.isEmpty = false
-- Lean.Parser.Extension
Lean.Parser.withOpenDecl : Lean.Parser.Parser → Lean.Parser.Parser
-- Init.Data.Nat.Basic
Nat.le_add_right_of_le : ∀ {n m k : ℕ}, n ≤ m → n ≤ m + k
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.isIso_iff_of_hasRightResolutions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_4} {H : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} H] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.HasRightResolutions] {F G : CategoryTheory.Functor D₂ H}
  (α : F ⟶ G), CategoryTheory.IsIso α ↔ ∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.rel₂_of_memoizedLeft : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Productive α₁ m] [inst_3 : Std.Iterators.Finite α₂ m] {right : Std.IterM m β₂}
  {b' b : Option { out // ∃ it, it.IsPlausibleOutput out }} {left' left : Std.IterM m β₁},
  Option.SomeLtNone.lt emptyRelation b' b →
    Std.Iterators.Types.Zip.Rel₂ m { internalState := { left := left, memoizedLeft := b', right := right } }
      { internalState := { left := left', memoizedLeft := b, right := right } }
-- Mathlib.Topology.ContinuousMap.Basic
/-- A family `φ i` of continuous maps `C(S i, β)`, where the domains `S i` contain a neighbourhood
of each point in `α` and the functions `φ i` agree pairwise on intersections, can be glued to
construct a continuous map in `C(α, β)`.  -/
ContinuousMap.liftCover : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {ι : Type u_5} →
          (S : ι → Set α) →
            (φ : (i : ι) → C(↑(S i), β)) →
              (∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩) →
                (∀ (x : α), ∃ i, S i ∈ nhds x) → C(α, β)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.trans : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet α cmp}, t₁.Equiv t₂ → t₂.Equiv t₃ → t₁.Equiv t₃
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_iInf : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal}, a + iInf f = ⨅ b, a + f b
-- Init.Data.Sum.Lemmas
Sum.getLeft?_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, x.getLeft? = none ↔ x.isRight = true
-- Init.Data.List.Nat.Range
List.find?_range_eq_none : ∀ {n : ℕ} {p : ℕ → Bool}, List.find? p (List.range n) = none ↔ ∀ i < n, (!p i) = true
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α), M.transpose.transpose = M
-- Mathlib.Order.Filter.Extr
IsMinFilter.inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {f g : α → β} {a : α} {l : Filter α},
  IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => f x ⊓ g x) l a
-- Mathlib.RingTheory.Localization.Integral
/-- `coeffIntegerNormalization p` gives the coefficients of the polynomial
`integerNormalization p`  -/
IsLocalization.coeffIntegerNormalization : {R : Type u_1} →
  [inst : CommRing R] →
    (M : Submonoid R) →
      {S : Type u_2} → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [IsLocalization M S] → Polynomial S → ℕ → R
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.neg : ∀ {G : Type u_4} [inst : InvolutiveNeg G] [inst_1 : TopologicalSpace G] [ContinuousNeg G] {s : Set G},
  IsPathConnected s → IsPathConnected (-s)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.ofMapRelIff_coe : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α → β) [inst : Std.Antisymm r]
  [inst_1 : Std.Refl s] (hf : ∀ (a b : α), s (f a) (f b) ↔ r a b), ⇑(RelEmbedding.ofMapRelIff f hf) = f
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.sphere_zero_eq : ∀ {n : Type u_7} [inst : Fintype n] (r : ℝ), 0 ≤ r → Metric.sphere 0 r = {x | ∑ i, x.ofLp i ^ 2 = r ^ 2}
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.addSubgroupCongr_apply : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H = K) (x : ↥H), ↑((AddEquiv.addSubgroupCongr h) x) = ↑x
-- Mathlib.Data.Quot
Quotient.mk_eq_iff_out : ∀ {α : Sort u_1} {s : Setoid α} {x : α} {y : Quotient s}, ⟦x⟧ = y ↔ x ≈ y.out
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.mapPushoutAdj_unit_app : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition] [inst_3 : Q.IsStableUnderCobaseChange]
  (f : X ⟶ Y) [inst_4 : P.HasPushoutsAlong f] [inst_5 : P.IsStableUnderCobaseChangeAlong f]
  [inst_6 : Q.HasOfPrecompProperty Q] (hPf : P f) (hQf : Q f) (A : P.Under Q X),
  (CategoryTheory.MorphismProperty.Under.mapPushoutAdj P Q f hPf hQf).unit.app A =
    CategoryTheory.MorphismProperty.Under.homMk (CategoryTheory.Limits.pushout.inl A.hom f) ⋯ ⋯
-- Mathlib.Data.Set.NAry
/-- The other direction does not hold because of the `u`-`u` cross terms on the RHS.  -/
Set.image2_distrib_subset_right : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {s : Set α}
  {t : Set β} {u : Set γ} {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'} {f₂ : β → γ → β'} {g' : α' → β' → ε},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)) →
    Set.image2 f (Set.image2 g s t) u ⊆ Set.image2 g' (Set.image2 f₁ s u) (Set.image2 f₂ t u)
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
RingSeminorm.toRingNorm.congr_simp : ∀ {K : Type u_2} [inst : Field K] (f f_1 : RingSeminorm K) (e_f : f = f_1) (hnt : f ≠ 0),
  f.toRingNorm hnt = f_1.toRingNorm ⋯
-- Mathlib.Data.Int.Lemmas
Int.natAbs_eq_iff_sq_eq : ∀ {a b : ℤ}, a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_zpow_apply_self : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (x : α) (n : ℤ), (f.cycleOf x ^ n) x = (f ^ n) x
-- Std.Data.HashSet.Raw
/-- Two hash sets are equivalent in the sense of `Equiv` iff all their values are equal.
 -/
Std.HashSet.Raw.«term_~m_» : Lean.TrailingParserDescr
-- Init.Data.Vector.Lemmas
Vector.toArray_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n},
  (Vector.map f xs).toArray = Array.map f xs.toArray
-- Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
HomologicalComplex.quasiIsoAt_π_of_isLimit_of_isEventuallyConstantTo : ∀ {C : Type u_1} {J : Type u_2} {ι : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_5, u_2} J] {c : ComplexShape ι} [CategoryTheory.IsCofiltered J]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [∀ (j : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c j))]
  {cF : CategoryTheory.Limits.Cone F} (hcF : CategoryTheory.Limits.IsLimit cF)
  [inst_5 : CategoryTheory.CategoryWithHomology C] (q₀ q₁ q₂ : ι),
  c.prev q₁ = q₀ →
    c.next q₁ = q₂ →
      ∀ (j : J),
        (F.comp (HomologicalComplex.eval C c q₀)).IsEventuallyConstantTo j →
          (F.comp (HomologicalComplex.eval C c q₁)).IsEventuallyConstantTo j →
            (F.comp (HomologicalComplex.eval C c q₂)).IsEventuallyConstantTo j → QuasiIsoAt (cF.π.app j) q₁
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_union_self_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s \ t ∪ t = s ∪ t
-- Init.Data.UInt.Lemmas
UInt8.ofNatClamp_bitVecToNat : ∀ (n : BitVec 8), UInt8.ofNatClamp n.toNat = { toBitVec := n }
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instIsGeneratedByCarrierObjTopCatToTopCat : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] (Y : GeneratedByTopCat X),
  Topology.IsGeneratedBy X ↑(GeneratedByTopCat.toTopCat.obj Y)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.posSubmonoid_def : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R), x ∈ ValuativeRel.posSubmonoid R ↔ 0 <ᵥ x
-- Mathlib.Order.Bounds.Basic
DirectedOn.le_of_maximal : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α},
  DirectedOn (fun x y => x ≤ y) s → Maximal (fun x => x ∈ s) a → b ∈ s → b ≤ a
-- Mathlib.Topology.UniformSpace.Basic
Uniform.tendsto_nhds_left : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {f : Filter β} {u : β → α} {a : α},
  Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (u x, a)) f (uniformity α)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RocSliceData.range : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RocSliceData α → Std.Roc α
-- Init.Data.Nat.Gcd
Nat.instAssociativeGcd : Std.Associative Nat.gcd
-- Mathlib.Analysis.Complex.Schwarz
/-- Equality case in the **Schwarz Lemma**: in the setup of `norm_dslope_le_div_of_mapsTo_ball`,
if `‖dslope f c z₀‖ = R₂ / R₁` holds at a point in the ball
then the map `f` is affine with slope `dslope f c z₀`.

Note that this lemma requires the codomain to be a strictly convex space.
Indeed, for `E = ℂ × ℂ` there is a counterexample:
the map `f := fun z ↦ (z, z ^ 2)` sends `ball 0 1` to `closedBall 0 1`,
`‖dslope f 0 0‖ = ‖deriv f 0‖ = ‖(1, 0)‖ = 1`, but the map is not an affine map.
 -/
Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z₀ : ℂ}
  [StrictConvexSpace ℝ E],
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) →
      z₀ ∈ Metric.ball c R₁ →
        ‖dslope f c z₀‖ = R₂ / R₁ → Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (Metric.ball c R₁)
-- Mathlib.Topology.Compactness.Lindelof
/-- The intersection of a Lindelöf set and a closed set is a Lindelöf set.  -/
IsLindelof.inter_right : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof s → IsClosed t → IsLindelof (s ∩ t)
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool}, t.WF → (Std.DTreeMap.Raw.filter f t).WF
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.isMin_iff : ∀ {R : Type u} [inst : CommSemiring R] {x : PrimeSpectrum R}, IsMin x ↔ x.asIdeal ∈ minimalPrimes R
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.le_norm : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α]
  (ctx : Lean.Grind.Linarith.Context α) (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert lhs rhs p = true →
    Lean.Grind.Linarith.Expr.denote ctx lhs ≤ Lean.Grind.Linarith.Expr.denote ctx rhs →
      Lean.Grind.Linarith.Poly.denote' ctx p ≤ 0
-- Mathlib.Topology.CantorBendixson
CantorBendixson.perfectKernel_empty : ∀ {X : Type u} [inst : TopologicalSpace X], CantorBendixson.perfectKernel ∅ = ∅
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_zero : ∀ (h : ℝ), UpperHalfPlane.qExpansion h 0 = 0
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_comp_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) (CategoryTheory.CategoryStruct.comp f g) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom h)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- A coroot, seen as an element of the span of coroots.  -/
RootPairing.corootSpanMem : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_6) → [inst_5 : CommRing S] → [inst_6 : Module S N] → ι → ↥(P.corootSpan S)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.ofHom_hom : ∀ (R : Type u) [inst : CommRing R] {A B : AlgCat R} (f : A ⟶ B), AlgCat.ofHom (AlgCat.Hom.hom f) = f
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInvEquiv_symm_mul : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S),
  ↑((S.leftInvEquiv hS).symm x) * ↑x = 1
-- Lean.Meta.Tactic.Grind.MarkAccessible
Lean.Meta.Grind.markGrindName : Lean.Name → Lean.Name
-- Mathlib.Dynamics.Flow
Flow.nonempty_orbit : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) (x : α), (ϕ.orbit x).Nonempty
-- Mathlib.RingTheory.Perfection
PreTilt.coeff.eq_1 : ∀ {O : Type u₂} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] (n : ℕ),
  PreTilt.coeff n = Perfection.coeff (ModP O p) p n
-- Mathlib.Topology.Bases
/-- A topological space with discrete topology is separable iff it is countable.  -/
TopologicalSpace.separableSpace_iff_countable : ∀ {α : Type u} [t : TopologicalSpace α] [DiscreteTopology α], TopologicalSpace.SeparableSpace α ↔ Countable α
-- Std.Data.ByteSlice
instSliceableByteSliceNat_8 : Std.Rii.Sliceable ByteSlice ℕ ByteSlice
-- Mathlib.Analysis.Seminorm
/-- Let `p` be a seminorm on a vector space over a `NormedField`.
If there is a scalar `c` with `‖c‖>1`, then any `x` such that `p x ≠ 0` can be
moved by scalar multiplication to any `p`-shell of width `‖c‖`. Also recap information on the
value of `p` on the rescaling element that shows up in applications.  -/
Seminorm.rescale_to_shell : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {c : 𝕜},
  1 < ‖c‖ →
    ∀ {ε : ℝ}, 0 < ε → ∀ {x : E}, p x ≠ 0 → ∃ d, d ≠ 0 ∧ p (d • x) < ε ∧ ε / ‖c‖ ≤ p (d • x) ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x