mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.realSize_tail : ∀ {α : Type u_1} (le : α → α → Bool) (s : Batteries.BinomialHeap.Imp.Heap α),
  (Batteries.BinomialHeap.Imp.Heap.tail le s).realSize = s.realSize - 1
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.equiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (p : (X : C) × (Y : C) × (X ≅ Y)),
  CategoryTheory.WalkingIso.equiv.symm p = CategoryTheory.WalkingIso.fromIso p.snd.snd
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.pullback_factors_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] (y : CategoryTheory.Subobject Y) (h : W ⟶ X),
  ((CategoryTheory.Subobject.pullback f).obj y).Factors h ↔ y.Factors (CategoryTheory.CategoryStruct.comp h f)
-- Mathlib.RingTheory.MvPolynomial.Tower
MvPolynomial.aeval_map_algebraMap : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B]
  (x : σ → B) (p : MvPolynomial σ R),
  (MvPolynomial.aeval x) ((MvPolynomial.map (algebraMap R A)) p) = (MvPolynomial.aeval x) p
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries_sum : ∀ {ι : Type u_1} {f : ι → ℕ → ℂ} {S : Finset ι} {s : ℂ},
  (∀ i ∈ S, LSeriesSummable (f i) s) → LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (f : NumberField.mixedEmbedding.realMixedSpace K → ENNReal),
  ∫⁻ (x : NumberField.mixedEmbedding.realMixedSpace K) in (NumberField.mixedEmbedding.polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(NumberField.mixedEmbedding.polarCoordReal K).symm x) =
    ∫⁻ (x : NumberField.mixedEmbedding.realMixedSpace K), f x
-- Mathlib.Algebra.Group.Hom.Defs
instCoeTCZeroHomOfZeroHomClass.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [inst_3 : ZeroHomClass F M N], instCoeTCZeroHomOfZeroHomClass = { coe := ZeroHomClass.toZeroHom }
-- Init.Prelude
/-- Lifts a type to a higher universe level.

`ULift α` wraps a value of type `α`. Instead of occupying the same universe as `α`, which would be
the minimal level, it takes a further level parameter and occupies their maximum. The resulting type
may occupy any universe that's at least as large as that of `α`.

The resulting universe of the lifting operator is the first parameter, and may be written explicitly
while allowing `α`'s level to be inferred.

The related type `PLift` can be used to lift a proposition or type by one level.

Examples:
 * `(Nat : Type 0)`
 * `(ULift Nat : Type 0)`
 * `(ULift Nat : Type 1)`
 * `(ULift Nat : Type 5)`
 * `(ULift.{7} (PUnit : Type 3) : Type 7)`
 -/
ULift : Type s → Type (max s r)
-- Init.Data.Fin.Lemmas
Fin.instLawfulIdentityHMulOfNat : ∀ {n : ℕ} [inst : NeZero n], Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1
-- Lean.Elab.InfoTree.Types
Lean.Elab.OptionInfo.mk.inj : ∀ {stx : Lean.Syntax} {optionName declName : Lean.Name} {stx_1 : Lean.Syntax} {optionName_1 declName_1 : Lean.Name},
  { stx := stx, optionName := optionName, declName := declName } =
      { stx := stx_1, optionName := optionName_1, declName := declName_1 } →
    stx = stx_1 ∧ optionName = optionName_1 ∧ declName = declName_1
-- Mathlib.GroupTheory.Coset.Basic
/-- Equality of two left cosets `a + s` and `b + s`.  -/
LeftAddCosetEquivalence : {α : Type u_1} → [Add α] → Set α → α → α → Prop
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_one_right : ∀ (b : Ordinal.{u_1}), Ordinal.log b 1 = 0
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_self : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → a / a = 1
-- Mathlib.Algebra.Group.Units.Defs
/-- Constructs an inv operation for a `Monoid` consisting only of units.  -/
invOfIsUnit : {M : Type u_1} → [inst : Monoid M] → (∀ (a : M), IsUnit a) → Inv M
-- Mathlib.Order.Filter.Pointwise
Filter.isCentralScalar : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] [inst_1 : SMul αᵐᵒᵖ β] [IsCentralScalar α β],
  IsCentralScalar α (Filter β)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
