mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The `E₂` cohomological spectral sequence indexed by `ℕ × ℕ` attached to
a first quadrant spectral object indexed by `EInt`.  -/
CategoryTheory.Abelian.SpectralObject.E₂SpectralSequenceNat : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Y : CategoryTheory.Abelian.SpectralObject C EInt) →
        [Y.IsFirstQuadrant] → CategoryTheory.SpectralSequence C (fun r => ComplexShape.spectralSequenceNat (r, 1 - r)) 2
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.instLocallyDirectedIsOpenImmersionDirectedCover : {X : AlgebraicGeometry.Scheme} →
  AlgebraicGeometry.Scheme.Cover.LocallyDirected (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.symm_trans_self : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), e.symm.trans e = AffineEquiv.refl k P₂
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₃_app : ∀ (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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) (X_1 : J),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).inv.app X).τ₃.app X_1 =
    CategoryTheory.CategoryStruct.id (X.X₃.obj X_1)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_eq_nat : ∀ {o : Ordinal.{u_1}} {n : ℕ}, o.card = ↑n ↔ o = ↑n
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the forward direction of `hasFDerivAtFilter_iff_isLittleO`. -/
HasFDerivAtFilter.isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → (fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[L] fun p => p.1 - p.2
-- Mathlib.Data.Fintype.Sets
/-- A set on a fintype, when coerced to a type, is a fintype.  -/
setFintype : {α : Type u_1} → [Fintype α] → (s : Set α) → [DecidablePred fun x => x ∈ s] → Fintype ↑s
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.posRootForm_posForm_pos_of_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [inst_7 : LinearOrder S] [inst_8 : IsStrictOrderedRing S] [IsDomain R]
  [inst_10 : Algebra S R] [inst_11 : FaithfulSMul S R] [inst_12 : P.IsValuedIn S] [inst_13 : Module S M]
  [inst_14 : IsScalarTower S R M] [inst_15 : Module S N] [IsScalarTower S R N] {x : ↥(P.rootSpan S)},
  x ≠ 0 → 0 < ((P.posRootForm S).posForm x) x
-- Lean.Meta.Tactic.Subst
/-- Given `x`, try to find an equation of the form `heq : x = rhs` or `heq : lhs = x`,
and runs `substCore` on it. Throws an exception if no such equation is found.
 -/
Lean.Meta.substVar : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instIsMulCommutative_iSup : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {ι : Type u_2} [Nonempty ι] [inst_6 : Preorder ι]
  [IsDirectedOrder ι] {S : ι →o NonUnitalSubalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)],
  IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongrLinearEquiv_apply : ∀ (R : Type uR) (S : Type uS) (M₂ : Type v₂) (M₃ : Type v₃) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M₃] [inst_5 : Module S M₃] [inst_6 : Module R M₃]
  [inst_7 : SMulCommClass R S M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ≃ ι₂) (a : MultilinearMap R (fun x => M₂) M₃),
  (MultilinearMap.domDomCongrLinearEquiv R S M₂ M₃ σ) a = (MultilinearMap.domDomCongrEquiv σ).toFun a
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.motives.nonConst : Lean.Option Bool
-- Mathlib.NumberTheory.FrobeniusNumber
/-- The characterizing property of `Nat.setGcd`.  -/
Nat.dvd_setGcd_iff : ∀ {s : Set ℕ} {n : ℕ}, n ∣ Nat.setGcd s ↔ ∀ m ∈ s, n ∣ m
-- Batteries.Data.Array.Merge
/-- `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
not contain duplicates. Equal elements are merged using `merge`. If `merge` respects the order
(i.e. for all `x`, `y`, `y'`, `z`, if `x < y < z` and `x < y' < z` then `x < merge y y' < z`)
then the resulting array is again sorted.
 -/
Array.mergeDedupWith : {α : Type u_1} → [ord : Ord α] → Array α → Array α → (α → α → α) → Array α
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.Tendsto.eventually_ne_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α},
  Filter.Tendsto f l Filter.atBot → ∀ (c : β), ∀ᶠ (x : α) in l, f x ≠ c
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_monotone : Monotone EReal.exp
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.instMonadPostconditionT : {m : Type w → Type w'} → [Monad m] → Monad (Std.Iterators.PostconditionT m)
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Literal.unsat_of_limplies_complement : ∀ {α : Type u_1} {t : Type u_2} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α t] (x : t) (l : Std.Sat.Literal α),
  Std.Tactic.BVDecide.LRAT.Internal.Limplies α x l →
    Std.Tactic.BVDecide.LRAT.Internal.Limplies α x l.negate → Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α x
