mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Control.Lawful.Lemmas
Exists.choose.congr_simp : ∀ {α : Sort u_1} {p p_1 : α → Prop} (e_p : p = p_1) (P : ∃ a, p a), P.choose = ⋯.choose
-- Mathlib.Algebra.CharP.Quotient
Ideal.natCast_mem_of_charP_quotient : ∀ {R : Type u_1} [inst : CommRing R] (p : ℕ) (I : Ideal R) [CharP (R ⧸ I) p], ↑p ∈ I
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.map_relations_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)), (P.map F η).relations.I = P.relations.I
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- The natural isomorphism
`F.mapShortComplex ⋙ rightHomologyFunctor D ≅ rightHomologyFunctor C ⋙ F`
for a functor `F : C ⥤ D` which preserves homology.  -/
CategoryTheory.ShortComplex.rightHomologyFunctorIso : {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] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.PreservesZeroMorphisms] →
                [inst_5 : CategoryTheory.Limits.HasKernels C] →
                  [inst_6 : CategoryTheory.Limits.HasCokernels C] →
                    [inst_7 : CategoryTheory.Limits.HasKernels D] →
                      [inst_8 : CategoryTheory.Limits.HasCokernels D] →
                        [F.PreservesHomology] →
                          F.mapShortComplex.comp (CategoryTheory.ShortComplex.rightHomologyFunctor D) ≅
                            (CategoryTheory.ShortComplex.rightHomologyFunctor C).comp F
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal : ∀ {α : Type u_2} [inst : TopologicalSpace α] (Λ : CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal)
  (f : CompactlySupportedContinuousMap α NNReal),
  (CompactlySupportedContinuousMap.toRealPositiveLinear Λ) f.toReal = ↑(Λ f)
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Database.stacks : Mathlib.CrossRef.Database
-- Std.Http.Data.Chunk
/-- Interprets the chunk data as a UTF-8 encoded string.
 -/
