mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_desc_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
  (p : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
      ((CochainComplex.mappingCone.desc φ α β eq).f p) =
    β.f p
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.vaddAntidiagonal_min_vadd_min : ∀ {G : Type u_1} {P : Type u_2} [inst : LinearOrder G] [inst_1 : LinearOrder P] [inst_2 : VAdd G P]
  [inst_3 : IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty)
  (hnt : t.Nonempty), Finset.VAddAntidiagonal (hs.min hns +ᵥ ht.min hnt) ⋯ = {(hs.min hns, ht.min hnt)}
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommGrp C} {f g : A ⟶ B},
  f = g ↔ f.hom.hom.hom = g.hom.hom.hom
-- Mathlib.Algebra.Polynomial.Module.AEval
/-- Construct an `R[X]`-linear equivalence out of `AEval R M a` from an `R`-linear map out of `M`.
 -/
LinearEquiv.ofAEval : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          (a : A) →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module A M] →
                  [inst_5 : Module R M] →
                    [inst_6 : IsScalarTower R A M] →
                      {N : Type u_4} →
                        [inst_7 : AddCommMonoid N] →
                          [inst_8 : Module R N] →
                            [inst_9 : Module (Polynomial R) N] →
                              [IsScalarTower R (Polynomial R) N] →
                                (f : M ≃ₗ[R] N) →
                                  (∀ (m : M), f (a • m) = Polynomial.X • f m) → Module.AEval R M a ≃ₗ[Polynomial R] N
-- Init.Grind.AC
Lean.Grind.AC.Expr.denote_var : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (x : Lean.Grind.AC.Var),
  Lean.Grind.AC.Expr.denote ctx (Lean.Grind.AC.Expr.var x) = Lean.Grind.AC.Var.denote ctx x
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.byteIdx_offset_le_utf8ByteSize : ∀ {s : String.Slice} {p : s.Pos}, p.offset.byteIdx ≤ s.utf8ByteSize
-- Mathlib.Topology.Compactification.StoneCech
instInhabitedStoneCech : {α : Type u} → [inst : TopologicalSpace α] → [Inhabited α] → Inhabited (StoneCech α)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varFinsetLeft.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (i : α),
  (FirstOrder.Language.var (Sum.inl i)).varFinsetLeft = {i}
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.instIsPresentableOfIsAccessibleCategory : ∀ (C : Type u) [hC : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsAccessibleCategory.{w, v, u} C] (X : C),
  CategoryTheory.IsPresentable.{w, v, u} X
-- Mathlib.Topology.MetricSpace.Isometry
/-- Alternative constructor for isometric bijections,
taking as input an isometry, and a right inverse.  -/
IsometryEquiv.mk' : {β : Type v} →
  [inst : PseudoEMetricSpace β] →
    {α : Type u} →
      [inst_1 : EMetricSpace α] → (f : α → β) → (g : β → α) → (∀ (x : β), f (g x) = x) → Isometry f → α ≃ᵢ β
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.AttributeEntry.toOLeanEntry : {γ : Type} → Lean.KeyedDeclsAttribute.AttributeEntry γ → Lean.KeyedDeclsAttribute.OLeanEntry
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {M : C} →
              [inst_4 : CategoryTheory.MonObj M] →
                {X : D} →
                  (smul : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X) →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                              CategoryTheory.MonObj.one X)
                            smul =
                          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom)
                        CategoryTheory.ModObj.one_smul._autoParam →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                CategoryTheory.MonObj.mul X)
                              smul =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) smul))
                          CategoryTheory.ModObj.mul_smul._autoParam →
                        CategoryTheory.ModObj M X
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero_product_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β], 0 ×ˢ 0 = 0
-- Mathlib.Algebra.Order.Hom.Ring
/-- Composition of `OrderRingIso`s as an `OrderRingIso`.  -/
OrderRingIso.trans : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Mul α] →
        [inst_1 : Add α] →
          [inst_2 : LE α] →
            [inst_3 : Mul β] →
              [inst_4 : Add β] →
                [inst_5 : LE β] → [inst_6 : Mul γ] → [inst_7 : Add γ] → [inst_8 : LE γ] → α ≃+*o β → β ≃+*o γ → α ≃+*o γ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_some_getD_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α}
  {fallback : β}, m.contains a = true → m[a]? = some (m.getD a fallback)
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.HasInjectiveDimensionLT.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X : C} {n : ℕ},
  (∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : CategoryTheory.Abelian.Ext Y X i), e = 0) →
    CategoryTheory.HasInjectiveDimensionLT X n
