mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_self : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c : P) (R : ℝ), EuclideanGeometry.inversion c R c = c
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.inv_prodComparison_map_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] {Z : D} (h : F.obj B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B))
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.snd) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
-- Lean.Server.Rpc.Basic
Lean.Server.ReferencedObject.id : Lean.Server.ReferencedObject → USize
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_mul : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a →
    ∀ (f g : PowerSeries R), PowerSeries.subst a (f * g) = PowerSeries.subst a f * PowerSeries.subst a g
-- Mathlib.Order.Filter.Map
Filter.comap_snd_neBot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β}, (Filter.comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot
-- Mathlib.Data.Sym.Basic
/-- This is the `List.Perm` setoid lifted to `Vector`.

See note [reducible non-instances].
 -/
List.Vector.Perm.isSetoid : (α : Type u_1) → (n : ℕ) → Setoid (List.Vector α n)
-- Mathlib.FieldTheory.Separable
/-- If `E / K / F` is an extension tower, `E` is separable over `F`, then it's also separable
over `K`.  -/
Algebra.isSeparable_tower_top_of_isSeparable : ∀ (F : Type u_1) (L : Type u_2) [inst : CommRing F] (E : Type u_4) [inst_1 : Field L] [inst_2 : Ring E]
  [inst_3 : Algebra F L] [inst_4 : Algebra F E] [inst_5 : Algebra L E] [IsScalarTower F L E] [Algebra.IsSeparable F E],
  Algebra.IsSeparable L E
-- Std.Do.Internal.Ensures.Lemmas
/-- `MonadAttach.attach` is bind-faithful with `x`.  -/
Std.Do.Internal.ErasesTo.of_attach : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m] [WeaklyLawfulMonadAttach m]
  {α : Type u_1} {x : m α}, Std.Do.Internal.ErasesTo (MonadAttach.attach x) x
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.uniqueProd_apply : ∀ (R : Type u_8) (M : Type u_9) (N : Type u_10) [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace N] [inst_4 : AddCommMonoid N] [inst_5 : Unique N]
  [inst_6 : Module R M] [inst_7 : Module R N] (x : N × M), (ContinuousLinearEquiv.uniqueProd R M N) x = x.2
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.Props : Type
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sum_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ] [inst : Fintype ι],
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.covariance (∑ i, X i) Y μ = ∑ i, ProbabilityTheory.covariance (X i) Y μ
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView.thenBranch : Lean.Elab.Term.Do.DoIfView → Lean.Syntax
-- Mathlib.Order.Hom.Bounded
/-- `BoundedOrderHomClass F α β` states that `F` is a type of bounded order morphisms.

You should extend this class when you extend `BoundedOrderHom`.  -/
BoundedOrderHomClass : (F : Type u_6) →
  (α : Type u_7) →
    (β : Type u_8) → [inst : LE α] → [inst_1 : LE β] → [BoundedOrder α] → [BoundedOrder β] → [FunLike F α β] → Prop
