mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₂.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {F : ι → Type u_4}
  {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h)
  [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_6 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_7 : IsDirectedOrder ι]
  (ih ih_1 : (i : ι) → F₁ i → F₂ i → F i) (e_ih : ih = ih_1)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y))
  (a a_1 : DirectLimit F₁ f₁),
  a = a_1 →
    ∀ (a_2 a_3 : DirectLimit F₂ f₂),
      a_2 = a_3 → DirectLimit.map₂ f₁ f₂ f ih compat a a_2 = DirectLimit.map₂ f₁ f₂ f ih_1 ⋯ a_1 a_3
-- Mathlib.AlgebraicGeometry.Normalization
/-- The diagram of affine schemes that we glue to form the normalization.  -/
AlgebraicGeometry.Scheme.Hom.normalizationGlueData : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [AlgebraicGeometry.QuasiCompact f] →
      [AlgebraicGeometry.QuasiSeparated f] →
        AlgebraicGeometry.Scheme.Cover.RelativeGluingData (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover Y)
-- Mathlib.Order.BoundedOrder.Basic
OrderBot.ext_bot : ∀ {α : Type u_1} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α} (B : OrderBot α),
  (∀ (y x : α), y ≤ x ↔ y ≤ x) → ⊥ = ⊥
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.smul : ∀ {𝕜 : 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 : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜']
  [inst_7 : Module 𝕜' F] [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'},
  HasFDerivWithinAt c c' s x →
    HasFDerivWithinAt f f' s x → HasFDerivWithinAt (c • f) (c x • f' + c'.smulRight (f x)) s x
-- Mathlib.Topology.MetricSpace.Basic
/-- Pull back a metric space structure by a uniform embedding. This is a version of
`MetricSpace.induced` useful in case if the domain already has a `UniformSpace` structure.  -/
IsUniformEmbedding.comapMetricSpace : {α : Type u_2} →
  {β : Type u_3} → [inst : UniformSpace α] → [m : MetricSpace β] → (f : α → β) → IsUniformEmbedding f → MetricSpace α
-- Lean.Expr
Lean.instInhabitedLiteral : Inhabited Lean.Literal
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instIsEmpty : ∀ {α : Type u_1} [inst : TopologicalSpace α] [IsEmpty α], IsEmpty (TopologicalSpace.NonemptyCompacts α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_eq_getLastD_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {fallback : α}, t.maxKeyD fallback = t.keys.getLastD fallback
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.sSup_unit_ball_eq_norm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : DenselyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F),
  sSup ((fun x => ‖f x‖) '' Metric.ball 0 1) = ‖f‖
-- Mathlib.Topology.UniformSpace.Defs
/-- Every set in the uniformity filter includes the diagonal.  -/
UniformSpace.Core.refl : ∀ {α : Type u} (self : UniformSpace.Core α), Filter.principal SetRel.id ≤ self.uniformity
-- Mathlib.RingTheory.RamificationInertia.Basic
/-- Let `R` be an integral domain, let `S` be a finite flat `R`-algebra, and let `p` be a prime
ideal of `R`. Then the sum over all prime ideals `q` of `S` lying over `p` of the ramification
index of `q` times the inertia degree of `q` equals the rank of `S` as an `R`-module.  -/
Ideal.sum_ramification_inertia_eq_finrank : ∀ {R : Type u_1} [inst : CommRing R] (p : Ideal R) [p.IsPrime] (S : Type u_2) [inst_2 : CommRing S]
  [inst_3 : Algebra R S] [IsDomain R] [Module.Finite R S] [Module.Flat R S] [inst_7 : Fintype ↑(p.primesOver S)],
  ∑ q, (↑q).ramificationIdx R * (↑q).inertiaDeg R = Module.finrank R S
-- Mathlib.Analysis.Calculus.FDeriv.Pow
HasFDerivWithinAt.pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x →
    ∀ (n : ℕ), HasFDerivWithinAt (f ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') s x
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coneOfDiagramTerminal_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (hX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C)
  [inst_2 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)],
  (CategoryTheory.Limits.coneOfDiagramTerminal hX F).pt = F.obj X
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.comap_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {W : Type u_5}
  [inst_2 : TopologicalSpace W] (f : C(W, X)) (g : C(X, Y)),
  LocallyConstant.comap (g.comp f) = LocallyConstant.comap f ∘ LocallyConstant.comap g
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.wasDeleted : Lean.Widget.DiffTag
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symmₗ_linearMapAt : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ∀ (y : E b), (Bundle.Trivialization.symmₗ R e b) ((Bundle.Trivialization.linearMapAt R e b) y) = y
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ D` creates
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.createsColimitOfOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.CreatesLimit K.op F.op] → CategoryTheory.CreatesColimit K F
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_eq_right : ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, IsAddUnit b → (a + b = b ↔ a = 0)
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The Gaussian pdf is measurable.  -/
ProbabilityTheory.measurable_uncurry_gaussianPDFReal : Measurable fun x =>
  match x with
  | (μ, v, x) => ProbabilityTheory.gaussianPDFReal μ v x
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_injective : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x}))
  [SimplyConnectedSpace E], Function.Injective ⇑(hp.fundamentalGroupToMulOpposite e)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressParams.mk : Lean.Lsp.VersionedTextDocumentIdentifier →
  Array Lean.Lsp.LeanFileProgressProcessingInfo → Lean.Lsp.LeanFileProgressParams
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Basic.0.Array.ofFn.go.congr_simp : ∀ {α : Type u} {n : ℕ} (f f_1 : Fin n → α),
  f = f_1 →
    ∀ (acc acc_1 : Array α),
      acc = acc_1 → ∀ (i i_1 : ℕ) (e_i : i = i_1) (a : i ≤ n), Array.ofFn.go✝ f acc i a = Array.ofFn.go✝ f_1 acc_1 i_1 ⋯
-- Mathlib.Algebra.Quaternion
/-- The cardinality of the quaternions, as a type.  -/
Cardinal.mk_quaternion : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R], Cardinal.mk (Quaternion R) = Cardinal.mk R ^ 4
-- Mathlib.Data.List.AList
AList.lookup.congr_simp : ∀ {α : Type u} {β : α → Type v} {inst : DecidableEq α} [inst_1 : DecidableEq α] (a : α) (s s_1 : AList β),
  s = s_1 → AList.lookup a s = AList.lookup a s_1
-- Mathlib.Algebra.Order.Module.Defs
SMulPosReflectLE.toSMulPosStrictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β] [inst_3 : Zero β]
  [SMulPosReflectLE α β], SMulPosStrictMono α β
-- Mathlib.Data.Sigma.Order
Sigma.instDenselyOrdered : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)],
  DenselyOrdered ((i : ι) × α i)
-- Aesop.Forward.Substitution
Aesop.Substitution.mk.inj : ∀ {premises : Array (Option Lean.Expr)} {levels : Array (Option Lean.Level)} {premises_1 : Array (Option Lean.Expr)}
  {levels_1 : Array (Option Lean.Level)},
  { premises := premises, levels := levels } = { premises := premises_1, levels := levels_1 } →
    premises = premises_1 ∧ levels = levels_1
-- Mathlib.Topology.EMetricSpace.Defs
WeakPseudoEMetricSpace.edist_self : ∀ {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] (x : α), edist x x = 0
-- Mathlib.Tactic.ClickSuggestions.Unfold
/-- Determine whether `e` contains no internal names or raw projections.
We only consider the explicit parts of `e`, because it may happen that an
instance implicit argument is marked as an internal detail, but that is not a problem.  -/
_private.Mathlib.Tactic.ClickSuggestions.Unfold.0.Mathlib.Tactic.ClickSuggestions.isUserFriendly : Lean.Expr → Lean.MetaM Bool
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.empty_subset : ∀ (x : ZFSet.{u}), ∅ ⊆ x
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instInvOneClass.eq_1 : ∀ {α : Type u} [inst : Inv α],
  WithOne.instInvOneClass = { toOne := WithOne.instOne, toInv := WithOne.instInv, inv_one := ⋯ }
-- Mathlib.Algebra.DirectSum.Module
/-- The linear map between direct sums induced by a family of linear maps.  -/
DirectSum.lmap : {R : Type u} →
  [inst : Semiring R] →
    {ι : Type v} →
      {M : ι → Type w} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            {N : ι → Type u_1} →
              [inst_3 : (i : ι) → AddCommMonoid (N i)] →
                [inst_4 : (i : ι) → Module R (N i)] →
                  ((i : ι) → M i →ₗ[R] N i) → (DirectSum ι fun i => M i) →ₗ[R] DirectSum ι fun i => N i
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.id_compHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (AlgebraicGeometry.Scheme.PartialMap.id X).compHom f = AlgebraicGeometry.Scheme.Hom.toPartialMap f
-- Mathlib.Topology.Algebra.Group.Compact
/-- Every topological group in which there exists a compact set with nonempty interior
is locally compact.  -/
TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group : ∀ {G : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  (K : TopologicalSpace.PositiveCompacts G), LocallyCompactSpace G
-- Lean.Server.GoTo
_private.Lean.Server.GoTo.0.Lean.Server.locationLinksFromInstanceProjection.extractInstances : Lean.Expr → Lean.Server.GoToM (Array Lean.Name)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- The canonical comparison functor between the indexing category of the presentation and the
comma category `CostructuredArrow yoneda A`. This functor is always final.  -/
CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (P : CategoryTheory.Limits.IndObjectPresentation A) →
        CategoryTheory.Functor P.I (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
-- Init.Control.Lawful.MonadLift.Instances
_private.Init.Control.Lawful.MonadLift.Instances.0.ExceptT.bindCont.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.equivTree_symm_apply : ∀ (a : BinaryTree Unit), DyckWord.equivTree.symm a = DyckWord.ofTree a
-- Batteries.Logic
congrFun₂ : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f g : (a : α) → (b : β a) → γ a b},
  f = g → ∀ (a : α) (b : β a), f a b = g a b
-- Batteries.Data.String.Lemmas
String.all_eq : ∀ (s : String) (p : Char → Bool), String.Legacy.all s p = s.toList.all p
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Submodule.toSubalgebra_toSubmodule : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : Submodule R A)
  (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p),
  Subalgebra.toSubmodule (p.toSubalgebra h_one h_mul) = p
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_eq`. -/
setOf_gauge_lt_eq : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Absorbent ℝ s → ∀ (a : ℝ), {x | gauge s x < a} = ⋃ r ∈ Set.Ioo 0 a, r • s
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.restrict_compl_sigmaFiniteSet : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ],
  μ.restrict μ.sigmaFiniteSetᶜ = ⊤ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ
