mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The `I`-adic Cauchy condition can be checked on successive `n`.  -/
AdicCompletion.isAdicCauchy_iff : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : ℕ → M), AdicCompletion.IsAdicCauchy I M f ↔ ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
-- Mathlib.Order.Filter.Pointwise
Filter.map_neg : ∀ {α : Type u_2} [inst : Neg α] {f : Filter α}, Filter.map Neg.neg f = -f
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.match_1.eq_3 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option (Computation α))) → Sort u_2) (c : Computation α)
  (S' : Stream'.Seq (Option (Computation α))) (h_1 : Unit → motive none)
  (h_2 : (S' : Stream'.Seq (Option (Computation α))) → motive (some (none, S')))
  (h_3 : (c : Computation α) → (S' : Stream'.Seq (Option (Computation α))) → motive (some (some c, S'))),
  (match some (some c, S') with
    | none => h_1 ()
    | some (none, S') => h_2 S'
    | some (some c, S') => h_3 c S') =
    h_3 c S'
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.centralizer_eq_top_iff_subset : ∀ {R : Type u_1} [inst : Semiring R] {s : Set R}, Subsemiring.centralizer s = ⊤ ↔ s ⊆ ↑(Subsemiring.center R)
-- Init.Data.Range.Polymorphic.Basic
/-- If the smallest value in the range satisfies the upper bound and has a successor, the size is
  one larger than the size of the range starting at the successor.  -/
Std.Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some : ∀ {α : Type u} {inst : LE α} {inst_1 : Std.PRange.UpwardEnumerable α} {inst_2 : Std.Rxc.HasSize α}
  [self : Std.Rxc.LawfulHasSize α] (lo hi lo' : α),
  lo ≤ hi → Std.PRange.succ? lo = some lo' → Std.Rxc.HasSize.size lo hi = Std.Rxc.HasSize.size lo' hi + 1
-- Init.PropLemmas
right_eq_ite_iff : ∀ {α : Sort u_1} {p : Prop} [inst : Decidable p] {x y : α}, (y = if p then x else y) ↔ p → y = x
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.uniqueLinearEquiv_symm_apply : ∀ (R : Type u_1) {α : Type u_3} (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M]
  [inst_3 : Subsingleton α] (a : α) (a_1 : M), (Finsupp.uniqueLinearEquiv R M a).symm a_1 = fun₀ | a => a_1
-- Mathlib.RingTheory.DedekindDomain.Basic
/-- An integral domain is a Dedekind domain iff and only if it is
Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field.
In particular, this definition does not depend on the choice of this fraction field.  -/
isDedekindDomain_iff : ∀ (A : Type u_2) [inst : CommRing A] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra A K] [IsFractionRing A K],
  IsDedekindDomain A ↔
    IsDomain A ∧ IsNoetherianRing A ∧ Ring.DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ y, (algebraMap A K) y = x
-- Std.Do.SPred.SPred
Std.Do.SPred.forall_nil : ∀ {α : Sort u_1} {P : α → Std.Do.SPred []}, Std.Do.SPred.forall P = { down := ∀ (a : α), (P a).down }
-- Mathlib.GroupTheory.Index
AddSubgroup.index_pi : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_3} [inst_1 : Fintype ι] (H : ι → AddSubgroup G),
  (AddSubgroup.pi Set.univ H).index = ∏ i, (H i).index
-- Mathlib.Analysis.MeanInequalities
Real.summable_Lp_add_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p : ℝ},
  1 ≤ p →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) → (Summable fun i => g i ^ p) → Summable fun i => (f i + g i) ^ p
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_eq_prod_sdiff_singleton_mul : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∈ s → ∀ (f : ι → M), ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.coreLeftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  F.leftUnitor.core =
    (CategoryTheory.Functor.id C).coreComp F ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.coreId C) F.core ≪≫ F.core.leftUnitor
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_zero' : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {r : ℝ} (x : E),
  0 < r → Seminorm.closedBall 0 x r = Set.univ
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.coeff_hermite_succ_zero : ∀ (n : ℕ), (Polynomial.hermite (n + 1)).coeff 0 = -(Polynomial.hermite n).coeff 1
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A copy induces an embedding of neighbor sets.  -/
SimpleGraph.Copy.mapNeighborSet : {α : Type u_4} →
  {β : Type u_5} →
    {A : SimpleGraph α} → {B : SimpleGraph β} → (f : A.Copy B) → (a : α) → ↑(A.neighborSet a) ↪ ↑(B.neighborSet (f a))
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instOne : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → One (WithVal v)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_vadd_left_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P} {v : V}, v ∈ s.direction → (s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y)
-- Init.ByCases
if_true : ∀ {α : Sort u_1} {x : Decidable True} (t e : α), (if True then t else e) = t
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_allOnes : ∀ {n w acc : ℕ}, n ≤ w → (BitVec.allOnes w).cpopNatRec n acc = acc + n
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.length_iter_eq_size : ∀ {γ : Type u} {α β : Type v} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  {s : Std.Slice γ} [Std.Iterators.Finite α Id] [inst_3 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id]
  [inst_5 : Std.Slice.SliceSize γ] [Std.Slice.LawfulSliceSize γ], s.iter.length = s.size
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mk'.congr_simp : ∀ {R : Type u} [inst : NonAssocSemiring R] (s s_1 : Set R) (e_s : s = s_1) (sm sm_1 : Submonoid R) (e_sm : sm = sm_1)
  (hm : ↑sm = s) (sa sa_1 : AddSubmonoid R) (e_sa : sa = sa_1) (ha : ↑sa = s),
  Subsemiring.mk' s sm hm sa ha = Subsemiring.mk' s_1 sm_1 ⋯ sa_1 ⋯
-- Mathlib.Data.Seq.Computation
Computation.LiftRel.swap : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β),
  Computation.LiftRel (Function.swap R) cb ca ↔ Computation.LiftRel R ca cb
-- Mathlib.Algebra.Group.Conj
IsAddConj.setoid.eq_1 : ∀ (α : Type u_1) [inst : AddMonoid α], IsAddConj.setoid α = { r := IsAddConj, iseqv := ⋯ }
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_invalid_of_isInvalidContinuationByte_eq_false : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte b = false →
    ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.invalid
-- Lean.Environment
Lean.EnvExtension.instInhabitedAsyncMode : Inhabited Lean.EnvExtension.AsyncMode
-- Mathlib.Analysis.Normed.Field.Lemmas
Filter.tendsto_inv₀_cobounded : ∀ {α : Type u_1} [inst : NormedDivisionRing α], Filter.Tendsto Inv.inv (Bornology.cobounded α) (nhds 0)
-- Aesop.Search.Queue
Aesop.LIFOQueue.mk.sizeOf_spec : ∀ (goals : Array Aesop.GoalRef), sizeOf { goals := goals } = 1 + sizeOf goals
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
_private.Mathlib.RingTheory.DedekindDomain.AdicValuation.0.IsDedekindDomain.HeightOneSpectrum.valuation.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain.HeightOneSpectrum.valuation K v = v.intValuation.extendToLocalization ⋯ K
-- Mathlib.Data.ZMod.Units
/-- For each `n ≥ 0`, the unit group of `ZMod n` is finite.  -/
ZMod.instFiniteZModUnits : ∀ (n : ℕ), Finite (ZMod n)ˣ
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.coeffList.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (P : Polynomial R),
  P.coeffList = List.map P.coeff (List.range P.degree.succ).reverse
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- When `M` is a module over a ring `S`, and `S` is an algebra over `R`, then `M` inherits a
module structure over `R`. Not an instance because `S` cannot be inferred.

The preferred way of setting this up is `[Module R M] [Module S M] [IsScalarTower R S M]`.
 -/
Module.restrictScalars : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid M] → [inst_2 : CommSemiring R] → [Algebra R S] → [Module S M] → Module R M
-- Mathlib.Data.Finset.Max
Finset.map_toDual_max : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α),
  WithBot.map (⇑OrderDual.toDual) s.max = (Finset.image (⇑OrderDual.toDual) s).min
-- Mathlib.Util.AtomM
/-- If an atomic expression has already been encountered, get the index and the stored form of the
atom (which will be defeq at the specified transparency, but not necessarily syntactically equal).
If the atomic expression has *not* already been encountered, store it in the list of atoms, and
return the new index (and the stored form of the atom, which will be itself).

In a normalizing tactic, the expression returned by `addAtom` should be considered the normal form.
 -/
Mathlib.Tactic.AtomM.addAtom : Lean.Expr → Mathlib.Tactic.AtomM (ℕ × Lean.Expr)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.inv_epsilon : Hyperreal.epsilon⁻¹ = Hyperreal.omega
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullback₂_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f],
  (CategoryTheory.PreZeroHypercover.pullback₂ f E).I₀ = E.I₀
