mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_map_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) {X Y : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c}
  (f : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).map f).left =
    CategoryTheory.Over.homMk f.left.left ⋯
-- Mathlib.GroupTheory.OrderOfElement
nsmulCoprime_symm_apply : ∀ {n : ℕ} {G : Type u_6} [inst : AddGroup G] (h : (Nat.card G).Coprime n) (g : G),
  (nsmulCoprime h).symm g = (Nat.card G).gcdB n • g
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_sdiff_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Icc a b \ {a} = Set.Ioc a b
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.scale.inj : ∀ {a : ℕ} {a_1 : Mathlib.Tactic.Linarith.CompSource} {a_2 : ℕ} {a_3 : Mathlib.Tactic.Linarith.CompSource},
  Mathlib.Tactic.Linarith.CompSource.scale a a_1 = Mathlib.Tactic.Linarith.CompSource.scale a_2 a_3 →
    a = a_2 ∧ a_1 = a_3
-- Aesop.Script.SScript
_private.Aesop.Script.SScript.0.Aesop.Script.SScript.render.renderSTactic? : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [Lean.MonadQuotation m] →
        ℕ → Aesop.Script.Step → Aesop.Script.SScript → m (Option (Lean.Syntax.Tactic × Aesop.Script.SScript))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_smul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (c : ℝ) (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.norm (c • x) = |c| ^ Module.finrank ℚ K * NumberField.mixedEmbedding.norm x
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.toBitVec_maxValueSealed_eq_intMaxSealed : ISize.maxValueSealed✝.toBitVec = BitVec.Signed.intMaxSealed✝ System.Platform.numBits
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- Fully faithful functors are stable by composition.  -/
CategoryTheory.Functor.FullyFaithful.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
            {F : CategoryTheory.Functor C D} →
              F.FullyFaithful → {G : CategoryTheory.Functor D E} → G.FullyFaithful → (F.comp G).FullyFaithful
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.tendsto_nhdsWithin_nhdsWithin : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : PseudoMetricSpace β] {t : Set β}
  {f : α → β} {a : α} {b : β},
  Filter.Tendsto f (nhdsWithin a s) (nhdsWithin b t) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_closure_right`.

---

Replacing a set by its closure does not change the Hausdorff edistance.  -/
EMetric.hausdorffEdist_closure₂ : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Metric.hausdorffEDist s (closure t) = Metric.hausdorffEDist s t
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.homologyι_singleObjOpcyclesSelfIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).homologyι j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).inv h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).hom h
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.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}
  {x : E}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → DifferentiableAt 𝕜 (f + g) x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The connecting homomorphism
`(t.truncGELT a b).obj X ⟶ ((t.truncLT a).obj X)⟦1⟧`,
as a natural transformation.  -/
CategoryTheory.Triangulated.TStructure.truncGELTδLT : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} 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 : ℤ) → t.truncGELT a b ⟶ (t.truncLT a).comp (CategoryTheory.shiftFunctor C 1)
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The `AddSubgroup.inclusion` between `lp` spaces, as a linear map.  -/
lp.linearMapOfLE : (𝕜 : Type u_1) →
  {α : Type u_3} →
    (E : α → Type u_4) →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [inst_1 : NormedRing 𝕜] →
          [inst_2 : (i : α) → Module 𝕜 (E i)] →
            [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] → {p q : ENNReal} → p ≤ q → ↥(lp E p) →ₗ[𝕜] ↥(lp E q)
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.ofUpperSet_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : Topology.WithUpperSet α},
  Topology.WithUpperSet.ofUpperSet a ≤ Topology.WithUpperSet.ofUpperSet b ↔ a ≤ b
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types,
where `G` is locally-full and cover-dense, and `ℱ, ℱ'` are sheaves,
we may obtain a natural isomorphism between sheaves.
 -/
CategoryTheory.Functor.IsCoverDense.Types.sheafIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {G : CategoryTheory.Functor C D} →
            [G.IsCoverDense K] →
              [G.IsLocallyFull K] →
                {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} → (G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) → (ℱ ≅ ℱ')
-- Init.Data.Array.Lemmas
List.modify_toArray : ∀ {α : Type u_1} {f : α → α} {l : List α} {i : ℕ}, l.toArray.modify i f = (l.modify i f).toArray
-- Lean.Util.OccursCheck
_private.Lean.Util.OccursCheck.0.Lean.occursCheck.visit : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → Lean.Expr → ExceptT Unit (StateT Lean.ExprSet m) Unit
-- Mathlib.Order.Filter.NAry
Filter.map₂_pure : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {a : α} {b : β},
  Filter.map₂ m (pure a) (pure b) = pure (m a b)
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.convAlgebraMap_apply : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid C] [inst_4 : Module R C] [inst_5 : Coalgebra R C]
  [inst_6 : CommSemiring S] [inst_7 : Algebra S A] [inst_8 : SMulCommClass R S A] (s : S) (c : C),
  ((algebraMap S (WithConv (C →ₗ[R] A))) s).ofConv c = s • (algebraMap R A) (CoalgebraStruct.counit c)
