mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.min_ne_of_ne_of_lt : ∀ {R : Type u_2} [inst : LinearOrder R] {a b c : R}, a ≠ c → c < b → min a b ≠ c
-- Mathlib.Algebra.Notation.Defs
/-- `a -ᵥ b` computes the difference of `a` and `b`. The meaning of this notation is
type-dependent, but it is intended to be used for additive torsors. 

Conventions for notations in identifiers:

 * The recommended spelling of `-ᵥ` in identifiers is `vsub`. -/
VSub.vsub : {G : outParam (Type u_1)} → {P : Type u_2} → [self : VSub G P] → P → P → G
-- Init.Data.BitVec.Bitblast
/-- The current quotient.  -/
BitVec.DivModState.q : {w : ℕ} → BitVec.DivModState w → BitVec w
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.minKey! ∈ t
-- Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
/-- For a convex continuous function `f` on `[0, ∞)`, if `μ` is absolutely continuous
with respect to `ν`, then
`ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν`.  -/
MeasureTheory.mul_le_integral_rnDeriv_of_ac : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  ConvexOn ℝ (Set.Ici 0) f →
    ContinuousWithinAt f (Set.Ici 0) 0 →
      MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
        μ.AbsolutelyContinuous ν →
          ν.real Set.univ * f (μ.real Set.univ / ν.real Set.univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
-- Init.Data.Nat.Div.Basic
Nat.mod_eq_sub_mod : ∀ {a b : ℕ}, a ≥ b → a % b = (a - b) % b
-- Mathlib.Analysis.Complex.Polynomial.Basic
Polynomial.Gal.splits_ℚ_ℂ : ∀ {p : Polynomial ℚ}, Fact (Polynomial.map (algebraMap ℚ ℂ) p).Splits
-- Init.Data.String.Slice
String.Slice.instBEq : BEq String.Slice
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_pow : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : WithVal v) (n : ℕ), (x ^ n).ofVal = x.ofVal ^ n
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousVAdd : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  Topology.IsQuotientMap f →
    ∀ [ContinuousConstVAdd G E],
      (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) →
        ∀ [ProperlyDiscontinuousVAdd G E] [LocallyCompactSpace E] [T2Space E],
          IsCoveringMapOn f (f '' {e | AddAction.stabilizer G e = ⊥})
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.one_fin_two : ∀ {α : Type u} [inst : Zero α] [inst_1 : One α], 1 = !![1, 0; 0, 1]
-- Mathlib.Logic.Nontrivial.Defs
/-- In a nontrivial type, there exists a pair of distinct terms.  -/
Nontrivial.exists_pair_ne : ∀ {α : Type u_3} [self : Nontrivial α], ∃ x y, x ≠ y
-- Mathlib.Algebra.Group.Action.Defs
SemigroupAction.toSMul : {α : Type u_9} → {β : Type u_10} → {inst : Semigroup α} → [self : SemigroupAction α β] → SMul α β
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.mk₀.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y),
  CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ f =
    CategoryTheory.Localization.SmallShiftedHom.mk W (CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f)
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Limits.coneOfSectionCompCoyoneda_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : ↑(F.comp (CategoryTheory.coyoneda.obj X)).sections) (j : J),
  (CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s).π.app j = ↑s j
-- Mathlib.Analysis.Normed.Ring.Basic
Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg : ∀ {R : Type u_5} {ι : Type u_6} {ι' : Type u_7} [inst : Semiring R] [Finite ι] [Finite ι'] {F : Type u_8}
  [inst_3 : FunLike F R ℝ] [NonnegHomClass F R ℝ] [MulHomClass F R ℝ] (v : F) (x : ι → R) (y : ι' → R),
  ⨆ a, v (x a.1 * y a.2) = (⨆ i, v (x i)) * ⨆ j, v (y j)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Given `X : D` and `F : C ⥤ D`, to upgrade a functor `G : E ⥤ C` to a functor
`E ⥤ StructuredArrow X F`, it suffices to provide maps `X ⟶ F.obj (G.obj Y)` for all `Y` making
the obvious triangles involving all `F.map (G.map g)` commute.

This is of course the same as providing a cone over `F ⋙ G` with cone point `X`, see
`Functor.toStructuredArrowIsoToStructuredArrow`.  -/
CategoryTheory.Functor.toStructuredArrow : {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] →
            (G : CategoryTheory.Functor E C) →
              (X : D) →
                (F : CategoryTheory.Functor C D) →
                  (f : (Y : E) → X ⟶ F.obj (G.obj Y)) →
                    (∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) →
                      CategoryTheory.Functor E (CategoryTheory.StructuredArrow X F)
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasStrictFDerivAt.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {f : E → E} {f' : E →L[𝕜] E},
  HasStrictFDerivAt f f' x → f x = x → ∀ (n : ℕ), HasStrictFDerivAt f^[n] (f' ^ n) x
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_mapIso_inv_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : ∐ f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.mapIso p).inv h) =
    CategoryTheory.CategoryStruct.comp (p b).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) h)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- Markov's inequality for `Finset.card` and `tsum` in `ℝ≥0∞`.  -/
