mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.natTransOpCyclesToCycles_app : ∀ (C : Type u_1) {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) (i j : ι)
  [inst_2 : CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c),
  (HomologicalComplex.natTransOpCyclesToCycles C c i j).app K = K.opcyclesToCycles i j
-- Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
_private.Mathlib.NumberTheory.NumberField.Ideal.Asymptotics.0.NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop_aux₁ : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {C : ClassGroup (NumberField.RingOfIntegers K)}
  {J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} {s : ℝ},
  ClassGroup.mk0 J = C⁻¹ →
    Nat.card { I // ↑(Ideal.absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C } =
      Nat.card { I // ↑J ∣ ↑I ∧ Submodule.IsPrincipal ↑I ∧ ↑(Ideal.absNorm ↑I) ≤ s * ↑(Ideal.absNorm ↑J) }
-- Mathlib.GroupTheory.FreeGroup.Orbit
FreeGroup.startsWith.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (w w_1 : α × Bool),
  w = w_1 → ∀ (a a_1 : FreeGroup α), a = a_1 → FreeGroup.startsWith w a = FreeGroup.startsWith w_1 a_1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RiiSlice : Type u_1 → Type u_1
-- Mathlib.Topology.Compactness.Compact
Topology.IsClosedEmbedding.noncompactSpace : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NoncompactSpace X] {f : X → Y},
  Topology.IsClosedEmbedding f → NoncompactSpace Y
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instHasOfPostcompPropertySchemeIsSeparated : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.IsFinite @AlgebraicGeometry.IsSeparated
-- Mathlib.Order.WellQuasiOrder
WellQuasiOrderedLE.to_wellFoundedLT : ∀ {α : Type u_1} [inst : Preorder α] [WellQuasiOrderedLE α], WellFoundedLT α
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.untop_one : ∀ {α : Type u} [inst : One α], WithTop.untop 1 ⋯ = 1
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {p : M × M'} {f : M → N} {g : M' → N'}
  {df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)},
  HasMFDerivAt% f p.1 df →
    ∀ {dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)},
      HasMFDerivAt% g p.2 dg → HasMFDerivAt% (Prod.map f g) p ((mfderiv% f p.1).prodMap (mfderiv% g p.2))
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedMethods : Inhabited Lean.Meta.Simp.Methods
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_lt_enorm : ∀ (α : Type u_2) [inst : NontriviallyNormedField α] {r : ENNReal}, r ≠ ⊤ → ∃ x, r < ‖x‖ₑ
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
borel_eq_generateFrom_Ico : ∀ (α : Type u_5) [inst : TopologicalSpace α] [SecondCountableTopology α] [inst_2 : LinearOrder α] [OrderTopology α],
  borel α = MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Set.Ico l u = S}
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balRight.fun_cases_unfolding : ∀ {α : Type u_1} (v : α) (motive : RBTree.RBNode α → RBTree.RBNode α → RBTree.RBNode α → Prop),
  (∀ (l a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
      motive l (RBTree.RBNode.node RBTree.RBColor.red a x b)
        (RBTree.RBNode.node RBTree.RBColor.red l v (RBTree.RBNode.node RBTree.RBColor.black a x b))) →
    (∀ (l : RBTree.RBNode α),
        (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
            l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
          ∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
            motive (RBTree.RBNode.node RBTree.RBColor.black a x b) l
              ((RBTree.RBNode.node RBTree.RBColor.red a x b).balance1 v l)) →
      (∀ (l : RBTree.RBNode α),
          (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
              l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
            ∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
              motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c)) l
                (RBTree.RBNode.node RBTree.RBColor.red (a.setRed.balance1 x b) y
                  (RBTree.RBNode.node RBTree.RBColor.black c v l))) →
        (∀ (l : RBTree.RBNode α),
            (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
              ∀ (l_1 : RBTree.RBNode α),
                (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                    l_1 = RBTree.RBNode.node RBTree.RBColor.black a x b → False) →
                  (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
                      l_1 = RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) →
                        False) →
                    motive l_1 l (RBTree.RBNode.node RBTree.RBColor.red l_1 v l)) →
          ∀ (l r : RBTree.RBNode α), motive l r (l.balRight v r)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Icc_add_Icc : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [AddLeftReflectLE α]
  [ExistsAddOfLE α] {a b c d : α}, a ≤ b → c ≤ d → Set.Icc a b + Set.Icc c d = Set.Icc (a + c) (b + d)
-- Batteries.Data.String.Lemmas
String.Pos.Raw.utf8GetAux?.eq_2 : ∀ (x x_1 : String.Pos.Raw) (c : Char) (cs : List Char),
  String.Pos.Raw.utf8GetAux? (c :: cs) x x_1 = if x = x_1 then some c else String.Pos.Raw.utf8GetAux? cs (x + c) x_1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.specTargetImageFactorization_comp_assoc : ∀ {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.Spec A) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.specTargetImageFactorization f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.specTargetImageRingHom f)) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.RingTheory.HopkinsLevitzki
