mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.rw.sizeOf_spec : ∀ (i : Mathlib.Tactic.ClickSuggestions.RwInfo) (arr : Array Mathlib.Tactic.ClickSuggestions.RwLemma),
  sizeOf (Mathlib.Tactic.ClickSuggestions.Candidates.rw✝ i arr) = 1 + sizeOf i + sizeOf arr
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.nonAssocRing : {R : Type u} →
  {M : Type v} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [Module R M] → [Module Rᵐᵒᵖ M] → NonAssocRing (TrivSqZeroExt R M)
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m.keys.contains k = m.contains k
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
ContinuousLinearMap.toPointwiseConvergenceCLM_apply : ∀ {𝕜₁ : Type u_4} (𝕜₂ : Type u_5) [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_7)
  (F : Type u_8) [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F]
  [inst_9 : ContinuousSMul 𝕜₁ E] [inst_10 : ContinuousConstSMul 𝕜₂ F] (x : E →SL[σ] F),
  (ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜₂ σ E F) x = x
-- Lean.Declaration
/-- Number of fields (i.e., without counting inductive datatype parameters)  -/
Lean.RecursorRule.nfields : Lean.RecursorRule → ℕ
-- Mathlib.GroupTheory.Transfer
AddSubgroup.leftTransversals.diff_self : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {A : Type u_2} [inst_1 : AddCommGroup A] (ϕ : ↥H →+ A)
  (T : H.LeftTransversal) [inst_2 : H.FiniteIndex], AddSubgroup.leftTransversals.diff ϕ T T = 0
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ : C₁} {X₂ Y₂ : C₂} {X₃ : C₃}
  (f₂ : X₂ ⟶ Y₂) (g : (F.obj X₁).obj Y₂ ⟶ X₃),
  adj₂.homEquiv (CategoryTheory.CategoryStruct.comp ((F.obj X₁).map f₂) g) =
    CategoryTheory.CategoryStruct.comp f₂ (adj₂.homEquiv g)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The Haar measure on the locally compact additive group `G`, scaled so that
`addHaarMeasure K₀ K₀ = 1`.  -/
MeasureTheory.Measure.addHaarMeasure : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalAddGroup G] →
        [inst : MeasurableSpace G] → [BorelSpace G] → TopologicalSpace.PositiveCompacts G → MeasureTheory.Measure G
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.leftAdjointSquare.comp_vhcomp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f x y z : B} {g₁ : a ⟶ d} {h₁ : b ⟶ e} {k₁ : c ⟶ f}
  {g₂ : d ⟶ x} {h₂ : e ⟶ y} {k₂ : f ⟶ z} {l₁ : a ⟶ b} {l₂ : b ⟶ c} {l₃ : d ⟶ e} {l₄ : e ⟶ f} {l₅ : x ⟶ y} {l₆ : y ⟶ z}
  (α : CategoryTheory.CategoryStruct.comp g₁ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁)
  (β : CategoryTheory.CategoryStruct.comp h₁ l₄ ⟶ CategoryTheory.CategoryStruct.comp l₂ k₁)
  (γ : CategoryTheory.CategoryStruct.comp g₂ l₅ ⟶ CategoryTheory.CategoryStruct.comp l₃ h₂)
  (δ : CategoryTheory.CategoryStruct.comp h₂ l₆ ⟶ CategoryTheory.CategoryStruct.comp l₄ k₂),
  CategoryTheory.Bicategory.leftAdjointSquare.comp α β γ δ =
    CategoryTheory.Bicategory.leftAdjointSquare.vcomp (CategoryTheory.Bicategory.leftAdjointSquare.hcomp α β)
      (CategoryTheory.Bicategory.leftAdjointSquare.hcomp γ δ)
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂LeftUnitorHom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f : a ⟶ b) →
        [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.leftUnitor f).hom
-- Mathlib.Order.Types.Arithmetic
OrderType.instMul : Mul OrderType.{u}
-- Mathlib.Combinatorics.Graph.Basic
/-- Two graphs with the same vertex set and unary incidences are equal.  -/
Graph.ext_inc : ∀ {α : Type u_1} {β : Type u_2} {G₁ G₂ : Graph α β},
  G₁.vertexSet = G₂.vertexSet → (∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x) → G₁ = G₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey!
-- Init.Data.UInt.Basic
instNegUInt32 : Neg UInt32
-- Mathlib.Algebra.GroupWithZero.Action.Center
Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe : ∀ (G₀ : Type u_1) [inst : GroupWithZero G₀] (a : ↥(Subgroup.center G₀ˣ)),
  ↑↑((Subgroup.centerUnitsEquivUnitsCenter G₀) a) = ↑↑a
