mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.eq_finset_univ : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddKleinFour G] [inst_2 : Fintype G] [inst_3 : DecidableEq G] {x y : G},
  x ≠ 0 → y ≠ 0 → x ≠ y → {x + y, x, y, 0} = Finset.univ
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.ennrealVariation_eq_self : ∀ {X : Type u_1} {mX : MeasurableSpace X} (μ : MeasureTheory.VectorMeasure X ENNReal), μ.ennrealVariation = μ
-- Std.Async.ContextAsync
Std.Async.ContextAsync.instMonadAwaitAsyncTask : Std.Async.MonadAwait Std.Async.AsyncTask Std.Async.ContextAsync
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderParsedState.mk : Lean.Parser.ModuleParserState →
  Lean.Language.SnapshotTask Lean.Language.Lean.HeaderProcessedSnapshot → Lean.Language.Lean.HeaderParsedState
-- Lean.Widget.UserWidget
/-- Pretty name of user widget to display to the user.  -/
Lean.Widget.UserWidgetDefinition.name : Lean.Widget.UserWidgetDefinition → String
-- Mathlib.Algebra.Lie.Nilpotent
_private.Mathlib.Algebra.Lie.Nilpotent.0.LieModule.coe_lowerCentralSeries_eq_int_aux : ∀ (R₁ : Type u_1) (R₂ : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R₁] [inst_1 : CommRing R₂]
  [inst_2 : AddCommGroup M] [inst_3 : LieRing L] [inst_4 : LieAlgebra R₁ L] [inst_5 : LieAlgebra R₂ L]
  [inst_6 : Module R₁ M] [inst_7 : Module R₂ M] [inst_8 : LieRingModule L M] [LieModule R₁ L M] (k : ℕ),
  have I := LieModule.lowerCentralSeries R₂ L M k;
  have S := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x};
  ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
SimpleGraph.extremalNumber_of_fintypeCard_eq : ∀ {n : ℕ} {V : Type u_1} {W : Type u_2} {H : SimpleGraph W} [inst : Fintype V],
  Fintype.card V = n → SimpleGraph.extremalNumber n H = {G | H.Free G}.sup fun x => x.edgeFinset.card
-- Mathlib.Data.Matrix.Mul
/-- Permuting vectors on both sides of a dot product is a no-op.  -/
comp_equiv_dotProduct_comp_equiv : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalNonAssocSemiring α] (x y : n → α) (e : m ≃ n), x ∘ ⇑e ⬝ᵥ y ∘ ⇑e = x ⬝ᵥ y
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_le_size_insertMany : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ}, m.size ≤ (m.insertMany l).size
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to the empty set is 0 (if you want to have the more reasonable
value `∞` instead, use `Metric.infEDist`, which takes values in `ℝ≥0∞`)  -/
Metric.infDist_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, Metric.infDist x ∅ = 0
-- Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
/-- In an Archimedean linearly ordered group (with the order topology), a subgroup is
discrete iff it is cyclic.  -/
Subgroup.discrete_iff_cyclic : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [MulArchimedean G] {H : Subgroup G}, IsCyclic ↥H ↔ DiscreteTopology ↥H
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f : ∀ (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] (X : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D))
  (X_1 : C),
  (((CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso C D).inv.app X).app X_1).f =
    (X.obj X_1).p
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.embeddingUpInt_areComplementary : ∀ (n₀ n₁ : ℤ), n₀ + 1 = n₁ → (ComplexShape.embeddingUpIntLE n₀).AreComplementary (ComplexShape.embeddingUpIntGE n₁)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- the pullback cone is a limit  -/
CategoryTheory.IsPullback.isLimit' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (self : CategoryTheory.IsPullback fst snd f g),
  Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk fst snd ⋯))
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.tensorUnit_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {X Y : C} {f : X ⟶ Y},
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C D)).map f =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The `Subfield` generated by a set.  -/
Subfield.closure : {K : Type u} → [inst : DivisionRing K] → Set K → Subfield K
-- Mathlib.Algebra.Order.SuccPred.TypeTags
instPredOrderAdditive : {X : Type u_1} → [inst : Preorder X] → [h : PredOrder X] → PredOrder (Additive X)
-- Init.Data.Nat.Basic
Nat.le_of_not_lt : ∀ {a b : ℕ}, ¬a < b → b ≤ a
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.instDecidableEqList.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (ys : List α) → (Unit → motive []) → ((head : α) → (tail : List α) → motive (head :: tail)) → motive ys
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The composition of a primitive additive character with an injective monoid homomorphism
is also primitive.  -/
AddChar.IsPrimitive.compMulHom_of_isPrimitive : ∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : CommMonoid R'] {R'' : Type u_1} [inst_2 : CommMonoid R'']
  {φ : AddChar R R'} {f : R' →* R''}, φ.IsPrimitive → Function.Injective ⇑f → (f.compAddChar φ).IsPrimitive