-- Mathlib.Topology.UniformSpace.Matrix
Matrix.uniformContinuous : ∀ (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [inst : UniformSpace 𝕜] {β : Type u_4} [inst_1 : UniformSpace β]
  {f : β → Matrix m n 𝕜}, UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous fun x => f x i j
-- Batteries.Data.Vector.Basic
/-- Fold a function `f` over the list from the left, returning the vector of partial results.
 -/
Vector.scanl : {β : Type u_1} → {α : Type u_2} → {n : ℕ} → (β → α → β) → β → Vector α n → Vector β (n + 1)
-- Mathlib.Combinatorics.Hindman
/-- The strong form of **Hindman's theorem**: in any finite cover of an FP-set, one the parts
contains an FP-set.  -/
Hindman.FP_partition_regular : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (s : Set (Set M)),
  s.Finite → Hindman.FP a ⊆ ⋃₀ s → ∃ c ∈ s, ∃ b, Hindman.FP b ⊆ c
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_le_comm : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel (Lean.Order.join P Q) (Lean.Order.join Q P)
-- Batteries.Data.List.Lemmas
List.sum_flatten : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0]
  [Std.Associative fun x1 x2 => x1 + x2] {l : List (List α)}, l.flatten.sum = (List.map List.sum l).sum
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.le_one : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ},
  ProbabilityTheory.IsMeasurableRatCDF f → ∀ (a : α) (q : ℚ), f a q ≤ 1