ENNReal.finset_card_const_le_le_of_tsum_le : ∀ {ι : Type u_4} {a : ι → ENNReal} {c : ENNReal},
  c ≠ ⊤ → ∑' (i : ι), a i ≤ c → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ (hf : {i | ε ≤ a i}.Finite), ↑hf.toFinset.card ≤ c / ε
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instAddAction : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → AddAction α (UpperSet α)
-- Mathlib.Analysis.Convex.Gauge
/-- The Minkowski functional. Given a set `s` in a real vector space, `gauge s` is the functional
which sends `x : E` to the smallest `r : ℝ` such that `x` is in `s` scaled by `r`.  -/
gauge : {E : Type u_2} → [inst : AddCommGroup E] → [Module ℝ E] → Set E → E → ℝ
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.closure_subset_preimage : ∀ {α : Type ua} [inst : UniformSpace α] {U : SetRel α α}, U ∈ uniformity α → ∀ (s : Set α), closure s ⊆ U.preimage s
-- Std.Http.Data.URI.Basic
/-- Query string represented as an array of key-value pairs. Both keys and values are stored as
`EncodedQueryParam` for proper application/x-www-form-urlencoded encoding. Values are optional to
support parameters without values (e.g., "?flag"). Order is preserved based on insertion order.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.4
 -/
Std.Http.URI.Query : Type
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.ι_sigmaSpec_assoc : ∀ {ι : Type u} (R : ι → CommRingCat) (i : ι) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun i => AlgebraicGeometry.Spec (R i)) i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.sigmaSpec R) h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i => ↑(R i)) i))) h
-- Mathlib.Order.Compare
cmpLE_eq_cmp : ∀ {α : Type u_3} [inst : Preorder α] [Std.Total fun x1 x2 => x1 ≤ x2] [inst_2 : DecidableLE α] [inst_3 : DecidableLT α]
  (x y : α), cmpLE x y = cmp x y
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piRightHom_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] {ι : Type u_4}
  (M : ι → Type u_5) [inst_7 : (i : ι) → AddCommMonoid (M i)] [inst_8 : (i : ι) → Module R (M i)] (x : N)
  (f : (i : ι) → M i), (TensorProduct.piRightHom R S N M) (x ⊗ₜ[R] f) = fun j => x ⊗ₜ[R] f j
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_zero : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X], AlgebraicGeometry.Scheme.ord 0 = 0
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.toRingSeminorm : {R : Type u_2} → [inst : NonUnitalNonAssocRing R] → RingNorm R → RingSeminorm R
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp F U c).inv.hom =
    CategoryTheory.CategoryStruct.id
      (((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).comp
              (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)).obj
          c).pt
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.commMap.eq_1 : ∀ (K : Type u_1) [inst : Field K],
  NumberField.mixedEmbedding.commMap K =
    { toFun := fun x => (fun w => (x (↑w).embedding).re, fun w => x (↑w).embedding), map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.diff : ∀ {α : Type u} {s t s' t' : Set α} {l : Filter α}, s ≤ᶠ[l] t → t' ≤ᶠ[l] s' → s \ s' ≤ᶠ[l] t \ t'
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_dvd_iff_le : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {a n : ℕ}, a ≠ 0 → (p ^ n ∣ a ↔ n ≤ padicValNat p a)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_eq_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k fallback : α}, t.contains k = true → t.getKeyD k fallback = k
-- Mathlib.FieldTheory.SeparableClosure
/-- A compositum of separable extensions is separable.  -/
IntermediateField.isSeparable_iSup : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Type u_1}
  {t : ι → IntermediateField F E} [h : ∀ (i : ι), Algebra.IsSeparable F ↥(t i)], Algebra.IsSeparable F ↥(⨆ i, t i)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if we `declName` is tagged with `funCC` modifier.
 -/
