mathlib-initiative/mathlib-types huggingface dataset:
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.mk.inj : ∀ {Map : (α : Type) → Type → [BEq α] → [Hashable α] → Type}
  {mkMap : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Map α β}
  {mapFind? : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → Option β}
  {mapInsert : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → β → Map α β}
  {Set : (α : Type) → [BEq α] → [Hashable α] → Type}
  {mkSet : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Set α}
  {setFind? : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Option α}
  {setInsert : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Set α}
  {Map_1 : (α : Type) → Type → [BEq α] → [Hashable α] → Type}
  {mkMap_1 : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Map_1 α β}
  {mapFind?_1 : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map_1 α β → α → Option β}
  {mapInsert_1 : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map_1 α β → α → β → Map_1 α β}
  {Set_1 : (α : Type) → [BEq α] → [Hashable α] → Type}
  {mkSet_1 : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Set_1 α}
  {setFind?_1 : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set_1 α → α → Option α}
  {setInsert_1 : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set_1 α → α → Set_1 α},
  { Map := Map, mkMap := mkMap, mapFind? := mapFind?, mapInsert := mapInsert, Set := Set, mkSet := mkSet,
        setFind? := setFind?, setInsert := setInsert } =
      { Map := Map_1, mkMap := mkMap_1, mapFind? := mapFind?_1, mapInsert := mapInsert_1, Set := Set_1,
        mkSet := mkSet_1, setFind? := setFind?_1, setInsert := setInsert_1 } →
    Map = Map_1 ∧
      mkMap ≍ mkMap_1 ∧
        mapFind? ≍ mapFind?_1 ∧
          mapInsert ≍ mapInsert_1 ∧ Set = Set_1 ∧ mkSet ≍ mkSet_1 ∧ setFind? ≍ setFind?_1 ∧ setInsert ≍ setInsert_1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_lt_one : ∀ {x : NNReal} {z : ℝ}, x < 1 → 0 < z → x ^ z < 1
-- Mathlib.Data.Num.Lemmas
PosNum.testBit.eq_2 : ∀ (x : ℕ), (x = 0 → False) → PosNum.one.testBit x = false
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
BinaryTree.mem_treesOfNumNodesEq_numNodes : ∀ (x : BinaryTree Unit), x ∈ BinaryTree.treesOfNumNodesEq x.numNodes
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_one : ∀ {α : Type u_1} {f : Fin 1 → Option α}, Fin.findSome? f = f 0
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.inclLiftToInitial_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (x : C),
  (CategoryTheory.WithInitial.inclLiftToInitial F hZ).inv.app x = CategoryTheory.CategoryStruct.id (F.obj x)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_sub_natCast : ∀ (r : ENNReal) (n : ℕ), ⌈r - ↑n⌉ₑ = ⌈r⌉ₑ - ↑n
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is the set of vertices
in `s` adjacent to `v` in `G`.  -/
SimpleGraph.isBipartiteWith_neighborFinset : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet v)]
  [inst_1 : DecidableRel G.Adj], G.IsBipartiteWith ↑s ↑t → v ∈ s → G.neighborFinset v = {w ∈ t | G.Adj v w}
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_exp_Iic_zero : ∫ (x : ℝ) in Set.Iic 0, Real.exp x = 1
-- Mathlib.Algebra.Lie.Classical
/-- A matrix defining a canonical odd-rank symmetric bilinear form.

It looks like this as a `(2l+1) x (2l+1)` matrix of blocks:

```
[ 2 0 0 ]
[ 0 0 1 ]
[ 0 1 0 ]
```

where sizes of the blocks are:

```
[`1 x 1` `1 x l` `1 x l`]
[`l x 1` `l x l` `l x l`]
[`l x 1` `l x l` `l x l`]
```
 -/
LieAlgebra.Orthogonal.JB : (l : Type u_4) → (R : Type u₂) → [DecidableEq l] → [CommRing R] → Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂Iso_eqToIso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {x y : B} (f g : x ⟶ y) (hfg : f = g),
  F.map₂Iso (CategoryTheory.eqToIso hfg) = CategoryTheory.eqToIso ⋯
