mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.π₀_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  {Z : HomologicalComplex C c} (h : K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.ι K)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.π₀ K) h) =
    h
-- Init.Data.Nat.Basic
Nat.mul_succ : ∀ (n m : ℕ), n * m.succ = n * m + n
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The subtraction in the Ore localization,
as a difference of an element of `X` and `S`.  -/
AddOreLocalization.oreSub : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_2} → [inst_2 : AddAction R X] → X → ↥S → AddOreLocalization S X
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_subset_coe : ∀ {α : Type u_1} [inst : LE α] {s t : UpperSet α}, ↑s ⊆ ↑t ↔ t ≤ s
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_bot : ∀ {α : Type u_1} {V : Type u_2} [inst : Zero α] [inst_1 : One α], SimpleGraph.adjMatrix α ⊥ = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.getKey! a = m.getKeyD a default
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
/-- A presheaf on a category which is `FinitaryExtensive` is a sheaf iff it preserves finite products.
 -/
CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.FinitaryPreExtensive C]
  [CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F ↔
    CategoryTheory.Limits.PreservesFiniteProducts F
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.top_supp_eq_univ : ∀ {V : Type u} (c : ⊤.ConnectedComponent), c.supp = Set.univ
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailReaderT : {ρ : Type u} → {m : Type u → Type v} → [inst : Monad m] → [Lean.Order.MonadTail m] → Lean.Order.MonadTail (ReaderT ρ m)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.curry.sizeOf_spec : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p : Mathlib.Tactic.ITauto.Proof),
  sizeOf (Mathlib.Tactic.ITauto.Proof.curry ak p) = 1 + sizeOf ak + sizeOf p
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_nnnorm_mul : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : RCLike α] (A : Matrix l m α) (B : Matrix m n α), ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
-- Mathlib.Topology.Bornology.BoundedOperation
tendsto_sub_const_cobounded : ∀ {R : Type u_1} [inst : SeminormedAddCommGroup R] (x : R),
  Filter.Tendsto (fun x_1 => x_1 - x) (Bornology.cobounded R) (Bornology.cobounded R)
-- Init.Data.String.Defs
String.endPos_eq_zero_iff : ∀ {b : String}, b.rawEndPos = 0 ↔ b = ""
-- Mathlib.Topology.Compactness.LocallyCompact
Function.locallyCompactSpace : ∀ {Y : Type u_2} {ι : Type u_3} [inst : TopologicalSpace Y] [LocallyCompactSpace Y] [CompactSpace Y],
  LocallyCompactSpace (ι → Y)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_zero : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  [Nonempty n], Matrix.detp s 0 = 0
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.realize_sentence : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.ElementarySubstructure M) (φ : L.Sentence),
  ↥S ⊨ φ ↔ M ⊨ φ
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.toLCNFType.whnfEta : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (u : Rˣ) (r s t : R) (u_1 : Rˣ) (r_1 s_1 t_1 : R),
  ({ u := u, r := r, s := s, t := t } = { u := u_1, r := r_1, s := s_1, t := t_1 }) =
    (u = u_1 ∧ r = r_1 ∧ s = s_1 ∧ t = t_1)
-- Mathlib.Order.WellFoundedSet
BddBelow.wellFoundedOn_lt : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α] [LocallyFiniteOrder α],
  BddBelow s → s.WellFoundedOn fun x1 x2 => x1 < x2
-- Mathlib.Tactic.Ring.RingNF
/-- Raw form: the representation `ring` uses internally.  -/
Mathlib.Tactic.RingNF.RingMode.raw : Mathlib.Tactic.RingNF.RingMode
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsEquivalenceOfRingEquiv_inverse : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S),
  (ModuleCat.restrictScalarsEquivalenceOfRingEquiv e).inverse = ModuleCat.restrictScalars ↑e.symm
-- Mathlib.Tactic.CongrExclamation
/-- Try to apply `Function.hfunext`, returning the new goals if it succeeds.
Like `Lean.MVarId.obviousFunext?`, we only do so if at least one side of the `HEq` is a lambda.
This prevents unfolding of things like `Set`.

Need to have `Mathlib/Logic/Function/Basic.lean` imported for this to succeed.
 -/
Lean.MVarId.obviousHfunext? : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instAddCommGroup : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : AddCommGroup R] → AddCommGroup (HahnSeries Γ R)
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.kroneckerTMulAlgEquiv_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Fintype n]
  [inst_6 : DecidableEq n] [inst_7 : CommSemiring S] [inst_8 : Algebra R S] [inst_9 : Algebra S A]
  [inst_10 : IsScalarTower R S A] [inst_11 : Fintype m] [inst_12 : DecidableEq m]
  (x : TensorProduct R (Matrix m m A) (Matrix n n B)),
  (Matrix.kroneckerTMulAlgEquiv m n R S A B) x = (kroneckerTMulLinearEquiv m m n n R S A B) x