Std.Http.Chunk.toString? : Std.Http.Chunk → Option String
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.isDetpBalanced_submatrix_equiv_iff : ∀ {n : Type u_1} {m : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommSemiring R] {A : Matrix n n R} {a b : R} {e₁ e₂ : m ≃ n},
  (A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b ↔ A.IsDetpBalanced a b
-- Init.Data.Nat.Fold
/-- `Nat.dfoldRev` evaluates `f` on the numbers up to `n` exclusive, in decreasing order:
* `Nat.dfoldRev f 3 init = f 0 <| f 1 <| f 2 <| init`
The input and output types of `f` are indexed by the current index, i.e. `f : (i : Nat) → (h : i < n) → α (i + 1) → α i`.
 -/
Nat.dfoldRev : (n : ℕ) →
  {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldRev._auto_1 → Type u} →
    ((i : ℕ) → (h : i < n) → α (i + 1) ⋯ → α i ⋯) → α n ⋯ → α 0 ⋯
-- Lean.Elab.Tactic.Try
/-- Erases tactics `skip` and `done` from `tacs`  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.filterSkipDone : Array (Lean.TSyntax `tactic) → Array (Lean.TSyntax `tactic)
-- Mathlib.Order.Partition.Finpartition
Finpartition.sum_card_parts : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s), ∑ i ∈ P.parts, i.card = s.card
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ico_left : ∀ {α : Type v} [inst : Preorder α] (a : α), ⋃ b, Set.Ico b a = Set.Iio a
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.PreservesEpimorphisms.of_iso`. -/
CategoryTheory.Functor.preservesEpimorphisms.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.PreservesEpimorphisms] (α : F ≅ G), G.PreservesEpimorphisms
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.opNorm_prod : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (f : E [⋀^ι]→L[𝕜] F) (g : E [⋀^ι]→L[𝕜] G), ‖f.prod g‖ = max ‖f‖ ‖g‖
-- Mathlib.CategoryTheory.Noetherian
/-- A category is Noetherian if it is essentially small and all objects are Noetherian.  -/
CategoryTheory.Noetherian : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.SetTheory.Ordinal.Notation
NONote.instLinearOrder : LinearOrder NONote
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.id_apply : ∀ (R : RingCat) (r : ↑R), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id R)) r = r
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mulVec_surjective_of_invertible : ∀ {m : Type u} [inst : DecidableEq m] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Fintype m] (A : Matrix m m R)
  [Invertible A], Function.Surjective A.mulVec
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.hasAnyFVar.visit : (Lean.FVarId → Bool) → Lean.Expr → Bool
-- Mathlib.Data.Rat.Defs
Rat.addCommGroup : AddCommGroup ℚ
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl : ∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : IsDomain R] [inst_4 : IsDomain S] [inst_5 : IsDomain T] [inst_6 : Algebra R S] {P : Ideal R}
  [inst_7 : P.IsPrime] [inst_8 : FaithfulSMul R S] [inst_9 : Algebra S T] [inst_10 : Algebra R T]
  [inst_11 : IsScalarTower R S T] [inst_12 : Module.IsTorsionFree R T] [inst_13 : Module.IsTorsionFree S T]
  [Algebra.IsSeparable (FractionRing S) (FractionRing T)],
  Algebra.IsSeparable (FractionRing (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)))
    (FractionRing (Localization (Algebra.algebraMapSubmonoid T P.primeCompl)))
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.ObjectProperty.HasInducedTStructure.exists_triangle_zero_one : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} 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}
  {P : CategoryTheory.ObjectProperty C} {t : CategoryTheory.Triangulated.TStructure C} {inst_6 : P.IsTriangulated}
  [self : P.HasInducedTStructure t] (A : C),
  P A →
    ∃ X Y,
      ∃ (_ : t.IsLE X 0) (_ : t.IsGE Y 1),
        ∃ f g h,
          ∃ (_ :
            CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
            P.isoClosure X ∧ P.isoClosure Y
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.map_neg₂ : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {N : Type u_7} [inst_4 : AddCommMonoid N] [inst_5 : Module S N]
  {M' : Type u_12} {P' : Type u_13} [inst_6 : AddCommGroup M'] [inst_7 : AddCommGroup P'] [inst_8 : Module R M']
  [inst_9 : Module R₂ P'] [inst_10 : Module S₂ P'] [inst_11 : SMulCommClass S₂ R₂ P'] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x : M') (y : N), (f (-x)) y = -(f x) y
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.coe_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], ↑⊥ = {0}
-- Mathlib.SetTheory.Ordinal.Family
/-- The range of a family indexed by ordinals.  -/
Ordinal.brange : {α : Type u_1} → (o : Ordinal.{u_3}) → ((a : Ordinal.{u_3}) → a < o → α) → Set α
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`.  -/
SubgroupClass.inclusion : {G : Type u_1} →
  [inst : Group G] →
    {S : Type u_4} →
      [inst_1 : SetLike S G] →
        [inst_2 : SubgroupClass S G] → [inst_3 : LE S] → [IsConcreteLE S G] → {H K : S} → H ≤ K → ↥H →* ↥K
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.val_step_filterMap.match_3.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} {base : X.base ⟶ Y.base} {fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber}
  {base_1 : X.base ⟶ Y.base} {fiber_1 : (F.map base_1).toFunctor.obj X.fiber ⟶ Y.fiber},
  { base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 } → base = base_1 ∧ fiber ≍ fiber_1
-- Init.Data.ByteArray.Basic
/-- Retrieves the byte at the indicated index. Callers must prove that the index is in bounds. The index
is represented by a platform-specific fixed-width integer \(either 32 or 64 bits\).

Because `USize` is big enough to address all memory on every platform that Lean supports, there are
in practice no `ByteArray`s for which `uget` cannot retrieve all elements.
 -/
ByteArray.uget : (a : ByteArray) → (i : USize) → autoParam (i.toNat < a.size) ByteArray.uget._auto_1 → UInt8
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of two strictly monotone functions is strictly monotone.  -/
StrictMono.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
  [AddLeftStrictMono α] [AddRightStrictMono α], StrictMono f → StrictMono g → StrictMono fun x => f x + g x
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbit_addSubmonoid_subset : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] (S : AddSubmonoid M) (a : α),
  AddAction.orbit (↥S) a ⊆ AddAction.orbit M a