-- Init.Data.FloatArray.Basic
/-- Reference implementation for `forIn`  -/
FloatArray.forIn : {β : Type v} → {m : Type v → Type w} → [Monad m] → FloatArray → β → (Float → β → m (ForInStep β)) → m β
-- Mathlib.RingTheory.RingHom.Surjective
RingHom.surjective_isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.val_toList : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {t : RBTree.RBMap α β cmp}, (↑t).toList = t.toList
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_injective : ∀ (p : ENNReal) {V : Type u_4}, Function.Injective WithLp.ofLp
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_C : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (r : R),
  (MvPolynomial.rename f) (MvPolynomial.C r) = MvPolynomial.C r
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.excenter signs = (s.exsphere signs).center
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- Homs in `TopModuleCat` as one field structures over `ContinuousLinearMap`.  -/
TopModuleCat.Hom : {R : Type u} → [inst : Ring R] → [inst_1 : TopologicalSpace R] → TopModuleCat R → TopModuleCat R → Type v
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.transition.inj : ∀ {thm thm_1 : Mathlib.Meta.FunProp.GeneralTheorem},
  Mathlib.Meta.FunProp.Theorem.transition thm = Mathlib.Meta.FunProp.Theorem.transition thm_1 → thm = thm_1
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.ext : ∀ {q : ℕ} {x y : LucasLehmer.X q}, x.1 = y.1 → x.2 = y.2 → x = y
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ext_contains_unit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtDHashMap α fun x => Unit},
  (∀ (k : α), m₁.contains k = m₂.contains k) → m₁ = m₂
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeLeftOpOfCone c))
  (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
-- Mathlib.GroupTheory.OrderOfElement
Subsingleton.addOrderOf_eq : ∀ {G : Type u_1} [inst : AddMonoid G] [Subsingleton G] (x : G), addOrderOf x = 1
-- Mathlib.Algebra.Homology.Functor
HomologicalComplex.quasiIso_iff_evaluation : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} V] [inst_2 : CategoryTheory.Abelian V] {ι : Type u_3}
  {c : ComplexShape ι} {K₁ K₂ : HomologicalComplex (CategoryTheory.Functor T V) c} (f : K₁ ⟶ K₂),
  QuasiIso f ↔ ∀ (t : T), QuasiIso ((((CategoryTheory.evaluation T V).obj t).mapHomologicalComplex c).map f)
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.List.applyId.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] (xs : List (α × α)) (x : α),
  Plausible.InjectiveFunction.List.applyId xs x = (List.dlookup x (List.map Prod.toSigma xs)).getD x
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_eq_sum : ∀ {σ : Type u_1} {R : Type u_4} [inst : AddCommMonoid R] [inst_1 : Fintype σ] (f : σ →₀ R), Finsupp.degree f = ∑ i, f i
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.IsBasis.contract_indep_sdiff_iff`. -/
Matroid.IsBasis.contract_indep_diff_iff : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis I X → ((M.contract X).Indep (J \ X) ↔ M.Indep (J \ X ∪ I))
-- Mathlib.Order.Disjoint
complementedLattice_iff : ∀ (α : Type u_2) [inst : Lattice α] [inst_1 : BoundedOrder α], ComplementedLattice α ↔ ∀ (a : α), ∃ b, IsCompl a b
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.padicNormE.is_rat : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ_[p]), ∃ q', ‖q‖ = ↑q'
-- Aesop.Util.Unfold
Aesop.unfoldManyTarget : (Lean.Name → Option (Option Lean.Name)) → Lean.MVarId → Lean.MetaM (Option (Lean.MVarId × Array Lean.Name))
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.coe_toNatLinearEquiv : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] (e : M ≃+ M₂),
  ⇑e.toNatLinearEquiv = ⇑e
-- Init.Data.List.Basic
List.partition.loop : {α : Type u} → (α → Bool) → List α → List α × List α → List α × List α
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.divLeft.eq_1 : ∀ {G : Type u_5} [inst : Group G] (a : G),
  Equiv.divLeft a = { toFun := fun b => a / b, invFun := fun b => b⁻¹ * a, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.copy_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {Q' H' : C} (eQ : Q' ≅ h.Q) (eH : H' ≅ h.H),
  (h.copy eQ eH).Q = Q'
-- Init.NotationExtra
unexpandMkArray7 : Lean.PrettyPrinter.Unexpander
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `TopologicalSpace.NonemptyCompacts.lipschitz_prod`. -/
EMetric.NonemptyCompacts.lipschitz_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : EMetricSpace α] [inst_1 : EMetricSpace β], LipschitzWith 1 fun p => p.1 ×ˢ p.2
-- Std.Data.TreeMap.Basic
Std.TreeMap.instSDiff : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → SDiff (Std.TreeMap α β cmp)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
isQuasiregular_iff_isUnit : ∀ {R : Type u_1} [inst : Ring R] {x : R}, IsQuasiregular x ↔ IsUnit (1 + x)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.coe_toAddSubmonoid_symm_apply : ∀ {M : Type u_1} [inst : MulOneClass M] (S : AddSubmonoid (Additive M)),
  ↑((RelIso.symm Submonoid.toAddSubmonoid) S) = ⇑Additive.ofMul ⁻¹' ↑S
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.restrictPreimage_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty),
  (e.restrictPreimage hs).source = Subtype.val ⁻¹' e.source
-- Mathlib.RingTheory.Localization.Basic
Localization.algEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (a : S),
  (Localization.algEquiv M S).symm a = (IsLocalization.map (Localization M) (RingHom.id R) ⋯) a
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPair.noConfusionType : Sort v✝ → CategoryTheory.Limits.WalkingParallelPair → CategoryTheory.Limits.WalkingParallelPair → Sort v✝
-- Init.Data.Nat.Lemmas
Nat.max_min_distrib_right : ∀ (a b c : ℕ), max (min a b) c = min (max a c) (max b c)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.transIsBigOIsLittleO : {α : Type u_1} →
  {E : Type u_3} →
    {G : Type u_5} →
      {F' : Type u_7} →
        [inst : Norm E] →
          [inst_1 : Norm G] →
            [inst_2 : SeminormedAddCommGroup F'] →
              {l : Filter α} → Trans (fun x1 x2 => x1 =O[l] x2) (fun x1 x2 => x1 =o[l] x2) fun x1 x2 => x1 =o[l] x2
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F],
  Topology.IsEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap
-- Mathlib.Order.Lattice
exists_le_and_iff_exists : ∀ {α : Type u} [inst : SemilatticeInf α] {P : α → Prop} {x₀ : α}, Antitone P → ((∃ x ≤ x₀, P x) ↔ ∃ x, P x)
-- Mathlib.Order.Monotone.Defs
antitoneOn_univ : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, AntitoneOn f Set.univ ↔ Antitone f
-- Batteries.Data.List.Lemmas
List.isPrefixOf?.eq_def : ∀ {α : Type u} [inst : BEq α] (x x_1 : List α),
  x.isPrefixOf? x_1 =
    match x, x_1 with
    | [], l₂ => some l₂
    | x, [] => none
    | x₁ :: l₁, x₂ :: l₂ => if (x₁ == x₂) = true then l₁.isPrefixOf? l₂ else none
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `limitFlipIsoCompLim` is natural with respect to diagrams.  -/
CategoryTheory.Limits.limCompFlipIsoWhiskerLim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
              (CategoryTheory.flipFunctor K J C).comp CategoryTheory.Limits.lim ≅
                (CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj CategoryTheory.Limits.lim
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabelPart.mk.inj : ∀ {value : String} {tooltip? : Option Lean.Lsp.InlayHintTooltip} {location? : Option Lean.Lsp.Location}
  {command? : Option Lean.Lsp.Command} {value_1 : String} {tooltip?_1 : Option Lean.Lsp.InlayHintTooltip}
  {location?_1 : Option Lean.Lsp.Location} {command?_1 : Option Lean.Lsp.Command},
  { value := value, tooltip? := tooltip?, location? := location?, command? := command? } =
      { value := value_1, tooltip? := tooltip?_1, location? := location?_1, command? := command?_1 } →
    value = value_1 ∧ tooltip? = tooltip?_1 ∧ location? = location?_1 ∧ command? = command?_1
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  (X : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)),
  ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).obj X).fiber =
    CategoryTheory.AsSmall.down.obj X.fiber
-- Mathlib.Algebra.GroupWithZero.Regular
/-- Non-zero elements of an integral domain are regular.  -/
IsRegular.of_ne_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] [IsCancelMulZero R] {a : R}, a ≠ 0 → IsRegular a
-- Init.Data.List.Nat.Count
_private.Init.Data.List.Nat.Count.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- A left homotopy on morphisms in the category of arrows of a preadditive category.  -/
CategoryTheory.Arrow.LeftHomotopy : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [CategoryTheory.Preadditive V] → {u v : CategoryTheory.Arrow V} → (u ⟶ v) → (u ⟶ v) → Type v_1
-- Mathlib.Tactic.Simps.Basic
/-- A prefix rule `prefix fieldName`  -/
Simps.ProjectionRule.prefix : Lean.Name → Lean.Syntax → Simps.ProjectionRule
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTriv_symm_fst : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι)
  (p : B × F), ↑(Z.localTriv i).symm p = ⟨p.1, (Z.coordChange i (Z.indexAt p.1) p.1) p.2⟩
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.integral_indicator_const : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  [CompleteSpace G] (e : E) ⦃s : Set X⦄ [MeasureTheory.IsFiniteMeasure (μ.variation.restrict s)],
  MeasurableSet s → ∫ᵛ (x : X), s.indicator (fun x => e) x ∂[B; μ] = (B e) (μ s)
-- Mathlib.CategoryTheory.Center.Localization
CategoryTheory.CatCenter.ext_of_localization : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W]
  (r s : CategoryTheory.CatCenter D), (∀ (X : C), r.app (L.obj X) = s.app (L.obj X)) → r = s
-- Mathlib.Algebra.Order.Sub.Basic
tsub_eq_tsub_min : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] (a b : α), a - b = a - min a b
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The natural degree of `cyclotomic' n R` is `totient n` if there is a primitive root of
unity in `R`.  -/
Polynomial.natDegree_cyclotomic' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
  IsPrimitiveRoot ζ n → (Polynomial.cyclotomic' n R).natDegree = n.totient
-- Mathlib.Tactic.NormNum.Core
/-- `norm_num1` normalizes numerical expressions in the goal. It is a basic version of `norm_num`
that does not call `simp`.

By default, it supports the operations `+` `-` `*` `/` `⁻¹` `^` and `%` over types with (at least)
an `AddMonoidWithOne` instance, such as `ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ`. If the goal has the form `A = B`,
`A ≠ B`, `A < B` or `A ≤ B`, where `A` and `B` are numerical expressions, `norm_num1` will try to
close it. It also has a relatively simple primality prover.
:e
This tactic is extensible. Extensions can allow `norm_num1` to evaluate more kinds of expressions,
or to prove more kinds of propositions. See the `@[norm_num]` attribute for further information on
extending `norm_num1`.

* `norm_num1 at l` normalizes at location(s) `l`.

Examples:
```lean
example : 43 ≤ 74 + (33 : ℤ) := by norm_num1
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num1
```
 -/
Mathlib.Tactic.normNum1Conv : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Set
Equiv.image_preimage : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set β), ⇑e '' ⇑e ⁻¹' s = s
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.of_pullback_snd_of_descendsAlong : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {X Y Z : C}
  {f : X ⟶ Z} {g : Y ⟶ Z} [P.DescendsAlong Q] [inst_2 : CategoryTheory.Limits.HasPullback f g],
  Q g → P (CategoryTheory.Limits.pullback.snd f g) → P f
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey a (Std.Internal.List.eraseKey k l) = (!k == a && Std.Internal.List.containsKey a l)
-- Init.Prelude
/-- Gets an optional value, returning a given default on `none`.