-- Mathlib.FieldTheory.Laurent
RatFunc.laurentAux_div : ∀ {R : Type u} [inst : CommRing R] (r : R) (p q : Polynomial R) [inst_1 : IsDomain R],
  (RatFunc.laurentAux r) ((algebraMap (Polynomial R) (RatFunc R)) p / (algebraMap (Polynomial R) (RatFunc R)) q) =
    (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p) /
      (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) q)
-- Mathlib.RingTheory.SimpleRing.Basic
IsSimpleRing.iff_injective_ringHom : ∀ (R : Type u) [inst : NonAssocRing R] [Nontrivial R],
  IsSimpleRing R ↔ ∀ {S : Type u} [inst_2 : NonAssocSemiring S] [Nontrivial S] (f : R →+* S), Function.Injective ⇑f
-- Mathlib.RingTheory.TensorProduct.Finite
Submodule.exists_fg_le_subset_range_rTensor_inclusion : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {I : Submodule R N}
  (s : Set (TensorProduct R (↥I) M)),
  s.Finite → ∃ J, ∃ (_ : J.FG) (hle : J ≤ I), s ⊆ ↑(LinearMap.rTensor M (Submodule.inclusion hle)).range
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Status.lam.sizeOf_spec : sizeOf Mathlib.Explode.Status.lam = 1
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
/-- The antidiagonal of `n` does not contain duplicate entries.  -/
List.Nat.nodup_antidiagonalTuple : ∀ (k n : ℕ), (List.Nat.antidiagonalTuple k n).Nodup
-- Mathlib.Algebra.Star.Conjneg
/-- Conjugation-negation. Sends `f` to `fun x ↦ conj (f (-x))`.  -/
conjneg : {G : Type u_2} → {R : Type u_3} → [AddGroup G] → [inst : CommSemiring R] → [StarRing R] → (G → R) → G → R
-- Mathlib.RingTheory.Regular.Category
/-- The short (exact) complex `M → M → M⧸xM` obtain from the scalar multiple of `x : R` on `M`.  -/
ModuleCat.smulShortComplex : {R : Type u} → [inst : CommRing R] → ModuleCat R → R → CategoryTheory.ShortComplex (ModuleCat R)
-- Mathlib.Order.BoundedOrder.Basic
eq_bot_of_top_eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊤ = ⊥ → ∀ (x : α), x = ⊥
-- Mathlib.Data.Fintype.Perm
mem_permsOfList_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {f : Equiv.Perm α},
  (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_normComp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ‖f.normComp‖ = ‖f‖
-- Init.Data.RArray
Lean.RArray.branch.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : ℕ) (a_1 a_2 : Lean.RArray α),
  sizeOf (Lean.RArray.branch a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.scMapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ)
  (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.scMapIso._auto_1),
  (CategoryTheory.ComposableArrows.scMapIso e h₁ h₂ i hi).inv = CategoryTheory.ComposableArrows.scMap e.inv h₂ h₁ i hi
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instWeakEquivalenceHomFullSubcategory : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.WeakEquivalence f.hom
-- Init.Data.Vector.Lemmas
Vector.all_bne : ∀ {α : Type u_1} {n : ℕ} {a : α} [inst : BEq α] {xs : Vector α n}, (xs.all fun x => a != x) = !xs.contains a
-- Mathlib.Lean.Meta.Simp
/-- Checks whether `declName` is in `SimpTheorems` as either a lemma or definition to unfold.  -/
Lean.Meta.SimpTheorems.contains : Lean.Meta.SimpTheorems → Lean.Name → Bool
-- Std.Do.PostCond
Std.Do.ExceptConds.entails.eq_3 : ∀ (ε : Type u) (ps_2 : Std.Do.PostShape) (x_2 y_2 : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps_2)),
  x_2.entails y_2 = ((∀ (e : ε), x_2.1 e ⊢ₛ y_2.1 e) ∧ x_2.2.entails y_2.2)
