mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get? k = none
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeffAddEquiv_symm_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (coeff : M →₀ R),
  MonoidAlgebra.coeffAddEquiv.symm coeff = MonoidAlgebra.ofCoeff coeff
-- Lean.Elab.Term.TermElabM
/-- Execute `x` and then tries to solve pending universe constraints.
Note that, stuck constraints will not be discarded.
 -/
Lean.Elab.Term.universeConstraintsCheckpoint : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Std.Http.Data.Request
/-- Builds an HTTP Request.
 -/
Std.Http.Request.Builder : Type
-- Lean.Elab.Coinductive
/-- Modifiers from the original `InductiveView` -/
Lean.Elab.Command.CoinductiveElabData.modifiers : Lean.Elab.Command.CoinductiveElabData → Lean.Elab.Modifiers
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of Haar measures**:
Given two Haar measures, they coincide in the following sense: they give the same value to open
sets, up to the multiplicative constant `haarScalarFactor μ' μ`.  -/
MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isOpen : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : μ'.IsHaarMeasure] {s : Set G}, IsOpen s → μ' s = μ'.haarScalarFactor μ • μ s
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ),
  ↑(Topology.RelCWComplex.skeletonLT C ↑n) ∪ ⋃ j, Topology.RelCWComplex.closedCell n j =
    ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
-- Init.Data.Option.Lemmas
Option.max_some_guard : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] {x : α} {p : α → Bool}, some x ⊔ Option.guard p x = some x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k' fallback : α},
  (k == k') = true → Std.Internal.List.getKeyD k l fallback = Std.Internal.List.getKeyD k' l fallback
-- Lean.Server.Requests
Lean.Server.LspResponse : Type → Type
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The codomain of a 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₁.tgt : Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Obj
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrange_prodMap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Type u_5} {N' : Type u_6}
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* N) (g : M' →* N'),
  MonoidHom.mrange (f.prodMap g) = (MonoidHom.mrange f).prod (MonoidHom.mrange g)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The associator as a term of `normalExpr`.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.associatorM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.RingTheory.PowerSeries.CoeffMulMem
PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal' : ∀ {A : Type u_1} [inst : Semiring A] {I : Ideal A} {f g : PowerSeries A} [I.IsTwoSided],
  (∀ (i : ℕ), (PowerSeries.coeff i) f ∈ I) → ∀ (i : ℕ), (PowerSeries.coeff i) (f * g) ∈ I
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_finsupp_lift_of_infinite : ∀ (α : Type u) (β : Type v) [Infinite α] [inst : Zero β] [Nontrivial β],
  Cardinal.mk (α →₀ β) = max (Cardinal.lift.{v, u} (Cardinal.mk α)) (Cardinal.lift.{u, v} (Cardinal.mk β))
-- Init.Data.Fin.Lemmas
Fin.coe_castAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), ↑(Fin.castAdd m i) = ↑i
-- Mathlib.RingTheory.LocalProperties.Basic
eq_zero_of_localization : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R),
  (∀ (J : Ideal R) (x : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0) → r = 0
-- Mathlib.Logic.IsEmpty.Defs
Function.isEmpty : ∀ {α : Sort u} {β : Sort v} [IsEmpty β] (f : α → β), IsEmpty α
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence is uniformly Cauchy if eventually all of its pairwise differences are
uniformly bounded  -/
UniformCauchySeqOn : {α : Type u_1} → {β : Type u_2} → {ι : Type u_4} → [UniformSpace β] → (ι → α → β) → Filter ι → Set α → Prop
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_apply : ∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁] (x : M₁) (r : R₁),
  (ContinuousLinearMap.toSpanSingleton R₁ x) r = r • x
-- Lean.Expr
Lean.Expr.hashEx : Lean.Expr → UInt64
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.mk : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} →
                  {B₂ : LinearMap.BilinForm R M₂} →
                    (toLinearEquiv : M₁ ≃ₗ[R] M₂) →
                      (∀ (n m : M₁), (B₂ ((↑toLinearEquiv).toFun n)) ((↑toLinearEquiv).toFun m) = (B₁ n) m) →
                        B₁.IsometryEquiv B₂