-- Lean.Elab.Do.Basic
/-- Pluggable builders for `pure` and `bind` applications.  -/
Lean.Elab.Do.Context.ops : Lean.Elab.Do.Context → Lean.Elab.Do.DoOpsRef
-- Mathlib.GroupTheory.GroupAction.Blocks
_private.Mathlib.GroupTheory.GroupAction.Blocks.0.MulAction.block_stabilizerOrderIso.match_1.eq_1 : ∀ (G : Type u_2) [inst : Group G] {X : Type u_1} [inst_1 : MulAction G X] (a : X)
  (motive : { B // a ∈ B ∧ MulAction.IsBlock G B } → Sort u_3) (B : Set X) (ha : a ∈ B) (hB : MulAction.IsBlock G B)
  (h_1 : (B : Set X) → (ha : a ∈ B) → (hB : MulAction.IsBlock G B) → motive ⟨B, ⋯⟩),
  (match ⟨B, ⋯⟩ with
    | ⟨B, ⋯⟩ => h_1 B ha hB) =
    h_1 B ha hB
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_counitIso_hom_app_hom_unmop : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon Cᴹᵒᵖ),
  ((MonObj.mopEquiv C).counitIso.hom.app X).hom.unmop = CategoryTheory.CategoryStruct.id X.X.unmop
-- Mathlib.Algebra.Order.GroupWithZero.Defs
le_of_mul_le_mul_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulReflectLE α],
  a * b ≤ a * c → 0 < a → b ≤ c