This function is `@[macro_inline]`, so `dflt` will not be evaluated unless `opt` turns out to be
`none`.

Examples:
 * `(some "hello").getD "goodbye" = "hello"`
 * `none.getD "goodbye" = "goodbye"`
 -/
Option.getD : {α : Type u_1} → Option α → α → α
-- Mathlib.Order.Hom.CompleteLattice
sSupHomClass.toSupBotHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [sSupHomClass F α β], SupBotHomClass F α β
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the `finrank` of a
cyclotomic extension is `n.totient`.  -/
IsCyclotomicExtension.finrank : ∀ {n : ℕ} [NeZero n] {K : Type u} (L : Type v) [inst : Field K] [inst_1 : CommRing L] [IsDomain L]
  [inst_3 : Algebra K L] [IsCyclotomicExtension {n} K L],
  Irreducible (Polynomial.cyclotomic n K) → Module.finrank K L = n.totient
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.smul_mem_rootSet : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] [inst_3 : Algebra S R]
  {G : Type u_1} [inst_4 : Monoid G] [inst_5 : MulSemiringAction G R] [SMulCommClass G S R] {f : Polynomial S} (g : G)
  {x : R}, x ∈ f.rootSet R → g • x ∈ f.rootSet R
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The natural isomorphism between the `n`-th index of the Tate complex and inhomogeneous
`n`-cochains for `0 ≤ n`.  -/
TateCohomology.tateComplex.evalNonneg : {R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] →
      [inst_2 : Fintype G] →
        (n : ℕ) →
          (tateComplexFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) ↑n) ≅
            (groupCohomology.cochainsFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℕ) n)
