mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- The product of two charted spaces is naturally a charted space, with the canonical
construction of the atlas of product maps.  -/
prodChartedSpace : (H : Type u_5) →
  [inst : TopologicalSpace H] →
    (M : Type u_6) →
      [inst_1 : TopologicalSpace M] →
        [ChartedSpace H M] →
          (H' : Type u_7) →
            [inst_3 : TopologicalSpace H'] →
              (M' : Type u_8) →
                [inst_4 : TopologicalSpace M'] → [ChartedSpace H' M'] → ChartedSpace (ModelProd H H') (M × M')
-- Mathlib.Order.WithBot
WithTop.untopA_mono : ∀ {α : Type u_1} [inst : LE α] {x y : WithTop α} [inst_1 : Nonempty α], x ≠ ⊤ → y ≤ x → y.untopA ≤ x.untopA
-- Mathlib.Algebra.Group.Prod
/-- Addition as an additive homomorphism.  -/
addAddHom : {α : Type u_6} → [inst : AddCommSemigroup α] → α × α →ₙ+ α
-- Mathlib.Topology.Algebra.ConstMulAction
continuousWithinAt_const_smul_iff₀ : ∀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀]
  [inst_2 : MulAction G₀ α] [ContinuousConstSMul G₀ α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} {c : G₀}
  {s : Set β}, c ≠ 0 → (ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b)
-- Init.Data.Array.MapIdx
Array.mapFinIdx_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β}
  {g : (i : ℕ) → β → i < (xs.mapFinIdx f).size → γ},
  (xs.mapFinIdx f).mapFinIdx g = xs.mapFinIdx fun i a h => g i (f i a h) ⋯
-- Mathlib.Tactic.CategoryTheory.CheckCompositions
/-- Find appearances of `CategoryStruct.comp C inst X Y Z f g`, and apply `f` to each.  -/
Mathlib.Tactic.CheckCompositions.forEachComposition : Lean.Expr → (Lean.Expr → Lean.MetaM Unit) → Lean.MetaM Unit
-- Mathlib.Analysis.Analytic.CPolynomial
HasFiniteFPowerSeriesAt.sub : ∀ {𝕜 : 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}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {x : E} {n m : ℕ},
  HasFiniteFPowerSeriesAt f pf x n →
    HasFiniteFPowerSeriesAt g pg x m → HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m)
-- Mathlib.Order.Partition.Finpartition
Finpartition.instInhabitedBot : (α : Type u_1) → [inst : Lattice α] → [inst_1 : OrderBot α] → Inhabited (Finpartition ⊥)
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the partial numerators `aᵢ` of the continued fraction are equal to one and the partial
denominators `bᵢ` correspond to integers.
 -/
GenContFract.of_partNum_eq_one_and_exists_int_partDen_eq : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K]
  {gp : GenContFract.Pair K}, (GenContFract.of v).s.get? n = some gp → gp.a = 1 ∧ ∃ z, gp.b = ↑z
-- Mathlib.RingTheory.Ideal.Height
Ideal.isMaximal_of_height_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [I.IsPrime] [FiniteRingKrullDim R],
  ↑I.height = ringKrullDim R → I.IsMaximal
-- Mathlib.Algebra.Ring.Hom.Defs
/-- The proposition that the function preserves addition  -/
RingHom.map_add' : ∀ {α : Type u_5} {β : Type u_6} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (self : α →+* β) (x y : α),
  (↑↑self).toFun (x + y) = (↑↑self).toFun x + (↑↑self).toFun y
-- Mathlib.Analysis.Normed.Group.Defs
ENormedAddCommMonoid.enorm_eq_zero : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ENormedAddCommMonoid E] (x : E), ‖x‖ₑ = 0 ↔ x = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.continuous_cos : Continuous Complex.cos
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- If the gcf already terminated at position `n`, nothing gets squashed.  -/
GenContFract.squashGCF_eq_self_of_terminated : ∀ {K : Type u_1} {n : ℕ} {g : GenContFract K} [inst : DivisionRing K], g.TerminatedAt n → g.squashGCF n = g
-- Mathlib.Algebra.Group.Commute.Units
isUnit_pow_succ_iff : ∀ {M : Type u_1} [inst : Monoid M] {n : ℕ} {a : M}, IsUnit (a ^ (n + 1)) ↔ IsUnit a
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_out : ∀ (c : Cardinal.{u_1}), Cardinal.mk (Quotient.out c) = c
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.coeff_eq_zero_of_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ},
  m.toSyn (m.degree f) < m.toSyn d → MvPolynomial.coeff d f = 0