-- Init.Data.Option.Lemmas
Option.merge_le_iff : ∀ {α : Type u_1} [inst : LE α] {f : α → α → α} {o₁ o₂ o₃ : Option α},
  (∀ (a b c : α), f a b ≤ c ↔ a ≤ c ∧ b ≤ c) → (Option.merge f o₁ o₂ ≤ o₃ ↔ o₁ ≤ o₃ ∧ o₂ ≤ o₃)
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instBiproduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Type v} (c : β → C)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasBiproduct c]
  [∀ (b : β), CategoryTheory.Injective (c b)], CategoryTheory.Injective (⨁ c)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_le_self_iff : ∀ {x : ℝ}, Real.sinh x ≤ x ↔ x ≤ 0
-- Mathlib.Order.Fin.Basic
/-- `Fin.castSucc` as an `OrderEmbedding`.

`castSuccOrderEmb i` embeds `i : Fin n` in `Fin (n+1)`.  -/
Fin.castSuccOrderEmb : {n : ℕ} → Fin n ↪o Fin (n + 1)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.ne_zero_of_coeff_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} {g : Γ},
  x.coeff g ≠ 0 → x ≠ 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.mk : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, DirSupClosed s → IsCofinal s → IsClub s
-- Mathlib.Algebra.Group.Action.End
MulAction.toPerm_one : ∀ (G : Type u_1) (α : Type u_5) [inst : Group G] [inst_1 : MulAction G α], MulAction.toPerm 1 = 1
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
/-- A Klein four-group is a group of cardinality four and exponent two.  -/
IsKleinFour : (G : Type u_1) → [Group G] → Prop
-- Lean.Elab.Tactic.Try
/-- Wraps a tactic suggestion as a term suggestion by prefixing with `by `.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.wrapSuggestionWithBy : Lean.Meta.Tactic.TryThis.Suggestion → Lean.Elab.Tactic.TacticM Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.mk : ∀ {𝕜 : 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] {f : E → F} {s : Set E},
  DifferentiableOn 𝕜 f s → ContinuousOn f (closure s) → DiffContOnCl 𝕜 f s
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instT1Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T1Space M], T1Space Mᵈᵃᵃ
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.liftHom.eq_def : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C)
  (x x_1 : CategoryTheory.FreeBicategory B) (x_2 : x ⟶ x_1),
  CategoryTheory.FreeBicategory.liftHom F x_2 =
    match x, x_1, x_2 with
    | x, x_3, CategoryTheory.FreeBicategory.Hom.of f => F.map f
    | a, .(a), CategoryTheory.FreeBicategory.Hom.id .(a) => CategoryTheory.CategoryStruct.id (F.obj a)
    | x, x_3, f.comp g =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.liftHom F f)
        (CategoryTheory.FreeBicategory.liftHom F g)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd_inj_iff : ∀ {R : Type u_1} {A : Type u_2} {x y : Unitization R A}, x.toProd = y.toProd ↔ x = y
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- Conjugating preserves self-adjointness.  -/
IsSelfAdjoint.conj_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] {T : E →L[𝕜] E},
  IsSelfAdjoint T → ∀ (S : E →L[𝕜] F), IsSelfAdjoint (S ∘SL T ∘SL ContinuousLinearMap.adjoint S)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
RingEquiv.ofRingHom.congr_simp : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f f_1 : R →+* S)
  (e_f : f = f_1) (g g_1 : S →+* R) (e_g : g = g_1) (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R),
  RingEquiv.ofRingHom f g h₁ h₂ = RingEquiv.ofRingHom f_1 g_1 ⋯ ⋯
-- Lean.Util.ShareCommon
Lean.ShareCommon.ShareCommonT : (Type u_1 → Type u_2) → Type u_1 → Type (max u_1 u_2)
-- Mathlib.Data.Int.Cast.Lemmas
MonoidHom.ext_int_iff : ∀ {M : Type u_5} [inst : Monoid M] {f g : ℤ →* M}, f = g ↔ f (-1) = g (-1) ∧ f.comp ↑Int.ofNatHom = g.comp ↑Int.ofNatHom
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instBEqHost : BEq Std.Http.Header.Host
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_add_termg : ∀ {α : Type u_1} [inst : AddCommGroup α] (n₁ : ℤ) (x a₁ : α) (n₂ : ℤ) (a₂ : α) (n' : ℤ) (a' : α),
  n₁ + n₂ = n' →
    a₁ + a₂ = a' →
      Mathlib.Tactic.Abel.termg n₁ x a₁ + Mathlib.Tactic.Abel.termg n₂ x a₂ = Mathlib.Tactic.Abel.termg n' x a'