OpenPartialHomeomorph.restrContDiff_source : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤),
  (OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).source =
    f.source ∩ {x | ContDiffAt 𝕜 n (↑f) x ∧ ContDiffAt 𝕜 n (↑f.symm) (↑f x)}
-- Mathlib.Topology.Category.TopCat.Yoneda
ContinuousMap.yonedaPresheaf'.eq_1 : ∀ (Y : Type w') [inst : TopologicalSpace Y],
  ContinuousMap.yonedaPresheaf' Y =
    { obj := fun X => C(↑(Opposite.unop X), Y),
      map := fun {X Y_1} f => TypeCat.ofHom fun g => g.comp (CategoryTheory.ConcreteCategory.hom f.unop), map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instDecidableLE_1 : {α : Type u_1} → [inst : PartialOrder α] → [DecidableLE α] → DecidableLE (NonemptyInterval α)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_eq_span_of_subset : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A},
  ↑(Submonoid.closure s) ⊆ ↑(Submodule.span R s) → Subalgebra.toSubmodule (Algebra.adjoin R s) = Submodule.span R s
-- Mathlib.Data.Multiset.Range
Multiset.range_add : ∀ (a b : ℕ), Multiset.range (a + b) = Multiset.range a + Multiset.map (fun x => a + x) (Multiset.range b)
-- Mathlib.GroupTheory.OreLocalization.OreSet
OreLocalization.oreSetComm.eq_1 : ∀ {R : Type u_2} [inst : CommMonoid R] (S : Submonoid R),
  OreLocalization.oreSetComm S =
    { ore_right_cancel := ⋯, oreNum := fun r x => r, oreDenom := fun x s => s, ore_eq := ⋯ }
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
/-- Given a path `γ` defined on the manifold with boundary `[a, b]`, its length (as the integral of
the norm of its manifold derivative) coincides with `pathELength` of the lift of `γ` to the real
line, between `a` and `b`.  -/
Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b : ℝ} [h : Fact (a < b)] {γ : ↑(Set.Icc a b) → M},
  ∫⁻ (t : ↑(Set.Icc a b)), ‖(mfderiv% γ t) 1‖ₑ = Manifold.pathELength I (γ ∘ Set.projIcc a b ⋯) a b
-- Mathlib.Algebra.Group.Basic
one_div_div : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), 1 / (a / b) = b / a
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.convex_basis_zero : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [LocallyConvexSpace 𝕜 E],
  (nhds 0).HasBasis (fun s => s ∈ nhds 0 ∧ Convex 𝕜 s) id