-- Init.Grind.Ring.Basic
Lean.Grind.CommRing.mk : {α : Type u} → [toRing : Lean.Grind.Ring α] → (∀ (a b : α), a * b = b * a) → Lean.Grind.CommRing α
-- Lean.Server.Completion.CompletionUtils
_private.Lean.Server.Completion.CompletionUtils.0.Lean.Server.Completion.minimizeGlobalIdentifierInContext.shortenInCurrentNamespace : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  (∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) → fderiv 𝕜 (∑ i ∈ u, A i) x = ∑ i ∈ u, fderiv 𝕜 (A i) x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {t : CategoryTheory.Limits.PushoutCocone f g} (ht : CategoryTheory.Limits.IsColimit t) [CategoryTheory.Epi g],
  CategoryTheory.Epi t.inl
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} {y : β},
  ContinuousWithinAt g t y →
    ContinuousWithinAt f s x → f ⁻¹' t ∈ nhdsWithin x s → f x = y → ContinuousWithinAt (g ∘ f) s x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceSub : Lean.Meta.Simp.DSimproc
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.var.inj : ∀ {i i_1 : Int.Internal.Linear.Var}, Int.Internal.Linear.Expr.var i = Int.Internal.Linear.Expr.var i_1 → i = i_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_eq_getElem?_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.minKey? = t.keysArray[0]?
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- The Gromov-Hausdorff distance between two spaces is bounded by the Hausdorff distance
of isometric copies of the spaces, in any metric space.  -/
GromovHausdorff.ghDist_le_hausdorffDist : ∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y] {γ : Type w} [inst_6 : MetricSpace γ]
  {Φ : X → γ} {Ψ : Y → γ},
  Isometry Φ → Isometry Ψ → GromovHausdorff.ghDist X Y ≤ Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.matchExpr : Lean.Syntax →
  Bool →
    Lean.Syntax →
      Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
-- Mathlib.Algebra.Group.WithOne.Defs
/-- Deconstruct an `x : WithOne α` to the underlying value in `α`, given a proof that `x ≠ 1`.  -/
WithOne.unone : {α : Type u} → {x : WithOne α} → x ≠ 1 → α
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- The cone associated to a weak pullback is a weak limit cone.  -/
CategoryTheory.Limits.weakPullback.isWeakLimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] →
            CategoryTheory.Limits.IsWeakLimit (CategoryTheory.Limits.weakPullback.cone f g)
-- Mathlib.Data.Set.Basic
Set.inter_eq_self_of_subset_left : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ∩ t = s
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.hasCardinalFilteredGenerator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.LocallySmall.{w, v, u} C]
  {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular],
  P.IsCardinalFilteredGenerator κ → CategoryTheory.HasCardinalFilteredGenerator C κ
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Every proper subgroup `H` of `G` is a proper normal subgroup of the normalizer of `H` in `G`.  -/
NormalizerCondition : (G : Type u_1) → [Group G] → Prop
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.eq_zero_of_bot_submodule : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (b : ↥⊥), b = 0
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.subsingleton : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G},
  UniqueAdd A B a0 b0 → Subsingleton { ab // ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 + ab.2 = a0 + b0 }
-- Mathlib.Topology.Connected.Basic
/-- A preconnected space is one where there is no non-trivial open partition.  -/
PreconnectedSpace : (α : Type u) → [TopologicalSpace α] → Prop
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
_private.Mathlib.Algebra.SkewMonoidAlgebra.Basic.0.SkewMonoidAlgebra.smul : {k : Type u_1} →
  {G : Type u_2} →
    [inst : AddMonoid k] → {S : Type u_3} → [SMulZeroClass S k] → S → SkewMonoidAlgebra k G → SkewMonoidAlgebra k G
-- Mathlib.CategoryTheory.Shift.Opposite
/-- If an adjunction `F ⊣ G` is compatible with `CommShift` structures on `F` and `G`, then
the opposite adjunction `OppositeShift.adjunction adj` is compatible with the opposite
`CommShift` structures.
 -/
CategoryTheory.Adjunction.commShift_op : ∀ {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] (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A],
  (CategoryTheory.OppositeShift.adjunction A adj).CommShift A
-- Init.Data.AC
Lean.Data.AC.Expr.toList.eq_1 : ∀ (idx : ℕ), (Lean.Data.AC.Expr.var idx).toList = [idx]
-- Mathlib.Data.Fin.Fin2
Fin2.rev.eq_def : ∀ {n : ℕ} (x : Fin2 n),
  x.rev =
    match n, x with
    | .(n + 1), Fin2.fz => Fin2.last
    | .(n + 1), i.fs => i.rev.castSucc
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.empty_eq_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, Std.ExtTreeMap.empty = ∅
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_ratCast_nonneg : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : Field R] [inst_2 : IsOrderedRing R] (q : ℚ),
  0 ≤ ArchimedeanClass.mk ↑q
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_nonneg : ∀ {x : ℝ}, 0 ≤ Real.arcsin x ↔ 0 ≤ x
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.realize_neg : ∀ {α : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Mul R] [inst_2 : Neg R] [inst_3 : One R] [inst_4 : Zero R]
  [inst_5 : FirstOrder.Ring.CompatibleRing R] (x : FirstOrder.Language.ring.Term α) (v : α → R),
  FirstOrder.Language.Term.realize v (-x) = -FirstOrder.Language.Term.realize v x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic.0.CategoryTheory.Abelian.Ext.add_hom' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ} (α β : CategoryTheory.Abelian.Ext X Y n),
  (α + β).hom' = α.hom' + β.hom'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toList_insert_perm : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k},
  (m.insert k v).toList.Perm (⟨k, v⟩ :: List.filter (fun x_2 => decide ¬(k == x_2.fst) = true) m.toList)