-- Init.Data.Option.Lemmas
Option.ite_none_right_eq_some : ∀ {α : Type u_1} {a : α} {p : Prop} {x : Decidable p} {b : Option α}, (if p then b else none) = some a ↔ p ∧ b = some a
-- Mathlib.Data.Set.Card
Set.encard_sdiff_add_encard_inter : ∀ {α : Type u_1} (s t : Set α), (s \ t).encard + (s ∩ t).encard = s.encard
-- Mathlib.Algebra.Group.Action.Option
Option.instFaithfulSMul : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] [FaithfulSMul M α], FaithfulSMul M (Option α)
-- Mathlib.Data.FP.Basic
FP.Float.finite : [C : FP.FloatCfg] → Bool → (e : ℤ) → (m : ℕ) → FP.ValidFinite e m → FP.Float
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedObj : Inhabited Mathlib.Tactic.BicategoryLike.Obj
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonNameMap : {α : Type} → [Lean.FromJson α] → Lean.FromJson (Lean.NameMap α)
-- Mathlib.MeasureTheory.Constructions.Pi
Equiv.arrowCongr'.eq_1 : ∀ {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂),
  hα.arrowCongr' hβ = hα.arrowCongr hβ
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem.alts : Lean.Meta.Match.Problem → List Lean.Meta.Match.Alt
-- Init.Grind.Interactive
/-- `intros~` is shorthand for `intros (internalize := false)`.  -/
Lean.Parser.Tactic.Grind.symIntrosLight : Lean.ParserDescr
-- Mathlib.Topology.Order.IsLUB
IsGLB.frequently_nhds_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsGLB s a → s.Nonempty → ∃ᶠ (x : α) in nhds a, x ∈ s
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
aemeasurable_id' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, AEMeasurable (fun x => x) μ
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofArrows_category : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {S : C} (R : CategoryTheory.Sieve S),
  (CategoryTheory.Sieve.ofArrows (fun f => f.obj.left) fun f => f.obj.hom) = R
-- Init.Grind.Config
/-- When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
`CommRing`.
 -/
Lean.Grind.Config.linarith : Lean.Grind.Config → Bool
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.closure_eq_of_le : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {t : NonUnitalSubsemiring R},
  s ⊆ ↑t → t ≤ NonUnitalSubsemiring.closure s → NonUnitalSubsemiring.closure s = t
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The first projection on a domain in a product is `C^∞`.  -/
contDiffOn_fst : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {s : Set (E × F)}, ContDiffOn 𝕜 n Prod.fst s
-- Mathlib.RepresentationTheory.Rep.Res
Rep.instPreservesColimitsResFunctor : ∀ {G : Type v1} {H : Type v2} [inst : Monoid G] [inst_1 : Monoid H] (f : H →* G) {k : Type u} [inst_2 : Ring k],
  CategoryTheory.Limits.PreservesColimits (Rep.resFunctor f)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] {Z : HomotopyCategory D (ComplexShape.down ℕ)}
      (h :
        (HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶
          Z),
      CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f)
          (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj F).hom h) =
        CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom
          (CategoryTheory.CategoryStruct.comp
            ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
              ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ))
            h)
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.initCapacity : ℕ
-- Mathlib.Algebra.Order.Sub.Basic
AddLECancellable.tsub_right_inj : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α},
  AddLECancellable a → AddLECancellable b → AddLECancellable c → b ≤ a → c ≤ a → (a - b = a - c ↔ b = c)
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The basis of `S ⊗[T] J/J²` induced from the basis on `I/I²`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basisLeft : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    Module.Basis σ S
                      (TensorProduct (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) S
                        (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toExtension.Cotangent)
-- Init.Data.List.Perm
List.Perm.cons_inv : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Perm (a :: l₂) → l₁.Perm l₂
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.brecOn.eq : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {motive : Turing.TM1.Stmt Γ Λ σ → Sort u} (t : Turing.TM1.Stmt Γ Λ σ)
  (F_1 : (t : Turing.TM1.Stmt Γ Λ σ) → Turing.TM1.Stmt.below t → motive t),
  Turing.TM1.Stmt.brecOn t F_1 = F_1 t (Turing.TM1.Stmt.brecOn.go t F_1).2
-- Mathlib.MeasureTheory.Measure.Regular
IsCompact.exists_isOpen_lt_of_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α},
  IsCompact K → ∀ (r : ENNReal), μ K < r → ∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < r
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k k' : α} {f : β → β},
  (m.modify k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_mul_two`. -/
Ordinal.principal_mul_two : Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) 2
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {a k : α} {v : β k}, (m.insert k v).get? a = if h : (k == a) = true then some (cast ⋯ v) else m.get? a
-- Init.Data.UInt.BasicAux
/-- Converts a `USize` into the corresponding `Fin USize.size`.  -/
USize.toFin : USize → Fin USize.size
-- Init.Internal.Order.Basic
Lean.Order.instCCPOExceptT : {m : Type u_1 → Type u_2} →
  {ε α : Type u_1} → [inst : (α : Type u_1) → Lean.Order.CCPO (m α)] → Lean.Order.CCPO (ExceptT ε m α)
-- Mathlib.Data.Vector.Basic
List.Vector.ofFn_get : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n), List.Vector.ofFn v.get = v
-- Batteries.Data.List.Basic
/-- `rotate'` is the same as `rotate`, but slower. Used for proofs about `rotate`  -/
List.rotate' : {α : Type u_1} → List α → ℕ → List α
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabBVar : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.add_left_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν : MeasureTheory.Measure α},
  (μ₁ + μ₂).MutuallySingular ν ↔ μ₁.MutuallySingular ν ∧ μ₂.MutuallySingular ν
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- Note: this assumes `[IsLeftUniformAddGroup β] [IsRightUniformAddGroup β]`
instead of the more typical (and equivalent) `[IsUniformAddGroup β]` because this is used
in the proof of said equivalence.  -/
comap_addConj_nhds_zero : ∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : AddGroup β] [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β],
  Filter.comap (fun gx => gx.1 + gx.2 + -gx.1) (nhds 0) = Filter.comap Prod.snd (nhds 0)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- In a category with weak equivalences, a cylinder is the