-- Mathlib.Data.Finset.Insert
Finset.toList_singleton : ∀ {α : Type u_1} (a : α), {a}.toList = [a]
-- Mathlib.FieldTheory.Finite.Basic
/-- The sum of `x ^ i` as `x` ranges over the units of a finite field of cardinality `q`
is equal to `0` unless `(q - 1) ∣ i`, in which case the sum is `q - 1`.  -/
FiniteField.sum_pow_units : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] [inst_2 : DecidableEq K] (i : ℕ),
  ∑ x, ↑x ^ i = if Fintype.card K - 1 ∣ i then -1 else 0
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value_Ico : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {a : X} {l : Filter X},
      a ∈ s →
        ∀ [l.NeBot],
          l ≤ Filter.principal s →
            ∀ {f : X → α}, ContinuousOn f s → ∀ {v : α}, Filter.Tendsto f l (nhds v) → Set.Ico (f a) v ⊆ f '' s
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrder.mk.congr_simp : ∀ {α : Type u_1} [inst : Preorder α] (finsetIcc finsetIcc_1 : α → α → Finset α) (e_finsetIcc : finsetIcc = finsetIcc_1)
  (finsetIco finsetIco_1 : α → α → Finset α) (e_finsetIco : finsetIco = finsetIco_1)
  (finsetIoc finsetIoc_1 : α → α → Finset α) (e_finsetIoc : finsetIoc = finsetIoc_1)
  (finsetIoo finsetIoo_1 : α → α → Finset α) (e_finsetIoo : finsetIoo = finsetIoo_1)
  (finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b)
  (finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ a ≤ x ∧ x < b)
  (finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ a < x ∧ x ≤ b)
  (finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ a < x ∧ x < b),
  { finsetIcc := finsetIcc, finsetIco := finsetIco, finsetIoc := finsetIoc, finsetIoo := finsetIoo,
      finset_mem_Icc := finset_mem_Icc, finset_mem_Ico := finset_mem_Ico, finset_mem_Ioc := finset_mem_Ioc,
      finset_mem_Ioo := finset_mem_Ioo } =
    { finsetIcc := finsetIcc_1, finsetIco := finsetIco_1, finsetIoc := finsetIoc_1, finsetIoo := finsetIoo_1,
      finset_mem_Icc := ⋯, finset_mem_Ico := ⋯, finset_mem_Ioc := ⋯, finset_mem_Ioo := ⋯ }
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.ExprInfo.mk.injEq : ∀ (expr : Lean.Expr) (bvars : List Lean.FVarId) (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances)
  (cfg : Lean.Meta.Config) (expr_1 : Lean.Expr) (bvars_1 : List Lean.FVarId) (lctx_1 : Lean.LocalContext)
  (localInsts_1 : Lean.LocalInstances) (cfg_1 : Lean.Meta.Config),
  ({ expr := expr, bvars := bvars, lctx := lctx, localInsts := localInsts, cfg := cfg } =
      { expr := expr_1, bvars := bvars_1, lctx := lctx_1, localInsts := localInsts_1, cfg := cfg_1 }) =
    (expr = expr_1 ∧ bvars = bvars_1 ∧ lctx = lctx_1 ∧ localInsts = localInsts_1 ∧ cfg = cfg_1)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.symm : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, (fun x => f₁ x - f₂ x) =O[l] g → (fun x => f₂ x - f₁ x) =O[l] g
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w n : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec n → ℕ → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.mul_self : ∀ {α : Type u_1} [inst : BooleanRing α] (a : α), a * a = a
-- Std.Do.WP.Basic
Std.Do.StateT.instWP : {m : Type u → Type v} →
  {ps : Std.Do.PostShape} → {σ : Type u} → [Std.Do.WP m ps] → Std.Do.WP (StateT σ m) (Std.Do.PostShape.arg σ ps)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `Left.one_lt_inv_iff`.

---

Uses `left` co(ntra)variant.  -/
inv_of_one_lt_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a : α}, 1 < a⁻¹ → a < 1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_tensor_associator_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z X' : C}
  (f : X ⟶ X'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))
      (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Y))
        (CategoryTheory.CategoryStruct.id Z))
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.intervalIntegral_eq_integral_uIoc : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ)
  (μ : MeasureTheory.Measure ℝ),
  ∫ (x : ℝ) in a..b, f x ∂μ = (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Set.uIoc a b, f x ∂μ
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.forIn'_eq_match_step.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.flipCompEvaluation_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (a : A) (X : B),
  (CategoryTheory.flipCompEvaluation F a).inv.app X = CategoryTheory.CategoryStruct.id ((F.obj a).obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Taking the cone of a whiskered bicone results in a cone isomorphic to one gained
by whiskering the cone and postcomposing with a suitable isomorphism.  -/
CategoryTheory.Limits.Bicone.whiskerToCone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {K : Type w'} →
          {f : J → C} →
            (c : CategoryTheory.Limits.Bicone f) →
              (g : K ≃ J) →
                (c.whisker g).toCone ≅
                  (CategoryTheory.Limits.Cone.postcompose (CategoryTheory.Discrete.functorComp f ⇑g).inv).obj
                    (CategoryTheory.Limits.Cone.whisker
                      (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑g)) c.toCone)
-- Mathlib.Tactic.Linter.PPRoundtrip
/-- The "ppRoundtrip" linter emits a warning when the syntax of a command differs substantially
from the pretty-printed version of itself.

The linter makes an effort to start the highlighting at the first difference.
However, it may not always be successful.
It also prints both the source code and the "expected code" in a 5-character radius from
the first difference.
 -/
_private.Mathlib.Tactic.Linter.PPRoundtrip.0.Mathlib.Linter.PPRoundtrip.ppRoundtrip : Lean.Linter
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.instFunLike : {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 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → FunLike (P₁ ≃ᴬ[k] P₂) P₁ P₂
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- If `i + 1 = j`, `mkOfSucc i ≫ δ j` is the morphism `⦋1⦌ ⟶ ⦋n⦌` that
sends `0` and `1` to `i` and `i + 2`, respectively.  -/
SimplexCategory.mkOfSucc_δ_eq : ∀ {n : ℕ} {i : Fin n} {j : Fin (n + 2)},
  j = i.succ.castSucc →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.mkOfSucc i) (SimplexCategory.δ j) =
      SimplexCategory.intervalEdge (↑i) 2 ⋯
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.right.sizeOf_spec : sizeOf Nat.Partrec.Code.right = 1
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.repr.match_1.splitter : (motive : ONote → Sort u_1) →
  (x : ONote) → (Unit → motive ONote.zero) → ((e : ONote) → (n : ℕ+) → (a : ONote) → motive (e.oadd n a)) → motive x
-- Init.Sym.Lemmas
Lean.Sym.UInt8.eq_eq_true : ∀ (a b : UInt8), decide (a = b) = true → (a = b) = True
-- Init.Data.List.MinMax
/-- This lemma is also applicable given the following instances:

```
[LE α] [Min α] [IsLinearOrder α] [LawfulOrderMax α]
```
 -/
List.foldl_max : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] [Std.Associative max] {l : List α} {a : α},
  List.foldl max a l = a ⊔ l.max?.getD a
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.coe_op : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R), ↑S.op = MulOpposite.unop ⁻¹' ↑S
-- Mathlib.Data.Nat.Choose.Basic
Nat.add_one_mul_choose_eq : ∀ (n k : ℕ), (n + 1) * n.choose k = (n + 1).choose (k + 1) * (k + 1)
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- `AddMonoidAlgebra.mapDomain` as a linear equiv.  -/
AddMonoidAlgebra.mapDomainLinearEquiv : (R : Type u_1) →
  (S : Type u_2) →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] → [inst_2 : Module R S] → M ≃ N → AddMonoidAlgebra S M ≃ₗ[R] AddMonoidAlgebra S N
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- A general inner product space structure implies a real inner product structure.