-- Mathlib.Data.Nat.Cast.Defs
Nat.binCast.eq_1 : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R] [inst_2 : Add R], Nat.binCast 0 = 0
-- Batteries.Data.List.Lemmas
List.countPBefore_lt_countP_of_lt_length_of_pos : ∀ {α : Type u_1} {i : ℕ} {p : α → Bool} {xs : List α} {h : i < xs.length},
  p xs[i] = true → List.countPBefore p xs i < List.countP p xs
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- Möbius inversion for functions to an `AddCommGroup`, where the equalities only hold on a
well-behaved set.  -/
ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on : ∀ {R : Type u_1} [inst : AddCommGroup R] {f g : ℕ → R} (s : Set ℕ),
  (∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) →
    ((∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔
      ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 • g x.2 = f n)
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.compHom_apply_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] (g : N →+ P) (hmn : M →+ N), (AddMonoidHom.compHom g) hmn = g.comp hmn
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_smul`. -/
Ideal.ramificationIdx'_smul : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (q : Ideal S)
  {G : Type u_4} [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [SMulCommClass G R S] (g : G),
  (g • q).ramificationIdx R = q.ramificationIdx R
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsShortNF.mk : ∀ {R : Type u_1} [inst : CommRing R] {W : WeierstrassCurve R}, W.a₁ = 0 → W.a₂ = 0 → W.a₃ = 0 → W.IsShortNF
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
/-- **Alias** of the forward direction of `Set.finite_vadd_set`. -/
Set.Finite.of_vadd_set : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {s : Set α},
  (a +ᵥ s).Finite → s.Finite
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [inst : LinearOrder ι] {τ : Ω → WithTop ι}
  {f : MeasureTheory.Filtration ι m} [Countable ι],
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | ↑i ≤ τ ω}
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instInfSet : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → InfSet (ConvexCone R M)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_smulRightₗ : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : Module R S] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₂] [inst_6 : Module S M₂]
  [inst_7 : IsScalarTower R S M₂] [inst_8 : TopologicalSpace S] [inst_9 : TopologicalSpace M₂]
  [inst_10 : ContinuousSMul S M₂] [inst_11 : TopologicalSpace M] [inst_12 : AddCommMonoid M] [inst_13 : Module R M]
  [inst_14 : ContinuousAdd M₂] [inst_15 : Module T M₂] [inst_16 : ContinuousConstSMul T M₂]
  [inst_17 : SMulCommClass R T M₂] [inst_18 : SMulCommClass S T M₂] (c : M →L[R] S), ⇑c.smulRightₗ = c.smulRight
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidal_leftUnitor : ∀ (M : Type u) [inst : Monoid M] (X : CategoryTheory.Discrete M),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor X = CategoryTheory.Discrete.eqToIso ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.PseudoCore.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F : CategoryTheory.OplaxFunctor B C}
  {mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)}
  {mapCompIso :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)}
  {mapIdIso_hom :
    autoParam (∀ {a : B}, (mapIdIso a).hom = F.mapId a) CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom._autoParam}
  {mapCompIso_hom :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).hom = F.mapComp f g)
      CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom._autoParam}
  {mapIdIso_1 : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)}
  {mapCompIso_1 :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)}
  {mapIdIso_hom_1 :
    autoParam (∀ {a : B}, (mapIdIso_1 a).hom = F.mapId a)
      CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom._autoParam}
  {mapCompIso_hom_1 :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso_1 f g).hom = F.mapComp f g)
      CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom._autoParam},
  { mapIdIso := mapIdIso, mapCompIso := mapCompIso, mapIdIso_hom := mapIdIso_hom, mapCompIso_hom := mapCompIso_hom } =
      { mapIdIso := mapIdIso_1, mapCompIso := mapCompIso_1, mapIdIso_hom := mapIdIso_hom_1,
        mapCompIso_hom := mapCompIso_hom_1 } →
    mapIdIso = mapIdIso_1 ∧ mapCompIso = mapCompIso_1
-- Mathlib.Topology.Algebra.Monoid
/-- Right-multiplication by a right-invertible element of a topological monoid is proper, i.e.,
inverse images of compact sets are compact.  -/
Filter.tendsto_cocompact_mul_right : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [SeparatelyContinuousMul M] {a b : M},
  a * b = 1 → Filter.Tendsto (fun x => x * a) (Filter.cocompact M) (Filter.cocompact M)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_eq_some_get : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} {h' : m.contains a = true}, m.get? a = some (m.get a h')
-- Mathlib.Analysis.Calculus.DiffContOnCl
diffContOnCl_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {c : F},
  DiffContOnCl 𝕜 (fun x => c) s
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.haveLebesgueDecompositionSMulRight : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν] (r : NNReal),
  μ.HaveLebesgueDecomposition (r • ν)
-- Aesop.Rule
Aesop.Safety.almostSafe : Aesop.Safety
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.Λ'.act.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {a : Turing.TM0.Stmt Γ} {a_1 : Λ} {a_2 : Turing.TM0.Stmt Γ} {a_3 : Λ},
  Turing.TM0to1.Λ'.act a a_1 = Turing.TM0to1.Λ'.act a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Group.Defs
AddGroup.toSubNegMonoid : {A : Type u} → [self : AddGroup A] → SubNegMonoid A
-- Init.Core
Fin.mk.injEq : ∀ {n : ℕ} (val : ℕ) (isLt : val < n) (val_1 : ℕ) (isLt_1 : val_1 < n), (⟨val, isLt⟩ = ⟨val_1, isLt_1⟩) = (val = val_1)
-- Mathlib.Order.Cover
Pi.exists_forall_eq_of_wcovBy : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [Nonempty ι],
  a ⩿ b → ∃ i, ∀ (j : ι), j ≠ i → a j = b j
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.Measure.isProbabilityMeasure_map : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsProbabilityMeasure μ] {f : α → β},
  AEMeasurable f μ → MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map f μ)
-- Lean.Expr
Lean.BinderInfo.instImplicit.sizeOf_spec : sizeOf Lean.BinderInfo.instImplicit = 1
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_comp_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f g : CategoryTheory.Subobject A) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((f ⊓ g).ofLE f ⋯) (CategoryTheory.CategoryStruct.comp f.arrow h) =
    CategoryTheory.CategoryStruct.comp (f ⊓ g).arrow h
-- Mathlib.Order.SupClosed
InfClosed.insert_lowerBounds : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α} {a : α}, InfClosed s → a ∈ lowerBounds s → InfClosed (insert a s)
-- Mathlib.Data.Finsupp.Defs
/-- `Finsupp α M`, denoted `α →₀ M`, is the type of functions `f : α → M` such that
`f x = 0` for all but finitely many `x`.  -/
«term_→₀_» : Lean.TrailingParserDescr
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_cons_head : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), (a ::ₘ s).erase a = s
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.liftr_iff : ∀ {P : PFunctor.{uA, uB}} {α : Type u} (r : α → α → Prop) (x y : ↑P α),
  Functor.Liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {fallback : β} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.alter t k f) k fallback =
    (f (Std.ExtDTreeMap.Const.get? t k)).getD fallback
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.expandIfNecessary.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.expandIfNecessary ⟨{ size := size, buckets := buckets }, hm⟩ =
    if Std.DHashMap.Internal.numBucketsForCapacity✝ size ≤ buckets.size then ⟨{ size := size, buckets := buckets }, hm⟩
    else
      match Std.DHashMap.Internal.Raw₀.expand ⟨buckets, hm⟩ with
      | ⟨buckets', h'⟩ => ⟨{ size := size, buckets := buckets' }, h'⟩
-- Init.Data.Vector.Lemmas
Vector.any_append : ∀ {α : Type u_1} {n m : ℕ} {f : α → Bool} {xs : Vector α n} {ys : Vector α m}, (xs ++ ys).any f = (xs.any f || ys.any f)
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_id : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R],
  MvPolynomial.bind₂ (RingHom.id (MvPolynomial σ R)) = MvPolynomial.join₂
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.partialOrder : {α : Type u_2} →
  [inst : TopologicalSpace α] →
    {β : Type u_5} →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] → [PartialOrder β] → PartialOrder (CompactlySupportedContinuousMap α β)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instSMulMemClass : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], SMulMemClass (LieSubmodule R L M) R M
-- Mathlib.Topology.Category.CompHausLike.SigmaComparison
CompHausLike.sigmaComparison.eq_1 : ∀ {P : TopCat → Prop} [inst : CompHausLike.HasExplicitFiniteCoproducts P]
  (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) {α : Type u} [inst_1 : Finite α] (σ : α → Type u)
  [inst_2 : (a : α) → TopologicalSpace (σ a)] [inst_3 : ∀ (a : α), CompactSpace (σ a)]
  [inst_4 : ∀ (a : α), T2Space (σ a)] [inst_5 : ∀ (a : α), CompHausLike.HasProp P (σ a)],
  CompHausLike.sigmaComparison X σ =
    TypeCat.ofHom fun x a =>
      (CategoryTheory.ConcreteCategory.hom
          (X.map (CompHausLike.ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ }).op))
        x
-- Mathlib.Analysis.Convex.Body
/-- Convex bodies in a fixed seminormed space $V$ form a pseudo-metric space under the Hausdorff
metric.  -/
ConvexBody.instPseudoMetricSpace : {V : Type u_1} → [inst : SeminormedAddCommGroup V] → [inst_1 : NormedSpace ℝ V] → PseudoMetricSpace (ConvexBody V)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.ofReal_rpow_of_nonneg : ∀ {x p : ℝ}, 0 ≤ x → 0 ≤ p → ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f U)
      (f.hom.c.app (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U))) =
    X.presheaf.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Topology.ContinuousMap.Algebra
/-- The `AddSubmonoid` of continuous maps `α → β`.  -/
continuousAddSubmonoid : (α : Type u_1) →
  (β : Type u_2) →
    [TopologicalSpace α] →
      [inst : TopologicalSpace β] → [inst_1 : AddZeroClass β] → [ContinuousAdd β] → AddSubmonoid (α → β)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.rightAdjointMate_comp_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (fᘁ) X) (ε_ X Xᘁ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ f) (ε_ Y Yᘁ)
-- Std.Sync.CancellationContext
/-- Creates a new root cancellation context.
 -/
Std.CancellationContext.new : BaseIO Std.CancellationContext
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (κ : Cardinal.{w})
  (S : CategoryTheory.SmallCategoryCardinalLT κ),
  (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape (CategoryTheory.SmallCategoryCardinalLT.categoryFamily κ S)
-- Init.Data.Fin.Lemmas
Fin.castAdd_castAdd : ∀ {m n p : ℕ} (i : Fin m), Fin.castAdd p (Fin.castAdd n i) = Fin.cast ⋯ (Fin.castAdd (n + p) i)
-- Init.Data.List.Erase
List.eraseIdx_eq_nil_iff : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l.eraseIdx i = [] ↔ l = [] ∨ l.length = 1 ∧ i = 0
-- Init.Data.Nat.Dvd
Nat.dvd_mod_iff : ∀ {k m n : ℕ}, k ∣ n → (k ∣ m % n ↔ k ∣ m)
-- Batteries.Data.Int
Int.testBit.eq_2 : ∀ (x m : ℕ), (Int.negSucc m).testBit x = !m.testBit x
-- Mathlib.Data.Fin.Fin2
_private.Mathlib.Data.Fin.Fin2.0.Fin2.toNat.match_1.eq_1 : ∀ (motive : (x : ℕ) → Fin2 x → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (n + 1) Fin2.fz)
  (h_2 : (n : ℕ) → (i : Fin2 n) → motive (n + 1) i.fs),
  (match n + 1, Fin2.fz with
    | .(n + 1), Fin2.fz => h_1 n
    | .(n + 1), i.fs => h_2 n i) =
    h_1 n
-- Aesop.Util.Basic
Aesop.isHypRedundantReducibleRigid : Lean.Expr → Lean.MetaM Bool
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Ric.length_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.Rxc.HasSize α] [Std.Rxc.LawfulHasSize α] {r : Std.Ric α},
  r.iter.length = r.size
-- Mathlib.SetTheory.Ordinal.Notation
ONote.cmp.eq_2 : ∀ (x : ONote), (x = ONote.zero → False) → x.cmp ONote.zero = Ordering.gt
-- Mathlib.Data.DFinsupp.Module
/-- Dependent functions with finite support inherit a module structure from such a structure on
each coordinate.  -/
DFinsupp.module : {ι : Type u} →
  {γ : Type w} →
    {β : ι → Type v} →
      [inst : Semiring γ] →
        [inst_1 : (i : ι) → AddCommMonoid (β i)] → [(i : ι) → Module γ (β i)] → Module γ (Π₀ (i : ι), β i)
-- Mathlib.GroupTheory.Divisible
/-- **Alias** of `DivisibleBy.surjective_smul`. -/
smul_right_surj_of_divisibleBy : ∀ (A : Type u_1) (α : Type u_2) [inst : AddMonoid A] [inst_1 : SMul α A] [inst_2 : Zero α] [DivisibleBy A α] {n : α},
  n ≠ 0 → Function.Surjective fun a => n • a