mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAtFilter_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (L : Filter (E × E)), HasFDerivAtFilter 0 0 L
-- Mathlib.RingTheory.Prime
Prime.abs : ∀ {α : Type u_1} [inst : CommRing α] [inst_1 : LinearOrder α] {p : α}, Prime p → Prime |p|
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec.map_inv : ∀ {R S : CommRingCat} (f : R ⟶ S) [inst : CategoryTheory.IsIso f],
  AlgebraicGeometry.Spec.map (CategoryTheory.inv f) = CategoryTheory.inv (AlgebraicGeometry.Spec.map f)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.IsReduced.of_reduce_eq : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeAddGroup.reduce L = L → FreeAddGroup.IsReduced L
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.map_zero : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B), f 0 = 0
-- Mathlib.Data.Multiset.Dedup
Multiset.le_dedup_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s ≤ s.dedup ↔ s.Nodup
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_eq_one_iff : ∀ {d : ℤ} {x : ℤ√d}, x.norm.natAbs = 1 ↔ IsUnit x
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.card_left : ∀ {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [inst : DecidableEq α] {v w₁ w₂ : α} {t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → s.card = r
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent.map.eq_1 : ∀ {A : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommRing A] (I : Ideal A) [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module A M₁] [inst_4 : Module A M₂] (φ : M₁ →ₗ[A] M₂),
  Ideal.primaryComponent.map I φ =
    LinearMap.codRestrict (Ideal.primaryComponent M₂ I) (φ.domRestrict (Ideal.primaryComponent M₁ I)) ⋯
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3) (sz : ℕ)
  (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced)
  (h_1 : (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr),
  (match Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr => h_2 sz k' v' l' r' hr) =
    h_2 sz k' v' l' r' hr
-- Mathlib.NumberTheory.SelbergSieve
SelbergSieve.toBoundingSieve : SelbergSieve → BoundingSieve
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
SpectrumRestricts.cfc_eq_restrict : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S]
  [inst_10 : Ring A] [inst_11 : StarRing A] [inst_12 : Algebra S A] [inst_13 : Algebra R S] [inst_14 : Algebra R A]
  [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [inst_18 : TopologicalSpace A]
  [inst_19 : ContinuousFunctionalCalculus S A q] [inst_20 : ContinuousFunctionalCalculus R A p]
  [ContinuousMap.UniqueHom R A] (f : C(S, R)),
  Topology.IsClosedEmbedding ⇑(algebraMap R S) →
    ∀ {a : A}, p a → q a → SpectrumRestricts a ⇑f → ∀ (g : R → R), cfc g a = cfc (fun x => (algebraMap R S) (g (f x))) a
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.seminormedCommGroup.eq_1 : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F],
  Prod.seminormedCommGroup =
    { toNorm := Prod.seminormedGroup.toNorm, toGroup := Prod.seminormedGroup.toGroup, mul_comm := ⋯,
      toPseudoMetricSpace := Prod.seminormedGroup.toPseudoMetricSpace, dist_eq := ⋯ }
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.instLT : {α : ℚ} → LT (Std.Time.Internal.UnitVal α)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_eq_zero : ∀ {m : ℕ∞}, ↑m = 0 ↔ m = 0
-- Mathlib.CategoryTheory.Preadditive.Schur
/-- An auxiliary lemma for Schur's lemma.

If `X ⟶ X` is finite dimensional, and every nonzero endomorphism is invertible,
then `X ⟶ X` is 1-dimensional.
 -/
CategoryTheory.finrank_endomorphism_eq_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : Field 𝕜] [IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] {X : C},
  (∀ (f : X ⟶ X), CategoryTheory.IsIso f ↔ f ≠ 0) → ∀ [I : FiniteDimensional 𝕜 (X ⟶ X)], Module.finrank 𝕜 (X ⟶ X) = 1