-- Mathlib.GroupTheory.Torsion
/-- The torsion additive submonoid of a torsion additive monoid is `⊤`.  -/
IsAddTorsion.torsion_eq_top : ∀ {G : Type u_1} [inst : AddCommMonoid G], IsAddTorsion G → AddCommMonoid.addTorsion G = ⊤
-- Mathlib.Algebra.Group.Action.Defs
/-- Associativity of `+ᵥ` and `+`  -/
AddSemigroupAction.add_vadd : ∀ {G : Type u_9} {P : Type u_10} {inst : AddSemigroup G} [self : AddSemigroupAction G P] (g₁ g₂ : G) (p : P),
  (g₁ + g₂) +ᵥ p = g₁ +ᵥ g₂ +ᵥ p
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path.mk₂_vertex : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (p q : X.Path 1) (h : p.vertex 1 = q.vertex 0) (a : Fin (Nat.succ 2)),
  (p.mk₂ q h).vertex a = ![p.vertex 0, p.vertex 1, q.vertex 1] a
-- Mathlib.Topology.Category.TopCat.Adjunctions
/-- Equipping a type with the trivial topology is right adjoint to the forgetful functor
`Top ⥤ Type`.  -/
TopCat.adj₂ : CategoryTheory.forget TopCat ⊣ TopCat.trivial
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The natural isomorphism `FA ⨿ F- ≅ F(A ⨿ -)`, provided each `coprodComparison F A B` is an
isomorphism (as `B` changes).
 -/
CategoryTheory.Limits.coprodComparisonNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{w, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] →
            [inst_3 : CategoryTheory.Limits.HasBinaryCoproducts D] →
              (A : C) →
                [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] →
                  F.comp (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) ≅
                    (CategoryTheory.Limits.coprod.functor.obj A).comp F
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of a sum is bounded above by the maximum of the valuations.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : R),
  v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.nullSingletonClass_hausdorff : ∀ (X : Type u_2) [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d : ℝ},
  0 < d → MeasureTheory.NullSingletonClass (MeasureTheory.Measure.hausdorffMeasure d)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Alternative version of `List.prod_set` when the list is over a group  -/
List.prod_set' : ∀ {G : Type u_7} [inst : CommGroup G] (L : List G) (n : ℕ) (a : G),
  (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.hom_eq_iff : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] {f g : FreeAddMonoid α →+ M},
  f = g ↔ ∀ (x : α), f (FreeAddMonoid.of x) = g (FreeAddMonoid.of x)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
StarAlgHom.ext_continuousMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [ContinuousMap.UniqueHom R A] (a : A) [CompactSpace ↑(spectrum R a)]
  (φ ψ : C(↑(spectrum R a), R) →⋆ₐ[R] A),
  Continuous ⇑φ →
    Continuous ⇑ψ →
      φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
          ψ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) →
        φ = ψ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
        ⟨k, v⟩ ∈ l → (↑(m.insertMany l)).getD k' fallback = cast ⋯ v
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.id_app : ∀ {C D : CategoryTheory.Cat} (F : C ⟶ D) (X : ↑C),
  (CategoryTheory.CategoryStruct.id F).toNatTrans.app X = CategoryTheory.CategoryStruct.id (F.toFunctor.obj X)
-- Mathlib.ModelTheory.Definability
/-- Shows that definability is closed under finite projections.  -/
Set.Definable.image_comp : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1}
  {s : Set (β → M)}, A.Definable L s → ∀ (f : α → β) [Finite α] [Finite β], A.Definable L ((fun g => g ∘ f) '' s)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.operator.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.operator = 1