-- Mathlib.GroupTheory.OrderOfElement
mod_natCard_zsmul : ∀ {G : Type u_6} [inst : AddGroup G] (a : G) (n : ℤ), (n % ↑(Nat.card G)) • a = n • a
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.submonoidMap_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {f : M →* N},
  Function.Injective ⇑f → ∀ (M' : Submonoid M), Function.Injective ⇑(f.submonoidMap M')
-- Mathlib.Data.Matrix.Basic
Matrix.decidableEq : {m : Type u_2} →
  {n : Type u_3} → {α : Type u_11} → [DecidableEq α] → [Fintype m] → [Fintype n] → DecidableEq (Matrix m n α)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.simp : ℤ →
  Lean.Meta.Grind.Arith.CommRing.EqCnstr →
    ℤ → Lean.Grind.CommRing.Mon → Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_pos_of_addOrderOf_pos : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M},
  0 < addOrderOf m → ∀ (a : α), 0 < AddAction.period m a
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- `shrinkCoyoneda.obj X` is corepresented by `X`.  -/
CategoryTheory.shrinkCoyonedaCorepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      (X : Cᵒᵖ) → (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).CorepresentableBy (Opposite.unop X)
-- Std.Time.Format
Std.Time.PlainDate.instToString : ToString Std.Time.PlainDate
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_push : ∀ {m n : ℤ}, m < n → (m<...=n).toArray = (m<...=n - 1).toArray.push n
-- Mathlib.FieldTheory.IntermediateField.Basic
AlgHom.equivFieldRange_apply_coe : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L') (a : L), ↑(f.equivFieldRange a) = f a
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toList.induct_unfolding : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)]
  (motive : {i j : ι} → Monoid.CoprodI.NeWord M i j → List ((i : ι) × M i) → Prop),
  (∀ (i : ι) (x : M i) (a : x ≠ 1), motive (Monoid.CoprodI.NeWord.singleton x a) [⟨i, x⟩]) →
    (∀ (x x_1 j k : ι) (w₁ : Monoid.CoprodI.NeWord M x j) (_hne : j ≠ k) (w₂ : Monoid.CoprodI.NeWord M k x_1),
        motive w₁ w₁.toList → motive w₂ w₂.toList → motive (w₁.append _hne w₂) (w₁.toList ++ w₂.toList)) →
      ∀ {i j : ι} (_w : Monoid.CoprodI.NeWord M i j), motive _w _w.toList