data of a weak equivalence `π : I ⟶ A` equipped with two sections  -/
HomotopicalAlgebra.Cylinder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → C → Type (max u v)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.lift.congr_simp : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra.FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I)
  (g g_1 : A →ₐ[R] B ⧸ I), g = g_1 → Algebra.FormallySmooth.lift I hI g = Algebra.FormallySmooth.lift I hI g_1
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.lt_card_ge_iff_apply_ge_of_antitone : ∀ {n : ℕ} {α : Type u_1} {j : Fin n} {f : Fin n → α} [inst : Preorder α] {a : α} [inst_1 : DecidableLE α],
  Antitone f → (↑j < {i | a ≤ f i}.card ↔ a ≤ f j)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.uniqueDiffOn_extendCoordChange_target : ∀ {𝕜 : 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} {e e' : OpenPartialHomeomorph M H},
  UniqueDiffOn 𝕜 (ModelWithCorners.extendCoordChange e e').target
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_fintype : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] [inst_1 : Fintype α], Ordinal.type r = ↑(Fintype.card α)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- (Impl) Establish an equivalence between the category of cones for `F` and for the "grown" `F`.
 -/
CategoryTheory.Over.ConstructProducts.conesEquiv : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (B : C) →
        (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) →
          CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F) ≌
            CategoryTheory.Limits.Cone F
-- Lean.Meta.Hint
Lean.Meta.Hint.DiffGranularity.noConfusionType : Sort v✝ → Lean.Meta.Hint.DiffGranularity → Lean.Meta.Hint.DiffGranularity → Sort v✝
-- Mathlib.Analysis.Normed.Group.Uniform
locallyLipschitz_neg_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E},
  LocallyLipschitz (-f) ↔ LocallyLipschitz f
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Whether the rewrite introduces new metavariables with the replacement.  -/
Mathlib.Tactic.LibraryRewrite.RewriteInterface.makesNewMVars : Mathlib.Tactic.LibraryRewrite.RewriteInterface → Bool
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.multicofork_pt : ∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T}
  (d : CompleteLattice.MulticoequalizerDiagram x u v), d.multicofork.pt = x
-- Init.Grind.Ring.Basic
/-- A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers,
satisfying appropriate compatibilities.

Use `CommRing` if the multiplication is commutative.
 -/
Lean.Grind.Ring : Type u → Type u
-- Lean.Message
Lean.MessageLog.mk.sizeOf_spec : ∀ (reported unreported : Lean.PersistentArray Lean.Message) (loggedKinds : Lean.NameSet),
  sizeOf { reported := reported, unreported := unreported, loggedKinds := loggedKinds } =
    1 + sizeOf reported + sizeOf unreported + sizeOf loggedKinds
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_right_inj : ∀ {w : ℕ} (a b c : BitVec w), (c + a == c + b) = (a == b)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.sub : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [IsNoetherianRing K] {f g : V →ₗ[K] V₂},
  f.HasFiniteRange → g.HasFiniteRange → (f - g).HasFiniteRange
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X},
  R f → CategoryTheory.Presieve.map F R (F.map f)
-- Lean.Parser.Term
Lean.Parser.Term.macroDollarArg.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongrEquiv_apply : ∀ {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 : M [⋀^ι]→ₗ[R] N),
  (AlternatingMap.domDomCongrEquiv σ) f = AlternatingMap.domDomCongr σ f