-- Lean.CoreM
Lean.Core.liftIOCore : {α : Type} → IO α → Lean.CoreM α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.some : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → (x y : R) → W'.Nonsingular x y → W'.Point
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF →
    ∀ {l : List α} {k k' : α},
      cmp k k' = Ordering.eq →
        k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).get! k' = k
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
PartialEquiv.piecewise.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (e e_1 : PartialEquiv α β) (e_e : e = e_1) (e' e'_1 : PartialEquiv α β)
  (e_e' : e' = e'_1) (s s_1 : Set α) (e_s : s = s_1) (t t_1 : Set β) (e_t : t = t_1)
  {inst : (x : α) → Decidable (x ∈ s)} [inst_1 : (x : α) → Decidable (x ∈ s_1)] {inst_2 : (y : β) → Decidable (y ∈ t)}
  [inst_3 : (y : β) → Decidable (y ∈ t_1)] (H : e.IsImage s t) (H' : e'.IsImage s t),
  e.piecewise e' s t H H' = e_1.piecewise e'_1 s_1 t_1 ⋯ ⋯
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Z.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (S S_1 : FermatLastTheoremForThreeGen.Solution✝ hζ),
  S = S_1 →
    ∀ [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
      FermatLastTheoremForThreeGen.Solution.Z✝ S = FermatLastTheoremForThreeGen.Solution.Z✝ S_1
-- Mathlib.Data.Finset.Basic
Finset.filter_and : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : DecidableEq α]
  (s : Finset α), {a ∈ s | p a ∧ q a} = Finset.filter p s ∩ Finset.filter q s
-- Mathlib.GroupTheory.Index
MonoidHom.finite_iff_finite_ker_range : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G'),
  Finite G ↔ Finite ↥f.ker ∧ Finite ↥f.range
-- Init.Notation
/-- `term` is the builtin syntax category for terms. A term denotes an expression
in lean's type theory, for example `2 + 2` is a term. The difference between
`Term` and `Expr` is that the former is a kind of syntax, while the latter is
the result of elaboration. For example `by simp` is also a `Term`, but it elaborates
to different `Expr`s depending on the context.  -/
Lean.Parser.Category.term : Lean.Parser.Category
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_le_size_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)}, m.size ≤ (m.insertMany l).size
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring of a `CommSemiring` is a `CommSemiring`.  -/
Subsemiring.toCommSemiring : {R : Type u_1} → [inst : CommSemiring R] → (s : Subsemiring R) → CommSemiring ↥s
-- Mathlib.Topology.UniformSpace.ProdApproximation
/-- The natural bilinear map sending `f, g` to the function `(x, y) ↦ f x * g y` on `X × Y`.  -/
ContinuousMap.prodMul : {X : Type u_5} →
  {Y : Type u_6} →
    {R : Type u_7} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] → [inst_4 : IsTopologicalRing R] → C(X, R) →ₗ[R] C(Y, R) →ₗ[R] C(X × Y, R)
-- Mathlib.Order.Hom.Basic
OrderIso.symm_bijective : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β], Function.Bijective OrderIso.symm
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.mem_range_veblen_iff_le_invVeblen₁ : ∀ {o x : Ordinal.{u}}, Ordinal.omega0 ^ x ∈ Set.range (Ordinal.veblen o) ↔ o ≤ x.invVeblen₁
-- Lean.Elab.MutualInductive
/-- Assignment to do once all level metavariables in `Level` are converted to parameters.  -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ResultingUniverseResult.assign? : Lean.Elab.Command.ResultingUniverseResult✝ → Option (Lean.LMVarId × Lean.Level)
-- Mathlib.Combinatorics.Tiling.Tile
/-- An alternative extensionality principle for `PlacedTile` that avoids `HEq`, using existence of a
common group element.  -/
DiscreteTiling.PlacedTile.ext_iff_of_exists : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {pt₁ pt₂ : DiscreteTiling.PlacedTile ps},
  pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ ∃ g, ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
-- Std.Http.Data.Body.Full
/-- Builds a request with a text body.
Sets `Content-Type: text/plain; charset=utf-8`.
 -/
Std.Http.Request.Builder.text : Std.Http.Request.Builder → String → Std.Async.Async (Std.Http.Request Std.Http.Body.Full)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.eq_true_of_isValid : ∀ (ctx : Nat.Internal.Linear.Context) {c : Nat.Internal.Linear.PolyCnstr},
  c.isValid = true → Nat.Internal.Linear.PolyCnstr.denote ctx c = True
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.polarization_apply_eq_zero_iff : ∀ {ι : 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 : Fintype ι]
  (m : M), P.Polarization m = 0 ↔ P.RootForm m = 0
-- Mathlib.GroupTheory.Congruence.Defs
Con.commMagma.eq_1 : ∀ {M : Type u_4} [inst : CommMagma M] (c : Con M), c.commMagma = { toMul := c.hasMul, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₁ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.contractibleTriangleFunctor C).map f).hom₁ = f
-- Init.WF
PSigma.SkipLeft : (α : Type u) → {β : Type v} → (β → β → Prop) → (_ : α) ×' β → (_ : α) ×' β → Prop
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_intMax : ∀ {i : ℕ} (w : ℕ), (BitVec.intMax w).getLsbD i = decide (i + 1 < w)
-- Mathlib.Algebra.Order.SuccPred
Order.add_one_le_iff : ∀ {α : Type u_1} {x y : α} [inst : Preorder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α] [NoMaxOrder α],
  x + 1 ≤ y ↔ x < y
