mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Congruence.Defs
/-- A congruence relation that preserves scalar multiplication.  -/
SMulCon : (S : Type u_2) → (M : Type u_3) → [SMul S M] → Type u_3
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.eqId_iff_eq : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ), A.EqId ↔ A.fst = Δ
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Cell.Const.get?.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option ((_ : α) × β) → Sort u_3) (p : (_ : α) × β) (h_1 : Unit → motive none)
  (h_2 : (p : (_ : α) × β) → motive (some p)),
  (match some p with
    | none => h_1 ()
    | some p => h_2 p) =
    h_2 p
-- Std.Data.ExtDTreeMap.Basic
/-- Carries out a monadic action on each mapping in the tree map in ascending order.  -/
Std.ExtDTreeMap.forM : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} →
        [inst : Monad m] →
          [LawfulMonad m] →
            [Std.TransCmp cmp] → ((a : α) → β a → m PUnit.{w + 1}) → Std.ExtDTreeMap α β cmp → m PUnit.{w + 1}
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instZero.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Zero M], Filter.Germ.instZero = { zero := ↑0 }
-- Mathlib.CategoryTheory.Subobject.WellPowered
CategoryTheory.essentiallySmall_monoOver : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u₁} C]
  [CategoryTheory.WellPowered.{w, v, u₁} C] (X : C),
  CategoryTheory.EssentiallySmall.{w, v, max u₁ v} (CategoryTheory.MonoOver X)
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppLeft_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι]
  (t : TensorProduct R (ι →₀ M) N) (i : ι),
  ((TensorProduct.finsuppLeft R S M N ι) t) i = (LinearMap.rTensor N (Finsupp.lapply i)) t
-- Mathlib.Data.List.Nodup
List.nodup_singleton : ∀ {α : Type u} (a : α), [a].Nodup
-- Mathlib.Topology.UniformSpace.UniformEmbedding
uniformContinuous_uniformly_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] {e : β → α} (h_e : IsUniformInducing e) (h_dense : DenseRange e) {f : β → γ},
  UniformContinuous f → ∀ [CompleteSpace γ], UniformContinuous (⋯.extend f)
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_copy : ∀ {R : Type u} [inst : NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- A free group with a finite number of generators is finitely presented.  -/
Group.IsFinitelyPresented.instFreeGroupOfFinite : ∀ {α : Type u_3} [Finite α], Group.IsFinitelyPresented (FreeGroup α)
-- Mathlib.Topology.NhdsWithin
nhdsWithin_eq : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (s : Set α),
  nhdsWithin a s = ⨅ t ∈ {t | a ∈ t ∧ IsOpen t}, Filter.principal (t ∩ s)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- A family of gluing data consists of
1. An index type `J`
2. A locally ringed space `U i` for each `i : J`.
3. A locally ringed space `V i j` for each `i j : J`.
   (Note that this is `J × J → LocallyRingedSpace` rather than `J → J → LocallyRingedSpace` to
   connect to the limits library more easily.)
4. An open immersion `f i j : V i j ⟶ U i` for each `i j : J`.
5. A transition map `t i j : V i j ⟶ V j i` for each `i j : J`.

such that
6. `f i i` is an isomorphism.
7. `t i i` is the identity.
8. `V i j ×[U i] V i k ⟶ V i j ⟶ V j i` factors through `V j k ×[U j] V j i ⟶ V j i` via some
   `t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i`.
9. `t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _`.

We can then glue the spaces `U i` together by identifying `V i j` with `V j i`, such
that the `U i`'s are open subspaces of the glued space.
 -/
AlgebraicGeometry.LocallyRingedSpace.GlueData : Type (u_1 + 1)
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.isClosed_iff_bsup : ∀ {s : Set Ordinal.{u}},
  IsClosed s ↔
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorAssoc_toLinearEquiv : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] [inst_7 : Invertible 2] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂)
  (Q₃ : QuadraticForm R M₃), (Q₁.tensorAssoc Q₂ Q₃).toLinearEquiv = TensorProduct.assoc R M₁ M₂ M₃