-- Mathlib.Topology.MetricSpace.Defs
instMetricSpaceAdditive : {X : Type u_1} → [MetricSpace X] → MetricSpace (Additive X)
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstSubInt : Lean.Expr → Lean.MetaM Bool
-- Lean.Expr
/-- Return the binder information if `e` is a lambda or forall expression, and `.default` otherwise.
 -/
Lean.Expr.binderInfo : Lean.Expr → Lean.BinderInfo
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
multiplicative action on `Set β`.  -/
Set.distribMulActionSet : {α : Type u_1} →
  {β : Type u_2} → [inst : Monoid α] → [inst_1 : AddMonoid β] → [DistribMulAction α β] → DistribMulAction α (Set β)
-- Mathlib.Data.NNRat.Defs
NNRat.bddBelow_coe : ∀ (s : Set ℚ≥0), BddBelow (NNRat.cast '' s)
-- Init.Data.String.Lemmas.Pattern.Find.String
String.contains_string_iff : ∀ {t s : String}, s.contains t = true ↔ t.toList <:+: s.toList
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.instFullCompObjPostOfFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : C) [G.Faithful], (CategoryTheory.CostructuredArrow.post F G S).Full
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.instEssSurjOppositeRightOp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} [F.EssSurj], F.rightOp.EssSurj
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_add_mul_I : ∀ (x y : ℂ), Complex.exp (x + y * Complex.I) = Complex.exp x * (Complex.cos y + Complex.sin y * Complex.I)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.le_comap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {f : M →ₙ+ N},
  S ≤ AddSubsemigroup.comap f (AddSubsemigroup.map f S)
-- Std.Do.PostCond
Std.Do.ExceptConds.entails.refl : ∀ {ps : Std.Do.PostShape} (x : Std.Do.ExceptConds ps), x.entails x
-- Mathlib.Topology.Homotopy.HSpaces
/-- The definition `toHSpace` is not an instance because its additive version would
lead to a diamond since a topological field would inherit two `HSpace` structures, one from the
`MulOneClass` and one from the `AddZeroClass`. In the case of a group, we make
`IsTopologicalGroup.hSpace` an instance."  -/
IsTopologicalGroup.toHSpace : (M : Type u) → [inst : MulOneClass M] → [inst_1 : TopologicalSpace M] → [ContinuousMul M] → HSpace M
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_sub_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  ⌊a - 1⌋ = ⌊a⌋ - 1
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.ext_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.Hom M N}, f = g ↔ ∀ (x : M), f x = g x
-- Init.Data.Nat.Lemmas
Nat.le_mul_of_pos_left : ∀ {n : ℕ} (m : ℕ), 0 < n → m ≤ n * m
-- Mathlib.Geometry.Euclidean.Projection
/-- If the orthogonal projections of a point onto two subspaces are equal, so is the projection
onto their supremum.  -/
EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s₁ s₂ : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s₁] [inst_6 : Nonempty ↥s₂] [inst_7 : s₁.direction.HasOrthogonalProjection]
  [inst_8 : s₂.direction.HasOrthogonalProjection] {p : P},
  ↑((EuclideanGeometry.orthogonalProjection s₁) p) = ↑((EuclideanGeometry.orthogonalProjection s₂) p) →
    ∀ [inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection],
      ↑((EuclideanGeometry.orthogonalProjection (s₁ ⊔ s₂)) p) = ↑((EuclideanGeometry.orthogonalProjection s₁) p)
