mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_succ_div_top : ∀ {M : Type u_4} (f : ℕ → M) {m n : ℕ} [inst : CommGroup M],
  m ≤ n → (∏ i ∈ Finset.Ico m (n + 1), f i) / f n = ∏ i ∈ Finset.Ico m n, f i
-- Mathlib.Data.Nat.Bitwise
Nat.bitwise_of_ne_zero : ∀ {f : Bool → Bool → Bool} {n m : ℕ},
  n ≠ 0 → m ≠ 0 → Nat.bitwise f n m = Nat.bit (f n.bodd m.bodd) (Nat.bitwise f (n / 2) (m / 2))
-- Init.Data.BitVec.Basic
/-- Shifts a bitvector to the right. This is a logical right shift - the high bits are filled with
zeros.

As a numeric operation, this is equivalent to `x / 2^s`, rounding down.

SMT-LIB name: `bvlshr` except this operator uses a `Nat` shift value.
 -/
BitVec.ushiftRight : {n : ℕ} → BitVec n → ℕ → BitVec n
-- Std.Data.HashSet.Raw
/-- Inserts multiple mappings into the hash set by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the first occurrence takes precedence.

Note: this precedence behavior is true for `HashSet` and `HashSet.Raw`. The `insertMany` function on
`HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw` behaves differently: it will prefer the last
appearance.
 -/
Std.HashSet.Raw.insertMany : {α : Type u} → [BEq α] → [Hashable α] → {ρ : Type v} → [ForIn Id ρ α] → Std.HashSet.Raw α → ρ → Std.HashSet.Raw α
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The 2-morphism defined by the following pasting diagram:
```
        a －－－－－－ ▸ a
       ◥  ＼     η      ◥
  g ／      ＼ f     ／ g
  ／    ε      ◢   ／
b －－－－－－ ▸ b
```
 -/
CategoryTheory.Bicategory.rightZigzag : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          (CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g) →
            (CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b) →
              (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id a) ⟶
                CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id b) g)
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.ofQuotientStabilizer_mk : ∀ (G : Type u) {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (x : X) (g : G),
  AddAction.ofQuotientStabilizer G x ↑g = g +ᵥ x
-- Init.Data.Bool
Bool.and_comm : ∀ (x y : Bool), (x && y) = (y && x)
-- Aesop.Tree.Data
Aesop.GoalId.instLT : LT Aesop.GoalId
-- Mathlib.RingTheory.PowerSeries.Order
/-- If the `n`th coefficient of a formal power series is nonzero,
then the order of the power series is less than or equal to `n`.  -/
PowerSeries.order_le : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} (n : ℕ), (PowerSeries.coeff n) φ ≠ 0 → φ.order ≤ ↑n
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_isBasis'_iff : ∀ {α : Type u_1} {M : Matroid α} {I D X : Set α}, (M.delete D).IsBasis' I X ↔ M.IsBasis' I (X \ D)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.vadd_Icc : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [AddLeftReflectLE α]
  [ExistsAddOfLE α] (a b c : α), a +ᵥ Set.Icc b c = Set.Icc (a + b) (a + c)
-- Init.Data.Vector.Lemmas
Vector.toArray_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n), (Vector.mk xs h).toArray = xs
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.compHom_id : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y), f.compHom (CategoryTheory.CategoryStruct.id Y) = f
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_slice : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} (h : p₀ ≤ p₁) (p : (s.slice p₀ p₁ h).Pos),
  p.Splits (s.slice p₀ (String.Slice.Pos.ofSlice p) ⋯).copy (s.slice (String.Slice.Pos.ofSlice p) p₁ ⋯).copy
-- Std.Http.Data.Version
/-- `HTTP/1.1`
 -/
Std.Http.Version.v11 : Std.Http.Version
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.isNormal_ord : Order.IsNormal Cardinal.ord
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.instIsTopologicalSemiring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Module R A] [IsTopologicalSemiring A] (s : NonUnitalSubalgebra R A), IsTopologicalSemiring ↥s
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.mem_bipartiteBelow : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {b : β} [inst : (a : α) → Decidable (r a b)] {a : α},
  a ∈ Finset.bipartiteBelow r s b ↔ a ∈ s ∧ r a b
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The right dual of the object `X`.  -/
CategoryTheory.«term_ᘁ» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Valuation.ValuationRing
Function.Surjective.valuationRing : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [PreValuationRing R] [inst_2 : CommRing S]
  [inst_3 : IsDomain S] (f : R →+* S), Function.Surjective ⇑f → ValuationRing S
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.applyAsHom_apply : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : CommMonoid G] {A : Rep.{u_1, u, v} k G} (g : G) (x : ↑A),
  (Rep.Hom.hom (A.applyAsHom g)) x = (A.ρ g) x