-- Mathlib.Data.Nat.Prime.Basic
Nat.coprime_two_right : ∀ {n : ℕ}, n.Coprime 2 ↔ Odd n
-- Mathlib.Topology.UniformSpace.Basic
Filter.HasBasis.uniformity_closure : ∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {p : ι → Prop} {U : ι → SetRel α α},
  (uniformity α).HasBasis p U → (uniformity α).HasBasis p fun i => closure (U i)
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.AddCommMonCat.Hom.mk.sizeOf_spec : ∀ {A B : AddCommMonCat} (hom' : ↑A →+ ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Init.Data.Slice.List.Basic
instSliceableListSliceNat_1 : {α : Type u} → Std.Rco.Sliceable (ListSlice α) ℕ (ListSlice α)
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.not_isUnit_of_natDegree_pos_of_isReduced : ∀ {R : Type u_1} [inst : CommRing R] [IsReduced R] (p : Polynomial R), 0 < p.natDegree → ¬IsUnit p
-- Lean.Data.Lsp.TextSync
Lean.Lsp.SaveOptions.includeText : Lean.Lsp.SaveOptions → Bool
-- Mathlib.Logic.IsEmpty.Defs
Fin.isEmpty : IsEmpty (Fin 0)
-- Mathlib.Data.Tree.Basic
BinaryTree.node.inj : ∀ {α : Type u} {value : α} {left right : BinaryTree α} {value_1 : α} {left_1 right_1 : BinaryTree α},
  BinaryTree.node value left right = BinaryTree.node value_1 left_1 right_1 →
    value = value_1 ∧ left = left_1 ∧ right = right_1
-- Std.Http.Data.URI.Basic
/-- Returns the default port number for this URI scheme: 443 for `https`, 80 for everything else.
 -/
Std.Http.URI.Scheme.defaultPort : Std.Http.URI.Scheme → UInt16
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.lt : {α : Type u} →
  (self : Std.Packages.PreorderOfLEArgs α) →
    let this := self.le;
    LT α
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.isoOpEquiv_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A B : Cᵒᵖ) (g : Opposite.unop B ≅ Opposite.unop A),
  (CategoryTheory.isoOpEquiv A B).symm g = g.op
-- Mathlib.Order.Restriction
Preorder.restrictLe₂_apply : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} {a b : α} (hab : a ≤ b) (f : (i : ↑(Set.Iic b)) → π ↑i)
  (i : ↑(Set.Iic a)), Preorder.restrictLe₂ hab f i = f ⟨↑i, ⋯⟩
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.glue!.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (r : Std.DTreeMap.Internal.Impl α β) →
      (sz' : ℕ) →
        (k' : α) →
          (v' : β k') →
            (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
              r = Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'' →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | r@h:(Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') => h_2 r sz' k' v' l'' r'' h) =
    h_1 ()
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_lt_iff_one_lt_mul' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α}, a⁻¹ < b ↔ 1 < a * b
-- Init.System.IO
/-- The `Task` is waiting to be run.

It can be waiting for dependencies to complete or sitting in the task manager queue waiting for a
thread to run on.
 -/
IO.TaskState.waiting : IO.TaskState
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_modifyKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k (Std.Internal.List.modifyKey k f l) =
      if Std.Internal.List.containsKey k l = true then some k else none
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.degree_pos_of_ne_zero_of_nonunit : ∀ {R : Type u} [inst : DivisionRing R] {p : Polynomial R}, p ≠ 0 → ¬IsUnit p → 0 < p.degree
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.medial_points : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [inst_5 : CharZero k] (s : Affine.Simplex k P n)
  (i : Fin (n + 1)), s.medial.points i = s.faceOppositeCentroid i
-- Mathlib.Data.Int.GCD
_private.Mathlib.Data.Int.GCD.0.Nat.P.match_1.splitter : (motive : ℕ × ℤ × ℤ → Sort u_1) → (x : ℕ × ℤ × ℤ) → ((r : ℕ) → (s t : ℤ) → motive (r, s, t)) → motive x
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.Scheme.Hom.isConnected_preimage : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyConnected f],
  IsOpenMap ⇑f → ∀ {s : Set ↥S}, IsConnected s → IsClosed s → IsConnected (⇑f ⁻¹' s)
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.inv : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  IsSolvableByRad F α → IsSolvableByRad F α⁻¹
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
Complex.borelSpace : BorelSpace ℂ
-- Mathlib.NumberTheory.FactorisationProperties
Nat.instDecidableAbundant : (n : ℕ) → Decidable n.Abundant
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Two subalgebras that are equal are also equivalent as algebras.

This is the `Subalgebra` version of `LinearEquiv.ofEq` and `Equiv.setCongr`.  -/
Subalgebra.equivOfEq : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S T : Subalgebra R A) → S = T → ↥S ≃ₐ[R] ↥T
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Meta.Grind.Params.insertFunCC : Lean.Meta.Grind.Params → Lean.Name → Lean.Meta.Grind.Params
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.instAdd : Add Cardinal.{u}
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_of_contains_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, (m.erase k).contains a = true → m.contains a = true
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_sub_leadingTerm_lt_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f : MvPolynomial σ R},
  m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f) ↔ m.degree f ≠ 0
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitor_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) {Y : C}
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X X' : CategoryTheory.GradedObject J D) (φ : X ⟶ X')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X').obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  {Z : CategoryTheory.GradedObject J D} (h : X' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.mapBifunctorMapMap F p φ
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj Y)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X').hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom
      (CategoryTheory.CategoryStruct.comp φ h)
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.lift.congr_simp : ∀ {R : Type u} [inst : Ring R] (I : Ideal R) {S : Type v} [inst_1 : I.IsTwoSided] [inst_2 : Semiring S]
  (f f_1 : R →+* S) (e_f : f = f_1) (H : ∀ a ∈ I, f a = 0), Ideal.Quotient.lift I f H = Ideal.Quotient.lift I f_1 ⋯