-- Mathlib.GroupTheory.QuotientGroup.Basic
_private.Mathlib.GroupTheory.QuotientGroup.Basic.0.QuotientGroup.termQ : Lean.ParserDescr
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_subset_coe : ∀ {x y : ZFSet.{u}}, ↑x ⊆ ↑y ↔ x ⊆ y
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_le_minKey?_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k km kme : α} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ (hkme : Std.Internal.List.minKey? (Std.Internal.List.eraseKey k l) = some kme),
      (Std.Internal.List.minKey? l).get ⋯ = km → (compare km kme).isLE = true
-- Mathlib.Data.Set.Basic
Set.mem_sep : ∀ {α : Type u} {s : Set α} {p : α → Prop} {x : α}, x ∈ s → p x → x ∈ {x | x ∈ s ∧ p x}
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_sup : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s t : Subsemiring R)
  (f : R →+* S), Subsemiring.map f (s ⊔ t) = Subsemiring.map f s ⊔ Subsemiring.map f t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_addY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P Q : Fin 3 → R), (W'.map f).addY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addY P Q)
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.pos_mono : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → ∀ ⦃t : Set α⦄, 0 < μ t → 0 < ν t
-- Mathlib.Tactic.FunProp.FunctionData
/-- Is `f` a constant function?  -/
Mathlib.Meta.FunProp.FunctionData.isConstantFun : Mathlib.Meta.FunProp.FunctionData → Bool
-- Mathlib.Topology.Order.Real
EReal.instT2Space : T2Space EReal
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (self : W₁.FunctorialFactorizationData W₂),
  CategoryTheory.CategoryStruct.comp self.i self.p = CategoryTheory.Arrow.leftToRight
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `nnnorm_le_nnnorm_add_nnnorm_sub`. -/
nnnorm_le_insert : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊
-- Lean.Elab.DeprecatedArg
/-- State: `declName → (oldArg → entry)`  -/
Lean.Elab.DeprecatedArgState : Type
-- Init.Data.Dyadic.Basic
Dyadic.of_ne_zero : ∀ {n k : ℤ} {hn : n % 2 = 1}, Dyadic.ofOdd n k hn ≠ 0
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.instIsDominantToImageOfQuasiCompact : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.IsDominant (AlgebraicGeometry.Scheme.Hom.toImage f)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.ext : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {f g : ContIntertwiningMap π₁ π₂},
  f.toContinuousLinearMap = g.toContinuousLinearMap → f = g
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.hcongr_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D}, F = G → ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
-- Lean.Elab.Tactic.Try
/-- Erases `sorry` tactics from `s`  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.filterSorry : Array (Lean.TSyntax `tactic) → Array (Lean.TSyntax `tactic)
-- Mathlib.Computability.Ackermann
Nat.Partrec.Code.eval_pappAck_step_succ : ∀ (c : Nat.Partrec.Code) (n : ℕ),
  (Nat.Partrec.Code.pappAck.step c).eval (n + 1) = ((Nat.Partrec.Code.pappAck.step c).eval n).bind c.eval