-- Mathlib.Topology.Bornology.Basic
Bornology.ext_iff' : ∀ {α : Type u_2} {t t' : Bornology α}, t = t' ↔ ∀ (s : Set α), s ∈ Bornology.cobounded α ↔ s ∈ Bornology.cobounded α
-- Mathlib.Data.Nat.Count
Nat.count_true : ∀ (n : ℕ), Nat.count (fun x => True) n = n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {combined : ℕ} [inst_2 : SizeOf α]
  {w : ℕ} (n : ℕ) (inner : aig.RefVec w) (h : combined = w * n),
  sizeOf { w := w, n := n, inner := inner, h := h } = 1 + sizeOf w + sizeOf n + sizeOf inner + sizeOf h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} [inst_2 : SizeOf α] {len : ℕ}
  (x : aig.RefVec (len * w)) (h : 0 < len), sizeOf { len := len, x := x, h := h } = 1 + sizeOf len + sizeOf x + sizeOf h
-- Mathlib.Order.Filter.NAry
/-- The image of a binary function `m : α → β → γ` as a function `Filter α → Filter β → Filter γ`.
Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.  -/
Filter.map₂ : {α : Type u_1} → {β : Type u_3} → {γ : Type u_5} → (α → β → γ) → Filter α → Filter β → Filter γ
-- Lean.Parser.Command
Lean.Parser.Command.openRenaming : Lean.Parser.Parser
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.isMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α], Order.IsPredLimit (Order.pred a) → IsMin a
-- Mathlib.Analysis.Normed.Group.Real
Real.norm_two : ‖2‖ = 2
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The empty pre-`0`-hypercover.  -/
CategoryTheory.PreZeroHypercover.empty : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (S : C) → CategoryTheory.PreZeroHypercover S
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_21 : HSub Std.Time.Minute.Offset Std.Time.Hour.Offset Std.Time.Minute.Offset
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∈ m₂ → (m₁ \ m₂).get! k = default
-- Init.Data.Array.Sort.Lemmas
Array.mergeSort_perm : ∀ {α : Type u_1} {xs : Array α} {le : α → α → Bool}, (xs.mergeSort le).Perm xs
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.sieve₀_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D),
  (E.map F).sieve₀ = CategoryTheory.Sieve.functorPushforward F E.sieve₀
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negY_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R}, P 2 = 0 → W'.negY P = -P 1
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a functor `F` preserves the left homology of a short complex `S`, this is the
canonical isomorphism `(S.map F).homology ≅ F.obj S.homology`.  -/
CategoryTheory.ShortComplex.mapHomologyIso : {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] →
            (S : CategoryTheory.ShortComplex C) →
              (F : CategoryTheory.Functor C D) →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : S.HasHomology] →
                    [inst_6 : (S.map F).HasHomology] →
                      [F.PreservesLeftHomologyOf S] → (S.map F).homology ≅ F.obj S.homology
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiable_finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  (Differentiable 𝕜 fun x => Fin.cons (φ x) (φs x)) ↔ Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instLeftCancelSemigroup : {α : Type u_1} → [LeftCancelSemigroup α] → LeftCancelSemigroup (Lex α)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
            Z).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
        Z)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqErrorCode.beq : Lean.JsonRpc.ErrorCode → Lean.JsonRpc.ErrorCode → Bool