-- Mathlib.Combinatorics.SimpleGraph.Hall
SimpleGraph.union_eq_univ_of_forall_ncard_le : ∀ {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {p₁ p₂ : Set V},
  G.IsBipartiteWith p₁ p₂ → (∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard) → p₁ ∪ p₂ = Set.univ
-- Mathlib.Order.Interval.Finset.Floor
Int.cast_mem_Iic_iff : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {b : α} {n : ℤ},
  ↑n ∈ Set.Iic b ↔ n ∈ Set.Iic ⌊b⌋
-- Mathlib.RingTheory.RingHom.Flat
/-- `Spec S → Spec R` is generalizing if `R →+* S` is flat.  -/
RingHom.Flat.generalizingMap_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.Flat → GeneralizingMap (PrimeSpectrum.comap f)
-- Init.Data.String.Basic
String.Pos.cast_lt_iff : ∀ {s t : String} {pos : s.Pos} {pos' : t.Pos} {h : s = t}, pos.cast h < pos' ↔ pos < pos'.cast ⋯
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s t : Set α},
  AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (s \ t)
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_of_eq : ∀ {n : ℕ} {i j : Fin n} [inst : NeZero n], i = j → j.cycleRange i = 0
-- Init.Data.UInt.Basic
/-- Multiplies two 64-bit unsigned integers, wrapping around on overflow.  Usually accessed via the `*`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.mul : UInt64 → UInt64 → UInt64
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.proved.sizeOf_spec : sizeOf Lean.Meta.Simp.DischargeResult.proved = 1
-- Mathlib.Data.TypeVec
TypeVec.prod.mk.eq_def : ∀ (x : ℕ) (x_1 x_2 : TypeVec.{u} x) (x_3 : Fin2 x),
  TypeVec.prod.mk x_3 =
    match (motive := (x : ℕ) → (x_4 x_5 : TypeVec.{u} x) → (x_6 : Fin2 x) → x_4 x_6 → x_5 x_6 → x_4.prod x_5 x_6) x,
      x_1, x_2, x_3 with
    | n.succ, α, β, i.fs => TypeVec.prod.mk i
    | n.succ, x, x_4, Fin2.fz => Prod.mk
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGED.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α fun x => β) (fallback : α × β),
  Std.DTreeMap.Internal.Impl.Const.getEntryGED k t fallback =
    (Std.DTreeMap.Internal.Impl.Const.getEntryGE? k t).getD fallback
-- Std.Http.Data.Chunk
/-- A proposition asserting that `s` is a valid extension value, meaning every character passes
`Char.quotedStringChar` (i.e. is `qdtext` or a valid `quoted-pair` payload).

Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension
 -/
Std.Http.Chunk.IsValidExtensionValue : String → Prop
-- Init.Data.Bool
Bool.instLT : LT Bool
-- Mathlib.RingTheory.Length
Submodule.length_le_length_restrictScalars : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (A : Type u_5)
  [inst_3 : Ring A] [inst_4 : SMul A R] [inst_5 : Module A M] [inst_6 : IsScalarTower A R M] (p : Submodule R M),
  Module.length R ↥p ≤ Module.length A ↥(Submodule.restrictScalars A p)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.ofLinearOrder_fst : ∀ (ι : Type w) [inst : LinearOrder ι] (x : ↑{x | x.1 < x.2}),
  (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).fst x = (↑x).1
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instPartialOrder.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E], AddGroupSeminorm.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Mathlib.Algebra.Category.CommHopfAlgCat
commHopfAlgCatEquivCogrpCommAlgCat_counitIso_hom_app : ∀ (R : Type u) [inst : CommRing R] (X : (CategoryTheory.Grp (CommAlgCat R)ᵒᵖ)ᵒᵖ),
  (commHopfAlgCatEquivCogrpCommAlgCat R).counitIso.hom.app X =
    CategoryTheory.CategoryStruct.id
      (Opposite.op
        { X := Opposite.op (CommAlgCat.of R ↑(Opposite.unop (Opposite.unop X).X)), grp := CommAlgCat.grpObjOpOf })
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
SSet.instNonemptyNerveOfNonempty : ∀ (T : Type u) [inst : Preorder T] [Nonempty T], (CategoryTheory.nerve T).Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.right.injEq : ∀ {J : CategoryTheory.Limits.MulticospanShape} (a a_1 : J.R),
  (CategoryTheory.Limits.WalkingMulticospan.right a = CategoryTheory.Limits.WalkingMulticospan.right a_1) = (a = a_1)