-- Mathlib.ModelTheory.Syntax
/-- Substitutes the functions in a given term with expressions.  -/
FirstOrder.Language.Term.substFunc : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} → {α : Type u'} → L.Term α → ({n : ℕ} → L.Functions n → L'.Term (Fin n)) → L'.Term α
-- Lean.Meta.Basic
Lean.Meta.instInhabitedAbstractMVarsResult : Inhabited Lean.Meta.AbstractMVarsResult
-- Mathlib.Order.CompleteLattice.Defs
iSup_lt_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteSemilatticeSup α] {l : α} {f : ι → α},
  iSup f < l ↔ ∃ b < l, ∀ (i : ι), f i ≤ b
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_generateFrom : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {s : Set (Set β)} {f : α → β},
  (∀ t ∈ s, MeasurableSet (f ⁻¹' t)) → Measurable f
-- Mathlib.Data.Finsupp.Basic
/-- The `Finsupp` version of `Pi.uniqueOfIsEmpty`.  -/
Finsupp.uniqueOfLeft : {α : Type u_1} → {R : Type u_10} → [inst : Zero R] → [IsEmpty α] → Unique (α →₀ R)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ordCompare_minKey_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtDTreeMap α (fun x => β) compare}
  {k : α} {f : β → β} {he : Std.ExtDTreeMap.Const.modify t k f ≠ ∅},
  compare ((Std.ExtDTreeMap.Const.modify t k f).minKey he) (t.minKey ⋯) = Ordering.eq
-- Mathlib.Order.CompleteLattice.Defs
sInf_le : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, a ∈ s → sInf s ≤ a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.denote_toPolyC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (e : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Poly.denote ctx (e.toPolyC c) = Lean.Grind.CommRing.Expr.denote ctx e
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.ext_iff : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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]
  {D1 D2 : LieDerivation R L M}, D1 = D2 ↔ ∀ (a : L), D1 a = D2 a
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if the ENode associate with `e` has support for function equality
congruence closure. See `Grind.Config.funCC` for additional details.
 -/
Lean.Meta.Grind.useFunCC : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.IsPrincipal.add_eq_right : ∀ {a o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o → a < o → a + o = o
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- When the ancestrality relation is well founded, we say that `h : A.PairingCore`
is regular.  -/
SSet.Subcomplex.PairingCore.IsRegular : {X : SSet} → {A : X.Subcomplex} → A.PairingCore → Prop
-- Init.Data.Option.Attach
Option.isNone_attachWith : ∀ {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), o = some a → p a), (o.attachWith p H).isNone = o.isNone
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.coe_sup : ∀ {E : Type u_3} [inst : AddGroup E] (p q : NonarchAddGroupSeminorm E), ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_one : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  ↑1 = 1
-- Mathlib.FieldTheory.Finite.Basic
/-- The prime subfield is finite.  -/
Subfield.fintypeBot : (F : Type u_3) → [inst : Field F] → (p : ℕ) → [Fact (Nat.Prime p)] → [CharP F p] → Fintype ↥⊥
-- Init.Omega.Int
Lean.Omega.Prod.of_not_lex : ∀ {α : Type u_1} {r : α → α → Prop} [DecidableEq α] {β : Type u_2} {s : β → β → Prop} {p q : α × β},
  ¬Prod.Lex r s p q → ¬r p.1 q.1 ∧ (p.1 ≠ q.1 ∨ ¬s p.2 q.2)