-- Mathlib.Topology.Order.DenselyOrdered
/-- The closure of the interval `(-∞, a)` is the closed interval `(-∞, a]`, unless `a` is a bottom
element.  -/
closure_Iio' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (Set.Iio a).Nonempty → closure (Set.Iio a) = Set.Iic a
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The limit cone `LightProfinite.limitCone F` is indeed a limit cone.  -/
LightProfinite.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.CountableCategory J] →
      (F : CategoryTheory.Functor J LightProfinite) → CategoryTheory.Limits.IsLimit (LightProfinite.limitCone F)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- The underlying inverse of `pullbackDiagonalIso`  -/
CategoryTheory.Limits.pullbackDiagonalMapIso.inv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
        {U V₁ V₂ : C} →
          (f : X ⟶ Y) →
            (i : U ⟶ Y) →
              (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) →
                (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) →
                  [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂] →
                    CategoryTheory.Limits.pullback i₁ i₂ ⟶
                      CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal f)
                        (CategoryTheory.Limits.pullback.map
                          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
                          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
                          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
                          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_add_fmod : ∀ (a b : ℤ), b * a.fdiv b + a.fmod b = a
-- Mathlib.Algebra.Lie.TensorProduct
TensorProduct.LieModule.lie_tmul_right : ∀ {R : Type u} [inst : CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (x : L) (m : M) (n : N), ⁅x, m ⊗ₜ[R] n⁆ = ⁅x, m⁆ ⊗ₜ[R] n + m ⊗ₜ[R] ⁅x, n⁆
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.degMatrix.congr_simp : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ {inst_1 : DecidableRel G.Adj} [inst_2 : DecidableRel G_1.Adj] {inst_3 : DecidableEq V} [inst_4 : DecidableEq V]
      [inst_5 : AddMonoidWithOne R] (a a_1 : V),
      a = a_1 → ∀ (a_2 a_3 : V), a_2 = a_3 → SimpleGraph.degMatrix R G a a_2 = SimpleGraph.degMatrix R G_1 a_1 a_3
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_zero : Ordinal.lift.{u_2, u_1} 0 = 0
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.orderHom_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {N : Type u_2}
  [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N] (f : M →+o N) (a : M),
  (ArchimedeanClass.orderHom f) (ArchimedeanClass.mk a) = ArchimedeanClass.mk (f a)
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Given a valuation `x` of the variable in an `R`-algebra `A`, the bijection induced by the unique
`R`-algebra homomorphism from `R[X]` to `A` sending `X` to `x`.  -/
Polynomial.aevalEquiv : (R : Type u) →
  (A : Type z) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A ≃ (Polynomial R →ₐ[R] A)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
dvd_iff_padicValNat_ne_zero : ∀ {p n : ℕ} [Fact (Nat.Prime p)], n ≠ 0 → (p ∣ n ↔ padicValNat p n ≠ 0)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinf_X₃ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupHomology.H1CoresCoinf A S).X₃ = groupHomology.H1 (A.quotientToCoinvariants S)
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_add_cosh : ∀ (x : ℝ), Real.sinh x + Real.cosh x = Real.exp x
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (homEquiv homEquiv_1 : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (e_homEquiv : homEquiv = homEquiv_1)
  (unit unit_1 : CategoryTheory.Functor.id C ⟶ F.comp G) (e_unit : unit = unit_1)
  (counit counit_1 : G.comp F ⟶ CategoryTheory.Functor.id D) (e_counit : counit = counit_1)
  (homEquiv_unit :
    ∀ {X : C} {Y : D} {f : F.obj X ⟶ Y}, (homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (unit.app X) (G.map f))
  (homEquiv_counit :
    ∀ {X : C} {Y : D} {g : X ⟶ G.obj Y},
      (homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (counit.app Y)),
  { homEquiv := homEquiv, unit := unit, counit := counit, homEquiv_unit := homEquiv_unit,
      homEquiv_counit := homEquiv_counit } =
    { homEquiv := homEquiv_1, unit := unit_1, counit := counit_1, homEquiv_unit := ⋯, homEquiv_counit := ⋯ }
-- Mathlib.Algebra.Homology.Bifunctor
/-- Auxiliary definition for `mapBifunctorHomologicalComplex`.  -/
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] →
                  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                    {I₁ : Type u_4} →
                      {I₂ : Type u_5} →
                        {c₁ : ComplexShape I₁} →
                          (c₂ : ComplexShape I₂) →
                            [F.PreservesZeroMorphisms] →
                              [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                HomologicalComplex C₁ c₁ →
                                  CategoryTheory.Functor (HomologicalComplex C₂ c₂) (HomologicalComplex₂ D c₁ c₂)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.add_measure : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s : Set α} {μ ν : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε],
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn f s ν → MeasureTheory.IntegrableOn f s (μ + ν)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.Submartingale.sum_mul_upcrossingStrat_le : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    ∫ (x : Ω), (∑ k ∈ Finset.range n, MeasureTheory.upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
      ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_add : ∀ (a b : UInt8), (a + b).toUInt64 = (a.toUInt64 + b.toUInt64) % 256
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.degree_freeMonic : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ) [Nontrivial R], (Polynomial.freeMonic R n).degree = ↑n
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- `Complex.arg` and `Circle.exp ∘ (↑)` define an equivalence between `Circle` and `(-π, π]`.  -/
Circle.argEquiv : Circle ≃ ↑(Set.Ioc (-Real.pi) Real.pi)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- The penultimate vertex of a walk, or the only vertex in a nil walk.  -/
SimpleGraph.Walk.penultimate : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → V
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Node.id : Mathlib.Tactic.Widget.StringDiagram.IdNode → Mathlib.Tactic.Widget.StringDiagram.Node
-- Mathlib.NumberTheory.LSeries.Dirichlet
DirichletCharacter.delta_mul : ∀ {n : ℕ} (χ : DirichletCharacter ℂ n), (LSeries.delta * fun n_1 => χ ↑n_1) = LSeries.delta
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instOfNatWithTopENat_2 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I 3 M], IsManifold I 2 M
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.leftInverse_lcomapDomain_mapDomain : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {β : Type u_9} (f : α → β) (hf : Function.Injective f),
  Function.LeftInverse (⇑(Finsupp.lcomapDomain f hf)) (Finsupp.mapDomain f)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.strictLimitsClosureIter.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {β : Type w'} [inst_2 : LinearOrder β]
  [inst_3 : SuccOrder β] [inst_4 : WellFoundedLT β] (b : β),
  P.strictLimitsClosureIter J b = transfiniteIterate (fun Q => Q.strictLimitsClosureStep J) b P
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Symbols.eq_1 : ∀ (L : FirstOrder.Language), L.Symbols = ((l : ℕ) × L.Functions l ⊕ (l : ℕ) × L.Relations l)
-- Mathlib.RingTheory.Localization.AsSubring
Localization.isLocalization_range_mapToFractionRing : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] (B : Type u_3) [inst_4 : CommRing B] [inst_5 : Algebra A B]
  [inst_6 : IsLocalization S B] (hS : S ≤ nonZeroDivisors A),
  IsLocalization S ↥(Localization.mapToFractionRing K S B hS).range
-- Mathlib.Order.RelSeries
RelSeries.toList_getElem : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) {i : ℕ} (hi : i < p.toList.length), p.toList[i] = p.toFun ⟨i, ⋯⟩
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.length_map : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [inst_1 : Monad m]
  [inst_2 : Std.IteratorLoop α m m] [Std.Iterators.Finite α m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m]
  {it : Std.IterM m β} {f : β → β'}, (Std.IterM.map f it).length = it.length
-- Mathlib.RingTheory.Ideal.Maps
Ideal.gc_map_comap : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S], GaloisConnection (Ideal.map f) (Ideal.comap f)
-- Mathlib.Topology.UniformSpace.Defs
exists_mem_nhds_ball_subset_of_mem_nhds : ∀ {α : Type ua} [inst : UniformSpace α] {a : α} {U : Set α},
  U ∈ nhds a → ∃ V ∈ nhds a, ∃ t ∈ uniformity α, ∀ a' ∈ V, UniformSpace.ball a' t ⊆ U
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.IsMarkovKernel.comapRight : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : γ → β} (κ : ProbabilityTheory.Kernel α β) (hf : MeasurableEmbedding f),
  (∀ (a : α), (κ a) (Set.range f) = 1) → ProbabilityTheory.IsMarkovKernel (κ.comapRight hf)
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.addSubgroupCongr.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H = K),
  AddEquiv.addSubgroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β} {f : Option β → Option β},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.alter m k f) k fallback =
    (f (Std.ExtDHashMap.Const.get? m k)).getD fallback
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.val_inv_toUnits_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(pinGroup Q)), ↑(pinGroup.toUnits x)⁻¹ = ↑x⁻¹
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL!.match_5.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (l : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)),
  l = Std.DTreeMap.Internal.Impl.leaf →
    (match l with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr => h_2 ls lk lv ll lr) ≍
      h_1 ()
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getElimNameInfo.throwUnsupportedInductionType : Lean.Name → String → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.MeasureTheory.Measure.Decomposition.Hahn
MeasureTheory.IsHahnDecomposition.le_on : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsHahnDecomposition μ ν s → μ.restrict s ≤ ν.restrict s
-- Mathlib.Order.LiminfLimsup
/-- The `blimsup` of a function `u` along a filter `f`, bounded by a predicate `p`, is the infimum
of the `a` such that the inequality `u x ≤ a` eventually holds for `f`, whenever `p x` holds.  -/
Filter.blimsup : {α : Type u_1} → {β : Type u_2} → [ConditionallyCompleteLattice α] → (β → α) → Filter β → (β → Prop) → α
-- Mathlib.RingTheory.Localization.FractionRing
/-- Given a ring `A` and a localization map to a fraction ring
`f : A →+* K`, we get an `A`-isomorphism between the fraction ring of `A` as a quotient
type and `K`.  -/
FractionRing.algEquiv : (A : Type u_4) →
  [inst : CommRing A] →
    (K : Type u_6) → [inst_1 : CommRing K] → [inst_2 : Algebra A K] → [IsFractionRing A K] → FractionRing A ≃ₐ[A] K
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.mem_smul_pointwise_iff_exists : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G] (m : G) (a : α)
  (S : Subgroup G), m ∈ a • S ↔ ∃ s ∈ S, a • s = m