-- Lean.DocString.Types
Lean.Doc.Block.ul.inj : ∀ {i : Type u} {b : Type v} {items items_1 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))},
  Lean.Doc.Block.ul items = Lean.Doc.Block.ul items_1 → items = items_1
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.Entry.modified : Lean.Meta.GeneralizeTelescope.Entry → Bool
-- Mathlib.Algebra.Group.Defs
isAddCommutative_iff : ∀ {M : Type u_2} [inst : Add M], IsAddCommutative M ↔ ∀ (a b : M), a + b = b + a
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_neg : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M) (a : A), D (-a) = -D a
-- Mathlib.Data.Vector.Defs
/-- A `nil` vector maps to a `nil` vector.  -/
List.Vector.map_nil : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), List.Vector.map f List.Vector.nil = List.Vector.nil
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_singleton : ∀ {m n : ℕ}, n = m + 1 → (m<...=n).toList = [m + 1]
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.congrRight_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] (e : Y ≃ Z) (g : LocallyConstant X Y),
  (LocallyConstant.congrRight e) g = LocallyConstant.map (⇑e) g
-- Mathlib.Data.Set.Basic
Set.ssubset_def : ∀ {α : Type u} {s t : Set α}, (s ⊂ t) = (s ⊆ t ∧ ¬t ⊆ s)
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.condExp_ae_eq : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0}, MeasureTheory.Martingale f ℱ μ → ∀ {i j : ι}, i ≤ j → μ[f j | ↑ℱ i] =ᵐ[μ] f i
-- Mathlib.Algebra.Homology.Localization
/-- The functor `HomotopyCategory C c ⥤ HomologicalComplexUpToQuasiIso C c` from the homotopy
category to the localized category with respect to quasi-isomorphisms.  -/
HomologicalComplexUpToQuasiIso.Qh : {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] →
            [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] →
              [c.QFactorsThroughHomotopy C] →
                CategoryTheory.Functor (HomotopyCategory C c) (HomologicalComplexUpToQuasiIso C c)
-- Init.Data.Order.PackageFactories
_private.Init.Data.Order.PackageFactories.0.Std.FactoryInstances.isGE_compare : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α],
  (∀ (a b : α), a ≤ b ∨ b ≤ a) → ∀ {a b : α}, (compare a b).isGE = true ↔ b ≤ a
