mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.coeMonoidHom_apply : ∀ {α : Type u_1} [inst : MulOneClass α] (a : α), WithZero.coeMonoidHom a = ↑a
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.elabLevel : Lean.Syntax → Lean.Elab.TermElabM Lean.Level
-- Mathlib.Order.Fin.Tuple
Fin.snocOrderIso_symm_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)] (f : (i : Fin (n + 1)) → α i),
  (RelIso.symm (Fin.snocOrderIso α)) f = (f (Fin.last n), Fin.init f)
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_iff_norm' : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r ↔ ‖a - b‖ < r
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
dist_iteratedFDerivWithin_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (s : Set E) (x : E) (g : E → F) (t : Set E) (y : E),
  dist (iteratedFDerivWithin 𝕜 0 f s x) (iteratedFDerivWithin 𝕜 0 g t y) = dist (f x) (g y)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.α_sq : ∀ {q : ℕ}, LucasLehmer.X.α ^ 2 = 3
-- Mathlib.RingTheory.DualNumber
DualNumber.ideal_trichotomy : ∀ {K : Type u_2} [inst : DivisionRing K] (I : Ideal (DualNumber K)), I = ⊥ ∨ I = Ideal.span {DualNumber.eps} ∨ I = ⊤
-- Init.Data.Int.Order
Int.neg_le_sub_left_of_le_add : ∀ {a b c : ℤ}, c ≤ a + b → -a ≤ b - c
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The property that two morphisms become equal in the localized category.  -/
CategoryTheory.AreEqualizedByLocalization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → {X Y : C} → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ'_two : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ' 2 = 1
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.InducingFunctorData.rightUnitor_eq : ∀ {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.MonoidalCategoryStruct D]
  {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) (X : D),
  F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom =
    (((self.μIso X (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).symm ≪≫
          CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (F.obj X)) self.εIso.symm) ≪≫
        CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom
-- Mathlib.Data.SetLike.Basic
SetLike.mem_of_subsingleton : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] [Subsingleton B] (S : A) [h : Nonempty ↥S] {b : B}, b ∈ S
-- Mathlib.GroupTheory.OrderOfElement
zmultiples_abs : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (g : G),
  AddSubgroup.zmultiples |g| = AddSubgroup.zmultiples g
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatchAt_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt p pos pos' ↔ ∃ (h : pos ≠ s.endPos), pos' = pos.next h ∧ p (pos.get h)
-- Lean.ReducibilityAttrs
Lean.instReprReducibilityStatus.repr : Lean.ReducibilityStatus → ℕ → Std.Format
-- Aesop.Rule.Basic
Aesop.Rule.instHashable : {α : Type} → Hashable (Aesop.Rule α)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- A regular conditional probability distribution of the point at time `a + 1` given the
trajectory up to time `a` corresponds to the kernel `κ a`.  -/
ProbabilityTheory.Kernel.condDistrib_trajMeasure : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)}
  [inst_2 : MeasureTheory.IsProbabilityMeasure μ₀] {a : ℕ} [inst_3 : StandardBorelSpace (X (a + 1))]
  [inst_4 : Nonempty (X (a + 1))],
  ⇑(ProbabilityTheory.condDistrib (fun x => x (a + 1)) (Preorder.frestrictLe a)
        (ProbabilityTheory.Kernel.trajMeasure μ₀
          κ)) =ᵐ[MeasureTheory.Measure.map (Preorder.frestrictLe a) (ProbabilityTheory.Kernel.trajMeasure μ₀ κ)]
    ⇑(κ a)
-- Std.Data.DHashMap.IteratorLemmas
_private.Std.Data.DHashMap.IteratorLemmas.0.Std.DHashMap.keys_inner : ∀ {α : Type u} {β : α → Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α β}, m.inner.keys = m.keys
-- Init.Data.Rat.Lemmas
Rat.floor_monotone : ∀ {a b : ℚ}, a ≤ b → a.floor ≤ b.floor
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
List.stronglyMeasurable_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : Monoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  {m : MeasurableSpace α} (l : List (α → M)),
  (∀ f ∈ l, MeasureTheory.StronglyMeasurable f) → MeasureTheory.StronglyMeasurable l.prod
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of `p` is less than `1` if `p` is prime.