-- Mathlib.Order.Heyting.Basic
compl_compl_inf_distrib : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a b : α), (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The edist to a union is the minimum of the edists  -/
Metric.infEDist_union : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
  Metric.infEDist x (s ∪ t) = min (Metric.infEDist x s) (Metric.infEDist x t)
-- Lean.Meta.IndPredBelow
/-- A new declaration of type `∀ x y z, <nth motive> ... (h x y z)` for all `h ∈ vars`  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl.motive : Lean.LocalDecl → ℕ → Array Lean.FVarId → Lean.Meta.IndPredBelow.NewDecl✝
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.isAddUnit_of_mem_ofAddUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M}, x ∈ S.ofAddUnits → IsAddUnit x
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity_assoc : ∀ {X Y Z T : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T)
  {Z_1 : CategoryTheory.Functor T.Modules X.Modules}
  (h_1 :
    AlgebraicGeometry.Scheme.Modules.pullback
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Modules.pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (AlgebraicGeometry.Scheme.Modules.pullbackComp g h).inv
          (AlgebraicGeometry.Scheme.Modules.pullback f))
        (CategoryTheory.CategoryStruct.comp
          ((AlgebraicGeometry.Scheme.Modules.pullback h).associator (AlgebraicGeometry.Scheme.Modules.pullback g)
              (AlgebraicGeometry.Scheme.Modules.pullback f)).hom
          (CategoryTheory.CategoryStruct.comp
            ((AlgebraicGeometry.Scheme.Modules.pullback h).whiskerLeft
              (AlgebraicGeometry.Scheme.Modules.pullbackComp f g).hom)
            (CategoryTheory.CategoryStruct.comp
              (AlgebraicGeometry.Scheme.Modules.pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom h_1)))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h_1
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero : ∀ {R : Type u_1} {K : Type u_4} [inst : CommSemiring R] [inst_1 : Field K] [inst_2 : Algebra R K],
  Function.Injective ⇑(algebraMap R K) →
    ∀ {p : Polynomial R} {r s : R},
      (Polynomial.aeval ((algebraMap R K) r / (algebraMap R K) s)) p = 0 →
        s ∈ nonZeroDivisors R → (Polynomial.aeval ((algebraMap R K) r)) (p.scaleRoots s) = 0
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_ofSubsingleton_id_le : ∀ (𝕜 : Type u) {ι : Type v} (G : Type wG) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : Fintype ι] [inst_4 : Subsingleton ι] (i : ι),
  ‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ ≤ 1
-- Std.Time.Zoned.ZoneRules
/-- The local time type associated with this transition.
 -/
Std.Time.TimeZone.Transition.localTimeType : Std.Time.TimeZone.Transition → Std.Time.TimeZone.LocalTimeType
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_update_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ) {a : R},
  a ≠ 0 → (p.update n a).support = insert n p.support
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).inv.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
-- Mathlib.Data.Set.Basic
Set.ofPred_false : ∀ {α : Type u}, {_a | False} = ∅
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `FunLike.coe_sub`. -/
ContinuousLinearMap.coe_sub' : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Sub F] [inst_2 : Sub β]
  [IsSubApply F α β] (f g : F), ⇑(f - g) = ⇑f - ⇑g