This is not registered as an instance since
* `𝕜` does not appear in the return type `InnerProductSpace ℝ E`,
* It is likely to create instance diamonds, as it builds upon the diamond-prone
  `NormedSpace.restrictScalars`.

However, it can be used in a proof to obtain a real inner product space structure from a given
`𝕜`-inner product space structure.  -/
InnerProductSpace.rclikeToReal : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → InnerProductSpace ℝ E
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.is_add_left_invariant_outerMeasure : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [inst_2 : AddGroup G]
  [inst_3 : SeparatelyContinuousAdd G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) = μ K) →
    ∀ (g : G) (A : Set G), μ.outerMeasure ((fun x => g + x) ⁻¹' A) = μ.outerMeasure A
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).get? k' = if h : cmp k k' = Ordering.eq then cast ⋯ (f (t.get? k)) else t.get? k'
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Icc_left : ∀ {α : Type u_2} {a₁ a₂ b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₁ ≤ a₂ → Finset.Icc a₂ b ⊆ Finset.Icc a₁ b
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.instSMulCommClass : ∀ {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : MulAction G β] [inst_3 : MulAction G' β] [SMulCommClass G G' β], SMulCommClass G G' (α ↪ β)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfpFamily_le_fp : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}},
  (∀ (i : ι), Monotone (f i)) → ∀ {a b : Ordinal.{u}}, a ≤ b → (∀ (i : ι), f i b ≤ b) → Ordinal.nfpFamily f a ≤ b
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_add : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (ν' : MeasureTheory.Measure β)
  [MeasureTheory.SFinite ν'], μ.prod (ν + ν') = μ.prod ν + μ.prod ν'
-- Init.Data.UInt.Basic
/-- Bitwise or for 32-bit unsigned integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.lor : UInt32 → UInt32 → UInt32
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic)
to the integers, or is densely ordered.  -/
LinearOrderedAddCommGroup.discrete_or_denselyOrdered : ∀ (G : Type u_2) [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G],
  Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G
-- Mathlib.Geometry.Manifold.IsManifold.Basic
instAddCommGroupTangentSpace : {𝕜 : Type u_2} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_1} →
      [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] → (_x : M) → AddCommGroup (TangentSpace I _x)