See also `padicNorm.padicNorm_p_lt_one` for a version assuming `1 < p`.  -/
padicNorm.padicNorm_p_lt_one_of_prime : ∀ {p : ℕ} [Fact (Nat.Prime p)], padicNorm p ↑p < 1
-- Mathlib.Order.Cover
CovBy.exists_set_insert : ∀ {α : Type u_1} {s t : Set α}, s ⋖ t → ∃ a ∉ s, insert a s = t
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.mk.injEq : ∀ (carrier : Type u) [str : AddGroup carrier] (carrier_1 : Type u) (str_1 : AddGroup carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_piecewise_const' : ∀ {Ω : Type u_1} {s : Set Ω} [inst : DecidablePred fun x => x ∈ s] {ι' : Type u_4} {α : Type u_5}
  [inst_1 : AddCommGroup α] [inst_2 : Nonempty ι'] {i j : ι'} {f : ι' → Ω → α},
  MeasureTheory.stoppedValue f (s.piecewise (fun x => ↑i) fun x => ↑j) = s.indicator (f i) + sᶜ.indicator (f j)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedStats : Inhabited Lean.Meta.Simp.Stats
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {hm : m ≤ m0}
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤),
  MeasurableSet t →
    μ t ≠ ⊤ →
      ∫⁻ (a : α) in t, ↑‖↑↑↑((MeasureTheory.condExpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ ≤
        μ (s ∩ t)
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_of_injective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2}
  {J : Type u_3} (X : I → C) (ι : J → I),
  Function.Injective ι →
    ∀ (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ ι))
      (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁)
      [CategoryTheory.Limits.HasCoproduct fun k => X ↑k],
      CategoryTheory.Mono (CategoryTheory.Limits.Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.pos : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], Order.IsSuccLimit a → 0 < a
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfLocalizations.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) (k : S.LocalizationMap P),
  f.mulEquivOfLocalizations k =
    { toFun := ⇑(f.lift ⋯), invFun := ⇑(k.lift ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatEraShort : Std.Time.DateFormatSymbols → Std.Time.Year.Era → String
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instPartialOrder.eq_1 : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  ClosedAddSubgroup.instPartialOrder G = PartialOrder.ofSetLike (ClosedAddSubgroup G) G
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.loopless_iff_forall_isCircuit : ∀ {α : Type u_1} {M : Matroid α}, M.Loopless ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.unitToPushforwardObjUnit_val_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {X : Cᵒᵖ}
  (a : ↑(S.obj.obj X)),
  (CategoryTheory.ConcreteCategory.hom ((SheafOfModules.unitToPushforwardObjUnit φ).val.app X)) a =
    (CategoryTheory.ConcreteCategory.hom (φ.hom.app X)) a
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_fixedPoints : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] {a : α},
  a ∈ AddAction.fixedPoints M α ↔ ∀ (m : M), m +ᵥ a = a
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
CategoryTheory.Functor.instFaithfulPlusMapHomotopyCategoryPlusOfFull : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] [F.Full] [F.Faithful],
  F.mapHomotopyCategoryPlus.Faithful
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
Polynomial.isOpen_image_comap_of_monic : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R),
  g.Monic → IsOpen (PrimeSpectrum.comap Polynomial.C '' (PrimeSpectrum.zeroLocus {g} \ PrimeSpectrum.zeroLocus {f}))
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type}
  [inst_1 : CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ),
  CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso A K =
    CategoryTheory.Iso.refl
      (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K)
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.toPresheafedSpace_obj_op : ∀ (R : CommRingCat),
  AlgebraicGeometry.Spec.toPresheafedSpace.obj (Opposite.op R) =
    (AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edgeFinset_sup_edge : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj]
  [inst_2 : Fintype ↑(G ⊔ SimpleGraph.edge s t).edgeSet] (hn : ¬G.Adj s t),
  s ≠ t → (G ⊔ SimpleGraph.edge s t).edgeFinset = Finset.cons s(s, t) G.edgeFinset ⋯
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_one : ∀ (n : ℕ), SimplexCategory.δ₀Iter 1 ⋯ = SimplexCategory.δ 0
-- Init.Data.Vector.Lemmas
Vector.getElem_of_append : ∀ {α : Type u_1} {n m k : ℕ} {a : α} {xs : Vector α n} {xs₁ : Vector α m} {xs₂ : Vector α k} (w : m + 1 + k = n),
  xs = Vector.cast w (xs₁.push a ++ xs₂) → xs[m] = a
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- Write the iterated derivative as the composition of a continuous linear equiv and the iterated
Fréchet derivative  -/
iteratedDerivWithin_eq_equiv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜},
  iteratedDerivWithin n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDerivWithin 𝕜 n f s