IsSemiprimaryRing.isNoetherian_iff_isArtinian : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemiprimaryRing R],
  IsNoetherian R M ↔ IsArtinian R M
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- Asymptotically, the characteristic function for the poles of `f * g` is less than or equal to the
sum of the characteristic functions for the poles of `f` and `g`, respectively.
 -/
ValueDistribution.characteristic_mul_top_eventuallyLE : ∀ {f₁ f₂ : ℂ → ℂ},
  Meromorphic f₁ →
    (∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) →
      Meromorphic f₂ →
        (∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) →
          ValueDistribution.characteristic (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop]
            ValueDistribution.characteristic f₁ ⊤ + ValueDistribution.characteristic f₂ ⊤
-- Mathlib.RingTheory.Algebraic.Defs
/-- A subalgebra is algebraic if all its elements are algebraic.  -/
Subalgebra.IsAlgebraic : {R : Type u} → {A : Type v} → [inst : CommRing R] → [inst_1 : Ring A] → [inst_2 : Algebra R A] → Subalgebra R A → Prop
-- Init.Data.Nat.ToString
Nat.digitChar_eq_four : ∀ {n : ℕ}, n.digitChar = '4' ↔ n = 4
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.B_off_diag_nonpos : ∀ (n : ℕ) (i j : Fin n), i ≠ j → CartanMatrix.B n i j ≤ 0
-- Init.Data.Nat.Lemmas
Nat.mul_ne_mul_right : ∀ {a b c : ℕ}, a ≠ 0 → (a * b ≠ a * c ↔ b ≠ c)
-- Mathlib.Algebra.Lie.Prod
LieHom.inr_apply : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (x : L₂), (LieHom.inr R L₁ L₂) x = (0, x)
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.fg_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  ⊤.FG ↔ S.FG
-- Std.Internal.UV.System
/-- Information about the current user.
 -/
Std.Internal.UV.System.PasswdInfo : Type
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.subgroup_antitone : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  Antitone MulArchimedeanClass.subgroup
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.Cat.exp_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : CategoryTheory.Cat),
  (CategoryTheory.Cat.exp C).obj D = CategoryTheory.Cat.of (CategoryTheory.Functor C ↑D)
-- Mathlib.NumberTheory.Padics.RingHoms
/-- `nthHomSeq f_compat r` bundles `PadicInt.nthHom f r`
as a Cauchy sequence of rationals with respect to the `p`-adic norm.
The `n`th value of the sequence is `((f n r).val : ℚ)`.
 -/
PadicInt.nthHomSeq : {R : Type u_1} →
  [inst : NonAssocSemiring R] →
    {p : ℕ} →
      {f : (k : ℕ) → R →+* ZMod (p ^ k)} →
        [hp_prime : Fact (Nat.Prime p)] →
          (∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) → R → PadicSeq p