-- Mathlib.Algebra.Algebra.Basic
/-- An alternate statement of `LinearMap.map_smul` for when `algebraMap` is more convenient to
work with than `•`.  -/
LinearMap.map_algebraMap_mul : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₗ[R] B) (a : A) (r : R),
  f ((algebraMap R A) r * a) = (algebraMap R B) r * f a
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExtractCoeff.mk.inj : ∀ {e k e' : Q(ℕ)} {ve' : Mathlib.Tactic.Ring.Common.ExProdNat e'} {p : Q(«$e» = «$e'» * «$k»)} {k_1 e'_1 : Q(ℕ)}
  {ve'_1 : Mathlib.Tactic.Ring.Common.ExProdNat e'_1} {p_1 : Q(«$e» = «$e'_1» * «$k_1»)},
  { k := k, e' := e', ve' := ve', p := p } = { k := k_1, e' := e'_1, ve' := ve'_1, p := p_1 } →
    k = k_1 ∧ e' = e'_1 ∧ ve' ≍ ve'_1 ∧ p = p_1
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.of_comul : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : Ring X] [inst_2 : Bialgebra R X],
  CoalgebraStruct.comul = CoalgebraStruct.comul
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_some_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α}, m.getKey? k = some k' ↔ ∃ (h : k ∈ m), m.getKey k h = k'
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.exists_eq_singleton_append_of_ne_startPos : ∀ {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.startPos),
  (p.prev hp).Splits t₁ t₂ → ∃ t₂', t₂ = String.singleton ((p.prev hp).get ⋯) ++ t₂'
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.subtypePerm_apply_pow_of_mem : ∀ {α : Type u_2} {g : Equiv.Perm α} {s : Finset α} (hs : ∀ (x : α), g x ∈ s ↔ x ∈ s) {n : ℕ} {x : α} (hx : x ∈ s),
  ↑((g.subtypePerm hs ^ n) ⟨x, hx⟩) = (g ^ n) x
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (lrk : α)
  (lrv : β lrk) (l r : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (lrk : α) →
        (lrv : β lrk) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_4 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)),
  (match Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.inner size lrk lrv l r with
    | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.inner size lrk lrv l r => h_2 size lrk lrv l r
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_3 size k v l r
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
      h_4 size k v l r lrs lrk lrv lrl lrr) =
    h_2 size lrk lrv l r
-- Lean.Parser.Types
Lean.Parser.instInhabitedFirstTokens : Inhabited Lean.Parser.FirstTokens
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_commute : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun Commute f)) (y : β),
  (∀ x ∈ s, Commute y (f x)) → Commute y (s.noncommProd f comm)
-- Mathlib.Topology.Defs.Filter
/-- A point `x` is an accumulation point of a filter `F` if `𝓝[≠] x ⊓ F ≠ ⊥`.
See also `ClusterPt`.  -/
AccPt : {X : Type u_1} → [TopologicalSpace X] → X → Filter X → Prop
-- Mathlib.LinearAlgebra.Ray
/-- A positive multiple of a vector is in the same ray as one it is in the same ray as.  -/
SameRay.pos_smul_left : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y : M} {S : Type u_5} [inst_5 : CommSemiring S]
  [inst_6 : PartialOrder S] [inst_7 : Algebra S R] [inst_8 : Module S M] [SMulPosMono S R] [IsScalarTower S R M]
  {a : S}, SameRay R x y → 0 < a → SameRay R (a • x) y