mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.OmegaLimit
/-- An element `y` is in the ω-limit of `x` w.r.t. `f` if the forward
images of `x` frequently (w.r.t. `f`) falls within an arbitrary neighbourhood of `y`.  -/
mem_omegaLimit_singleton_iff_mapClusterPt : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (x : α)
  (y : β), y ∈ omegaLimit f ϕ {x} ↔ MapClusterPt y f fun t => ϕ t x
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairComp_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {J : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} J]
  {K : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} K] (Fₗ : CategoryTheory.Functor C E)
  (Fᵣ : CategoryTheory.Functor D E') (Gₗ : CategoryTheory.Functor E J) (Gᵣ : CategoryTheory.Functor E' K) (c : C),
  (CategoryTheory.Join.mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (CategoryTheory.Join.left c) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (Gₗ.obj (Fₗ.obj c)))
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.invertibleEquivInvertibleFst_symm_apply_invOf : ∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Semiring R] [inst_2 : Module Rᵐᵒᵖ M] [inst_3 : Module R M]
  [inst_4 : SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (x_1 : Invertible x.fst),
  ⅟x = (⅟x.fst, -(MulOpposite.op ⅟x.fst • ⅟x.fst • x.snd))
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_inj_right : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → c ≤ a → a - b = a - c → b = c
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCall.mk.inj : ∀ {«to» : Lean.Lsp.CallHierarchyItem} {fromRanges : Array Lean.Lsp.Range} {to_1 : Lean.Lsp.CallHierarchyItem}
  {fromRanges_1 : Array Lean.Lsp.Range},
  { «to» := «to», fromRanges := fromRanges } = { «to» := to_1, fromRanges := fromRanges_1 } →
    «to» = to_1 ∧ fromRanges = fromRanges_1
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- Given `F : J ⥤ Type w₀`, and `c : F.CoconeTypes` a cocone that is a colimit,
this is the equivalence `F.ColimitType ≃ c.pt`.  -/
CategoryTheory.Functor.CoconeTypes.IsColimit.equiv : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} → {c : F.CoconeTypes} → c.IsColimit → F.ColimitType ≃ c.pt
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_singleton_mul : ∀ {R : Type u} [inst : CommSemiring R] (f g : R),
  PrimeSpectrum.zeroLocus {f * g} = PrimeSpectrum.zeroLocus {f} ∪ PrimeSpectrum.zeroLocus {g}
-- Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances
NumberField.LiesOver.instContinuousSMulCompletion : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L} [inst_3 : w.LiesOver v],
  ContinuousSMul v.Completion w.Completion
-- Std.Sync.Channel
/-- This function is a no-op and just a convenient way to expose the synchronous API of the channel.
 -/
Std.Channel.sync : {α : Type} → Std.Channel α → Std.Channel.Sync α
-- Mathlib.Order.Heyting.Hom
CoheytingHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] (f : CoheytingHom α β),
  (CoheytingHom.id β).comp f = f
-- Lean.Compiler.LCNF.Basic
/-- We set this flag to false during LCNF conversion if the Lean function
associated with this function was tagged as partial or unsafe. This
information affects how static analyzers treat function applications
of this kind. See `DefinitionSafety`.
`partial` and `unsafe` functions may not be terminating, but Lean
functions terminate, and some static analyzers exploit this
fact. So, we use the following semantics. Suppose we have a (large) natural
number `C`. We consider a nondeterministic model for computation of Lean expressions as
follows:
Each call to a partial/unsafe function uses up one "recursion token".
Prior to consuming `C` recursion tokens all partial functions must be called
as normal. Once the model has used up `C` recursion tokens, a subsequent call to
a partial function has the following nondeterministic options: it can either call
the function again, or return any value of the target type (even a noncomputable one).
Larger values of `C` yield less nondeterminism in the model, but even the intersection of
all choices of `C` yields nondeterminism where `def loop : A := loop` returns any value of type `A`.
The compiler fixes a choice for `C`. This is a fixed constant greater than 2^2^64,
which is allowed to be compiler and architecture dependent, and promises that it will
produce an execution consistent with every possible nondeterministic outcome of the `C`-model.
In the event that different nondeterministic executions disagree, the compiler is required to
exhaust resources or output a looping computation.
 -/