-- Init.Data.Rat.Basic
Rat.instDecidableLt : (a b : ℚ) → Decidable (a < b)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_smul : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : NormedRing 𝕜] [inst_5 : Module 𝕜 E] [inst_6 : IsBoundedSMul 𝕜 E] [inst_7 : DistribSMul 𝕜 F]
  (T : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      (∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) →
        ∀ (c : 𝕜) (f : ↥(α →₁ₛ[μ] E)),
          MeasureTheory.L1.SimpleFunc.setToL1S T (c • f) = c • MeasureTheory.L1.SimpleFunc.setToL1S T f
-- Init.Core
Std.Asymm.mk : ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a b : α), r a b → ¬r b a) → Std.Asymm r
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_pow_of_pell_lem : ∀ {a y k : ℕ}, y ≠ 0 → k ≠ 0 → y ^ k < a → ↑(y ^ k) < 2 * ↑a * ↑y - ↑y * ↑y - 1
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.inv : ∀ {α : Type u_2} [inst : Inv α] {f : Filter α}, f.NeBot → f⁻¹.NeBot
-- Mathlib.Tactic.Ring.Common
/-- A coefficient `value`, holding the data that `ring` uses to represent rational coefficients.
In this case these happen to always be natural numbers.  -/
Mathlib.Tactic.Ring.Common.ExProdNat.const : {e : Q(ℕ)} → Mathlib.Tactic.Ring.Common.btℕ e → Mathlib.Tactic.Ring.Common.ExProdNat e
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_infinite : ∀ {n : ℕ} {ι : Type u_3} (V : ι → Type u_4) [Infinite ι] (f : (i : ι) → V i),
  ¬(SimpleGraph.completeMultipartiteGraph V).CliqueFree n
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.mkIso_hom_f : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj)
  (hf :
    CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) =
      CategoryTheory.CategoryStruct.comp f.hom Y.d),
  (CategoryTheory.DifferentialObject.mkIso f hf).hom.f = f.hom
-- Mathlib.Condensed.Light.InternallyProjective
LightCondensed.ihom_map_val_app : ∀ (R : Type u) [inst : CommRing R] (A B P : LightCondMod R) (S : LightProfinite) (e : A ⟶ B)
  (x : ↑((P ⟹ A).obj.obj (Opposite.op S))),
  (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom P).map e).hom.app (Opposite.op S))) x =
    (LightCondensed.ihomPoints R P B S).symm
      (CategoryTheory.CategoryStruct.comp ((LightCondensed.ihomPoints R P A S) x) e)
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot : ∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension S K L] (M : Type u_1) [inst_4 : Field M] [inst_5 : Algebra K M],
  (∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) →
    Nonempty (L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.ker_dualMap_eq_dualCoannihilator_range : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  f.dualMap.ker = (Module.Dual.eval R M' ∘ₗ f).range.dualCoannihilator
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.integrable_comp_mul_right_iff : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] (g : ℝ → F) {R : ℝ},
  R ≠ 0 →
    (MeasureTheory.Integrable (fun x => g (x * R)) MeasureTheory.volume ↔
      MeasureTheory.Integrable g MeasureTheory.volume)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.IsOver.symm : ∀ {X Y S : AlgebraicGeometry.Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {f : X.PartialIso Y},
  AlgebraicGeometry.Scheme.PartialIso.IsOver sX sY f → AlgebraicGeometry.Scheme.PartialIso.IsOver sY sX f.symm
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.map_ωSup : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {f : α → β}
  (hf : OmegaCompletePartialOrder.ωScottContinuous f) (c : OmegaCompletePartialOrder.Chain α),
  f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map { toFun := f, monotone' := ⋯ })
-- Mathlib.Algebra.MvPolynomial.Supported
AlgEquiv.ofInjective.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective ⇑f),
  AlgEquiv.ofInjective f hf = AlgEquiv.ofInjective f hf
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Nat.UnifyZeroOrSuccResult.zero.sizeOf_spec : ∀ {n : Q(ℕ)} (pf : «$n» =Q 0), sizeOf (Mathlib.Meta.Nat.UnifyZeroOrSuccResult.zero pf) = 1 + sizeOf pf
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.stdSymm : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, Std.Symm (MeasureTheory.AEDisjoint μ)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_map_erase : ∀ {α : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq α] (f : α → M) {a : α} {l : List α},
  a ∈ l → f a + (List.map f (l.erase a)).sum = (List.map f l).sum
-- Lean.Server.References
/-- Document version for which these references have been collected.  -/
Lean.Server.TransientWorkerILean.version : Lean.Server.TransientWorkerILean → ℕ
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instAddSemigroup : {d : ℤ} → AddSemigroup (ℤ√d)
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.π_map_assoc : ∀ {k : Type u} {G H : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ)
  {Z : TopModuleCat k} (h : continuousCohomology n Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ContinuousCohomology.π X n)
      (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map φ f n) h) =
    CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cocyclesMap φ f n)
      (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.π Y n) h)
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.subseq_mem : ∀ {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α},
  (∀ (n : ℕ), V n ∈ uniformity α) →
    ∀ {u : ℕ → α}, CauchySeq u → ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_eq_get_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : a ∈ t}, t.getKey a h = (t.getKey? a).get ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.starIsoTerminal_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.WithTerminal.starIsoTerminal.hom =
    CategoryTheory.Limits.terminalIsTerminal.from CategoryTheory.WithTerminal.star