-- Lean.LocalContext
Lean.LocalContext.forM : {m : Type u_1 → Type u_2} →
  [Monad m] → Lean.LocalContext → (Lean.LocalDecl → m PUnit.{u_1 + 1}) → optParam ℕ 0 → m PUnit.{u_1 + 1}
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageRequestParams.message : Lean.Lsp.ShowMessageRequestParams → String
-- Mathlib.Util.Export
Lean.Export.OfState.get : {α : Type} →
  {inst : BEq α} → {inst_1 : Hashable α} → [self : Lean.Export.OfState α] → Lean.Export.State → Lean.Export.Alloc α
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.neg_neg_iff`.

---

Uses `left` co(ntra)variant.  -/
neg_lt_zero : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, -a < 0 ↔ 0 < a
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.associator_inv_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) (β : b ⟶ c)
  (γ : c ⟶ d),
  (CategoryTheory.Bicategory.Adj.Bicategory.associator α β γ).inv.τr =
    (CategoryTheory.Bicategory.associator γ.r β.r α.r).inv
-- Init.Data.BitVec.Lemmas
BitVec.none_eq_getElem?_iff : ∀ {w n : ℕ} {l : BitVec w}, none = l[n]? ↔ w ≤ n
-- Mathlib.Algebra.Lie.Abelian
LieModule.ker_eq_bot : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsFaithful R L M], LieModule.ker R L M = ⊥
-- Mathlib.Algebra.Homology.Opposite
Homotopy.op_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {ι : Type u_2} {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Preadditive V] {F G : HomologicalComplex V c} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂) (i j : ι),
  h.op.hom i j = (h.hom j i).op
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- Composite functors induce composite functors on matrix categories.
 -/
CategoryTheory.Functor.mapMatComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v₁, u_1} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            {E : Type u_2} →
              [inst_4 : CategoryTheory.Category.{v₁, u_2} E] →
                [inst_5 : CategoryTheory.Preadditive E] →
                  (F : CategoryTheory.Functor C D) →
                    [inst_6 : F.Additive] →
                      (G : CategoryTheory.Functor D E) →
                        [inst_7 : G.Additive] → (F.comp G).mapMat_ ≅ F.mapMat_.comp G.mapMat_
-- Lean.MonadEnv
Lean.getConstInfoCtor : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Lean.ConstructorVal
-- Init.Grind.Attr
/-- The `⇒` modifier instructs `grind` to select a multi-pattern by traversing all the hypotheses from
left to right, followed by the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
 -/
Lean.Parser.Attr.grindLR : Lean.ParserDescr
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_2 ()
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.ext' : ∀ {R : Type v} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type w}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyUnramified R A] {C : Type u_1} [inst_6 : Ring C]
  (f : B →+* C), IsNilpotent (RingHom.ker f) → ∀ (g₁ g₂ : A →ₐ[R] B), (∀ (x : A), f (g₁ x) = f (g₂ x)) → g₁ = g₂
-- Mathlib.Combinatorics.Quiver.Arborescence
Quiver.geodesicArborescence : {V : Type u} →
  [inst : Quiver V] →
    (r : V) →
      [inst_1 : Quiver.RootedConnected r] → Quiver.Arborescence (WideSubquiver.toType V (Quiver.geodesicSubtree r))
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  (i₁ i₂ i₃ : ι) {Z : ↑(F.obj { as := Opposite.op (sq₃ i₁ i₂ i₃).chosenPullback.pullback })}
  (h : (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc).toFunctor.obj (obj' i₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom i₁ i₃) (sq₃ i₁ i₂ i₃).p₁₃ (sq₃ i₁ i₂ i₃).p₁
        (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
      h
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAt.add : ∀ {𝕜 : 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] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → HasFDerivAt g g' x → HasFDerivAt (f + g) (f' + g') x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.cooper.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.CooperSplit),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.cooper c) = 1 + sizeOf c
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.multipliable_iff_of_mulSupport : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : γ → α} (e : ↑(Function.mulSupport f) ≃ ↑(Function.mulSupport g)),
  (∀ (x : ↑(Function.mulSupport f)), g ↑(e x) = f ↑x) → (Multipliable f ↔ Multipliable g)
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_fst : ∀ (s : (n : ℕ) × Finset (Fin n)), (FormalMultilinearSeries.changeOriginIndexEquiv.symm s).fst = s.fst - s.snd.card
-- Mathlib.Analysis.LocallyConvex.Separation
geometric_hahn_banach_closed_point : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s : Set E} {x : E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E],
  Convex ℝ s → IsClosed s → x ∉ s → ∃ f u, (∀ a ∈ s, f a < u) ∧ u < f x
-- Mathlib.Data.Set.Function
/-- **Alias** of the reverse direction of `Set.bijOn_univ`. -/
Function.Bijective.bijOn_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Bijective f → Set.BijOn f Set.univ Set.univ
-- Mathlib.Order.Closure
LowerAdjoint.mem_closed_iff_closure_le : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α),
  x ∈ l.closed ↔ u (l.toFun x) ≤ x
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
CategoryTheory.Monoidal.Transported.instSymmetricCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) →
          [inst_2 : CategoryTheory.MonoidalCategory C] →
            [CategoryTheory.SymmetricCategory C] →
              CategoryTheory.SymmetricCategory (CategoryTheory.Monoidal.Transported e)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.of_isAtomic : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsAtomic → φ.IsQF
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The following diagram
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
being a pullback for any monic `m` means that every monomorphism
in `C` is the pullback of a regular monomorphism; since regularity
is stable under base change, every monomorphism is regular.
Hence, `C` is a regular mono category.
It also follows that `C` is a balanced category.
 -/
CategoryTheory.HasSubobjectClassifier.isRegularMonoCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.HasSubobjectClassifier C],
  CategoryTheory.IsRegularMonoCategory C
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A function is strongly measurable if and only if it is measurable and has separable
range.  -/
stronglyMeasurable_iff_measurable_separable : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β],
  MeasureTheory.StronglyMeasurable f ↔ Measurable f ∧ TopologicalSpace.IsSeparable (Set.range f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.isLocalMin_T_real : ∀ {n k : ℕ},
  n ≠ 0 →
    k < n → Odd k → IsLocalMin (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) (Real.cos (↑k * Real.pi / ↑n))
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveOfNat : ∀ {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.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] [inst_4 : CategoryTheory.Limits.HasZeroObject D],
  CategoryTheory.Functor.Additive 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_union_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (mem : k ∈ t₂), (t₁ ∪ t₂).getKey k ⋯ = t₂.getKey k mem
-- Mathlib.RingTheory.Localization.Defs
Localization.mk_list_sum : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (l : List R) (b : ↥M),
  Localization.mk l.sum b = (List.map (fun a => Localization.mk a b) l).sum
-- Mathlib.Order.Interval.Finset.Fin
Fin.Ioc_sub_one_eq_Ioo : ∀ {n : ℕ} {a b : Fin n}, 0 < b → Finset.Ioc a (b - 1) = Finset.Ioo a b
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.unrev_ok : ∀ {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'}
  {S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'},
  StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
    { l := some (Turing.PartrecToTM2.unrev q), var := s, stk := S }
    { l := some q, var := none,
      stk :=
        Function.update (Function.update S Turing.PartrecToTM2.K'.rev []) Turing.PartrecToTM2.K'.main
          ((S Turing.PartrecToTM2.K'.rev).reverseAux (S Turing.PartrecToTM2.K'.main)) }
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.saturation_bot : ∀ {M : Type u_1} [inst : MulOneClass M], ⊥.saturation = ⊥
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RoiSlice : (α : Type u_1) → [Ord α] → Type u_1
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.mfderivWithin_mono : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M},
  MDiffAt[s] f x → UniqueMDiffAt[t] x → t ⊆ s → mfderiv[t] f x = mfderiv[s] f x
-- Mathlib.CategoryTheory.Sites.Sieves
/-- stability by precomposition  -/
CategoryTheory.Sieve.downward_closed : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.Sieve X) {Y Z : C}
  {f : Y ⟶ X}, self.arrows f → ∀ (g : Z ⟶ Y), self.arrows (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_of_natDegree_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree = 0 → Polynomial.derivative p = 0
-- Mathlib.Order.Category.HeytAlg
HeytAlg.mk.sizeOf_spec : ∀ (carrier : Type u_1) [str : HeytingAlgebra carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Algebra.Order.Module.Pointwise
BddBelow.smul_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulMono α β] {a : α} {s : Set β}, BddBelow s → 0 ≤ a → BddBelow (a • s)
-- Std.Async.System
/-- The user's ID.
 -/
Std.Async.System.SystemUser.userId : Std.Async.System.SystemUser → Option Std.Async.System.UserId
-- Mathlib.CategoryTheory.Opposites
/-- The equivalence between arrows of the form `A ⟶ B` and `B.unop ⟶ A.unop`. Useful for building
adjunctions.
Note that this (definitionally) gives variants
```
def opEquiv' (A : C) (B : Cᵒᵖ) : (Opposite.op A ⟶ B) ≃ (B.unop ⟶ A) :=
  opEquiv _ _