-- Lean.Parser.Basic
Lean.Parser.checkColEqFn : String → Lean.Parser.ParserFn
-- Mathlib.Order.Hom.Bounded
TopHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β] (f : TopHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_top' := ⋯ }
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
tendsto_closedBall_smallSets : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α), Filter.Tendsto (Metric.closedBall x) (nhds 0) (nhds x).smallSets
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_lt : ∀ {a b : ℝ}, a < b → a.sigmoid < b.sigmoid
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_le_opow_right : ∀ {a b c : Ordinal.{u_1}}, 0 < a → b ≤ c → a ^ b ≤ a ^ c
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.det_lapMatrix_eq_zero : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  [h : Nonempty V], (SimpleGraph.lapMatrix ℝ G).det = 0
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_div : ∀ (a b : UInt64), a < 4294967296 → b < 4294967296 → (a / b).toUInt32 = a.toUInt32 / b.toUInt32
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] (i : ι) (x : M i),
  Pi.single i x = Function.update 0 i x
-- Mathlib.Data.Set.Function
Set.LeftInvOn.prodMap : ∀ {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {f₁ : α₁ → β₁}
  {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂},
  Set.LeftInvOn g₁ f₁ s₁ →
    Set.LeftInvOn g₂ f₂ s₂ → Set.LeftInvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.congr_set_fun : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s t : Set H} {x : H} {f g : H → H'}, s =ᶠ[nhds x] t → f =ᶠ[nhds x] g → (P f s x ↔ P g t x)
-- Lean.Server.References
/-- Map from each module to all of its direct imports.
The current references in a file worker take precedence over those in .ilean files.
 -/
Lean.Server.References.AllDirectImportsMap : Type
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctor_map_f : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ)
  {X Y : CochainComplex C ℤ} (φ : X ⟶ Y) (x : ℤ), ((CochainComplex.shiftFunctor C n).map φ).f x = φ.f (x + n)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_inv_hom_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) (k : c ⟶ d),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η.inv k))
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η.hom k)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h k))
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U), hU.fromSpec = hU.fromSpec
-- Mathlib.Probability.StrongLaw
/-- The truncated and non-truncated versions of `Xᵢ` have the same asymptotic behavior, as they
almost surely coincide at all but finitely many steps. This follows from a probability computation
and Borel-Cantelli.  -/
ProbabilityTheory.strong_law_aux5 : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) MeasureTheory.volume →
    (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) →
      (∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) →
        ∀ᵐ (ω : Ω),
          (fun n =>
              ∑ i ∈ Finset.range n, ProbabilityTheory.truncation (X i) (↑i) ω -
                ∑ i ∈ Finset.range n, X i ω) =o[Filter.atTop]
            fun n => ↑n
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- `A.det` is invertible if `A` has a left inverse.  -/
Matrix.detInvertibleOfLeftInverse : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A B : Matrix n n α) → B * A = 1 → Invertible A.det
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.LFunctionTrivChar₁.eq_1 : ∀ (n : ℕ) [inst : NeZero n],
  DirichletCharacter.LFunctionTrivChar₁ n =
    Function.update (fun s => (s - 1) * DirichletCharacter.LFunctionTrivChar n s) 1 (∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹))
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A submagma of a left cancellative magma inherits left cancellation.  -/
MulMemClass.isLeftCancelMul : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] [IsLeftCancelMul M]
  (S : A), IsLeftCancelMul ↥S
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.mem_support_ind : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M)
  (hx : x ∈ s), x ∈ Function.support ↑(fs.toFun (fs.ind x hx))
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N], Function.Surjective ⇑AddMonoid.Coprod.fst
-- Mathlib.Logic.Basic
exists_iff_of_forall : ∀ {p : Prop} {q : p → Prop}, (∀ (h : p), q h) → ((∃ (h : p), q h) ↔ p)
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'_epsilon : ∀ {α : Type u_1}, RegularExpression.matches' 1 = 1
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- If there exists a pointwise right Kan extension of `F` along `L`,
then `L.ran.obj G` is a pointwise right Kan extension of `F`.  -/
CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounit : {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] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] →
                (F : CategoryTheory.Functor C H) →
                  [L.HasPointwiseRightKanExtension F] →
                    (CategoryTheory.Functor.RightExtension.mk (L.ran.obj F)
                        (L.ranCounit.app F)).IsPointwiseRightKanExtension
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {F : Type u_6} [inst_7 : FunLike F A B] [inst_8 : CoalgHomClass F R A B] (f : F), ⇑↑f = ⇑f
-- Mathlib.Tactic.DepRewrite
/-- We use a cache entry iff the upcoming traversal would abstract exactly the same occurrences
as the cached traversal.  -/
Mathlib.Tactic.DepRewrite.canUseCache : ℕ → ℕ → ℕ → Lean.Meta.Occurrences → Bool
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionUnitIso`, the structural isomorphism `- ⊙ᵣ 𝟙_ C  ≅ -`,
allowing one to specify the acting category.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.«termρᵣ[_]» : Lean.ParserDescr
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.instInhabitedResult.default : Lean.Meta.MonadSimp.Result
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α} {v : β k}, (cmp t.maxKey! (t.insertIfNew k v).maxKey!).isLE = true
-- Mathlib.CategoryTheory.Sites.LocalProperties
/-- A sheaf morphism is an isomorphism iff it becomes one after pulling back along each
element of a covering family.  -/
CategoryTheory.Sheaf.isIso_iff_of_coversTop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.GrothendieckTopology C}
  {A : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {ι : Type u_3} {X : ι → C},
  K.CoversTop X →
    ∀ {F G : CategoryTheory.Sheaf K A} (f : F ⟶ G),
      CategoryTheory.IsIso f ↔ ∀ (i : ι), CategoryTheory.IsIso ((K.overPullback A (X i)).map f)
-- Mathlib.Analysis.Normed.Ring.Basic
Finset.norm_prod_le' : ∀ {ι : Type u_4} {α : Type u_5} [inst : NormedCommRing α] (s : Finset ι),
  s.Nonempty → ∀ (f : ι → α), ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- If we're boundaryless, `(extChartAt I x).target` is a neighborhood of the key point  -/
extChartAt_target_mem_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] [I.Boundaryless] (x : M),
  (extChartAt I x).target ∈ nhds (↑(extChartAt I x) x)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.Equiv.eq_def : ∀ (m : Type w → Type w') (β : Type w) [inst : Monad m] [inst_1 : LawfulMonad m] (ita itb : Std.BundledIterM m β),
  Std.BundledIterM.Equiv m β ita itb =
    (Std.Iterators.HetT.map (Std.IterStep.mapIterator (Quot.mk (Std.BundledIterM.Equiv m β))) ita.step =
      Std.Iterators.HetT.map (Std.IterStep.mapIterator (Quot.mk (Std.BundledIterM.Equiv m β))) itb.step)
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- Access W-type underlying `Fix F`  -/
MvQPF.fixToW : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → MvQPF.Fix F α → (MvQPF.P F).W α
-- Lean.Level
Lean.Level.imax.sizeOf_spec : ∀ (a a_1 : Lean.Level), sizeOf (a.imax a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- If `f b = 0` for all `b ∈ t`, then the sum of `f a` with `a ∈ s` is the same as
the sum of `f a` with `a ∈ s ∖ t`.  -/
tsum_setElem_eq_tsum_setElem_sdiff : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (s t : Set β),
  (∀ b ∈ t, f b = 0) → ∑' (a : ↑s), f ↑a = ∑' (a : ↑(s \ t)), f ↑a
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_fromBlocks_zero₁₂ : ∀ {R : Type u_1} [inst : CommRing R] {m : Type u_3} {n : Type u_4} [inst_1 : DecidableEq m] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : Fintype n] (M₁₁ : Matrix m m R) (M₂₁ : Matrix n m R) (M₂₂ : Matrix n n R),
  (Matrix.fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGet?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.get? t₁ k = Std.DTreeMap.Raw.Const.get? t₂ k
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List (α × β)},
  Std.ExtTreeMap.ofList l cmp = ∅.insertMany l
-- Mathlib.Tactic.CategoryTheory.CheckCompositions
/-- Given a composition `CategoryStruct.comp _ _ X Y Z f g`,
infer the types of `f` and `g` and check whether their sources and targets agree,
at "instances and reducible" transparency, with `X`, `Y`, and `Z`,
reporting any discrepancies.  -/
Mathlib.Tactic.CheckCompositions.checkComposition : Lean.Expr → Lean.MetaM Unit
-- Std.Time.Zoned.TimeZone
/-- Creates an `Offset` from a given number of seconds.
 -/
Std.Time.TimeZone.Offset.ofSeconds : Std.Time.Second.Offset → Std.Time.TimeZone.Offset
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- Given a measure `μ : Measure α` and a function `f : α → ℝ≥0∞`, `μ.withDensity f` is the
measure such that for a measurable set `s` we have `μ.withDensity f s = ∫⁻ a in s, f a ∂μ`.  -/
MeasureTheory.Measure.withDensity : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.Measure α → (α → ENNReal) → MeasureTheory.Measure α
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUInt8 = OfNat.ofNat n
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd : ∀ {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [NeZero m]
  [hK : IsCyclotomicExtension {m} ℚ K], ¬p ∣ m → (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = 1
-- Mathlib.Algebra.GroupWithZero.Divisibility
not_isRelPrime_zero_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [Nontrivial α], ¬IsRelPrime 0 0
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- The function `fun x ↦ x⁻¹` is not integrable on any interval `(a, +∞)`.  -/
not_integrableOn_Ioi_inv : ∀ {a : ℝ}, ¬MeasureTheory.IntegrableOn (fun x => x⁻¹) (Set.Ioi a) MeasureTheory.volume
-- Lean.Meta.LazyDiscrTree
/-- Combine two initial results.  -/
Lean.Meta.LazyDiscrTree.InitResults.append : {α : Type} →
  Lean.Meta.LazyDiscrTree.InitResults α → Lean.Meta.LazyDiscrTree.InitResults α → Lean.Meta.LazyDiscrTree.InitResults α
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.superFactorial_two_mul : ∀ (n : ℕ), (2 * n).superFactorial = (∏ i ∈ Finset.range n, (2 * i + 1).factorial) ^ 2 * 2 ^ n * n.factorial
-- Mathlib.Data.Rel
SetRel.comp_subset_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R₁ R₂ : SetRel α β} {S₁ S₂ : SetRel β γ},
  R₁ ⊆ R₂ → S₁ ⊆ S₂ → R₁.comp S₁ ⊆ R₂.comp S₂
-- Mathlib.Data.Sum.Order
OrderIso.sumLexDualAntidistrib_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (a : α),
  (OrderIso.sumLexDualAntidistrib α β) (OrderDual.toDual (Sum.inl a)) = Sum.inr (OrderDual.toDual a)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- At least one of the "empty" complete equipartite subgraphs is contained in a simple graph.  -/
SimpleGraph.CompleteEquipartiteSubgraph.nonempty_of_eq_zero_or_eq_zero : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ}, r = 0 ∨ t = 0 → Nonempty (G.CompleteEquipartiteSubgraph r t)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.inclusion_mk : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  (h : S ≤ T) (x : A) (hx : x ∈ S), (Subalgebra.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
-- Init.Data.Float.Float
/-- Computes the hyperbolic arc sine (inverse sine) of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`asinh`.
 -/
Float.asinh : Float → Float
-- Mathlib.Data.Rel
SetRel.inv_univ : ∀ {α : Type u_1} {β : Type u_2}, SetRel.inv Set.univ = Set.univ
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- The results of applying `domDomCongr` to two maps are equal if and only if those maps are.  -/
AlternatingMap.domDomCongr_eq_iff : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N),
  AlternatingMap.domDomCongr σ f = AlternatingMap.domDomCongr σ g ↔ f = g
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk'_X_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d₀ : X₁ ⟶ X₀)
  (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0),
  (ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X 1 = X₁
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.mulAction.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : DecidableEq α] [inst_2 : Monoid α]
  [inst_3 : MulAction α β], Finset.mulAction = { toSMul := Finset.smul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.to_truncLT_obj_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {n : ℤ} {Y X : C} {f₁ f₂ : Y ⟶ (t.truncLT n).obj X},
  CategoryTheory.CategoryStruct.comp f₁ ((t.truncLTι n).app X) =
      CategoryTheory.CategoryStruct.comp f₂ ((t.truncLTι n).app X) →
    ∀ [t.IsLE Y (n - 1)], f₁ = f₂
-- Init.Data.Range.Polymorphic.SInt
ISize.le.eq_1 : ∀ (a b : ISize), a.le b = (a.toBitVec.sle b.toBitVec = true)
-- Mathlib.RingTheory.Binomial
Ring.multichoose_neg_add : ∀ (n k : ℕ), Ring.multichoose (-↑n) (n + k + 1) = 0
-- Init.Data.Range.Polymorphic.UInt
UInt64.rxiHasSize_eq_toBitVec : ∀ {lo : BitVec 64}, Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
-- Mathlib.Topology.Category.Stonean.EffectiveEpi
Stonean.effectiveEpiFamily_tfae : ∀ {α : Type} [inst : Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B),
  [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π),
      ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.convexCombPair_mem : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X} {x y : X},
  Convexity.IsConvexSet R s →
    x ∈ s →
      y ∈ s → ∀ {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), Convexity.convexCombPair a b ha hb hab x y ∈ s
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.id_map : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (x : F α), MvFunctor.map TypeVec.id x = x