-- Batteries.Data.BitVec.Lemmas
BitVec.msb_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool), (BitVec.ofFnBE f).msb = if h : n ≠ 0 then f ⟨0, ⋯⟩ else false
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.drop.aux.eq_def : ∀ {α : Type u} (x : ℕ),
  Stream'.WSeq.drop.aux x =
    match (motive := ℕ → Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))) x with
    | 0 => Computation.pure
    | n.succ => fun a => Stream'.WSeq.tail.aux a >>= Stream'.WSeq.drop.aux n
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instMembershipOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → [EquivBEq α] → [LawfulHashable α] → Membership α (Std.ExtHashMap α β)
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.mk.inj : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {inst : CommRing R} {inst_1 : LieRing L}
  {inst_2 : AddCommGroup M} {inst_3 : AddCommGroup N} {inst_4 : Module R M} {inst_5 : Module R N}
  {inst_6 : LieRingModule L M} {inst_7 : LieRingModule L N} {toLinearMap : M →ₗ[R] N}
  {map_lie' : ∀ {x : L} {m : M}, toLinearMap.toFun ⁅x, m⁆ = ⁅x, toLinearMap.toFun m⁆} {toLinearMap_1 : M →ₗ[R] N}
  {map_lie'_1 : ∀ {x : L} {m : M}, toLinearMap_1.toFun ⁅x, m⁆ = ⁅x, toLinearMap_1.toFun m⁆},
  { toLinearMap := toLinearMap, map_lie' := map_lie' } = { toLinearMap := toLinearMap_1, map_lie' := map_lie'_1 } →
    toLinearMap = toLinearMap_1
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.succeeded.injEq : ∀ (newRapps newRapps_1 : Array Aesop.RappRef),
  (Aesop.SafeRulesResult.succeeded newRapps = Aesop.SafeRulesResult.succeeded newRapps_1) = (newRapps = newRapps_1)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.mk.injEq : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (toPartialHomeomorph : PartialHomeomorph X Y) (open_source : IsOpen toPartialHomeomorph.source)
  (open_target : IsOpen toPartialHomeomorph.target) (toPartialHomeomorph_1 : PartialHomeomorph X Y)
  (open_source_1 : IsOpen toPartialHomeomorph_1.source) (open_target_1 : IsOpen toPartialHomeomorph_1.target),
  ({ toPartialHomeomorph := toPartialHomeomorph, open_source := open_source, open_target := open_target } =
      { toPartialHomeomorph := toPartialHomeomorph_1, open_source := open_source_1, open_target := open_target_1 }) =
    (toPartialHomeomorph = toPartialHomeomorph_1)
-- Mathlib.Algebra.Category.Ring.Under.Basic
AlgEquiv.toUnder_hom_right_apply : ∀ {R : CommRingCat} {A B : Type u} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra (↑R) A]
  [inst_3 : Algebra (↑R) B] (f : A ≃ₐ[↑R] B) (a : A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f.toUnder.hom)) a = f a
-- Mathlib.Data.Set.Basic
Set.empty_subset : ∀ {α : Type u} (s : Set α), ∅ ⊆ s
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₂_D₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' i₁₂'' : I₁₂),
  CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'') =
    -CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'')
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.natCast_nonneg : ∀ (α : Type u) [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] (n : ℕ), 0 ≤ ↑n
-- Init.Data.SInt.Lemmas
Int16.toInt32_neg_of_ne : ∀ {x : Int16}, x ≠ -32768 → (-x).toInt32 = -x.toInt32
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_lt_sdiff_right : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x < y → z ≤ x → x \ z < y \ z
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- If the domain of a `IsUniformInducing` map `f` is a T₀ space, then `f` is injective,
hence it is a `IsUniformEmbedding`.  -/
IsUniformInducing.isUniformEmbedding : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [T0Space α] {f : α → β},
  IsUniformInducing f → IsUniformEmbedding f