-- Mathlib.Order.CompactlyGenerated.Basic
/-- A compactness property for a complete lattice is that any subset has a finite subset with the
same `sSup`.  -/
CompleteLattice.IsSupFiniteCompact : (α : Type u_2) → [CompleteLattice α] → Prop
-- Mathlib.Algebra.Ring.Periodic
/-- **Alias** of the reverse direction of `Function.periodic_iterate_iff`.

---

The iterates `a`, `f a`, `f^[2] a` etc form a periodic sequence with period `n`
iff `a` is a periodic point for `f`.  -/
Function.IsPeriodicPt.periodic_iterate : ∀ {α : Type u_1} {f : α → α} {n : ℕ} {a : α}, Function.IsPeriodicPt f n a → Function.Periodic (fun x => f^[x] a) n
-- Mathlib.Algebra.Group.Basic
sub_eq_sub_iff_comm : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b c : α) {d : α}, a - b = c - d ↔ b - a = d - c
-- Lean.Elab.DocString
/-- Environment extension for docstring directives  -/
Lean.Doc.docDirectiveExt : Lean.SimpleScopedEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap (Array Lean.Name))
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShapeSymmetry.σ_ε₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  {c₁₂ : ComplexShape I₁₂} {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₂ c₁ c₁₂}
  [self : TotalComplexShapeSymmetry c₁ c₂ c₁₂] {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : I₂),
      TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) =
        c₂.ε₂ c₁ c₁₂ (i₂, i₁) * TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁' i₂
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_indicator_iff : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [inst_1 : Zero β] {s : Set α},
  MeasurableSet s → (AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s))