-- Mathlib.Topology.NhdsSet
/-- A proposition is true on a set neighborhood of `s`
iff it is eventually true near each point in the set.  -/
eventually_nhdsSet_iff_forall : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {p : X → Prop},
  (∀ᶠ (x : X) in nhdsSet s, p x) ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, p y
-- Mathlib.Data.Finset.Powerset
Finset.empty_mem_powerset : ∀ {α : Type u_1} (s : Finset α), ∅ ∈ s.powerset
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_congr_fun₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f g : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet s μ → Set.EqOn f g s → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
IsScalarTower.adjoin_range_toAlgHom : ∀ (R : Type u) (S : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : CommSemiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A] (t : Set A),
  Subalgebra.restrictScalars R (Algebra.adjoin (↥(IsScalarTower.toAlgHom R S A).range) t) =
    Subalgebra.restrictScalars R (Algebra.adjoin S t)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.IsRightKanExtension.mk : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F' : CategoryTheory.Functor D H} {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  {α : L.comp F' ⟶ F},
  Nonempty (CategoryTheory.CostructuredArrow.IsUniversal (CategoryTheory.Functor.RightExtension.mk F' α)) →
    F'.IsRightKanExtension α
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.proj.sizeOf_spec : ∀ (a : Lean.Name) (a_1 a_2 : ℕ),
  sizeOf (Lean.Meta.DiscrTree.Key.proj a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.Data.Finset.Insert
/-- Inserting an element to a finite set is equivalent to the option type.  -/
Finset.subtypeInsertEquivOption : {α : Type u_1} → [inst : DecidableEq α] → {t : Finset α} → {x : α} → x ∉ t → ↥(insert x t) ≃ Option ↥t
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeAppStaged : Lean.Expr → Array Lean.Expr → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Std.Data.Internal.List.Associative
Std.Internal.List.distinctKeys_interSmaller : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys (Std.Internal.List.interSmaller l₁ l₂)
-- Init.System.IO
IO.Process.StdioConfig.mk : IO.Process.Stdio → IO.Process.Stdio → IO.Process.Stdio → IO.Process.StdioConfig
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.ofValuation_toValuation : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : AddValuation R Γ₀), AddValuation.ofValuation (AddValuation.toValuation v) = v
-- Lean.Meta.Tactic.Split
/-- This method makes sure each discriminant is a free variable.
Return the tuple `(discrsNew, discrEqs, mvarId)`. `discrsNew` in an array representing the new discriminants, `discrEqs` is an array of auxiliary equality hypotheses
that connect the new discriminants to the original terms they represent.
Remark: `discrEqs.size ≤ discrsNew.size`

Remark:
  We should only generalize `discrs` occurrences as `match`-expression discriminants.
  For example, given the following goal.
  ```
  x : Nat
  ⊢ (match g x with
      | 0 => 1
      | Nat.succ y => g x) =
      2 * x + 1
  ```
  we should not generalize the `g x` in the rhs of the second alternative, and the two resulting goals
  for the `split` tactic  should be
  ```
  case h_1
  x x✝ : Nat
  h✝ : g x = 0
  ⊢ 1 = 2 * x + 1

  case h_2
  x x✝ y✝ : Nat
  h✝ : g x = Nat.succ y✝
  ⊢ g x = 2 * x + 1
  ```
 -/
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.generalizeMatchDiscrs : Lean.MVarId → Lean.Name → Lean.Expr → Array Lean.Expr → Lean.MetaM (Array Lean.FVarId × Array Lean.FVarId × Lean.MVarId)
-- Init.Data.String.Substring
/-- Converts a `String.Slice` into a `Substring.Raw`.
 -/
Substring.Raw.ofSlice : String.Slice → Substring.Raw
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_eq_sin_div_cos : ∀ (x : ℂ), Complex.tan x = Complex.sin x / Complex.cos x
-- Mathlib.Topology.Sets.BaseChangeNhds
TopologicalSpace.Compacts.baseChangeOpenNhds_id : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : TopologicalSpace.Compacts α} (U : ↑K.openNhds),
  TopologicalSpace.Compacts.baseChangeOpenNhds (CategoryTheory.CategoryStruct.id K) U = U
-- Mathlib.RingTheory.Localization.Submodule
/-- Map from ideals of `R` to submodules of `S` induced by `f`.  -/
IsLocalization.coeSubmodule : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Type u_2) → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → Ideal R → Submodule R S
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesOnBall_inv_one_add : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (𝕝 : Type u_8) [inst_1 : NormedDivisionRing 𝕝]
  [inst_2 : NormedAlgebra 𝕜 𝕝], HasFPowerSeriesOnBall (fun x => (1 + x)⁻¹) (alternatingGeometricSeries 𝕜 𝕝) 0 1
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentials.comm₂₃ : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ),
  pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm = pres.differentialsSolution.π