-- Mathlib.GroupTheory.Perm.Fin
Fin.cons_comp_cycleRange : ∀ {n : ℕ} {α : Type u_1} (a : α) (x : Fin n → α) (p : Fin (n + 1)), Fin.cons a x ∘ ⇑p.cycleRange = p.insertNth a x
-- Mathlib.MeasureTheory.VectorMeasure.AddContent
/-- Consider an additive content `m ` on a semi-ring of sets `C`, which is dominated by a finite
measure `μ`. Assume that `C` generates the sigma-algebra and covers the space up to measure zero.
Then `m` extends to a countably additive vector measure which is dominated by `μ`.  -/
_private.Mathlib.MeasureTheory.VectorMeasure.AddContent.0.MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom_of_cover : ∀ {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [CompleteSpace E]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {C : Set (Set α)} {m : MeasureTheory.AddContent E C},
  MeasureTheory.IsSetSemiring C →
    (∀ s ∈ C, ‖m s‖ₑ ≤ μ s) →
      hα = MeasurableSpace.generateFrom C →
        (∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) → ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
-- Mathlib.Order.Filter.Bases.Basic
Filter.disjoint_principal_principal : ∀ {α : Type u_1} {s t : Set α}, Disjoint (Filter.principal s) (Filter.principal t) ↔ Disjoint s t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_insertIfNew_le_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α} {v : β}, (cmp (t.insertIfNew k v).minKey! t.minKey!).isLE = true
-- Lean.Compiler.ExternAttr
Lean.getExternNameFor : Lean.Environment → Lean.Name → Lean.Name → Option String
-- Mathlib.Data.Fin.Tuple.Finset
Finset.filter_piFinset_eq_map_insertNthEquiv : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {p : Fin (n + 1)} (S : (i : Fin (n + 1)) → Finset (α i))
  (P : ((i : Fin n) → α (p.succAbove i)) → Prop) [inst : DecidablePred P],
  {r ∈ Fintype.piFinset S | P (p.removeNth r)} =
    Finset.map (Fin.insertNthEquiv α p).toEmbedding (S p ×ˢ {r ∈ Fintype.piFinset (p.removeNth S) | P r})
-- Batteries.Recycling.RBTree.Basic
/-- We say that `x ≈ y` under the comparator `cmp` if `cmp x y = .eq`. See also `cmpLT`.  -/
RBTree.RBNode.cmpEq : {α : Type u_1} → (α → α → Ordering) → α → α → Prop
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp_self : ∀ (c : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal c k) ⊆ Turing.PartrecToTM2.codeSupp c k
-- Mathlib.Order.Defs.PartialOrder
lt_iff_le_iff_gt_iff_ge : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (a < b ↔ a ≤ b) ↔ (b < a ↔ b ≤ a)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Structure witnessing that a binary bicone is a limit cone and a limit cocone.  -/
CategoryTheory.Limits.BinaryBicone.IsBilimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → CategoryTheory.Limits.BinaryBicone P Q → Type (max uC uC')
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_eq_bot_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) {f : G →+ N},
  AddSubgroup.map f H = ⊥ ↔ H ≤ f.ker