-- Mathlib.Logic.Function.Basic
/-- A binary injective function is injective when only the right argument varies.  -/
Function.Injective2.right : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
  Function.Injective2 f → ∀ (a : α), Function.Injective (f a)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Measurable.le : ∀ {β : Type u_2} {α : Type u_7} {m m0 : MeasurableSpace α} {x : MeasurableSpace β},
  m ≤ m0 → ∀ {f : α → β}, Measurable f → Measurable f
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Kˣ),
  ↑(v.valuationOfNeZero x) = (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- We construct a cover from another, by providing the needed fields and showing that the
provided fields are isomorphic with the original cover.  -/
AlgebraicGeometry.Scheme.Cover.copy : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [P.RespectsIso] →
    {X : AlgebraicGeometry.Scheme} →
      (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
        (J : Type u_1) →
          (obj : J → AlgebraicGeometry.Scheme) →
            (map : (i : J) → obj i ⟶ X) →
              (e₁ : J ≃ 𝒰.I₀) →
                (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)) →
                  (∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) →
                    AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X
-- Init.Data.BitVec.Lemmas
BitVec.cpop_zero : ∀ {w : ℕ}, (0#w).cpop = 0#w
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.congr_simp : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] [inst_8 : TopologicalSpace A] [inst_9 : IsSemitopologicalSemiring A]
  [inst_10 : ContinuousConstSMul R A] [inst_11 : ContinuousStar A] (x x_1 : A),
  x = x_1 → NonUnitalStarAlgebra.elemental R x = NonUnitalStarAlgebra.elemental R x_1
-- Mathlib.AlgebraicGeometry.Scheme
/-- The counit (`SpecΓIdentity.inv.op`) of the adjunction `Γ ⊣ Spec` as a natural isomorphism.
This is almost never needed in practical use cases. Use `ΓSpecIso` instead.
 -/
AlgebraicGeometry.Scheme.SpecΓIdentity : AlgebraicGeometry.Scheme.Spec.rightOp.comp AlgebraicGeometry.Scheme.Γ ≅ CategoryTheory.Functor.id CommRingCat
-- Mathlib.Order.Hom.Basic
OrderIso.toEquiv_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), e.symm.toEquiv = e.symm
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {a : α}, t.contains a = true → t.getKey? a = some (t.getKey! a)
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.lt_iff_le_carrier_ne : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {L₁ L₂ : IntermediateField.Lifts F E K},
  L₁ < L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier ≠ L₂.carrier
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_set_le_iff : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_5} {s : Set ι} {f : ι → α} {a : α},
  s.Nonempty → BddAbove (f '' s) → (⨆ i, f ↑i ≤ a ↔ ∀ i ∈ s, f i ≤ a)
-- Mathlib.NumberTheory.NumberField.CMField
/-- The complex conjugation as an isomorphism of the units of `K`.  -/
NumberField.IsCMField.unitsComplexConj : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : CharZero K] →
      [NumberField.IsCMField K] →
        [Algebra.IsIntegral ℚ K] → (NumberField.RingOfIntegers K)ˣ ≃* (NumberField.RingOfIntegers K)ˣ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_insertIfNew_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insertIfNew k v).size ≤ t.size + 1