Lean.Compiler.LCNF.Signature.safe : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Signature pu → Bool
-- Mathlib.MeasureTheory.Measure.OpenPos
Metric.measure_eball_pos : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
  [μ.IsOpenPosMeasure] (x : X) {r : ENNReal}, r ≠ 0 → 0 < μ (Metric.eball x r)
-- Mathlib.CategoryTheory.Limits.Fubini
/-- For each map, a map of cones.  -/
CategoryTheory.Limits.DiagramOfCones.map : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              (self : CategoryTheory.Limits.DiagramOfCones F) →
                {j j' : J} →
                  (f : j ⟶ j') → (CategoryTheory.Limits.Cone.postcompose (F.map f)).obj (self.obj j) ⟶ self.obj j'
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM_apply : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  [inst_8 : DecidableEq ι] (f : F [⋀^ι]→L[𝕜] G) (g : E →L[𝕜] F),
  (ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM G g) f = f.fderivCompContinuousLinearMap g
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.j_of_isShortNF_of_char_three : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) [inst_1 : W.IsElliptic] [W.IsShortNF] [CharP F 3], W.j = 0
-- Mathlib.Data.Finset.Powerset
/-- A version of `Finset.decidableExistsOfDecidableSSubsets` with a non-dependent `p`.
Typeclass inference cannot find `hu` here, so this is not an instance.  -/
Finset.decidableExistsOfDecidableSSubsets' : {α : Type u_1} →
  [DecidableEq α] →
    {s : Finset α} →
      {p : Finset α → Prop} → ((t : Finset α) → t ⊂ s → Decidable (p t)) → Decidable (∃ t, ∃ (_ : t ⊂ s), p t)
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piSplitAt_symm_apply : ∀ {ι : Type u_7} [inst : DecidableEq ι] (i : ι) (Y : ι → Type u_8) [inst_1 : (j : ι) → TopologicalSpace (Y j)]
  (f : Y i × ((j : { j // j ≠ i }) → Y ↑j)) (j : ι),
  (Homeomorph.piSplitAt i Y).symm f j = if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩
-- Mathlib.Topology.Inseparable
SeparationQuotient.continuous_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous SeparationQuotient.mk
-- Lean.Meta.Tactic.Split
Lean.Meta.Split.isDiscrGenException : Lean.Exception → Bool
-- Mathlib.Data.Fin.Rev
Fin.rev_injective : ∀ {n : ℕ}, Function.Injective Fin.rev
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.lc.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  (e : ι → M) (l : ι →₀ R), Module.DualBases.lc e l = l.sum fun i a => a • e i
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.composableArrows₃Functor_map : ∀ (C : Type u_1) {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (i j : ι) [inst_2 : CategoryTheory.CategoryWithHomology C] {K L : HomologicalComplex C c}
  (φ : K ⟶ L),
  (HomologicalComplex.HomologySequence.composableArrows₃Functor C i j).map φ =
    CategoryTheory.ComposableArrows.homMk₃ (HomologicalComplex.homologyMap φ i) (HomologicalComplex.opcyclesMap φ i)
      (HomologicalComplex.cyclesMap φ j) (HomologicalComplex.homologyMap φ j) ⋯ ⋯ ⋯
-- Mathlib.NumberTheory.Multiplicity
Int.two_pow_two_pow_add_two_pow_two_pow : ∀ {x y : ℤ}, ¬2 ∣ x → 4 ∣ x - y → ∀ (i : ℕ), emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1
-- Mathlib.Topology.Neighborhoods
IsClosed.mem_of_tendsto : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} [b.NeBot],
  IsClosed s → Filter.Tendsto f b (nhds x) → (∀ᶠ (x : α) in b, f x ∈ s) → x ∈ s
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_le_ker_comp : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
  {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃),
  f.ker ≤ (g ∘ₛₗ f).ker
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_sin : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ], IntervalIntegrable Real.sin μ a b
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_or_elim_r : ∀ {σs : List (Type u)} {P Q R T : Std.Do.SPred σs}, (P ∧ Q ⊢ₛ T) → (P ∧ R ⊢ₛ T) → P ∧ (Q ∨ R) ⊢ₛ T
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_toInt : ∀ (x : ISize), ISize.ofIntLE x.toInt ⋯ ⋯ = x
-- Mathlib.Data.Set.Prod
Equiv.sumPiEquivProdPi_symm_preimage_univ_pi : ∀ {ι : Type u_1} {ι' : Type u_2} (π : ι ⊕ ι' → Type u_4) (t : (i : ι ⊕ ι') → Set (π i)),
  ⇑(Equiv.sumPiEquivProdPi π).symm ⁻¹' Set.univ.pi t =
    (Set.univ.pi fun i => t (Sum.inl i)) ×ˢ Set.univ.pi fun i => t (Sum.inr i)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map.unique : ∀ {α : Type u} {β : Type v} {f : α → β} (g : FreeGroup α →* FreeGroup β),
  (∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)) → ∀ {x : FreeGroup α}, g x = (FreeGroup.map f) x
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.coe_mk_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target),
  ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.symm = ↑e.symm
-- Mathlib.CategoryTheory.Sigma.Basic
/-- (Implementation). An auxiliary definition to build the functor `desc`.  -/
CategoryTheory.Sigma.descMap : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (F : (i : I) → CategoryTheory.Functor (C i) D) →
            (X Y : (i : I) × C i) → (X ⟶ Y) → ((F X.fst).obj X.snd ⟶ (F Y.fst).obj Y.snd)
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.edist_toL1_zero : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β) (hf : MeasureTheory.Integrable f μ),
  edist (MeasureTheory.Integrable.toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ
-- Mathlib.Algebra.Group.Units.Equiv
toUnits.eq_1 : ∀ {G : Type u_5} [inst : Group G],
  toUnits =
    { toFun := fun x => { val := x, inv := x⁻¹, val_inv := ⋯, inv_val := ⋯ }, invFun := fun x => ↑x, left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ratCast_mul : ∀ {x : ℝ}, Irrational x → ∀ {q : ℚ}, q ≠ 0 → Irrational (↑q * x)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_inf : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C₁ C₂ : ConvexCone R M} {x : M}, x ∈ C₁ ⊓ C₂ ↔ x ∈ C₁ ∧ x ∈ C₂
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- Characterization of `a / b = c` assuming `b ≠ 0`.
See `div_eq_iff'` for a version assuming `c ≠ 0` instead.  -/
Ordinal.div_eq_iff : ∀ {a b c : Ordinal.{u_4}}, b ≠ 0 → (a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1))
-- Mathlib.Order.CompleteLattice.Basic
Equiv.iInf_congr : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : InfSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι'),
  (∀ (x : ι), g (e x) = f x) → ⨅ x, f x = ⨅ y, g y
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.map_id_obj : ∀ {X : TopCat} (x : ↑X)
  (U : TopologicalSpace.OpenNhds ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x)),
  (TopologicalSpace.OpenNhds.map (CategoryTheory.CategoryStruct.id X) x).obj U = U
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.zero_eq : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] (x : Submonoid A), 0 = Quotient.mk'' 0
-- Mathlib.GroupTheory.Congruence.Defs
/-- There is a Galois insertion of congruence relations on a type with a multiplication `M` into
binary relations on `M`.  -/
Con.gi : (M : Type u_1) → [inst : Mul M] → GaloisInsertion conGen DFunLike.coe
-- Mathlib.Topology.Connected.Basic
/-- A connected set is one that is nonempty and where there is no non-trivial open partition.  -/
IsConnected : {α : Type u} → [TopologicalSpace α] → Set α → Prop
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.shatters_shatterer : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α}, 𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instDiscreteTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [DiscreteTopology M], DiscreteTopology Mᵈᵃᵃ
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_sInf : ∀ {M : Type u_2} [inst : Add M] (S : Set (AddSubsemigroup Mᵃᵒᵖ)), (sInf S).unop = sInf (AddSubsemigroup.op ⁻¹' S)
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.instHasInjectiveDimensionLTHAddNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ)
  [CategoryTheory.HasInjectiveDimensionLT X n] (k : ℕ), CategoryTheory.HasInjectiveDimensionLT X (n + k)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_bot : ∀ {R : Type u} [inst : NonAssocSemiring R], ↑⊥ = Set.range Nat.cast