Lean.Meta.Grind.hasFunCCModifier : Lean.Name → Lean.Meta.Grind.GrindM Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_map_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited γ] {f : α → β → γ} {k k' : α},
  m.getKey? k = some k' →
    Std.DHashMap.Const.get! (Std.DHashMap.map f m) k = (Option.map (f k') (Std.DHashMap.Const.get? m k)).get!
-- Mathlib.Order.Filter.Map
Filter.map_comap_setCoe_val : ∀ {β : Type u_2} (f : Filter β) (s : Set β),
  Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ Filter.principal s
-- Mathlib.MeasureTheory.Group.Prod
/-- A *left*-invariant measure is quasi-preserved by *right*-multiplication.
This should not be confused with `(measurePreserving_mul_right μ g).quasiMeasurePreserving`.  -/
MeasureTheory.quasiMeasurePreserving_mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun h => h * g) μ μ
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- **Alias** of `OrdinalApprox.lfpApprox_mono_right`. -/
OrdinalApprox.lfpApprox_monotone : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α}, Monotone (OrdinalApprox.lfpApprox f x)
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- If `a` is an integer, then the `convs'` of its continued fraction expansion
are all equal to `a`.
 -/
GenContFract.convs'_of_int : ∀ (K : Type u_1) [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (n : ℕ) [IsStrictOrderedRing K]
  (a : ℤ), (GenContFract.of ↑a).convs' n = ↑a
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.min_def : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [K : LinearOrder β] (x y : (↑φ).Germ β),
  min x y = Filter.Germ.map₂ min x y
-- Init.Data.Char.Ordinal
/-- Packs `Char` bijectively into `Fin Char.numCodePoints` by shifting code points which are
greater than the surrogate code points by the number of surrogate code points.

The inverse of this function is called `Char.ofOrdinal`.
 -/
Char.ordinal : Char → Fin Char.numCodePoints
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Smoothness of a `C^n` section at `x₀` can be determined
using any trivialisation whose `baseSet` contains `x₀`.  -/
Bundle.Trivialization.contMDiffAt_section_iff : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} {x₀ : B} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [MemTrivializationAtlas e],
  x₀ ∈ e.baseSet →
    (ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) x₀ ↔
      ContMDiffAt IB (modelWithCornersSelf 𝕜 F) n (fun x => (↑e ⟨x, s x⟩).2) x₀)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_ofList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {l : List α}
  {k : α}, l.contains k = false → (Std.HashSet.Raw.ofList l).get! k = default
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.topEquiv_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : ↥⊤),
  LieIdeal.topEquiv x = ↑x
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.toNormedSpace : {A : Type u_1} → [self : NonUnitalCommCStarAlgebra A] → NormedSpace ℂ A
-- Init.System.Platform
/-- Is the current platform [Emscripten](https://emscripten.org/)?
 -/
System.Platform.isEmscripten : Bool
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `ℂ_[p]` is nonarchimedean.  -/
PadicComplex.isNonarchimedean : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], IsNonarchimedean norm
-- Std.Do.Triple.SpecLemmas
/-- Specification for `forIn` over a `Lean.Loop`. The cursor is `β ⊕ β`: `.inl b` means
"still iterating with `b`", `.inr b` means "finished with result `b`".
 -/
Std.Do.Spec.forIn_loop : ∀ {β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [Lean.Order.MonadTail m]
  [inst_2 : Std.Do.WPMonad m ps] {l : Lean.Loop} {init : β} {f : Unit → β → m (ForInStep β)}
  (measure : Std.Do.WhileVariant β ps) (inv : Std.Do.WhileInvariant β β ps),
  (∀ (b : β) (mb : ℕ),
      ⦃measure.eval b mb ∧ inv.1 (Sum.inl b)⦄
        f () b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => spred(∃ mb', measure.eval b' mb' ∧ ⌜mb' < mb⌝ ∧ inv.1 (Sum.inl b'))
          | ForInStep.done b' => inv.1 (Sum.inr b'),
          inv.2)⦄) →
    ⦃inv.1 (Sum.inl init)⦄ forIn l init f ⦃(fun b => inv.1 (Sum.inr b), inv.2)⦄
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.ins.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Init.Tactics
/-- `skip` does nothing.  -/
Lean.Parser.Tactic.skip : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c)
  {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y),
  (I.parallelPairDiagramOfIsColimit d hc).map h =
    CategoryTheory.Limits.parallelPair.parallelPairHom (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc) h
-- Mathlib.Topology.Instances.NNReal.Lemmas
ENNReal.iSup_pow : ∀ {ι : Sort u_1} [Nonempty ι] (f : ι → ENNReal) (n : ℕ), (⨆ i, f i) ^ n = ⨆ i, f i ^ n
-- Lean.Meta.Tactic.Assert
Lean.Meta.Hypothesis.userName : Lean.Meta.Hypothesis → Lean.Name
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.f_lie_v_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι] {i j : ι} {k : ↥b.support},
  P.root i = P.root j + P.root ↑k →
    ⁅RootPairing.GeckConstruction.f k, RootPairing.GeckConstruction.v b i⁆ =
      (↑(RootPairing.chainTopCoeff (↑k) i) + 1) • RootPairing.GeckConstruction.v b j