-- Init.Data.String.Lemmas.Intercalate
String.join_nil : String.join [] = ""
-- Mathlib.LinearAlgebra.DFinsupp
/-- If `DFinsupp.sumAddHom` applied with `AddSubmonoid.subtype` is injective then the additive
subgroups are independent.  -/
iSupIndep_of_dfinsuppSumAddHom_injective' : ∀ {ι : Type u_1} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : AddCommGroup N] (p : ι → AddSubgroup N),
  Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype) → iSupIndep p
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.isConstant_congr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {F G : CategoryTheory.Sheaf J D} (i : F ≅ G) [CategoryTheory.Sheaf.IsConstant J F],
  CategoryTheory.Sheaf.IsConstant J G
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
Projectivization.finite_iff_of_finite : ∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k],
  Finite (Projectivization k V) ↔ Finite V
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
MvQPF.Const.MvFunctor : {n : ℕ} → {A : Type u} → MvFunctor (MvQPF.Const n A)
-- Lean.Structure
/-- Gets the direct field names for the given structure, including subobject fields.  -/
Lean.getStructureFields : Lean.Environment → Lean.Name → Array Lean.Name
-- Std.Tactic.Do.Syntax
Lean.Elab.Tactic.Do.VCGen.Config.mk : Bool → Bool → Bool → Bool → Option ℕ → Bool → Bool → Bool → Lean.Elab.Tactic.Do.VCGen.Config
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_mul_self : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [ZeroLEOneClass M₀]
  [MulPosStrictMono M₀], 1 < a → a < a * a
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.ι_comp_colimitUnopIsoOpLimit_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J) {Z : C}
  (h : Opposite.unop (CategoryTheory.Limits.limit F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.unop j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitUnopIsoOpLimit F).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F (Opposite.op j)).unop h
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If a function is countably sub-additive then it is binary sub-additive  -/
rel_sup_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} [inst_2 : CompleteLattice α]
  (m : α → M),
  m ⊥ = 0 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) → ∀ (s₁ s₂ : α), R (m (s₁ ⊔ s₂)) (m s₁ + m s₂)
-- Init.Data.List.Nat.TakeDrop
List.lt_length_right_of_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {i : ℕ} {l : List α} {l' : List β},
  i < (List.zipWith f l l').length → i < l'.length
-- Lean.Parser.Extra
Lean.ppIndent.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Algebra.Operations
Submodule.one_eq_span_one_set : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A], 1 = Submodule.span R 1
-- Mathlib.Algebra.Ring.Subsemiring.Basic
AddSubsemigroup.mk.congr_simp : ∀ {M : Type u_3} [inst : Add M] (carrier carrier_1 : Set M) (e_carrier : carrier = carrier_1)
  (add_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier),
  { carrier := carrier, add_mem' := add_mem' } = { carrier := carrier_1, add_mem' := ⋯ }
-- Init.Data.Array.Lex.Lemmas
_private.Init.Data.Array.Lex.Lemmas.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Given two strongly co-Cartesian morphisms `φ`, `ψ` as follows
```
a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T
```
Then the composite `φ ≫ ψ` is also strongly co-Cartesian.  -/
CategoryTheory.Functor.IsStronglyCocartesian.comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S T : 𝒮} {a b c : 𝒳} {f : R ⟶ S} {g : S ⟶ T} {φ : a ⟶ b} {ψ : b ⟶ c}
  [p.IsStronglyCocartesian f φ] [p.IsStronglyCocartesian g ψ],
  p.IsStronglyCocartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)
-- Mathlib.Order.Preorder.Chain
/-- Flags are preserved under order isomorphisms.  -/
Flag.map : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → Flag α ≃ Flag β
-- Init.Data.ToString.Extra
instToStringList : {α : Type u} → [ToString α] → ToString (List α)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.ι_toNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] (U : ↑Y.affineOpens),
  CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).ι
      (AlgebraicGeometry.Scheme.Hom.toNormalization f) =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj ↑U).toSpecΓ
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map
          (CommRingCat.ofHom
            (integralClosure ↑(Y.presheaf.obj (Opposite.op ↑U))
                  ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ↑U)))).val.toRingHom))
        ((AlgebraicGeometry.Scheme.Hom.normalizationOpenCover f).f U))
-- Init.Data.UInt.Bitwise
UInt32.or_comm : ∀ (a b : UInt32), a ||| b = b ||| a
-- Init.Data.SInt.Lemmas
Int32.toISize_ofInt : ∀ {n : ℤ}, Int32.minValue.toInt ≤ n → n ≤ Int32.maxValue.toInt → (Int32.ofInt n).toISize = ISize.ofInt n
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.eq_empty_iff_erase_eq_empty_and_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] (k : α),
  t = ∅ ↔ t.erase k = ∅ ∧ k ∉ t
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.writeLspRequest : {α : Type u_1} → [Lean.ToJson α] → IO.FS.Stream → Lean.JsonRpc.Request α → IO Unit
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDeriv_even_sinh : ∀ (n : ℕ), iteratedDeriv (2 * n) Real.sinh = Real.sinh
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.id.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A : HomologicalComplex V c),
  A.id = { f := fun x => CategoryTheory.CategoryStruct.id (A.X x), comm' := ⋯ }
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.preimage.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} (F : CategoryTheory.Functor C D) [inst_2 : F.Full] (f f_1 : F.obj X ⟶ F.obj Y),
  f = f_1 → F.preimage f = F.preimage f_1
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.add_right_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T : Set α → β}
  [inst : AddMonoid β] {ν : MeasureTheory.Measure α},
  MeasureTheory.FinMeasAdditive μ T → MeasureTheory.FinMeasAdditive (μ + ν) T