-- Mathlib.Data.List.SplitLengths
List.take_splitLength : ∀ {α : Type u_1} (l : List α) (sz : List ℕ) (i : ℕ), List.take i (sz.splitLengths l) = (List.take i sz).splitLengths l
-- Mathlib.CategoryTheory.Triangulated.Generators
/-- All objects that can be reached by shifts, binary products, retracts and at most `n`
extensions from objects in `P`.  -/
CategoryTheory.ObjectProperty.triangEnvelopeIter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → ℕ → CategoryTheory.ObjectProperty C
-- Init.Data.Vector.Lemmas
Vector.mk_append_mk : ∀ {α : Type u_1} {n m : ℕ} {xs ys : Array α} (h : xs.size = n) (h' : ys.size = m),
  Vector.mk xs h ++ Vector.mk ys h' = Vector.mk (xs ++ ys) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.IsBilimit.mk.inj : ∀ {J : Type w} {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {B : CategoryTheory.Limits.Bicone F}
  {isLimit : CategoryTheory.Limits.IsLimit B.toCone} {isColimit : CategoryTheory.Limits.IsColimit B.toCocone}
  {isLimit_1 : CategoryTheory.Limits.IsLimit B.toCone} {isColimit_1 : CategoryTheory.Limits.IsColimit B.toCocone},
  { isLimit := isLimit, isColimit := isColimit } = { isLimit := isLimit_1, isColimit := isColimit_1 } →
    isLimit = isLimit_1 ∧ isColimit = isColimit_1
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
LieGroup.toContMDiffMul : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} {inst_4 : Group G} {inst_5 : TopologicalSpace G} {inst_6 : ChartedSpace H G} [self : LieGroup I n G],
  ContMDiffMul I n G
-- Lean.Parser.Command
Lean.Parser.Command.attribute.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousLinearEquiv.nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [CompleteSpace E] (e : E ≃L[𝕜] F), Set.range ContinuousLinearEquiv.toContinuousLinearMap ∈ nhds ↑e
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instHasLimits : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  CategoryTheory.Limits.HasLimits (GeneratedByTopCat X)
-- Init.Omega.Constraint
Lean.Omega.Constraint.combo_sat : ∀ {c₁ c₂ : Lean.Omega.Constraint} {x₁ x₂ : ℤ} (a : ℤ),
  c₁.sat x₁ = true → ∀ (b : ℤ), c₂.sat x₂ = true → (Lean.Omega.Constraint.combo a c₁ b c₂).sat (a * x₁ + b * x₂) = true
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.map_map : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] {M'' : Type u_6} {N'' : Type u_7} [inst_4 : AddZeroClass M'']
  [inst_5 : AddZeroClass N''] (f' : M' →+ M'') (g' : N' →+ N'') (f : M →+ M') (g : N →+ N') (x : AddMonoid.Coprod M N),
  (AddMonoid.Coprod.map f' g') ((AddMonoid.Coprod.map f g) x) = (AddMonoid.Coprod.map (f'.comp f) (g'.comp g)) x
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.mul_neg : ∀ {w : ℕ} (x y : BitVec w), x * (~~~y + 1#w) = ~~~(x * y) + 1#w
-- Init.Data.UInt.Lemmas
USize.toFin_mod : ∀ (a b : USize), (a % b).toFin = a.toFin % b.toFin
-- Mathlib.Algebra.Group.Conj
AddConjClasses.carrier_eq_preimage_mk : ∀ {α : Type u} [inst : AddMonoid α] {a : AddConjClasses α}, a.carrier = AddConjClasses.mk ⁻¹' {a}
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- The datum of an extra degeneracy is a technical condition on
augmented simplicial objects. The morphisms `s'` and `s n` of the
structure formally behave like extra degeneracies `σ (-1)`.  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.SimplicialObject.Augmented C → Type v_1
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
/-- **Alias** of the reverse direction of `SzemerediRegularity.stepBound_pos_iff`. -/
SzemerediRegularity.stepBound_pos : ∀ {n : ℕ}, 0 < n → 0 < SzemerediRegularity.stepBound n
-- Mathlib.Tactic.CongrExclamation
/-- A pass to clean up after `Lean.MVarId.preCongr!` and `Lean.MVarId.congrCore!`.  -/
Lean.MVarId.postCongr! : Congr!.Config → Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.affineLocally_respectsIso : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.v₀₁.τ₂ S.v₁₂.τ₂ = 0
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- A cocontinuous functor induces a pushforward functor on categories of sheaves.  -/
CategoryTheory.Functor.sheafPushforwardCocontinuous : {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] →
        (G : CategoryTheory.Functor C D) →
          (A : Type w) →
            [inst_2 : CategoryTheory.Category.{w', w} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [G.IsCocontinuous J K] →
                    [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] →
                      CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf K A)
-- Mathlib.Algebra.BigOperators.Intervals
/-- Gauss' summation formula  -/
Finset.sum_range_id : ∀ (n : ℕ), ∑ i ∈ Finset.range n, i = n * (n - 1) / 2
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendSingleIso.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : DecidableEq ι] (e : c.Embedding c') (X : C)
  [inst_4 : DecidableEq ι'] (i : ι) (i' : ι') (h : e.f i = i'),
  HomologicalComplex.extendSingleIso e X i i' h =
    {
      hom :=
        HomologicalComplex.mkHomToSingle
          (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c i).obj X).extendXIso e h).hom
            (HomologicalComplex.singleObjXSelf c i X).hom)
          ⋯,
      inv :=
        HomologicalComplex.mkHomFromSingle
          (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c i X).inv
            (((HomologicalComplex.single C c i).obj X).extendXIso e h).inv)
          ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Data.LawfulXor.Basic