-- Mathlib.Data.Sum.Order
Sum.not_inr_lt_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a : α} {b : β}, ¬Sum.inr b < Sum.inl a
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.IsDominant.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g)], AlgebraicGeometry.IsDominant g
-- Mathlib.Algebra.Order.Ring.StandardPart
_private.Mathlib.Algebra.Order.Ring.StandardPart.0.ArchimedeanClass.FiniteResidueField.mul_le_mul_of_nonneg_left' : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x y z : ArchimedeanClass.FiniteResidueField K}, x ≤ y → 0 ≤ z → z * x ≤ z * y
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_neg_vadd_inter : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ ((-c +ᵥ s) ∩ t) = μ (s ∩ (c +ᵥ t))
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `LinearMap.IsIdempotentElem.eq_projection`.

---

An idempotent linear operator is equal to the linear projection onto
its range along its kernel.  -/
LinearMap.IsIdempotentElem.eq_isCompl_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T : E →ₗ[R] E}
  (hT : IsIdempotentElem T), T = T.range.projection T.ker ⋯
-- Mathlib.GroupTheory.CoprodI
Monoid.toMulOneClass.hcongr_2 : ∀ (M M' : Type u),
  M = M' → ∀ (self : Monoid M) (self' : Monoid M'), self ≍ self' → self.toMulOneClass ≍ self'.toMulOneClass
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.map_write : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (b : Γ)
  (T : Turing.Tape Γ), Turing.Tape.map f (Turing.Tape.write b T) = Turing.Tape.write (f.f b) (Turing.Tape.map f T)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The construction `precompose` respects functor identities.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor C B) →
                (X : Type u₄) →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj
                        (CategoryTheory.Functor.id X) ≅
                      CategoryTheory.Functor.id (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
-- Mathlib.Data.Complex.Basic
Complex.inv_def : ∀ (z : ℂ), z⁻¹ = (starRingEnd ℂ) z * ↑(Complex.normSq z)⁻¹
-- Mathlib.Algebra.Group.PUnit
PUnit.instDiv_mathlib.eq_1 : PUnit.instDiv_mathlib = { div := fun x x_1 => PUnit.unit }
-- Mathlib.RingTheory.Congruence.Basic
/-- The infimum of a set of congruence relations on a given type with multiplication and
addition.  -/
RingCon.instInfSet : {R : Type u_3} → [inst : Add R] → [inst_1 : Mul R] → InfSet (RingCon R)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.condition : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) [inst_2 : CategoryTheory.Limits.HasCoend F] {i j : J}
  (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app i) (CategoryTheory.Limits.coend.ι F i) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (CategoryTheory.Limits.coend.ι F j)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.exists_blsub_cof : ∀ (o : Ordinal.{u}), ∃ f, o.cof.ord.blsub f = o
-- Mathlib.Analysis.MeanInequalities
/-- **Minkowski inequality**: the `L_p` seminorm of the infinite sum of two vectors is less than or
equal to the infinite sum of the `L_p`-seminorms of the summands, if these infinite sums both
exist. A version for `NNReal`-valued functions. For an alternative version, convenient if the
infinite sums are not already expressed as `p`-th powers, see `Lp_add_le_tsum_of_nonneg`.  -/
NNReal.Lp_add_le_hasSum : ∀ {ι : Type u} {f g : ι → NNReal} {A B : NNReal} {p : ℝ},
  1 ≤ p →
    HasSum (fun i => f i ^ p) (A ^ p) →
      HasSum (fun i => g i ^ p) (B ^ p) → ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)
-- Lean.Elab.Do.Basic
/-- The code is alive. (Or it is dead, but we failed to prove it so.)   -/
Lean.Elab.Do.CodeLiveness.alive : Lean.Elab.Do.CodeLiveness