-- Mathlib.Data.WSeq.Basic
/-- Get the tail of a weak sequence. This doesn't need a `Computation`
wrapper, unlike `head`, because `flatten` allows us to hide this
in the construction of the weak sequence itself.  -/
Stream'.WSeq.tail : {α : Type u} → Stream'.WSeq α → Stream'.WSeq α
-- Std.Tactic.BVDecide.Syntax
/-- Short-circuit multiplication as an abstraction-style optimization that triggers
if matching multiplications are not needed to proof a goal.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.shortCircuit : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Mathlib.Analysis.Seminorm
Seminorm.uniformity_eq_of_hasBasis : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {ι : Sort u_12} [inst_3 : UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p' : ι → Prop}
  {s : ι → Set E} (p : Seminorm 𝕜 E),
  (nhds 0).HasBasis p' s →
    (∃ r, p.closedBall 0 r ∈ nhds 0) →
      (∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i) →
        uniformity E = ⨅ r, ⨅ (_ : r > 0), Filter.principal {x | p (x.1 - x.2) < r}
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.mvPolynomialBasis_repr_apply : ∀ (R : Type u) [inst : CommRing R] (σ : Type u_1) (x : MvPolynomial σ R) (i : σ),
  ((KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) x)) i =
    (MvPolynomial.pderiv i) x
-- Mathlib.NumberTheory.ModularForms.Basic
SlashInvariantForm.constℝ.congr_simp : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (x x_1 : ℝ),
  x = x_1 → SlashInvariantForm.constℝ x = SlashInvariantForm.constℝ x_1
-- Mathlib.Analysis.Seminorm
Seminorm.ball_smul_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (r₁ : ℝ) {r₂ : ℝ}, r₂ ≠ 0 → Metric.ball 0 r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  (F : CategoryTheory.Functor C (Type w)) (X : C) (u : F.Elementsᵒᵖ),
  (CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj F X).ι.app u =
    TypeCat.ofHom fun t =>
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.shrinkYonedaObjObjEquiv t))) (Opposite.unop u).snd
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.State.mk.injEq : ∀ (numSteps : ℕ) (persistentCache transientCache : Lean.Meta.Sym.Simp.Cache)
  (funext : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr) (numSteps_1 : ℕ)
  (persistentCache_1 transientCache_1 : Lean.Meta.Sym.Simp.Cache)
  (funext_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr),
  ({ numSteps := numSteps, persistentCache := persistentCache, transientCache := transientCache, funext := funext } =
      { numSteps := numSteps_1, persistentCache := persistentCache_1, transientCache := transientCache_1,
        funext := funext_1 }) =
    (numSteps = numSteps_1 ∧
      persistentCache = persistentCache_1 ∧ transientCache = transientCache_1 ∧ funext = funext_1)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.copy_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {K' H' : C} (eK : K' ≅ h.K) (eH : H' ≅ h.H),
  (h.copy eK eH).i = CategoryTheory.CategoryStruct.comp eK.hom h.i
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- The neighbourhood filter of a nonzero element consists of all sets containing that
element.  -/
WithZeroTopology.nhds_of_ne_zero : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀}, γ ≠ 0 → nhds γ = pure γ
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.ext_iff : ∀ {R : Type u_1} [inst : NonAssocRing R] {p q : MulRingNorm R}, p = q ↔ ∀ (x : R), p x = q x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.toTree.processLeaf : Lean.Syntax → Lean.Elab.TermElabM FBinopElab.Tree✝
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.pair_subset : ∀ {α : Type u} {s : Set α}, s.Nontrivial → ∃ x y, x ≠ y ∧ {x, y} ⊆ s
-- Mathlib.Data.Finset.Sum
/-- Finsets on sum types are equivalent to pairs of finsets on each summand.  -/
Finset.sumEquiv : {α : Type u_4} → {β : Type u_5} → Finset (α ⊕ β) ≃o Finset α × Finset β
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.card_compl_support_modEq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {p n : ℕ} [hp : Fact (Nat.Prime p)] {σ : Equiv.Perm α},
  σ ^ p ^ n = 1 → σ.supportᶜ.card ≡ Fintype.card α [MOD p]