-- Init.Data.Vector.Lemmas
Vector.eq_or_ne_mem_of_mem : ∀ {α : Type u_1} {n : ℕ} {a b : α} {xs : Vector α n}, a ∈ xs.push b → a = b ∨ a ≠ b ∧ a ∈ xs
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.ι₁_ι : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.unionProd.ι₁ S T) (S.unionProd T).ι =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X T.ι
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- The canonical quotient of the path category of a category
is equivalent to the original category.  -/
CategoryTheory.quotientPathsEquiv : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Quotient (CategoryTheory.pathsHomRel C) ≌ C
-- Mathlib.Topology.Connected.PathComponentOne
OpenNormalAddSubgroup.pathComponentZero_carrier : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyPathConnectedSpace G], ↑(OpenNormalAddSubgroup.pathComponentZero G) = pathComponent 0
-- Lean.Message
/-- Produces a labeled note that can be appended to an error message.
 -/
Lean.MessageData.note : Lean.MessageData → Lean.MessageData
-- Init.Data.UInt.Bitwise
UInt64.and_le_right : ∀ {a b : UInt64}, a &&& b ≤ b
-- Mathlib.Data.Rel
SetRel.isRefl_iInter : ∀ {α : Type u_1} {ι : Sort u_5} {R : ι → SetRel α α} [∀ (i : ι), (R i).IsRefl], SetRel.IsRefl (⋂ i, R i)
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.FreeMonoidal.μIso_hom_freeMk_tmul_freeMk : ∀ (R : Type u) [inst : CommRing R] {X Y : Type u} (x : X) (y : Y),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.FreeMonoidal.μIso R X Y).hom)
      (ModuleCat.freeMk x ⊗ₜ[R] ModuleCat.freeMk y) =
    ModuleCat.freeMk (x, y)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.sub_iff_right : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =O[l] g → ((fun x => f₁ x - f₂ x) =O[l] g ↔ f₂ =O[l] g)
-- Mathlib.Topology.Instances.ENat
ENat.tendsto_natCast_nhds_top : Filter.Tendsto Nat.cast Filter.atTop (nhds ⊤)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_mul_le : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W),
  cs.length (w₁ * w₂) ≤ cs.length w₁ + cs.length w₂
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_dvd : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {b : β}, b ∈ s → s.gcd f ∣ f b
-- Mathlib.Tactic.TFAE
/-- See `haveIdLhs`.

We omit `many (ppSpace >> letIdBinder)`, as it makes no sense to add extra arguments to a
`tfae_have` decl.  -/
Mathlib.Tactic.TFAE.Parser.tfaeHaveIdLhs : Lean.Parser.Parser
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  (f : CompactlySupportedContinuousMap α β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Init.Data.Float.Float
/-- Computes the arc sine (inverse sine) of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`asin`.
 -/
Float.asin : Float → Float
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.right.eq_1 : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (X : CategoryTheory.Arrow T), X.right = X.right
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue_eq_get_getValue? : ∀ {α : Type u} [inst : BEq α] {β : Type v} {a : α} {l : List ((_ : α) × β)}
  {h : Std.Internal.List.containsKey a l = true},
  Std.Internal.List.getValue a l h = (Std.Internal.List.getValue? a l).get ⋯
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), Valued.v x.toCompletion = Valued.v x
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.iInf_ker_root'_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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),
  ⨅ i, LinearMap.ker (P.root' i) = (Submodule.span R (Set.range P.root')).dualCoannihilator
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_one : ∀ (R : Type u_1) {A : Type u_2} (M : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M], LinearMap.baseChange A 1 = 1
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.brecOn_1.eq : ∀ {motive_1 : Lean.Meta.Match.Pattern → Sort u} {motive_2 : List Lean.Meta.Match.Pattern → Sort u}
  (t : List Lean.Meta.Match.Pattern) (F_1 : (t : Lean.Meta.Match.Pattern) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Meta.Match.Pattern) → Lean.Meta.Match.Pattern.below_1 t → motive_2 t),
  Lean.Meta.Match.Pattern.brecOn_1 t F_1 F_2 = F_2 t (Lean.Meta.Match.Pattern.brecOn_1.go t F_1 F_2).2