-- Init.Core
proof_irrel : ∀ {a : Prop} (h₁ h₂ : a), h₁ = h₂
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_eq_zero_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ENormedAddMonoid ε] {f : α → ε}, MeasureTheory.eLpNormEssSup f μ = 0 ↔ f =ᵐ[μ] 0
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- The topology of `X` is finer than the compactly generated topology.  -/
UCompactlyGeneratedSpace.le_compactlyGenerated : ∀ {X : Type v} {t : TopologicalSpace X} [self : UCompactlyGeneratedSpace X], t ≤ TopologicalSpace.compactlyGenerated X
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instCommRingSubtypeMemCenter : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type u_1} → [inst_1 : Ring A] → [inst_2 : Algebra R A] → CommRing ↥(Subalgebra.center R A)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey he ∈ t
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The cosine zeta function is differentiable everywhere, except at `s = 1` if `a = 0`.  -/
HurwitzZeta.differentiableAt_cosZeta : ∀ (a : UnitAddCircle) {s : ℂ}, s ≠ 1 ∨ a ≠ 0 → DifferentiableAt ℂ (HurwitzZeta.cosZeta a) s
-- Mathlib.Topology.Order.LeftRightNhds
nhdsLT_basis_Ico : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] (a : α), (nhdsWithin a (Set.Iio a)).HasBasis (fun x => x < a) fun x => Set.Ico x a
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mapMahlerMeasure_nonneg : ∀ {A : Type u_1} [inst : Semiring A] (p : Polynomial A) (v : A →+* ℂ), 0 ≤ p.mapMahlerMeasure v
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_real_mul : ∀ (x : ℂ) {r : ℝ}, 0 < r → (↑r * x).arg = x.arg
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1 : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  (X : CategoryTheory.GradedObject I C),
  (((CategoryTheory.GradedObject.mapBifunctor (CategoryTheory.MonoidalCategory.curriedTensor C) I I).obj X).obj
        ((CategoryTheory.GradedObject.single₀ I).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).HasMap
    fun x =>
    match x with
    | (i₁, i₂) => i₁ + i₂
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquivLast_last : ∀ {n : ℕ}, finSuccEquivLast (Fin.last n) = none
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.funLike.eq_1 : ∀ {E : Type u_3} [inst : Group E], GroupSeminorm.funLike = { coe := fun f => f.toFun, coe_injective := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- A functor is said to preserve filtered colimits, if it preserves all colimits of shape `J`, where
`J` is a filtered category which is small relative to the universe in which morphisms of the source
live.
 -/
CategoryTheory.Limits.PreservesFilteredColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.le_tsum' : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [CanonicallyOrderedAdd α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α},
  Summable f → ∀ (i : ι), f i ≤ ∑' (i : ι), f i
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.subsingleton_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N), Subsingleton N ↔ 0 ∈ S
-- Mathlib.GroupTheory.Congruence.Defs
/-- Congruence relations are closed under multiplication  -/
Con.mul' : ∀ {M : Type u_1} [inst : Mul M] (self : Con M) {w x y z : M},
  self.toSetoid w x → self.toSetoid y z → self.toSetoid (w * y) (x * z)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Polynomial.cyclotomic_six : ∀ (R : Type u_1) [inst : Ring R], Polynomial.cyclotomic 6 R = Polynomial.X ^ 2 - Polynomial.X + 1
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_smul : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β] {R : Type u_2}
  [inst_3 : Zero R] [inst_4 : SMulWithZero R β] [inst_5 : ContinuousConstSMul R β] (r : R)
  (f : ZeroAtInftyContinuousMap α β), ⇑(r • f) = r • ⇑f
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.smul_def : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁] (f : A₁ ≃ₐ[R] A₁)
  (a : A₁), f • a = f a
-- Mathlib.Tactic.SetNotationForOrder
/-- Declare `∀ x ⊇ y, ...` as syntax for `∀ x, x ⊇ y → ...` and `∃ x ⊇ y, ...` as syntax for
`∃ x, x ⊇ y ∧ ...`  -/
Mathlib.Meta.SetNotationForOrder.«binderPred⊇_» : Lean.ParserDescr
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `monotoneOn_dual_iff`. -/
MonotoneOn.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instSemigroupWithZeroOfContinuousMul : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : SemigroupWithZero β] → [ContinuousMul β] → SemigroupWithZero (CompactlySupportedContinuousMap α β)
-- Mathlib.Data.Set.Lattice
Set.iUnion_nonempty_index : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : s.Nonempty → Set β), ⋃ (h : s.Nonempty), t h = ⋃ x, ⋃ (h : x ∈ s), t ⋯
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.normRule.inj : ∀ {r r_1 : Aesop.NormRule}, Aesop.BaseRuleSetMember.normRule r = Aesop.BaseRuleSetMember.normRule r_1 → r = r_1