-- Aesop.Forward.Match.Types
Aesop.Match.mk.inj : ∀ {subst : Aesop.Substitution} {patInstSubsts : Array Aesop.Substitution} {level : Aesop.SlotIndex}
  {forwardDeps conclusionDeps : Array Aesop.PremiseIndex} {subst_1 : Aesop.Substitution}
  {patInstSubsts_1 : Array Aesop.Substitution} {level_1 : Aesop.SlotIndex}
  {forwardDeps_1 conclusionDeps_1 : Array Aesop.PremiseIndex},
  { subst := subst, patInstSubsts := patInstSubsts, level := level, forwardDeps := forwardDeps,
        conclusionDeps := conclusionDeps } =
      { subst := subst_1, patInstSubsts := patInstSubsts_1, level := level_1, forwardDeps := forwardDeps_1,
        conclusionDeps := conclusionDeps_1 } →
    subst = subst_1 ∧
      patInstSubsts = patInstSubsts_1 ∧
        level = level_1 ∧ forwardDeps = forwardDeps_1 ∧ conclusionDeps = conclusionDeps_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.maxKey? = some km →
    (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey?.get ⋯ = kmi → (compare km kmi).isLE = true
-- Std.Data.DTreeMap.Internal.Zipper
Std.ToIterator.iter.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator γ Id α β] (x : γ),
  Std.ToIterator.iter x = (Std.ToIterator.iterM x).toIter
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.functor_map_app : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)} (φ : X ⟶ Y) (j : J),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).map φ).app j =
    ((CategoryTheory.evaluation J C).obj j).mapShortComplex.map φ
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.evalSimpAll : Lean.Elab.Tactic.Tactic
-- Init.Data.SInt.Basic
/-- Strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `<` operator.
 -/
Int32.lt : Int32 → Int32 → Prop
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.image_Ico_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictMonoOn f (Set.Icc a b) → f '' Set.Ico a b ⊆ Set.Ico (f a) (f b)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.instKanComplexObjIhomTerminal : ∀ (A : SSet), (A ⟹ ⊤_ SSet).KanComplex
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A sequentially complete uniform space with a countable basis of the uniformity filter is
complete.  -/
UniformSpace.complete_of_cauchySeq_tendsto : ∀ {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated],
  (∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α
-- Mathlib.Algebra.Polynomial.Reverse
/-- If `i ≤ N`, then `revAtFun N i` returns `N - i`, otherwise it returns `i`.
This is the map used by the embedding `revAt`.
 -/
Polynomial.revAtFun : ℕ → ℕ → ℕ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors is zero or `π` if and only if those two vectors are
not linearly independent.  -/
Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = 0 ∨ o.oangle x y = ↑Real.pi ↔ ¬LinearIndependent ℝ ![x, y]
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.isReal_iff : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K},
  w.IsReal ↔ NumberField.ComplexEmbedding.IsReal w.embedding
-- Init.Grind.Attr
/-- `symbol <prio>` sets the priority of a constant for `grind`’s pattern-selection
procedure. `grind` prefers patterns that contain higher-priority symbols.
Example:
```
opaque p : Nat → Nat → Prop
opaque q : Nat → Nat → Prop
opaque r : Nat → Nat → Prop

attribute [grind symbol low] p
attribute [grind symbol high] q

axiom bar {x y} : p x y → q x x → r x y → r y x
attribute [grind →] bar
```
Here `p` is low priority, `q` is high priority, and `r` is default. `grind` first
tries to find a multi-pattern covering `x` and `y` using only high-priority
symbols while scanning hypotheses left to right. This fails because `q x x` does
not cover `y`. It then allows both high and default symbols and succeeds with
the multi-pattern `q x x, r x y`. The term `p x y` is ignored due to `p`’s low
priority. Symbols with priority `0` are never used in patterns.
 -/
Lean.Parser.Attr.grindSym : Lean.ParserDescr