mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- `y` has equal unoriented angles to `x` and `z` if and only if it has equal oriented angles
(bisects the angle) or `x` and `z` are on the same ray.  -/
Orientation.angle_eq_iff_oangle_eq_or_sameRay : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V},
  x ≠ 0 →
    z ≠ 0 →
      (InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.bicartSq : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), (S.prod T).BicartSq (⊤.prod T) (S.prod ⊤) (S.unionProd T)
-- Mathlib.LinearAlgebra.Dual.BaseChange
IsBaseChange.toDualBaseChange.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j)
  [inst_9 : Module.Free R V] [inst_10 : Module.Finite R V],
  ibc.toDualBaseChange = LinearEquiv.ofBijective (IsBaseChange.toDualBaseChangeAux✝ ibc) ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyGE?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGE? k = t₂.getKeyGE? k
-- Mathlib.Algebra.Group.Commute.Units
/-- If `a ^ n = 1`, `n ≠ 0`, then `a` is a unit.  -/
Units.ofPowEqOne : {M : Type u_1} → [inst : Monoid M] → (a : M) → (n : ℕ) → a ^ n = 1 → n ≠ 0 → Mˣ
-- Init.Data.List.Lemmas
List.getElem_replicate : ∀ {α : Type u_1} {a : α} {n i : ℕ} (h : i < (List.replicate n a).length), (List.replicate n a)[i] = a
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, a wedge for `F` is a type of cones (specifically
the type of multiforks for `multicospanIndexEnd F`):
the point of universal of these wedges shall be the end of `F`.  -/
CategoryTheory.Limits.Wedge : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C) → Type (max (max (max u v) u') v')
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α}, m.contains a = false → m.get? a = none
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_alter_eq_sub_one : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, k ∈ m → (f m[k]?).isNone = true → (m.alter k f).size = m.size - 1
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_enorm_rpow_iff : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε} {p : ENNReal},
  MeasureTheory.AEStronglyMeasurable f μ →
    p ≠ 0 → p ≠ ⊤ → (MeasureTheory.Integrable (fun x => ‖f x‖ₑ ^ p.toReal) μ ↔ MeasureTheory.MemLp f p μ)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.pure_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α] (a : α)
  (n : ℕ), n • NonemptyInterval.pure a = NonemptyInterval.pure (n • a)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddCommSemigroup.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddCommSemigroup M] [inst_2 : ContinuousAdd M],
  SeparationQuotient.instAddCommSemigroup = { toAddSemigroup := SeparationQuotient.instAddSemigroup, add_comm := ⋯ }
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.instSemilatticeSupOfAddLeftMonoOfAddRightMono : {X : Type u_1} →
  {R : Type u_2} →
    [inst : AddZeroClass R] →
      [inst_1 : SemilatticeSup R] → [AddLeftMono R] → [AddRightMono R] → SemilatticeSup (PseudoMetric X R)
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_eq_prod_embeddings_gen : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (F : Type u_6)
  [inst_3 : Field F] [inst_4 : Algebra R F] (pb : PowerBasis R S),
  (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits →
    IsSeparable R pb.gen → (algebraMap R F) ((Algebra.norm R) pb.gen) = ∏ σ, σ pb.gen
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l : Filter α), Filter.EventuallyConst f l = (Filter.map f l).Subsingleton
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The application of a morphism of `𝒪ₓ`-modules to sections.  -/
AlgebraicGeometry.Scheme.Modules.Hom.app : {X : AlgebraicGeometry.Scheme} →
  {M N : X.Modules} → (M ⟶ N) → (U : X.Opens) → M.presheaf.obj (Opposite.op U) ⟶ N.presheaf.obj (Opposite.op U)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, (t₁ ∩ t₂).getD k fallback = if k ∈ t₂ then t₁.getD k fallback else fallback
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_one : ∀ (L : List ℕ), Nat.ofDigits 1 L = L.sum
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.hom_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (H : CategoryTheory.AddGrp C)
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X], CategoryTheory.AddMonObj.zero.hom.hom = CategoryTheory.AddMonObj.zero
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.moduleFiber : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] →
              {ι : Type u_5} → (Z : VectorBundleCore R B F ι) → (x : B) → Module R (Z.Fiber x)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift.unique : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂}
  {g : TensorProduct R M N →ₛₗ[σ₁₂] P₂}, (∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f' x) y) → g = TensorProduct.lift f'
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
/-- The algebra norm `algNormOfAlgEquiv` is power-multiplicative.  -/
IsUltrametricDist.isPowMul_algNormOfAlgEquiv : ∀ {K : Type u_1} [inst : NormedField K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ : Gal(L/K)),
  IsPowMul ⇑(IsUltrametricDist.algNormOfAlgEquiv σ)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.contains_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.contains k = t₂.contains k
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instLinearHomologicalComplexQuotient : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} (V : Type u) [inst_1 : CategoryTheory.Category.{v, u} V]
  [inst_2 : CategoryTheory.Preadditive V] (c : ComplexShape ι) [inst_3 : CategoryTheory.Linear R V],
  CategoryTheory.Functor.Linear R (HomotopyCategory.quotient V c)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMin.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr_2 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
  Std.DTreeMap.Internal.Impl.insertMin k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr_2 =
    match Std.DTreeMap.Internal.Impl.insertMin k v l' ⋯ with
    | { impl := l'', balanced_impl := hl''₁, size_impl := hl''₂ } =>
      { impl := Std.DTreeMap.Internal.Impl.balanceL k' v' l'' r' ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
-- Std.Time.Time.Unit.Second
/-- `Ordinal` represents a bounded value for second, which ranges between 0 and 59 or 60. This accounts
for potential leap second.
 -/
Std.Time.Second.Ordinal : Bool → Type
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.isClopen_sphere`.

---

For any valuation `v` compatible with the valuative relation on `R`, the sphere of radius `r`
around zero `{x | v.restrict x = r}` is clopen in the valuative topology.  -/
IsValuativeTopology.isClopen_sphere : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  {r : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, r ≠ 0 → IsClopen {x | v.restrict x = r}
-- Mathlib.LinearAlgebra.AffineSpace.Independent
affineIndependent_vadd : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P} {v : V}, AffineIndependent k (v +ᵥ p) ↔ AffineIndependent k p
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The forgetful functor `AffineScheme ⥤ Scheme`.  -/
AlgebraicGeometry.AffineScheme.forgetToScheme : CategoryTheory.Functor AlgebraicGeometry.AffineScheme AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddSemigroup α], Lex.instAddSemigroup = { toAdd := Lex.instAdd, add_assoc := ⋯ }
-- Std.Http.Data.Response
Std.Http.Response.mk.injEq : ∀ {t : Type} (line : Std.Http.Response.Head) (body : t) (extensions : Std.Http.Extensions)
  (line_1 : Std.Http.Response.Head) (body_1 : t) (extensions_1 : Std.Http.Extensions),
  ({ line := line, body := body, extensions := extensions } =
      { line := line_1, body := body_1, extensions := extensions_1 }) =
    (line = line_1 ∧ body = body_1 ∧ extensions = extensions_1)
-- Lean.Level
_private.Lean.Level.0.Lean.mkLevelMaxCore : Lean.Level → Lean.Level → (Unit → Lean.Level) → Lean.Level
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- A bilinear map `B : E × F → G` which is (jointly) continuous is **hypocontinuous**:
in curried form, it defines a continuous linear map `E →L[𝕜] F →L[𝕜] G`.

In the normed setting, the converse is true, see `ContinuousLinearMap.continuous₂`.
In general, however, hypocontinuity is a strictly weaker condition than joint continuity.  -/
ContinuousLinearMap.continuous_of_continuous_uncurry : ∀ {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₂] [inst_1 : NormedField 𝕜₃] {E : Type u_4} {F : Type u_5}
  {G : Type u_6} [inst_2 : AddCommGroup E] [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜₂ F] [inst_5 : AddCommGroup G]
  [inst_6 : Module 𝕜₃ G] [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  {𝕜₁ : Type u_7} [inst_10 : NontriviallyNormedField 𝕜₁] {σ : 𝕜₁ →+* 𝕜₂} [inst_11 : Module 𝕜₁ E] {τ : 𝕜₃ →+* 𝕜₂}
  [RingHomSurjective τ] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [inst_15 : IsTopologicalAddGroup F]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] (B : G →ₛₗ[τ] E →SL[σ] F), (Continuous fun p => (B p.1) p.2) → Continuous ⇑B
-- Mathlib.Order.Hom.Lex
Prod.Lex.uniqueProd_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Unique α] [inst_2 : LE β] (x : Lex (α × β)),
  (Prod.Lex.uniqueProd α β) x = (ofLex x).2
-- Batteries.Data.String.Lemmas
String.firstDiffPos_eq : ∀ (a b : String),
  a.firstDiffPos b = { byteIdx := String.utf8Len (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) a.toList b.toList).1 }
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_Perm_le : ∀ {α : Type u_2} {s B : Set α} {G : Subgroup (Equiv.Perm α)},
  MulAction.IsBlock (↥G) B → B ⊂ s → MulAction.stabilizer (Equiv.Perm α) s ≤ G → B.Subsingleton
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insert_eq_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α}, insert a m = m.insert a
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderiv_inv : ∀ {σ : Type u_1} {R : Type u_2} {i : σ} [inst : CommRing R] (f : (MvPowerSeries σ R)ˣ),
  (MvPowerSeries.pderiv R i) ↑f⁻¹ = -↑f⁻¹ ^ 2 * (MvPowerSeries.pderiv R i) ↑f
-- Mathlib.Data.Set.Lattice
Set.biInter_ge_eq_iInf : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {s : α → Set β}, ⋂ n, ⋂ m, ⋂ (_ : m ≥ n), s m = ⋂ n, s n
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
/-- Note that `2 ^ (n - 2) = 1` when `n ≤ 1`.  -/
ArithmeticFunction.carmichael_two_pow_of_ne_two : ∀ {n : ℕ}, n ≠ 2 → ArithmeticFunction.carmichael (2 ^ n) = 2 ^ (n - 2)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsScalarTower : ∀ (K : Type u_1) [inst : Field K] {L : Type u_3} [inst_1 : Ring L] [inst_2 : Algebra K L],
  IsScalarTower (NumberField.RingOfIntegers K) K L
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.mem_finsetWalkLengthLT_iff : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : G.LocallyFinite] {n : ℕ} {u v : V} {p : G.Walk u v},
  p ∈ G.finsetWalkLengthLT n u v ↔ p.length < n
-- Mathlib.Algebra.Group.Basic
ite_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (p : Prop) [inst_1 : Decidable p] (a b : α) (c : β),
  (if p then a else b) ^ c = if p then a ^ c else b ^ c
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
one_le_cfc : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  (∀ x ∈ spectrum R a, 1 ≤ f x) →
    autoParam (ContinuousOn f (spectrum R a)) one_le_cfc._auto_1 → autoParam (p a) one_le_cfc._auto_3 → 1 ≤ cfc f a
-- Mathlib.Order.InitialSeg
PrincipalSeg.isLowerSet_range : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : LT α] (f : α <i β),
  IsLowerSet (Set.range ⇑f.toRelEmbedding)
-- Mathlib.Data.ENat.Basic
ENat.toNat_sub : ∀ {n : ℕ∞}, n ≠ ⊤ → ∀ (m : ℕ∞), (m - n).toNat = m.toNat - n.toNat
-- Init.Data.Sum.Lemmas
Sum.inl.inj_iff : ∀ {α : Type u_1} {β : Type u_2} {a b : α}, Sum.inl a = Sum.inl b ↔ a = b
-- Mathlib.RingTheory.Noetherian.Basic
/-- If the first and final modules in an exact sequence are Noetherian,
then the middle module is also Noetherian.  -/
isNoetherian_of_range_eq_ker : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {P : Type u_7} [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  [IsNoetherian R M] [IsNoetherian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P), f.range = g.ker → IsNoetherian R N
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.findSome?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
commutative ring then the canonical map `R → ∏ (R ⧸ Iᵢ)` is surjective.  -/
Ideal.pi_quotient_surjective : ∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_3} [Finite ι] {I : ι → Ideal R},
  Pairwise (Function.onFun IsCoprime I) → ∀ (x : (i : ι) → R ⧸ I i), ∃ r, ∀ (i : ι), (Ideal.Quotient.mk (I i)) r = x i
-- Mathlib.Data.Fin.VecNotation
Matrix.head_cons : ∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m → α), Matrix.vecHead (Matrix.vecCons x u) = x
-- Mathlib.LinearAlgebra.Pi
LinearMap.lsum_single : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (S : Type u_1) [inst_4 : Fintype ι] [inst_5 : Semiring S]
  [inst_6 : (i : ι) → Module S (φ i)] [inst_7 : ∀ (i : ι), SMulCommClass R S (φ i)],
  (LinearMap.lsum R φ S) (LinearMap.single R φ) = LinearMap.id
-- Std.Http.Protocol.H1.Parser
/-- Parses an HTTP version string and returns the corresponding `Version` value.
Fails if the version is not recognized by `Version.ofNumber?`.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseHttpVersion : Std.Internal.Parsec.ByteArray.Parser Std.Http.Version
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.match_1.eq_1 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 :
    ByteArray.utf8DecodeChar?.FirstByte.invalid = ByteArray.utf8DecodeChar?.FirstByte.invalid →
      motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 :
    ByteArray.utf8DecodeChar?.FirstByte.invalid = ByteArray.utf8DecodeChar?.FirstByte.done →
      motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 :
    ByteArray.utf8DecodeChar?.FirstByte.invalid = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 :
    ByteArray.utf8DecodeChar?.FirstByte.invalid = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 :
    ByteArray.utf8DecodeChar?.FirstByte.invalid = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match h : ByteArray.utf8DecodeChar?.FirstByte.invalid with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) =
    h_1 ⋯
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.addZeroClass.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : Zero M₂] [inst_2 : AddZeroClass M₁] (f : M₁ → M₂)
  (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Surjective.addZeroClass f hf one mul = { toZero := inst_1, toAdd := inst, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.Logic.Basic
xor_iff_not_iff' : ∀ {a b : Prop}, Xor a b ↔ (¬a ↔ b)
-- Mathlib.Topology.Constructions.SumProd
isOpenQuotientMap_prodMap_iff : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] [Nonempty X] [Nonempty Z] {f : X → Y} {g : Z → W},
  IsOpenQuotientMap (Prod.map f g) ↔ IsOpenQuotientMap f ∧ IsOpenQuotientMap g
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.mergeWith : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {mergeFn : α → β → β → β} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.WF → (Std.TreeMap.Raw.mergeWith mergeFn t₁ t₂).WF
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- The "main pair" for a coalgebra `(A, α)` is the pair of morphisms `(G α, η_GA)`. It is always a
`G`-cosplit pair, and will be used to construct the right adjoint to the comparison functor and show
it is an equivalence.
 -/
CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra),
  F.IsCosplitPair (G.map A.a) (adj.unit.app (G.obj A.A))
-- Init.Data.Range.Polymorphic.Char
_private.Init.Data.Range.Polymorphic.Char.0.Char.instPreservesRxiSizeFinNumCodePointsMap : Char.map✝.PreservesRxiSize
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The property of a `RingSeminorm` that for all `x` and `y` in the ring, the norm of `x * y` is
less than the norm of `x` times the norm of `y`.  -/
RingSeminorm.mul_le' : ∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] (self : RingSeminorm R) (x y : R),
  self.toFun (x * y) ≤ self.toFun x * self.toFun y
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
/-- `∏' i : ι, (1 + f i)` is convergent if `∑' s : Finset ι, ∏ i ∈ s, f i` is convergent.

For complete normed ring, see also `multipliable_one_add_of_summable`.  -/
multipliable_one_add_of_summable_prod : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommSemiring α] [inst_1 : TopologicalSpace α] {f : ι → α},
  (Summable fun x => ∏ i ∈ x, f i) → Multipliable fun x => 1 + f x
-- Mathlib.Algebra.Group.Indicator
Set.indicator_add_eq_left : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] {f g : α → M},
  Disjoint (Function.support f) (Function.support g) → (Function.support f).indicator (f + g) = f
-- Mathlib.Topology.Algebra.UniformConvergence
instAddCommMonoidUniformFun : {α : Type u_1} → {β : Type u_2} → [AddCommMonoid β] → AddCommMonoid (UniformFun α β)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₀₁))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'._auto_3),
  (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).hom =
    X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.BitVecValue.mk.injEq : ∀ (n : ℕ) (val : BitVec n) (n_1 : ℕ) (val_1 : BitVec n_1),
  ({ n := n, val := val } = { n := n_1, val := val_1 }) = (n = n_1 ∧ val ≍ val_1)
-- Init.Data.Nat.Basic
Nat.zero_ne_one : 0 ≠ 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α} {f : β → β},
  (Std.DHashMap.Const.modify m k f).getKey! k = if k ∈ m then k else default
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_eq_singleton_of_isAtom : ∀ {α : Type u_2} [inst : TopologicalSpace α] [T0Space α] {s : TopologicalSpace.Closeds α}, IsAtom s → ∃ a, ↑s = {a}
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- The `Homeomorph` between the fiber of `PrimeSpectrum S → PrimeSpectrum R`
at a prime ideal `p : PrimeSpectrum R` and the prime spectrum of `κ(p) ⊗[R] S`.  -/
PrimeSpectrum.preimageHomeomorphFiber : (R : Type u_3) →
  (S : Type u_4) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : PrimeSpectrum R) → ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S)
-- Lean.Meta.Tactic.Grind.Proof
/-- Returns `true` if we can construct a congruence proof for `lhs = rhs` using `congrArg`, `congrFun`, and `congr`.
`f` (`g`) is the function of the `lhs` (`rhs`) application. `numArgs` is the number of arguments.
 -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.isCongrDefaultProofTarget : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Bool
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.limitRecOn_add_one : ∀ {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0)
  (H₂ : (o : Ordinal.{u_4}) → motive o → motive (o + 1))
  (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o),
  Ordinal.limitRecOn (o + 1) H₁ H₂ H₃ = H₂ o (Ordinal.limitRecOn o H₁ H₂ H₃)