xor_xor_cancel_comm_assoc : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] (a b : α), a ^^^ (b ^^^ a) = b
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.mem_inv_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S : Subsemiring R} {x : R}, x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t],
  (↑(Finset.map SimpleGraph.TripartiteFromTriangles.toTriangle t)).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- An induction principle for closure membership for predicates with two arguments.  -/
Subsemiring.closure_induction₂ : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R}
  {p : (x y : R) → x ∈ Subsemiring.closure s → y ∈ Subsemiring.closure s → Prop},
  (∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (x : R) (hx : x ∈ Subsemiring.closure s), p 0 x ⋯ hx) →
      (∀ (x : R) (hx : x ∈ Subsemiring.closure s), p x 0 hx ⋯) →
        (∀ (x : R) (hx : x ∈ Subsemiring.closure s), p 1 x ⋯ hx) →
          (∀ (x : R) (hx : x ∈ Subsemiring.closure s), p x 1 hx ⋯) →
            (∀ (x y z : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s)
                (hz : z ∈ Subsemiring.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
              (∀ (x y z : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s)
                  (hz : z ∈ Subsemiring.closure s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
                (∀ (x y z : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s)
                    (hz : z ∈ Subsemiring.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
                  (∀ (x y z : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s)
                      (hz : z ∈ Subsemiring.closure s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) →
                    ∀ {x y : R} (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s), p x y hx hy
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.intCast_add : ∀ {R : Type u_2} [inst : CommRing R] {b₁ b₂ : R} {a₁ a₂ : ℤ}, ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.congr_of_eventuallyEq_insert : ∀ {𝕜 : 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] {f g : E → F} {s : Set E}
  {x : E}, AnalyticWithinAt 𝕜 f s x → g =ᶠ[nhdsWithin x (insert x s)] f → AnalyticWithinAt 𝕜 g s x
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.extract : Substring.Raw → String.Pos.Raw → String.Pos.Raw → Substring.Raw
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstr.mk : Lean.Grind.Linarith.Poly → Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Lean.Meta.Grind.Arith.Linear.EqCnstr
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- **Alias** of the reverse direction of `ContinuousLinearMap.isIdempotentElem_toLinearMap_iff`. -/
ContinuousLinearMap.IsIdempotentElem.toLinearMap : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {f : M →L[R] M}, IsIdempotentElem f → IsIdempotentElem ↑f
-- Init.Data.UInt.Lemmas
UInt64.toUSize_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toUSize = USize.ofNat n
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_bitVecToNat : ∀ (n : BitVec 64), UInt64.ofNatLT n.toNat ⋯ = { toBitVec := n }
-- Init.Data.Nat.Fold
Nat.fold_eq_foldTR : @Nat.fold = @Nat.foldTR
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.SwapTrue.congr_simp : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o o_1 : Ordinal.{u}),
  o = o_1 →
    ∀ (a a_1 : I → Bool),
      a = a_1 →
        ∀ (a_2 a_3 : I),
          a_2 = a_3 → Profinite.NobelingProof.SwapTrue o a a_2 = Profinite.NobelingProof.SwapTrue o_1 a_1 a_3
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.lipschitzWith_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] [inst_1 : PseudoEMetricSpace β]
  {f : γ → UniformFun α β} {K : NNReal},
  LipschitzWith K f ↔ ∀ (c : α), LipschitzWith K fun x => UniformFun.toFun (f x) c
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isOpenEmbedding_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsOpenEmbedding ⇑DomMulAct.mk.symm
-- Mathlib.Algebra.Quaternion
Quaternion.im_idem : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a.im.im = a.im
-- Mathlib.Topology.Algebra.ConstMulAction
IsCompact.vadd : ∀ {α : Type u_4} {β : Type u_5} [inst : VAdd α β] [inst_1 : TopologicalSpace β] [ContinuousConstVAdd α β] (a : α)
  {s : Set β}, IsCompact s → IsCompact (a +ᵥ s)
-- Init.Data.List.Erase
List.mem_of_mem_erase : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l : List α}, a ∈ l.erase b → a ∈ l
-- Mathlib.Data.Sigma.Lex
/-- The lexicographical order on a sigma type. It takes in a relation on the index type and a
relation for each summand. `a` is related to `b` iff their summands are related or they are in the
same summand and are related through the summand's relation.  -/
Sigma.Lex : {ι : Type u_1} →
  {α : ι → Type u_2} → (ι → ι → Prop) → ((i : ι) → α i → α i → Prop) → (i : ι) × α i → (i : ι) × α i → Prop
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_eq_single_succ_iff : ∀ {n : ℕ} (i : Fin n) {M : Type u_1} [inst : Zero M] {y : M} {s : Fin n →₀ M} {x : M},
  (Finsupp.cons x s = fun₀ | i.succ => y) ↔ (s = fun₀ | i => y) ∧ x = 0
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.iso_w : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g),
  g.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left e.inv)
      (CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.Arrow.Hom.right e.hom))
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.defEvalConfigItem.hasInstance : Lean.Name → Lean.Expr → Lean.Elab.ConfigEval.M✝ Bool
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (h : W ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp h f = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruKernelSubobject f h w)
      (CategoryTheory.Limits.kernelSubobjectIso f).hom =
    CategoryTheory.Limits.kernel.lift f h w
-- Aesop.Stats.Basic
Aesop.ForwardInstantiationStats.mk : ℕ → ℕ → Aesop.ForwardInstantiationStats
-- Mathlib.RingTheory.Coalgebra.TensorProduct
/-- Comultiplication as a coalgebra hom.  -/
Coalgebra.comulCoalgHom : (R : Type u_5) →
  (C : Type u_6) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid C] →
        [inst_2 : Module R C] → [inst_3 : Coalgebra R C] → [Coalgebra.IsCocomm R C] → C →ₗc[R] TensorProduct R C C