-- Mathlib.Tactic.Bound.Attribute
/-- Map a hypothesis type to a score  -/
Mathlib.Tactic.Bound.hypPriority : Q(Prop) → Lean.MetaM ℕ
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- `ContinuousMultilinearMap.pi` as a `LinearIsometryEquiv`.  -/
ContinuousMultilinearMap.piₗᵢ : (𝕜 : Type u) →
  {ι : Type v} →
    (E : ι → Type wE) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
            [inst_3 : Fintype ι] →
              {ι' : Type v'} →
                [inst_4 : Fintype ι'] →
                  {E' : ι' → Type wE'} →
                    [inst_5 : (i' : ι') → NormedAddCommGroup (E' i')] →
                      [inst_6 : (i' : ι') → NormedSpace 𝕜 (E' i')] →
                        ((i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')) ≃ₗᵢ[𝕜]
                          ContinuousMultilinearMap 𝕜 E ((i : ι') → E' i)
-- Lean.Expr
Lean.instCoeExprExprStructEq : Coe Lean.Expr Lean.ExprStructEq
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap_pruneLE_eq_prependMapGE : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (z : Std.DTreeMap.Internal.Zipper α β) (lowerBound : α),
      Std.DTreeMap.Internal.Zipper.prependMap (Std.DTreeMap.Internal.Impl.pruneLE✝ t lowerBound) z =
        Std.DTreeMap.Internal.Zipper.prependMapGE t lowerBound z
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabFootnote : Type
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderProcessedSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {metaSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf}
  {result? : Option Lean.Language.Lean.HeaderProcessedState} {toSnapshot_1 : Lean.Language.Snapshot}
  {metaSnap_1 : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf}
  {result?_1 : Option Lean.Language.Lean.HeaderProcessedState},
  { toSnapshot := toSnapshot, metaSnap := metaSnap, result? := result? } =
      { toSnapshot := toSnapshot_1, metaSnap := metaSnap_1, result? := result?_1 } →
    toSnapshot = toSnapshot_1 ∧ metaSnap = metaSnap_1 ∧ result? = result?_1
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : A`, a localization map `F : A →+ B` away from `x`, and a map of `AddCommMonoid`s
`g : A →+ C` such that `g x` is invertible, the homomorphism induced from `B` to `C` sending
`z : B` to `g y - n • g x`, where `y : A, n : ℕ` are such that `z = F y - n • F x`.  -/
AddSubmonoid.LocalizationMap.AwayMap.lift : {A : Type u_4} →
  [inst : AddCommMonoid A] →
    (x : A) →
      {B : Type u_5} →
        [inst_1 : AddCommMonoid B] →
          AddSubmonoid.LocalizationMap.AwayMap x B →
            {C : Type u_6} → [inst_2 : AddCommMonoid C] → {g : A →+ C} → IsAddUnit (g x) → B →+ C
-- Mathlib.Data.Finsupp.MonomialOrder
/-- **Alias** of `MonomialOrder.wellFoundedLT_syn`.

---

`syn` is a well ordering  -/
MonomialOrder.wf : ∀ {σ : Type u_1} (self : MonomialOrder σ), WellFoundedLT self.syn
-- Mathlib.Topology.Order.OrderClosed
Dense.Ioi_eq_biUnion : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α]
  {s : Set α}, Dense s → ∀ (x : α), Set.Ioi x = ⋃ y ∈ s ∩ Set.Ioi x, Set.Ioi y
-- Lean.Meta.Sym.SymM
/-- When `true`, issues are collected during proof search and reported on failure.  -/
Lean.Meta.Sym.Config.verbose : Lean.Meta.Sym.Config → Bool
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nndist_ofDual : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] (a b : Xᵒᵈ), nndist (OrderDual.ofDual a) (OrderDual.ofDual b) = nndist a b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.le_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (cmp k t.minKey!).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.VarSet : Type
-- Init.Data.Iterators.Basic
/-- The output value could plausibly be emitted in a step after the next step.  -/
Std.IterM.IsPlausibleIndirectOutput.indirect : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it it' : Std.IterM m β} {out : β},
  it'.IsPlausibleSuccessorOf it → it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
-- Mathlib.Computability.Partrec
Partrec.vector_mOfFn : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : Fin n → α →. σ},
  (∀ (i : Fin n), Partrec (f i)) → Partrec fun a => List.Vector.mOfFn fun i => f i a
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.regularEpiOfPreserves_right : ∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_3, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D] {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.EffectiveEpi f]
  (F : CategoryTheory.Functor C D) [inst_3 : F.PreservesEffectiveEpis]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  (c : CategoryTheory.Limits.PullbackCone f f) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Functor.regularEpiOfPreserves f F c hc).right = F.map c.snd
-- Mathlib.Analysis.Calculus.Rademacher
/-- In a real finite-dimensional normed vector space,
the set of points where the norm is differentiable at is dense.  -/
dense_differentiableAt_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E],
  Dense {x | DifferentiableAt ℝ (fun x => ‖x‖) x}
-- Init.Data.Array.Extract
Array.extract_eq_self_iff : ∀ {α : Type u_1} {i j : ℕ} {as : Array α}, as.extract i j = as ↔ as.size = 0 ∨ i = 0 ∧ as.size ≤ j
-- Init.Data.AC
Lean.Data.AC.insert.eq_1 : ∀ (x : ℕ), Lean.Data.AC.insert x [] = [x]
-- Mathlib.LinearAlgebra.RootSystem.Basic
/-- In characteristic zero if there is no torsion, the correspondence between roots and coroots is
unique.

Formally, the point is that the hypothesis `hc` depends only on the range of the coroot mappings.  -/
RootPairing.ext : ∀ {ι : 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] [Finite ι] [CharZero R] [IsDomain R]
  [Module.IsTorsionFree R M] {P₁ P₂ : RootPairing ι R M N},
  P₁.toLinearMap = P₂.toLinearMap → P₁.root = P₂.root → Set.range ⇑P₁.coroot = Set.range ⇑P₂.coroot → P₁ = P₂
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom_ι_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncGTπ a).app X) ((t.truncGTIsoTruncGE a b h).hom.app X) =
    (t.truncGEπ b).app X
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
PresheafOfModules.homEquivOfIsLocallyBijective_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) {N : PresheafOfModules R}
  (hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf) [inst_1 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_2 : PresheafOfModules.IsLocallySurjective J f] [inst_3 : PresheafOfModules.IsLocallyInjective J f] (φ : M₂ ⟶ N),
  (PresheafOfModules.homEquivOfIsLocallyBijective f hN) φ = CategoryTheory.CategoryStruct.comp f φ
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasStrictFDerivAt.continuousMultilinear_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_5} {M : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H]
  {c : E → ContinuousMultilinearMap 𝕜 M H} {c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H} [inst_7 : Fintype ι],
  HasStrictFDerivAt c c' x → ∀ (u : (i : ι) → M i), HasStrictFDerivAt (fun y => (c y) u) (c'.flipMultilinear u) x
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.RingCat.Hom.mk.sizeOf_spec : ∀ {R S : RingCat} (hom' : ↑R →+* ↑S), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
`f : G → M` satisfying the multiplicative 1-cocycle condition, produces a 1-cocycle for the
representation on `Additive M` induced by the `MulDistribMulAction`.  -/
groupCohomology.cocyclesOfIsMulCocycle₁ : {G M : Type} →
  [inst : Group G] →
    [inst_1 : CommGroup M] →
      [inst_2 : MulDistribMulAction G M] →
        {f : G → M} → groupCohomology.IsMulCocycle₁ f → ↥(groupCohomology.cocycles₁ (Rep.ofMulDistribMulAction G M))
-- Mathlib.Analysis.Complex.HasPrimitives
_private.Mathlib.Analysis.Complex.HasPrimitives.0.Complex.mem_ball_re_aux : ∀ {c z : ℂ} {r x : ℝ},
  x ∈ Set.Ioo (z.re - (r - dist z c)) (z.re + (r - dist z c)) → ↑x + ↑z.im * Complex.I ∈ Metric.ball c r
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G),
  (CategoryTheory.Adjunction.mkOfHomEquiv adj).homEquiv = adj.homEquiv
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.minpoly_eq : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {S : IntermediateField K L}
  (x : ↥S), minpoly K x = minpoly K ↑x
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.funUnique_apply : ∀ (α : Type u_8) (β : Type u_9) [inst : Unique α] [inst_1 : MeasurableSpace β],
  ⇑(MeasurableEquiv.funUnique α β) = fun f => f default