-- Mathlib.Tactic.Simps.Basic
/-- Other attributes to apply to generated lemmas.  -/
Simps.Config.attrs : Simps.Config → Array Lean.Elab.Attribute
-- Mathlib.Topology.Order.IntermediateValue
/-- A bounded connected subset of a conditionally complete linear order includes the open interval
`(Inf s, Sup s)`.  -/
IsConnected.Ioo_csInf_csSup_subset : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {s : Set α},
  IsConnected s → BddBelow s → BddAbove s → Set.Ioo (sInf s) (sSup s) ⊆ s
-- Mathlib.Topology.EMetricSpace.Defs
uniformity_basis_edist_inv_nat : ∀ {α : Type u} [inst : PseudoEMetricSpace α],
  (uniformity α).HasBasis (fun x => True) fun n => {p | edist p.1 p.2 < (↑n)⁻¹}
-- Mathlib.Condensed.Light.Explicit
/-- A `LightCondAb` version of `LightCondensed.ofSheafLightProfinite`.  -/
LightCondMod.ofSheafLightProfinite : (R : Type u) →
  [inst : Ring R] →
    (F : CategoryTheory.Functor LightProfiniteᵒᵖ (ModuleCat R)) →
      [CategoryTheory.Limits.PreservesFiniteProducts F] →
        CategoryTheory.regularTopology.EqualizerCondition F → LightCondMod R
-- Init.Data.String.Decode
Char.utf8Size_pos : ∀ (c : Char), 0 < c.utf8Size
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioi_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Ioi a)), Subtype.val '' Set.Iio b = Set.Ioo a ↑b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.obj.η_def_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.MonObj X] {Z : D}
  (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F)
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.MonObj.one) h)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.add.sizeOf_spec : ∀ (k : ℤ) (v : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  sizeOf (Lean.Grind.CommRing.Poly.add k v p) = 1 + sizeOf k + sizeOf v + sizeOf p
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.d_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  (self : M.Derivation φ) {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)),
  self.d ((CategoryTheory.ConcreteCategory.hom (R.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (M.map f)) (self.d x)