-- Mathlib.Data.Multiset.Lattice
Multiset.le_sup : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Multiset α} {a : α}, a ∈ s → a ≤ s.sup
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- If a subset `A` of the `mixedSpace` is symmetric at real places, then its volume is
`2^ nrRealPlaces K` times the volume of its `plusPart`.  -/
NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart : ∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)},
  (∀ (x : NumberField.mixedEmbedding.mixedSpace K), x ∈ A ↔ (fun w => ‖x.1 w‖, x.2) ∈ A) →
    ∀ [inst_1 : NumberField K],
      MeasurableSet A →
        MeasureTheory.volume A =
          2 ^ NumberField.InfinitePlace.nrRealPlaces K * MeasureTheory.volume (NumberField.mixedEmbedding.plusPart A)
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The automorphism group of `F` is multiplicatively isomorphic to
(the multiplicative opposite of) the limit over the automorphism groups of
the Galois objects.  -/
CategoryTheory.PreGaloisCategory.autMulEquivAutGalois : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          CategoryTheory.Aut F ≃* (CategoryTheory.PreGaloisCategory.AutGalois F)ᵐᵒᵖ
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Let `u₁`, `u₂` be two uniform structures on `γ` and `𝔖₁ 𝔖₂ : Set (Set α)`. If `u₁ ≤ u₂` and
`𝔖₂ ⊆ 𝔖₁` then `𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂)`.  -/
UniformOnFun.mono : ∀ {α : Type u_1} {γ : Type u_3} ⦃u₁ u₂ : UniformSpace γ⦄,
  u₁ ≤ u₂ → ∀ ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄, 𝔖₂ ⊆ 𝔖₁ → UniformOnFun.uniformSpace α γ 𝔖₁ ≤ UniformOnFun.uniformSpace α γ 𝔖₂
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- `weightedVSub` gives equal results for two families of weights and two families of points
that are equal on `s`.  -/
Finset.weightedVSub_congr : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w₁ w₂ : ι → k},
  (∀ i ∈ s, w₁ i = w₂ i) → ∀ {p₁ p₂ : ι → P}, (∀ i ∈ s, p₁ i = p₂ i) → (s.weightedVSub p₁) w₁ = (s.weightedVSub p₂) w₂
-- Init.Data.SInt.Bitwise
Int32.and_comm : ∀ (a b : Int32), a &&& b = b &&& a
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.instPolynomial : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S], Algebra.FiniteType R (Polynomial S)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono'_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φH =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).H
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α),
  Std.DHashMap.Internal.AssocList.get? a Std.DHashMap.Internal.AssocList.nil = none
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      ¬r.size > Std.DTreeMap.Internal.delta * l.size → l.size > Std.DTreeMap.Internal.delta * r.size → Sort u_3)
  (size : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h : ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size)
  (h_1 : (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size)
  (h_1_1 :
    (h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size) →
      (h_2 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf h h_2)
  (h_2 :
    (size : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (h : ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size) →
              (h_2 : (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr) h h_2),
  (match Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_1 with
    | Std.DTreeMap.Internal.Impl.leaf, h, h_3 => h_1_1 h h_3
    | Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_3 => h_2 size lk lv ll lr h h_3) =
    h_2 size lk lv ll lr h h_1
-- Init.Data.BitVec.Lemmas
BitVec.and_not_self : ∀ {w : ℕ} (x : BitVec w), x &&& ~~~x = 0