-- Mathlib.Analysis.Convex.Combination
Finset.inf_le_centerMass : ∀ {R : Type u_1} {ι : Type u_5} {α : Type u_7} [inst : Field R] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α]
  [inst_3 : Module R α] [inst_4 : LinearOrder R] [IsOrderedAddMonoid α] [PosSMulMono R α] {s : Finset ι} {f : ι → α}
  {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ s, w i), s.inf' ⋯ f ≤ s.centerMass w f
-- Mathlib.Order.LiminfLimsup
/-- A version of `le_liminf_iff` with large inequalities in densely ordered spaces.  -/
Filter.le_liminf_iff' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β}
  [DenselyOrdered β] {x : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.le_liminf_iff'._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.le_liminf_iff'._auto_3 →
      (x ≤ Filter.liminf u f ↔ ∀ y < x, ∀ᶠ (a : α) in f, y ≤ u a)
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.mk : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          (toIntermediateField : IntermediateField k K) →
            [finiteDimensional : FiniteDimensional k ↥toIntermediateField] →
              [isGalois : IsGalois k ↥toIntermediateField] → FiniteGaloisIntermediateField k K
-- Init.Data.List.Monadic
List.mapM'.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → m β) (a : α) (l : List α),
  List.mapM' f (a :: l) = do
    let __do_lift ← f a
    let __do_lift_1 ← List.mapM' f l
    pure (__do_lift :: __do_lift_1)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_sum : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ] [inst : Fintype ι],
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    ProbabilityTheory.variance (∑ i, X i) μ = ∑ i, ∑ j, ProbabilityTheory.covariance (X i) (X j) μ
-- Mathlib.Data.Finsupp.Order
Finsupp.single_le_single : ∀ {ι : Type u_1} {α : Type u_3} [inst : Zero α] [inst_1 : Preorder α] {i : ι} {a b : α},
  ((fun₀ | i => a) ≤ fun₀ | i => b) ↔ a ≤ b
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.add_comp : ∀ {α : Type u_2} {β : Type u_3} {M : Type u_7} [inst : Add M] (f g : β → M) (z : α → β), (f + g) ∘ z = f ∘ z + g ∘ z
-- Init.Grind.Lemmas
Lean.Grind.eq_false_of_imp_eq_false : ∀ {a b : Prop}, (a → b) = False → b = False
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionItem.toJson : Lean.Lsp.CompletionItem → Lean.Json
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
/-- The canonical quotient map from a field `K` into the `ConjRootClass` of the field extension
`L / K`.  -/
ConjRootClass.mk : (K : Type u_1) → {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → L → ConjRootClass K L
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- `Real.cosh` as a `PartialEquiv` from $[0, ∞)$ to $[1, ∞)$.  -/
Real.coshPartialEquiv : PartialEquiv ℝ ℝ
-- Mathlib.Logic.Pairwise
Pairwise.set_pairwise : ∀ {α : Type u_1} {r : α → α → Prop}, Pairwise r → ∀ (s : Set α), s.Pairwise r
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation maps balls to balls and scales the radius by `ratio f`.  -/
Dilation.mapsTo_ball : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ℝ),
  Set.MapsTo (⇑f) (Metric.ball x r') (Metric.ball (f x) (↑(Dilation.ratio f) * r'))
-- Lean.Setup
Lean.instReprPlugin : Repr Lean.Plugin
-- Batteries.Lean.HashMap
/-- `O(|other|)` amortized. Merge two `HashMap`s.
The values of keys which appear in both maps are combined using `f`.
 -/
Std.HashMap.mergeWith : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] → {β : Type u_2} → (α → β → β → β) → Std.HashMap α β → Std.HashMap α β → Std.HashMap α β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.oldLayer : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {outWidth : ℕ} →
          (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget aig outWidth) →
            aig.RefVec (self.len * self.w)