-- Init.Data.SInt.Lemmas
Int16.toFin_toBitVec : ∀ (x : Int16), x.toBitVec.toFin = x.toUInt16.toFin
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stepAux.eq_7 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (x : σ)
  (x_1 : (k : K) → List (Γ k)), Turing.TM2.stepAux Turing.TM2.Stmt.halt x x_1 = { l := none, var := x, stk := x_1 }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.neg.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.neg c) = 1 + sizeOf c
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A nonempty affine subspace is `⊤` if and only if its direction is `⊤`.  -/
AffineSubspace.direction_eq_top_iff_of_nonempty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s : AffineSubspace k P}, (↑s).Nonempty → (s.direction = ⊤ ↔ s = ⊤)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.map_ofLE : ∀ {V : Type u_1} {G G' : SimpleGraph V} {M : G.Subgraph},
  M.IsMatching → ∀ (hGG' : G ≤ G'), (SimpleGraph.Subgraph.map (SimpleGraph.Hom.ofLE hGG') M).IsMatching
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.hom_apply : ∀ {V : Type u} {G : SimpleGraph V} (x : G.Subgraph) (v : ↑x.verts), x.hom v = ↑v
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.foldlM_toList : ∀ {m : Type w → Type u_1} {γ α β : Type w} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.IterM Id β}
  {f : γ → β → m γ} {init : γ}, List.foldlM f init it.toList.run = Std.IterM.foldM f init it
-- Mathlib.Computability.MyhillNerode
Language.IsRegular.finite_range_leftQuotient : ∀ {α : Type u} {L : Language α}, L.IsRegular → (Set.range L.leftQuotient).Finite
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
BinaryTree.coe_treesOfNumNodesEq : ∀ (n : ℕ), ↑(BinaryTree.treesOfNumNodesEq n) = {x | x.numNodes = n}
-- Init.Data.BitVec.Lemmas
/-- Shifting right by `n < w` yields a bitvector whose value is less than `2 ^ (w - n)`.
 -/
BitVec.toNat_ushiftRight_lt : ∀ {w : ℕ} (x : BitVec w), ∀ n ≤ w, (x >>> n).toNat < 2 ^ (w - n)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.mem_trivialFibrations_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C] [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.trivialFibrations C f ↔ HomotopicalAlgebra.Fibration f ∧ HomotopicalAlgebra.WeakEquivalence f
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderType.formatter : optParam Bool false → Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalNormedCommRing.toNonUnitalNormedRing : {α : Type u_5} → [self : NonUnitalNormedCommRing α] → NonUnitalNormedRing α
-- Init.Data.Array.Lemmas
Array.append_eq_append_iff : ∀ {α : Type u_1} {ws xs ys zs : Array α},
  ws ++ xs = ys ++ zs ↔ (∃ as, ys = ws ++ as ∧ xs = as ++ zs) ∨ ∃ cs, ws = ys ++ cs ∧ zs = cs ++ xs
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasAdditiveReduction.additiveReduction : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasAdditiveReduction R W],
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.c₄ < 1
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_max : ∀ (o₁ o₂ : Ordinal.{u_1}), Ordinal.omega (max o₁ o₂) = max (Ordinal.omega o₁) (Ordinal.omega o₂)
-- Mathlib.Tactic.TypeStar
/-- Check if `namePrefix.appendIndexAfter n` is unused, else recurse with `n+1`.  -/
_private.Mathlib.Tactic.TypeStar.0.Lean.Elab.Term.mkFreshLevelName.go : List Lean.Name → Lean.Name → ℕ → Lean.Name
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density of the set of naturals which are `1 mod m` is `m⁻¹`, for any `m ≠ 1`.

Note that if `m = 1`, this set is empty.
 -/
schnirelmannDensity_setOfPred_mod_eq_one : ∀ {m : ℕ}, m ≠ 1 → schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.mem_closedEBall`. -/
EMetric.mem_closedBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ Metric.closedEBall x ε ↔ edist y x ≤ ε
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.le_one : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → StieltjesFunction ℝ},
  ProbabilityTheory.IsCondKernelCDF f κ ν → ∀ (p : α × β) (x : ℝ), ↑(f p) x ≤ 1
-- Mathlib.CategoryTheory.Iso
CategoryTheory.isIso_of_hom_comp_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : Y ⟶ X},
  CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X → CategoryTheory.IsIso f
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.EquicontinuousWithinAt.continuousWithinAt_of_mem : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {H : Set (X → α)} {S : Set X} {x₀ : X},
  H.EquicontinuousWithinAt S x₀ → ∀ {f : X → α}, f ∈ H → ContinuousWithinAt f S x₀
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_mk : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S}
  {σ' : S →+* R} [inst_4 : RingHomInvPair σ σ'] [inst_5 : RingHomInvPair σ' σ] {f : M →ₛₗ[σ] M₂} {invFun : M₂ → M}
  {left_inv : Function.LeftInverse invFun f.toFun} {right_inv : Function.RightInverse invFun f.toFun},
  ⇑{ toLinearMap := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv } = ⇑f
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pushforwardSections_unitHomEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {M : SheafOfModules R}
  (f : SheafOfModules.unit R ⟶ M),
  SheafOfModules.pushforwardSections φ (M.unitHomEquiv f) =
    ((SheafOfModules.pushforward φ).obj M).unitHomEquiv
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.unitToPushforwardObjUnit φ)
        ((SheafOfModules.pushforward φ).map f))
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.Nondegenerate.ofSeparatingLeft : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] [IsDomain R₂]
  [Module.Free R₂ M₂] [Module.Finite R₂ M₂] {B : LinearMap.BilinForm R₂ M₂},
  LinearMap.SeparatingLeft B → B.Nondegenerate
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.weightedOrder_prod : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_4} (w : σ → ℕ)
  (f : ι → MvPowerSeries σ R) (s : Finset ι),
  MvPowerSeries.weightedOrder w (∏ i ∈ s, f i) = ∑ i ∈ s, MvPowerSeries.weightedOrder w (f i)
-- Mathlib.Data.Multiset.AddSub
Multiset.not_nodup_pair : ∀ {α : Type u_1} (a : α), ¬(a ::ₘ a ::ₘ 0).Nodup
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.rightKanExtension_hom_ext_iff : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} [inst_3 : L.HasRightKanExtension F]
  {G : CategoryTheory.Functor D H} {γ₁ γ₂ : G ⟶ L.rightKanExtension F},
  γ₁ = γ₂ ↔
    CategoryTheory.CategoryStruct.comp (L.whiskerLeft γ₁) (L.rightKanExtensionCounit F) =
      CategoryTheory.CategoryStruct.comp (L.whiskerLeft γ₂) (L.rightKanExtensionCounit F)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.forall_iff_succAbove : ∀ {n : ℕ} {P : Fin (n + 1) → Prop} (p : Fin (n + 1)),
  (∀ (i : Fin (n + 1)), P i) ↔ P p ∧ ∀ (i : Fin n), P (p.succAbove i)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.isPlausibleIndirectOutput_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] {it : Std.Iter α} {out : α},
  it.IsPlausibleIndirectOutput out ↔
    ∃ n, (it.internalState.next.bind fun x => Std.PRange.succMany? n x) = some out ∧ out < it.internalState.upperBound
-- Lean.Meta.CongrTheorems
/-- Tests whether we should use `subsingletonInst` kind for instances which depend on `eq`.
(Otherwise `fixKindsForDependencies`will downgrade them to Fixed
 -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.shouldUseSubsingletonInst : Lean.Meta.FunInfo → Array Lean.Meta.CongrArgKind → ℕ → Bool
-- Mathlib.Analysis.SpecificLimits.Normed
Summable.tendsto_alternating_series_tsum : ∀ {E : Type u_5} [inst : Ring E] [inst_1 : UniformSpace E] [IsUniformAddGroup E] [CompleteSpace E] {f : ℕ → E},
  Summable f →
    Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds (∑' (i : ℕ), (-1) ^ i * f i))
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_unitIso_inv_app_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core C), (E.core.unitIso.inv.app X).iso.inv = E.unitIso.hom.app X.of
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.ofPrime_asIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {p : Ideal R} (hp : Prime p),
  (IsDedekindDomain.HeightOneSpectrum.ofPrime hp).asIdeal = p
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.const_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.SimplicialObject.Augmented.const.obj X).left = (CategoryTheory.SimplicialObject.const C).obj X
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.associator_def : ∀ {R : Type u} [inst : CommSemiring R] (M N K : SemimoduleCat R),
  CategoryTheory.MonoidalCategoryStruct.associator M N K = SemimoduleCat.MonoidalCategory.associator M N K
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural embedding `M →+ AddMonoid.Coprod M N`.  -/
AddMonoid.Coprod.inl : {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M →+ AddMonoid.Coprod M N
-- Init.Data.List.Zip
Prod.map.eq_1 : ∀ {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) (a' : α₁) (b' : β₁),
  Prod.map f g (a', b') = (f a', g b')
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castLE_Iio : ∀ {m n : ℕ} (i : Fin m) (h : m ≤ n), Fin.castLE h '' Set.Iio i = Set.Iio (Fin.castLE h i)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.is_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : C),
  P.Is X ↔ P X
-- Mathlib.Algebra.Group.WithOne.Map
/-- The image of a binary function `f : α → β → γ` as a function
`WithZero α → WithZero β → WithZero γ`.

Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.  -/
WithZero.map₂ : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → WithZero α → WithZero β → WithZero γ
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- Composing a sheaf with a functor preserving limits of the same size as the hom sets in `C` yields a
functor between sheaf categories.

Note: the size of the limit that `F` is required to preserve in
`hasSheafCompose_of_preservesMulticospan` is in general larger than this.
 -/
CategoryTheory.hasSheafCompose_of_preservesLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  {F : CategoryTheory.Functor A B} [CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} F],
  J.HasSheafCompose F
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- If `f : X ⟶ Y⟦m⟧`, `n + m = 0` and `ha' : m + a = a'`, this lemma relates the two
morphisms `F.shiftMap f a a' ha'` and `(F.shift a').map (f⟦n⟧')`. Indeed,
via canonical isomorphisms, they both identify to morphisms
`(F.shift a).obj X ⟶ (F.shift a').obj Y`.
 -/
CategoryTheory.Functor.shiftIso_hom_app_comp_shiftMap_of_add_eq_zero : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {G : Type u_5} [inst_2 : AddGroup G]
  [inst_3 : CategoryTheory.HasShift C G] [inst_4 : F.ShiftSequence G] {X Y : C} {m : G}
  (f : X ⟶ (CategoryTheory.shiftFunctor C m).obj Y) (n : G) (hnm : n + m = 0) (a a' : G) (ha' : m + a = a'),
  CategoryTheory.CategoryStruct.comp ((F.shiftIso n a' a ⋯).hom.app X) (F.shiftMap f a a' ha') =
    (F.shift a').map
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map f)
        ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app Y))
-- Init.Grind.Attr
/-- The `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
theorem, and then the hypotheses from left to right. We say this is the default modifier.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
 -/
Lean.Parser.Attr.grindDef : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.nondegenerate_toBilin_iff : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {M : Matrix ι ι R₂} (b : Module.Basis ι R₂ M₂),
  ((Matrix.toBilin b) M).Nondegenerate ↔ M.Nondegenerate
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.State.mk.inj : ∀ {symState : Lean.Meta.Sym.State} {grindState : Lean.Meta.Grind.State} {goals : List Lean.Meta.Grind.Goal}
  {cache : Lean.Elab.Tactic.Grind.Cache} {symState_1 : Lean.Meta.Sym.State} {grindState_1 : Lean.Meta.Grind.State}
  {goals_1 : List Lean.Meta.Grind.Goal} {cache_1 : Lean.Elab.Tactic.Grind.Cache},
  { symState := symState, grindState := grindState, goals := goals, cache := cache } =
      { symState := symState_1, grindState := grindState_1, goals := goals_1, cache := cache_1 } →
    symState = symState_1 ∧ grindState = grindState_1 ∧ goals = goals_1 ∧ cache = cache_1
-- Mathlib.Data.PNat.Xgcd
/-- `v = [sp + 1, tp + 1]`, check `vp`  -/
PNat.XgcdType.v : PNat.XgcdType → ℕ × ℕ
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
TopCat.Hom.hom.eq_1 : ∀ {X Y : TopCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Lean.Parser.Term.Basic
Lean.Parser.tacticParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.ExtDTreeMap.Const.toList : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → List (α × β)
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- A locally finite order is a `SuccOrder`.
This is not an instance, because its `succ` field conflicts with computable `SuccOrder` structures
on `ℕ` and `ℤ`.  -/
LinearLocallyFiniteOrder.succOrder : (ι : Type u_1) → [inst : LinearOrder ι] → [LocallyFiniteOrder ι] → SuccOrder ι
-- Mathlib.Topology.Order.Basic
/-- In a second countable topological space with the order topology, the topology is generated
by half-infinite open intervals with endpoints in a countable set.  -/
exists_countable_generateFrom_Ioi_Iio : ∀ (α : Type u) [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] [SecondCountableTopology α],
  ∃ c, c.Countable ∧ ts = TopologicalSpace.generateFrom {s | ∃ a ∈ c, s = Set.Ioi a ∨ s = Set.Iio a}
-- Mathlib.Algebra.Lie.Prod
LieHom.snd_comp_inr : ∀ (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₂], (LieHom.snd R L₁ L₂).comp (LieHom.inr R L₁ L₂) = LieHom.id
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_smod : ∀ {w i : ℕ} {x y : BitVec w},
  (x.smod y).getLsbD i =
    match x.msb, y.msb with
    | false, false => (x % y).getLsbD i
    | false, true => if x % -y = 0#w then false else (x % -y + y).getLsbD i
    | true, false => if -x % y = 0#w then false else (y - -x % y).getLsbD i
    | true, true => (-(-x % -y)).getLsbD i
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_inj : ∀ {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ Fin.last n} {hj : j ≠ Fin.last n}, i.castPred hi = j.castPred hj ↔ i = j
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The bijection `Arrow (WalkingMultispan J) ≃ WalkingMultispan J ⊕ J.R ⊕ J.R`.  -/
CategoryTheory.Limits.WalkingMultispan.arrowEquiv : (J : CategoryTheory.Limits.MultispanShape) →
  CategoryTheory.Arrow (CategoryTheory.Limits.WalkingMultispan J) ≃ CategoryTheory.Limits.WalkingMultispan J ⊕ J.L ⊕ J.L
-- Mathlib.Data.ZMod.Basic
/-- `-1 : ZMod n` lifts to `n - 1 : R`. This avoids the characteristic assumption in `cast_neg`.  -/
ZMod.cast_neg_one : ∀ {R : Type u_1} [inst : Ring R] (n : ℕ), (-1).cast = ↑n - 1
-- Mathlib.Topology.CantorBendixson
/-- The perfect kernel of a closed set is perfect.  -/
CantorBendixson.perfect_perfectKernel : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → Perfect (CantorBendixson.perfectKernel s)
-- Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
CategoryTheory.Preadditive.DoldKan.equivalence_counitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Preadditive.DoldKan.equivalence.counitIso = AlgebraicTopology.DoldKan.N₂Γ₂
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instPow : {α : Type u_1} → {β : Type u_2} → [Pow α β] → Pow (Lex α) β
-- Mathlib.Algebra.Order.SuccPred
strictAnti_of_lt_sub_one : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Sub α] [inst_3 : One α]
  [inst_4 : PredSubOrder α] [IsPredArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMin a → f a < f (a - 1)) → StrictAnti f