-- Init.Data.Int.Gcd
Int.gcd_mul_right_left_of_gcd_eq_one : ∀ {n m k : ℤ}, n.gcd m = 1 → (n * k).gcd m = k.gcd m
-- Lean.Structure
Lean.StructureFieldInfo.mk.inj : ∀ {fieldName projFn : Lean.Name} {subobject? : Option Lean.Name} {binderInfo : Lean.BinderInfo}
  {autoParam? : Option Lean.Expr} {fieldName_1 projFn_1 : Lean.Name} {subobject?_1 : Option Lean.Name}
  {binderInfo_1 : Lean.BinderInfo} {autoParam?_1 : Option Lean.Expr},
  { fieldName := fieldName, projFn := projFn, subobject? := subobject?, binderInfo := binderInfo,
        autoParam? := autoParam? } =
      { fieldName := fieldName_1, projFn := projFn_1, subobject? := subobject?_1, binderInfo := binderInfo_1,
        autoParam? := autoParam?_1 } →
    fieldName = fieldName_1 ∧
      projFn = projFn_1 ∧ subobject? = subobject?_1 ∧ binderInfo = binderInfo_1 ∧ autoParam? = autoParam?_1
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.equiv_symm_apply_as : ∀ (X : Type u_3) (x : X), ((FundamentalGroupoid.equiv X).symm x).as = x
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.instSeminormedAddCommGroupPreGNS : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] → (f : A →ₚ[ℂ] ℂ) → [StarOrderedRing A] → SeminormedAddCommGroup f.PreGNS
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
      (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).inv =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv Y
-- Lean.Elab.MutualInductive
Lean.Elab.Command.bootstrap.inductiveCheckResultingUniverse : Lean.Option Bool
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_reindex : ∀ {n₁ n₂ : Type u} (i : n₁ → n₂) {S T : AlgebraicGeometry.Scheme} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n₂ f)
      (AlgebraicGeometry.AffineSpace.reindex i T) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex i S)
      (AlgebraicGeometry.AffineSpace.map n₁ f)
-- Init.Data.UInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toUSize : Bool → USize
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.HasRightHomology.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), S.HasRightHomology
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 2 ≠ 0 → Q 2 = 0 → ¬P ≈ Q
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsState : Type
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- **Alias** of `AddCircle.finite_setOfPred_addOrderOf_eq`. -/
AddCircle.finite_setOf_addOrderOf_eq : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {n : ℕ},
  0 < n → {u | addOrderOf u = n}.Finite
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.ext : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α] {s t : ClopenUpperSet α}, ↑s = ↑t → s = t
-- Lean.Parser.Basic
Lean.Parser.incQuotDepth : Lean.Parser.Parser → Lean.Parser.Parser
-- Init.SizeOfLemmas
Fin.sizeOf : ∀ {n : ℕ} (a : Fin n), sizeOf a = ↑a + 1
-- Mathlib.Algebra.Lie.SerreConstruction
_private.Mathlib.Algebra.Lie.SerreConstruction.0.CartanMatrix.Relations.adF_of_eq_eq_zero : ∀ (R : Type u) {B : Type v} [inst : CommRing R] (CM : Matrix B B ℤ) (i : B),
  CM i i = 2 → CartanMatrix.Relations.adF R CM (i, i) = 0
-- Init.Data.SInt.Lemmas
Int8.toInt16_div_of_ne_left : ∀ (a b : Int8), a ≠ Int8.minValue → (a / b).toInt16 = a.toInt16 / b.toInt16
-- Mathlib.Data.Fin.Tuple.Embedding
/-- Remove the first element from an injective (n + 1)-tuple.  -/
Fin.Embedding.tail : {α : Type u_1} → {n : ℕ} → (Fin (n + 1) ↪ α) → Fin n ↪ α
-- Batteries.Util.ProofWanted
theorem_wanted.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Int.Order
Int.lt_add_of_sub_right_lt : ∀ {a b c : ℤ}, a - c < b → a < b + c
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalExprRingMode.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.RingNF.RingMode
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- **Steinhaus Theorem** for finite mass sets.

In any locally compact group `G` with a Haar measure `μ` that's inner regular on finite measure
sets, for any measurable set `E` of finite positive measure, the set `E - E` is a neighbourhood of
`0`.  -/
MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos_ne_top : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [LocallyCompactSpace G]
  [μ.InnerRegularCompactLTTop] (E : Set G), MeasurableSet E → 0 < μ E → μ E ≠ ⊤ → E - E ∈ nhds 0