-- Mathlib.Algebra.Lie.Prod
LieAlgebra.Prod.bracket_apply : ∀ {L₁ : Type u_2} {L₂ : Type u_3} [inst : LieRing L₁] [inst_1 : LieRing L₂] (x y : L₁ × L₂),
  ⁅x, y⁆ = (⁅x.1, y.1⁆, ⁅x.2, y.2⁆)
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.disjWithin.eq_1 : ∀ (a b : ℝ),
  AbsolutelyContinuousOnInterval.disjWithin a b =
    {E |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ Set.uIcc a b ∧ (E.2 i).2 ∈ Set.uIcc a b) ∧
        (↑(Finset.range E.1)).PairwiseDisjoint fun i => Set.uIoc (E.2 i).1 (E.2 i).2}
-- Mathlib.LinearAlgebra.Pi
/-- A version of `Set.pi` for submodules. Given an index set `I` and a family of submodules
`p : (i : ι) → Submodule R (φ i)`, `pi I p` is the submodule of dependent functions
`f : (i : ι) → φ i` such that `f i` belongs to `p i` whenever `i ∈ I`.  -/
Submodule.pi : {R : Type u} →
  {ι : Type x} →
    [inst : Semiring R] →
      {φ : ι → Type u_1} →
        [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
          [inst_2 : (i : ι) → Module R (φ i)] → Set ι → ((i : ι) → Submodule R (φ i)) → Submodule R ((i : ι) → φ i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_image_Icc : Real.arcsin '' Set.Icc (-1) 1 = Set.Icc (-(Real.pi / 2)) (Real.pi / 2)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- This lemma is superseded by `uniformIntegrable_of` which only requires
`AEStronglyMeasurable`.  -/
MeasureTheory.uniformIntegrable_of' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [MeasureTheory.IsFiniteMeasure μ],
  1 ≤ p →
    p ≠ ⊤ →
      (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
        (∀ (ε : ℝ),
            0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) →
          MeasureTheory.UniformIntegrable f p μ
-- Std.Http.Data.Status
Std.Http.Status.networkAuthenticationRequired.sizeOf_spec : sizeOf Std.Http.Status.networkAuthenticationRequired = 1
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.instInfSet : {M : Type u_1} → [inst : Add M] → InfSet (AddSubsemigroup M)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `χ₀ U` and `χ m` form the appropriate pullback square.  -/
CategoryTheory.Subobject.Classifier.isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Subobject.Classifier C) {U X : C}
  (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (self.χ₀ U) (self.χ m) self.truth
-- Init.Grind.AC
Lean.Grind.AC.eq_erase_dup_rhs : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} {x : Std.IdempotentOp ctx.op}
  (lhs rhs rhs' : Lean.Grind.AC.Seq),
  rhs.eraseDup.beq' rhs' = true →
    Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs'
-- Std.Async.Basic
Std.Async.BaseAsync.instFunctor : Functor Std.Async.BaseAsync
-- Init.Data.Char.Lemmas
Char.notLTTotal : Std.Total fun x1 x2 => ¬x1 < x2
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  (t t_1 : Std.ExtTreeMap α β cmp), t = t_1 → t.maxKey! = t_1.maxKey!
-- Mathlib.Order.Heyting.Hom
CoheytingHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β]
  [inst_2 : CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Algebra.NeZero
not_neZero : ∀ {R : Type u_1} [inst : Zero R] {n : R}, ¬NeZero n ↔ n = 0
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_3),
  (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₃ =
    CategoryTheory.CategoryStruct.id ((X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁))
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).leadingCoeff = 1
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.toOneHom : {M : Type u_10} → {N : Type u_11} → [inst : MulOne M] → [inst_1 : MulOne N] → (M →* N) → OneHom M N
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_one_left_of_dvd : ∀ {R : Type u} [inst : CommRing R] {x y : R}, y ∣ x → IsCoprime (x + 1) y
-- Mathlib.RingTheory.Valuation.DiscreteValuativeRel
ValuativeRel.IsDiscrete.of_compatible_withZeroMulInt : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] (v : Valuation R (WithZero (Multiplicative ℤ)))
  [v.Compatible], ValuativeRel.IsDiscrete R
-- Mathlib.RingTheory.PowerSeries.Basic
Function.surjInv.eq_1 : ∀ {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) (b : β), Function.surjInv h b = Classical.choose ⋯
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.zeroLocus_biInf : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} {ι : Type u_1} (I : ι → Ideal ↑(X.presheaf.obj (Opposite.op U)))
  {t : Set ι}, t.Finite → X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.filter.go.eq_def : ∀ {α : Type u} {β : α → Type v} (f : (a : α) → β a → Bool) (acc a : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.filter.go✝ f acc a =
    match a with
    | Std.DHashMap.Internal.AssocList.nil => acc
    | Std.DHashMap.Internal.AssocList.cons k v t =>
      bif f k v then Std.DHashMap.Internal.AssocList.filter.go✝ f (Std.DHashMap.Internal.AssocList.cons k v acc) t
      else Std.DHashMap.Internal.AssocList.filter.go✝ f acc t
-- Mathlib.Algebra.Polynomial.Eval.Algebra
Polynomial.eval₂_comp' : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (x : S)
  (p q : Polynomial R),
  Polynomial.eval₂ (algebraMap R S) x (p.comp q) =
    Polynomial.eval₂ (algebraMap R S) (Polynomial.eval₂ (algebraMap R S) x q) p
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.allTR.loop.eq_1 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (h : 0 ≤ n), Nat.allTR.loop✝ n f 0 h = true
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Presieve.isSheaf_iff_of_nat_equiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P₁ : CategoryTheory.Functor Cᵒᵖ (Type w)} {P₂ : CategoryTheory.Functor Cᵒᵖ (Type w')}
  (e : ⦃X : C⦄ → P₁.obj (Opposite.op X) ≃ P₂.obj (Opposite.op X)),
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (Opposite.op Y)),
      e ((CategoryTheory.ConcreteCategory.hom (P₁.map f.op)) x) =
        (CategoryTheory.ConcreteCategory.hom (P₂.map f.op)) (e x)) →
    (CategoryTheory.Presieve.IsSheaf J P₁ ↔ CategoryTheory.Presieve.IsSheaf J P₂)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_units : ∀ {G : Type u_1} [inst : Monoid G] {y : Gˣ}, orderOf ↑y = orderOf y
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- A map from the coequalizer to `Y`  -/
CategoryTheory.IsSplitCoequalizer.rightSection : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f g : X ⟶ Y} → {Z : C} → {π : Y ⟶ Z} → CategoryTheory.IsSplitCoequalizer f g π → (Z ⟶ Y)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A sesquilinear form `B` is **positive semidefinite** if it is symmetric and nonnegative.  -/
LinearMap.IsPosSemidef : {R : Type u_1} →
  {M : Type u_5} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {I₁ : R →+* R} → [LE R] → (M →ₛₗ[I₁] M →ₗ[R] R) → Prop
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.tensorBimod_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z), (M.tensorBimod N).X = Bimod.TensorBimod.X M N
-- Init.Data.Vector.Lemmas
Vector.getElem_push : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α} {i : ℕ} (h : i < n + 1),
  (xs.push x)[i] = if h : i < n then xs[i] else x