-- Mathlib.Algebra.Group.Basic
add_sub_add_left_eq_sub : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), c + a - (c + b) = a - b
-- Mathlib.RingTheory.AdicCompletion.Completeness
/-- The canonical inclusion from the adic completion of `I ^ n • M` to
the adic completion of `M`.  -/
AdicCompletion.ofPowSMul : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_2) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → (n : ℕ) → AdicCompletion I ↥(I ^ n • ⊤) →ₗ[AdicCompletion I R] AdicCompletion I M
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_preimage_vadd_null : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : VAdd G α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α}, μ s = 0 → ∀ (c : G), μ ((fun x => c +ᵥ x) ⁻¹' s) = 0
-- Mathlib.Order.Interval.Finset.Defs
instFiniteSubtypeLeOfLocallyFiniteOrderBot : ∀ {α : Type u_1} [inst : Preorder α] {y : α} [LocallyFiniteOrderBot α], Finite { x // x ≤ y }
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.algHom_deriv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] {R : Type u_2} [inst_2 : CommRing R]
  [inst_3 : Differential R] [inst_4 : Algebra A R] [DifferentialAlgebra A R] {R' : Type u_3} [inst_6 : CommRing R']
  [inst_7 : Differential R'] [inst_8 : Algebra A R'] [DifferentialAlgebra A R'] [IsDomain R'] [Nontrivial R]
  (f : R →ₐ[A] R'), Function.Injective ⇑f → ∀ (x : R), IsSeparable A x → f x′ = (f x)′
-- Mathlib.Topology.Sion
/-- The Sion-von Neumann minimax theorem (saddle point form),
case of complete linear orders.  -/
Sion.exists_saddlePointOn' : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : CompleteLinearOrder β] [DenselyOrdered β] {X : Set E} {Y : Set F}
  {f : E → F → β} [inst_2 : TopologicalSpace E] [inst_3 : AddCommGroup E] [inst_4 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E],
  X.Nonempty →
    Convex ℝ X →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
            ∀ [inst_7 : TopologicalSpace F] [inst_8 : AddCommGroup F] [inst_9 : Module ℝ F] [IsTopologicalAddGroup F]
              [ContinuousSMul ℝ F],
              Convex ℝ Y →
                Y.Nonempty →
                  IsCompact Y →
                    (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                      (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) → ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
-- Init.Data.UInt.Bitwise
UInt64.toUSize_xor : ∀ (a b : UInt64), (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
-- Mathlib.Topology.Constructions.SumProd
/-- If `f` and `g` are maps with dense range, then `Prod.map f g` has dense range.  -/
DenseRange.prodMap : ∀ {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {ι : Type u_5} {κ : Type u_6}
  {f : ι → Y} {g : κ → Z}, DenseRange f → DenseRange g → DenseRange (Prod.map f g)
-- Mathlib.Computability.Primrec.Basic
_private.Mathlib.Computability.Primrec.Basic.0.Encodable.decodeSum.match_1.eq_2 : ∀ (motive : Bool → ℕ → Sort u_1) (x : Bool) (m : ℕ) (h_1 : (m : ℕ) → motive false m)
  (h_2 : (x : Bool) → (m : ℕ) → motive x m),
  (x = false → False) →
    (match x, m with
      | false, m => h_1 m
      | x, m => h_2 x m) =
      h_2 x m
-- Aesop.Tree.TreeM
Aesop.TreeM.State.tree : Aesop.TreeM.State → Aesop.Tree
-- Std.Net.Addr
Std.Net.SocketAddress.v6.sizeOf_spec : ∀ (addr : Std.Net.SocketAddressV6), sizeOf (Std.Net.SocketAddress.v6 addr) = 1 + sizeOf addr
-- Mathlib.Order.BoundedOrder.Basic
eq_top_mono : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, a ≤ b → a = ⊤ → b = ⊤
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If orders are finite, the divisor of the product of two meromorphic functions is the sum of the
divisors.

See `MeromorphicOn.exists_order_ne_top_iff_forall` and
`MeromorphicOn.order_ne_top_of_isPreconnected` for two convenient criteria to guarantee conditions
`h₂f₁` and `h₂f₂`.
 -/
MeromorphicOn.divisor_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f₁ f₂ : 𝕜 → 𝕜},
  MeromorphicOn f₁ U →
    MeromorphicOn f₂ U →
      (∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) →
        (∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) →
          MeromorphicOn.divisor (f₁ * f₂) U = MeromorphicOn.divisor f₁ U + MeromorphicOn.divisor f₂ U
-- Init.Data.Int.Gcd
Int.gcd_ediv_gcd_ediv_gcd_of_ne_zero_left : ∀ {n m : ℤ}, n ≠ 0 → (n / ↑(n.gcd m)).gcd (m / ↑(n.gcd m)) = 1
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosStrictMono.to_covariantClass_pos_mul_le : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulPosStrictMono α],
  CovariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
-- Init.Grind.AC
Lean.Grind.AC.simp_ac_cert.eq_1 : ∀ (c lhs rhs s s' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_ac_cert c lhs rhs s s' = (s.beq' (c.union_k lhs)).and' (s'.beq' (c.union_k rhs))