def opEquiv'' (A : Cᵒᵖ) (B : C) : (A ⟶ Opposite.op B) ≃ (B ⟶ A.unop) :=
  opEquiv _ _

def opEquiv''' (A B : C) : (Opposite.op A ⟶ Opposite.op B) ≃ (B ⟶ A) :=
  opEquiv _ _
```
 -/
CategoryTheory.opEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (A B : Cᵒᵖ) → (A ⟶ B) ≃ (Opposite.unop B ⟶ Opposite.unop A)
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.BlockMem.coe_top : ∀ (G : Type u_1) [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] (a : X), ↑⊤ = Set.univ
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.pushforward_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y)
  (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) {X_1 Y_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ}
  (f_1 : X_1 ⟶ Y_1),
  ((TopCat.Presheaf.pushforward C f).obj G).map f_1 = G.map ((TopologicalSpace.Opens.map f).map f_1.unop).op
-- Lean.Data.Lsp.Basic
Lean.Lsp.RenameFile.options? : Lean.Lsp.RenameFile → Option Lean.Lsp.CreateFile.Options
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB4OfSize.ofShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasCoproducts C}
  [self : CategoryTheory.AB4OfSize.{w, v, u} C] (α : Type w),
  CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete α) C
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.topEquiv_apply : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (x : ↥⊤), NonUnitalSubring.topEquiv x = ↑x
-- Mathlib.NumberTheory.Divisors
Nat.divisors_injective : Function.Injective Nat.divisors
-- Batteries.CodeAction.Attr
Batteries.CodeAction.TacticCodeActions.mk.injEq : ∀ (onAnyTactic : Array Batteries.CodeAction.TacticCodeAction)
  (onTactic : Lean.NameMap (Array Batteries.CodeAction.TacticCodeAction))
  (onAnyTactic_1 : Array Batteries.CodeAction.TacticCodeAction)
  (onTactic_1 : Lean.NameMap (Array Batteries.CodeAction.TacticCodeAction)),
  ({ onAnyTactic := onAnyTactic, onTactic := onTactic } = { onAnyTactic := onAnyTactic_1, onTactic := onTactic_1 }) =
    (onAnyTactic = onAnyTactic_1 ∧ onTactic = onTactic_1)
-- Mathlib.Order.Max
noMaxOrder_of_right : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMaxOrder β], NoMaxOrder (α × β)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.extract : ∀ {b e : String.Pos.Raw} {s : Substring.Raw},
  s.Valid → { str := s.toString, startPos := b, stopPos := e }.Valid → (s.extract b e).Valid
-- Mathlib.Analysis.InnerProductSpace.Continuous
DenseRange.eq_zero_of_inner_right : ∀ {E : Type u_4} {ι : Type u_6} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {x : E} {f : ι → E}, DenseRange f → (∀ (i : ι), inner 𝕜 (f i) x = 0) → x = 0
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instInhabitedOrigin.default : Mathlib.Meta.FunProp.Origin