-- Mathlib.Algebra.Homology.Single
CochainComplex.single₀_map_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {A B : V} (f : A ⟶ B), ((CochainComplex.single₀ V).map f).f 0 = f
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int8.beq_eq_decide_eq : ∀ {a b : Int8}, (a == b) = decide (a = b)
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- In a commutative Noetherian ring `R`, a prime ideal `p` has height no greater than `n` if and
only if it is a minimal ideal over some ideal generated by no more than `n` elements.  -/
Ideal.height_le_iff_exists_minimalPrimes : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] (n : ℕ∞),
  p.height ≤ n ↔ ∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Hilbert spaces, see `charFunDual_prod`
for the Banach space version.  -/
MeasureTheory.charFun_prod : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {mE : MeasurableSpace E} {mF : MeasurableSpace F}
  {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure F} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  (t : WithLp 2 (E × F)),
  MeasureTheory.charFun (MeasureTheory.Measure.map (WithLp.toLp 2) (μ.prod ν)) t =
    MeasureTheory.charFun μ t.ofLp.1 * MeasureTheory.charFun ν t.ofLp.2
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.eq_zero_of_smul_mem_span : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {i : ι},
  LinearIndepOn R v s → i ∈ s → ∀ (a : R), a • v i ∈ Submodule.span R (v '' (s \ {i})) → a = 0
-- Mathlib.NumberTheory.Padics.AddChar
PadicInt.eq_addChar_of_value_at_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [inst_3 : IsBoundedSMul ℤ_[p] R] [inst_4 : IsUltrametricDist R] [inst_5 : CompleteSpace R] {r : R}
  (hr : Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0)) {κ : AddChar ℤ_[p] R},
  Continuous ⇑κ → κ 1 = 1 + r → κ = PadicInt.addChar_of_value_at_one r hr
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] (r : α → β → Prop) (s : Set α),
  SemicontinuousOn r s = ∀ x ∈ s, SemicontinuousWithinAt r s x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.get? t.min! = some t.min!
-- Plausible.Testable
/-- Succeed when we find another example satisfying `p`.
In `success h`, `h` is an optional proof of the proposition.
Without the proof, all we know is that we found one example
where `p` holds. With a proof, the one test was sufficient to
prove that `p` holds and we do not need to keep finding examples.
 -/
Plausible.TestResult.success : {p : Prop} → Unit ⊕' p → Plausible.TestResult p
-- Init.Data.Fin.Basic
/-- Subtraction of a natural number from a `Fin`, with the bound narrowed.

This is a generalization of `Fin.pred`. It is guaranteed to not underflow or wrap around.

Examples:
* `(5 : Fin 9).subNat 2 (by decide) = (3 : Fin 7)`
* `(5 : Fin 9).subNat 0 (by decide) = (5 : Fin 9)`
* `(3 : Fin 9).subNat 3 (by decide) = (0 : Fin 6)`
 -/
Fin.subNat : {n : ℕ} → (m : ℕ) → (i : Fin (n + m)) → m ≤ ↑i → Fin n
-- Qq.Match
Qq.Impl.mkIsDefEq : (decls : List Qq.Impl.PatVarDecl) →
  Q(Lean.Expr) →
    Q(Lean.Expr) →
      Lean.MetaM
        (have a := Qq.Impl.mkIsDefEqType decls;
        Q(Lean.MetaM «$a»))