-- Mathlib.Topology.Irreducible
irreducibleSpace_def : ∀ (X : Type u_3) [inst : TopologicalSpace X], IrreducibleSpace X ↔ IsIrreducible ⊤
-- Mathlib.Algebra.Order.Group.Abs
mabs_div_le_one : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G}, |a / b|ₘ ≤ 1 ↔ a = b
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.inv_hom_id_app_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E']
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C)
  (X₂ : D) (X₃ : E),
  CategoryTheory.CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃) (((e.hom.app X₁).app X₂).app X₃) =
    CategoryTheory.CategoryStruct.id (((G.obj X₁).obj X₂).obj X₃)
-- Init.Control.Basic
/-- Lifts an operation from an inner monad to an outer monad, providing it with a reverse lifting
operator that allows outer monad computations to be run in the inner monad. The lifted operation is
required to return extra information that is required in order to reconstruct the reverse lift's
effects in the outer monad; this extra information is determined by `stM`.

This function takes the inner monad as an explicit parameter. Use `control` to infer the monad.
 -/
controlAt : (m : Type u → Type v) →
  {n : Type u → Type w} →
    [inst : MonadControlT m n] → [Bind n] → {α : Type u} → (({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) → n α
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.instSliceableRccSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.instSliceableRccSlice._auto_1) →
      Std.Rcc.Sliceable (Std.DTreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.RccSlice α β)
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.writeLspResponseErrorWithData : {α : Type u_1} → [Lean.ToJson α] → IO.FS.Stream → Lean.JsonRpc.ResponseError α → IO Unit
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.isWellOrder : ∀ {x : ZFSet.{u}}, x.IsOrdinal → IsWellOrder (↥x) (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
/-- **Alias** of `TensorProduct.coe_directSumRight`. -/
TensorProduct.coe_directSumRight' : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_2) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₂ : Type v₂}
  [inst_3 : DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [inst_4 : AddCommMonoid M₁']
  [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [inst_6 : Module R M₁'] [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_8 : Module S M₁'] [inst_9 : IsScalarTower R S M₁'],
  ⇑(TensorProduct.directSumRight R S M₁' M₂) = ⇑(TensorProduct.directSumRight R R M₁' M₂)
-- Init.Data.Fin.Lemmas
Fin.add_ofNat : ∀ {n : ℕ} [inst : NeZero n] (x : Fin n) (y : ℕ), x + Fin.ofNat n y = Fin.ofNat n (↑x + y)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkItem.mk.sizeOf_spec : ∀ (f : Std.Format) (indent : ℤ) (activeTags : ℕ),
  sizeOf { f := f, indent := indent, activeTags := activeTags } = 1 + sizeOf f + sizeOf indent + sizeOf activeTags
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- A field is finitely generated if and only if it is finitely generated over its prime
subfield.  -/
Field.fg_iff_fg_top_bot : ∀ {F : Type u_1} [inst : Field F], Field.FG F ↔ ⊤.FG
-- Mathlib.Topology.Covering.Quotient
AddSubgroup.isAddQuotientCoveringMap_of_comm : ∀ {G : Type u_4} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] (S : AddSubgroup G),
  IsDiscrete ↑S → IsAddQuotientCoveringMap QuotientAddGroup.mk ↥S
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- (Implementation): The homotopy of the morphisms `cylinder f g ⟶ E ⟶ F`.  -/
CategoryTheory.PreOneHypercover.cylinderHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
            (f g : E.Hom F) →
              CategoryTheory.PreOneHypercover.Homotopy ((CategoryTheory.PreOneHypercover.cylinderHom f g).comp f)
                ((CategoryTheory.PreOneHypercover.cylinderHom f g).comp g)
-- Mathlib.Order.Heyting.Hom
CoheytingHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] {f g : CoheytingHom α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a fallback : α},
  (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
-- Mathlib.Topology.Sets.BaseChangeNhds
TopologicalSpace.Opens.baseChangeCompactsInside_mono : ∀ {α : Type u_1} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α} (h : U ⟶ V),
  Monotone (TopologicalSpace.Opens.baseChangeCompactsInside h)
-- Mathlib.Data.Fin.SuccPred
Fin.pred_lt_iff : ∀ {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0), i.pred hi < j ↔ i < j.succ
-- Init.Conv
/-- `simp [thm]` performs simplification using `thm` and marked `@[simp]` lemmas.
See the `simp` tactic for more information.  -/
Lean.Parser.Tactic.Conv.simp : Lean.ParserDescr
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.zero_def`. -/
AddAut.one_def : ∀ (M : Type u_2) [inst : Add M], 0 = AddEquiv.refl M
-- Init.Data.Vector.Algebra
/-- Componentwise negation of vectors.  -/
Vector.neg : {α : Type u_1} → {n : ℕ} → [Neg α] → Vector α n → Vector α n
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.smul_of_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsPositive → ∀ {c : 𝕜}, 0 ≤ c → (c • T).IsPositive
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (p p_1 : Submodule R M) (e_p : p = p_1) (q q_1 : Submodule R M) (e_q : q = q_1)
  (h : Submodule.IsTopCompl p q), p.projectionL q h = p_1.projectionL q_1 ⋯
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.brecOn.go : {motive_1 : Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} →
  {motive_2 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u} →
    {motive_3 : List (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u} →
      {motive_4 : String × Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} →
        (t : Lean.Elab.ConfigEval.HandlerTrie✝) →
          ((t : Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below✝ t → motive_1 t) →
            ((t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
                Lean.Elab.ConfigEval.HandlerTrie.below_1✝ t → motive_2 t) →
              ((t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
                  Lean.Elab.ConfigEval.HandlerTrie.below_2✝ t → motive_3 t) →
                ((t : String × Lean.Elab.ConfigEval.HandlerTrie✝) →
                    Lean.Elab.ConfigEval.HandlerTrie.below_3✝ t → motive_4 t) →
                  motive_1 t ×' Lean.Elab.ConfigEval.HandlerTrie.below✝ t
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- An integral domain is a *discrete valuation ring* (DVR) if it's a local PID which
is not a field.  -/
IsDiscreteValuationRing : (R : Type u) → [inst : CommRing R] → [IsDomain R] → Prop
-- Lean.Meta.Tactic.Congr
/-- Try to apply a `hcongr` congruence theorem, and then tries to close resulting goals
using `Eq.refl`, `HEq.refl`, and assumption.
 -/
Lean.MVarId.hcongr? : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_eq_get_getElem? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {a : α} {h' : a ∈ m}, m[a] = m[a]?.get ⋯
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_succ_cons : ∀ {n : ℕ} {α : Sort u_3} (i : Fin (n + 1)) (x a : α) (p : Fin n → α),
  i.succ.insertNth x (Fin.cons a p) = Fin.cons a (i.insertNth x p)
-- Mathlib.Topology.Compactness.Lindelof
/-- The preimage of a Lindelöf set under a closed embedding is a Lindelöf set.  -/
Topology.IsClosedEmbedding.isLindelof_preimage : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → ∀ {K : Set Y}, IsLindelof K → IsLindelof (f ⁻¹' K)
-- Mathlib.Condensed.Module
/-- The condensed version of the free-forgetful adjunction.  -/
Condensed.freeForgetAdjunction : (R : Type (u + 1)) → [inst : Ring R] → Condensed.free R ⊣ Condensed.forget R
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The constant simplicial object is the constant functor.  -/
CategoryTheory.SimplicialObject.const : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.SimplicialObject C)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_zero_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) →
    ∀ (f : ↥(α →₁ₛ[μ] E)), MeasureTheory.L1.SimpleFunc.setToL1S T f = 0
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.le_max : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {c : Set (Module.Baer.ExtensionOf i f)} (hchain : IsChain (fun x1 x2 => x1 ≤ x2) c)
  (hnonempty : c.Nonempty), ∀ a ∈ c, a ≤ Module.Baer.ExtensionOf.max hchain hnonempty
-- Lean.Parser.Term
Lean.Parser.Command.docComment.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Basic
/-- If diagnostics are enabled, record that synth pending failures.  -/
Lean.Meta.recordSynthPendingFailure : Lean.Expr → Lean.MetaM Unit
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_injective : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ (o : Ordinal.{u}), Function.Injective (Ordinal.veblenWith f o)
-- Mathlib.Analysis.Normed.Group.Constructions
nnnorm_toAdd : ∀ {E : Type u_2} [inst : NNNorm E] (x : Multiplicative E), ‖Multiplicative.toAdd x‖₊ = ‖x‖₊
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] (X Y : C) [inst_3 : CategoryTheory.Preadditive C] (m₀ : M) (hm₀ : m₀ = 0),
  CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ 0 = 0
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_lt_of_lt : ∀ {a b c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → a < c → b < c → a * b < c
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.add_mk'_eq_mk'_of_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S), f x₁ + f.mk' x₂ y = f.mk' (x₁ + x₂) y
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.mul_iUnion₂ : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Mul α] (s : Set α) (t : (i : ι) → κ i → Set α),
  s * ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s * t i j