mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTransposeRingEquiv_apply : ∀ (m : Type u_2) (α : Type v) [inst : NonUnitalNonAssocSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  (a : Matrix m m α), (Matrix.conjTransposeRingEquiv m α) a = MulOpposite.op a.conjTranspose
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atTop_of_monotone : ∀ {ι : Type u_3} {α : Type u_4} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α},
  Monotone f → Filter.Tendsto f Filter.atTop Filter.atTop ∨ ∃ l, Filter.Tendsto f Filter.atTop (nhds l)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightId_inv_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightId L R).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Topology.Algebra.Monoid
continuousMul_sInf : ∀ {M : Type u_3} [inst : Mul M] {ts : Set (TopologicalSpace M)}, (∀ t ∈ ts, ContinuousMul M) → ContinuousMul M
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.ofWithBot_mono : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {boxes₁ : Finset (WithBot (BoxIntegral.Box ι))}
  {le_of_mem₁ : ∀ J ∈ boxes₁, J ≤ ↑I} {pairwise_disjoint₁ : (↑boxes₁).Pairwise Disjoint}
  {boxes₂ : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem₂ : ∀ J ∈ boxes₂, J ≤ ↑I}
  {pairwise_disjoint₂ : (↑boxes₂).Pairwise Disjoint},
  (∀ J ∈ boxes₁, J ≠ ⊥ → ∃ J' ∈ boxes₂, J ≤ J') →
    BoxIntegral.Prepartition.ofWithBot boxes₁ le_of_mem₁ pairwise_disjoint₁ ≤
      BoxIntegral.Prepartition.ofWithBot boxes₂ le_of_mem₂ pairwise_disjoint₂
-- Mathlib.Control.LawfulFix
Part.Fix.approx_mono' : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {i : ℕ},
  Part.Fix.approx (⇑f) i ≤ Part.Fix.approx (⇑f) i.succ
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- A subsemiring `S` includes `closure s` if and only if it includes `s`.  -/
Subsemiring.closure_le : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {t : Subsemiring R}, Subsemiring.closure s ≤ t ↔ s ⊆ ↑t
-- Init.Prelude
/-- `NonemptyType.{u}` is the type of nonempty types in universe `u`.
It is mainly used in constant declarations where we wish to introduce a type
and simultaneously assert that it is nonempty, but otherwise make the type
opaque.
 -/
NonemptyType : Type (max 0 (u + 1))
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.downAddHom.eq_1 : ∀ (G : Type u) [inst : Add G], downAddHom✝ G = { toFun := ULift.down, map_add' := ⋯ }
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mem_orbit_subMul_iff : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {p : SubMulAction R M} {x m : ↥p},
  x ∈ MulAction.orbit R m ↔ ↑x ∈ MulAction.orbit R ↑m
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toAdditive_toMultiplicative_apply : ∀ {G : Type u_2} [inst : AddZeroClass G] (a : Additive (Multiplicative G)),
  AddEquiv.toAdditive_toMultiplicative a = Multiplicative.toAdd (Additive.toMul a)
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
not_isAssociatedPrime_of_subsingleton : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Subsingleton M], ¬IsAssociatedPrime I M
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.isUnit_of_mem_ofUnits : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : M}, x ∈ S.ofUnits → IsUnit x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last.injEq : ∀ (hs : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof)) (decVars : Array Lean.FVarId)
  (hs_1 : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof)) (decVars_1 : Array Lean.FVarId),
  (Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last hs decVars =
      Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last hs_1 decVars_1) =
    (hs = hs_1 ∧ decVars = decVars_1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_toList_iff_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {v : β}, (k, v) ∈ t.toList ↔ t[k]? = some v
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_eq_bot : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S : Subsemiring R}, S.op = ⊥ ↔ S = ⊥
-- Std.Http.Data.Body.Any
/-- Receives the next body chunk. Returns `none` at end-of-stream.
 -/
Std.Http.Body.Any.recv : Std.Http.Body.Any → Std.Async.Async (Option Std.Http.Chunk)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castLEEmb_Ioo : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.map (Fin.castLEEmb h) (Finset.Ioo a b) = Finset.Ioo (Fin.castLE h a) (Fin.castLE h b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).maxKey ⋯ = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_sub_ofNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ)
  [inst_4 : n.AtLeastTwo], ⌊a - OfNat.ofNat n⌋ = ⌊a⌋ - OfNat.ofNat n
-- Mathlib.GroupTheory.Commutator.Basic
/-- The commutator of direct product is contained in the direct product of the commutators.

See `commutator_pi_pi_of_finite` for equality given `Fintype η`.
 -/
Subgroup.commutator_pi_pi_le : ∀ {η : Type u_4} {Gs : η → Type u_5} [inst : (i : η) → Group (Gs i)] (H K : (i : η) → Subgroup (Gs i)),
  ⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ ≤ Subgroup.pi Set.univ fun i => ⁅H i, K i⁆
-- Mathlib.Topology.MetricSpace.CantorScheme
/-- A scheme is antitone if each set contains its children.  -/
CantorScheme.Antitone : {β : Type u_1} → {α : Type u_2} → (List β → Set α) → Prop
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.coeff_weierstrassPSeries : ∀ (L : PeriodPair) (x : ℂ) (i : ℕ), (L.weierstrassPSeries x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.symm_e : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H), b.symm.e = b.f
-- Std.Data.HashSet.Raw
/-- Returns `true` if the given element is present in the set. There is also a `Prop`-valued version
of this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` use
`==` for comparisons, while for hash sets, both use `==`.
 -/
Std.HashSet.Raw.contains : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → α → Bool
-- Mathlib.Data.Nat.Prime.Basic
Nat.exists_dvd_of_not_prime : ∀ {n : ℕ}, 2 ≤ n → ¬Nat.Prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n
-- Mathlib.Data.Set.Functor
Set.failure_def : ∀ {α : Type u}, failure = ∅
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Matrix.mulVec_fin_two : ∀ {R : Type u_1} [inst : Semiring R] (m : Matrix (Fin 2) (Fin 2) R) (v : Fin 2 → R),
  m.mulVec v = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1]
-- Mathlib.Computability.Ackermann
ack.eq_1 : ∀ (x : ℕ), ack 0 x = x + 1
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The function `log⁺` equals `log (max 1 _)` for non-negative real numbers.  -/
Real.posLog_eq_log_max_one : ∀ {x : ℝ}, 0 ≤ x → x.posLog = Real.log (max 1 x)
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.SatisfiesM_foldlM.go : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α}
  {motive : ℕ → β → Prop} {f : β → α → m β},
  (∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])) →
    ∀ {i j : ℕ} {b : β},
      j ≤ as.size → as.size ≤ i + j → motive j b → SatisfiesM (motive as.size) (Array.foldlM.loop f as as.size ⋯ i j b)
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_eq_self_of_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, Disjoint s t → s \ t = s
-- Init.Data.BitVec.Lemmas
BitVec.toInt_shiftLeftZeroExtend : ∀ {w n : ℕ} {x : BitVec w}, (x.shiftLeftZeroExtend n).toInt = x.toInt * 2 ^ n
-- Lean.Data.Lsp.Extra
Lean.Lsp.instInhabitedLineRange.default : Lean.Lsp.LineRange
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_of : ∀ {α : Type u_1} (m : α), (FreeMonoid.of m).length = 1
-- Mathlib.CategoryTheory.Limits.Final
/-- If `F` is final,
the category of cocones on `F ⋙ G` is equivalent to the category of cocones on `G`,
for any `G : D ⥤ E`.
 -/
CategoryTheory.Functor.Final.coconesEquiv : {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.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                (G : CategoryTheory.Functor D E) →
                  CategoryTheory.Limits.Cocone (F.comp G) ≌ CategoryTheory.Limits.Cocone G
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_neg_bmod : ∀ {x : ℤ} {n : ℕ}, (-x.bmod n).bmod n = (-x).bmod n
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.associator_def : ∀ {C : Type u} [inst : CategoryTheory.Bicategory C] (X : C) (f g h : X ⟶ X),
  CategoryTheory.MonoidalCategoryStruct.associator f g h = CategoryTheory.Bicategory.associator f g h
-- Mathlib.Order.Defs.Unbundled
/-- `IsStrictTotalOrder X lt` means that the binary relation `lt` on `X` is a strict total order,
that is, `Std.Trichotomous lt` and `IsStrictOrder X lt`.  -/
IsStrictTotalOrder : (α : Sort u_1) → (α → α → Prop) → Prop
-- Init.Meta.Defs
Lean.Syntax.instCoeTSyntaxArrayOfTSyntax : {k k' : Lean.SyntaxNodeKinds} →
  [Coe (Lean.TSyntax k) (Lean.TSyntax k')] → Coe (Lean.TSyntaxArray k) (Lean.TSyntaxArray k')
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_EStateM : ∀ {ε σ α : Type} (x : EStateM ε σ α) (h : ε → EStateM ε σ α) (post : α → σ → Prop) (epost : ε → σ → Prop),
  ⦃ fun s => Std.Internal.Do.wp x post (fun e s' => Std.Internal.Do.wp (h e) post epost s') s ⦄
    MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function `f` tends to infinity along a filter,
then `f` multiplied by a negative constant (on the right) tends to negative infinity.  -/
Filter.Tendsto.atTop_mul_const_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x * r) l Filter.atBot
-- Mathlib.Order.CompleteLatticeIntervals
subset_sInf_of_within : ∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : InfSet α] [inst_2 : Inhabited ↑s] {t : Set ↑s},
  t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s → sInf (Subtype.val '' t) = ↑(sInf t)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `MonoidHom.domRestrict_mrange`. -/
MonoidHom.restrict_mrange : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) (f : M →* N),
  MonoidHom.mrange (f.domRestrict S) = Submonoid.map f S
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalStarAlgHom.ext_continuousMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [ContinuousMapZero.UniqueHom R A] (a : A) [CompactSpace ↑(quasispectrum R a)]
  (φ ψ : ContinuousMapZero (↑(quasispectrum R a)) R →⋆ₙₐ[R] A),
  Continuous ⇑φ →
    Continuous ⇑ψ → φ (ContinuousMapZero.id (quasispectrum R a)) = ψ (ContinuousMapZero.id (quasispectrum R a)) → φ = ψ
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- If the coefficients `f m` of an L-series are zero for `m ≤ n` and the L-series converges
at some point, then `f (n+1)` is the limit of `(n+1)^x * LSeries f x` as `x → ∞`.  -/
LSeries.tendsto_cpow_mul_atTop : ∀ {f : ℕ → ℂ} {n : ℕ},
  (∀ m ≤ n, f m = 0) →
    LSeries.abscissaOfAbsConv f < ⊤ →
      Filter.Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) Filter.atTop (nhds (f (n + 1)))
-- Mathlib.Data.List.Infix
List.get_inits : ∀ {α : Type u_1} (l : List α) (n : Fin l.inits.length), l.inits.get n = List.take (↑n) l
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.closedCell_subset_of_mem`. -/
Topology.CWComplex.Subcomplex.closedCell_subset_of_mem : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n},
  i ∈ E.I n → Topology.RelCWComplex.closedCell n i ⊆ ↑E
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccPrelimit_lift : ∀ {o : Ordinal.{v}}, Order.IsSuccPrelimit (Ordinal.lift.{u, v} o) ↔ Order.IsSuccPrelimit o
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Every element is a conjugate root of itself.
 -/
IsConjRoot.refl : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : A}, IsConjRoot R x x
-- Mathlib.Data.Fin.VecNotation
/-- We push `Fin.snoc` inside `vecCons`. This allows us to simplify e.g.
`Fin.snoc ![1, 3, 7] 5` to `![1, 3, 7, 5]`.  -/
Matrix.Fin.snoc_vecCons : ∀ {n : ℕ} {α : Type u_1} (x y : α) (p : Fin n → α), Fin.snoc (Matrix.vecCons y p) x = Matrix.vecCons y (Fin.snoc p x)
-- Mathlib.Data.Fin.Tuple.Basic
/-- Given an `(n + 2)`-tuple `m` and two indexes `i : Fin (n + 1)` and `j : Fin (n + 2)`,
one can remove `j`th element from `m`, then remove `i`th element from the result,
or one can remove `(j.succAbove i)`th element from `m`,
then remove `(i.predAbove j)`th element from the result.

These two operations correspond to removing the same two elements in a different order,
so they result in the same `n`-tuple.  -/
Fin.removeNth_removeNth_eq_swap : ∀ {n : ℕ} {α : Sort u_3} (m : Fin (n + 2) → α) (i : Fin (n + 1)) (j : Fin (n + 2)),
  i.removeNth (j.removeNth m) = (i.predAbove j).removeNth ((j.succAbove i).removeNth m)
-- Mathlib.Data.Multiset.Filter
Multiset.map_le_map_iff : ∀ {α : Type u_1} {β : Type v} {f : α → β},
  Function.Injective f → ∀ {s t : Multiset α}, Multiset.map f s ≤ Multiset.map f t ↔ s ≤ t
-- Init.Data.SInt.Lemmas
Int32.mul_sub : ∀ {a b c : Int32}, a * (b - c) = a * b - a * c
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_Δ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).Δ = ↑C.u⁻¹ ^ 12 * W.Δ
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `getThenInsertIfNew?` which can be used in the absence of balance
information but still assumes the preconditions of `getThenInsertIfNew?`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?! : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] →
        Std.DTreeMap.Internal.Impl α β → (k : α) → β k → Option (β k) × Std.DTreeMap.Internal.Impl α β
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.InfiniteNeg.not_infinitesimal : ∀ {x : ℝ*}, x.InfiniteNeg → ¬x.Infinitesimal
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivAt.const_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {c : ℝ}, HasFDerivAt f f' x → 0 < c → HasFDerivAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') x
-- Mathlib.Algebra.Lie.OfAssociative
Module.End.instLieModule : ∀ {R : Type u} [inst : CommRing R] {M : Type w} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  LieModule R (Module.End R M) M
-- Mathlib.Order.CompleteLattice.Basic
le_iInf₂_iff : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α},
  a ≤ ⨅ i, ⨅ j, f i j ↔ ∀ (i : ι) (j : κ i), a ≤ f i j
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- Given `φ : F ⟶ G`, this is the cocycle in `Cocycle (mappingCone φ) K n` that is
constructed from `α : Cochain F K m` (with `m + 1 = n`) and `β : Cocycle F K n`,
when a suitable cocycle relation is satisfied.  -/
CochainComplex.mappingCone.descCocycle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {K : CochainComplex C ℤ} →
              {n m : ℤ} →
                (α : CochainComplex.HomComplex.Cochain F K m) →
                  (β : CochainComplex.HomComplex.Cocycle G K n) →
                    m + 1 = n →
                      CochainComplex.HomComplex.δ m n α =
                          n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ →
                        CochainComplex.HomComplex.Cocycle (CochainComplex.mappingCone φ) K n
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasOxfordStrings : Sort u_1 → Sort (max 1 u_1)
-- Mathlib.Order.Interval.Multiset
Multiset.left_mem_Ico : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, a ∈ Multiset.Ico a b ↔ a < b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ Std.DHashMap.filter f m},
  Std.DHashMap.Const.get (Std.DHashMap.filter f m) k h' = Std.DHashMap.Const.get m k ⋯
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.eq_one_iff : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G} [inst_1 : N.Normal] (x : G), ↑x = 1 ↔ x ∈ N
-- Mathlib.Topology.FiberBundle.Constructions
/-- Given trivializations `e₁`, `e₂` for fiber bundles `E₁`, `E₂` over a base `B`, the forward
function for the construction `Trivialization.prod`, the induced
trivialization for the fiberwise product of `E₁` and `E₂`.  -/
Bundle.Trivialization.Prod.toFun' : {B : Type u_1} →
  [inst : TopologicalSpace B] →
    {F₁ : Type u_2} →
      [inst_1 : TopologicalSpace F₁] →
        {E₁ : B → Type u_3} →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
            {F₂ : Type u_4} →
              [inst_3 : TopologicalSpace F₂] →
                {E₂ : B → Type u_5} →
                  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                    Bundle.Trivialization F₁ Bundle.TotalSpace.proj →
                      Bundle.Trivialization F₂ Bundle.TotalSpace.proj →
                        (Bundle.TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → B × F₁ × F₂
-- Mathlib.Combinatorics.Enumerative.Composition
compositionFintype : (n : ℕ) → Fintype (Composition n)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
List.findSome?.match_1.congr_eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (x : Option β) (h_1 : (b : β) → motive (some b))
  (h_2 : Unit → motive none),
  x = none →
    (match x with
      | some b => h_1 b
      | none => h_2 ()) ≍
      h_2 ()
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
AhlswedeZhang.supSum_singleton : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Finset α} [Nonempty α],
  s ≠ Finset.univ → AhlswedeZhang.supSum {s} = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹
-- Mathlib.Topology.Algebra.MulAction
OrderDual.instContinuousSMul_left : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X], ContinuousSMul Mᵒᵈ X
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.instIsOrderedAddMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α], IsOrderedAddMonoid αᵐᵒᵖ
-- Mathlib.Analysis.Calculus.Deriv.Prod
/-- A variant of `hasStrictDerivAt_finCons` where the derivative variables are free on the RHS
instead.  -/
hasStrictDerivAt_finCons' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : F' 0} {φs' : (i : Fin n) → F' i.succ},
  HasStrictDerivAt (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x ↔
    HasStrictDerivAt φ φ' x ∧ HasStrictDerivAt φs φs' x
-- Init.Data.SInt.Basic
/-- Convert an `ISize` to `BitVec 64`, assuming that the system bit-width is 64.

This operation is intended for proof purposes.
 -/
ISize.toBitVec64 : ISize → System.Platform.numBits = 64 → BitVec 64
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G)
  [inst_2 : ∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))],
  (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit =
    {
      app := fun Y =>
        (((adj.homEquiv (G.obj Y) Y).symm.subtypeEquiv ⋯).trans
            (CategoryTheory.Limits.Cofork.IsColimit.homIso
                (CategoryTheory.Limits.colimit.isColimit
                  (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app Y)))
                    (adj.counit.app (F.obj (G.obj Y)))))
                Y).symm)
          ({ toFun := fun f => ⟨f.f, ⋯⟩, invFun := fun g => { f := ↑g, h := ⋯ }, left_inv := ⋯, right_inv := ⋯ }
            (CategoryTheory.CategoryStruct.id ((CategoryTheory.Monad.comparison adj).obj Y))),
      naturality := ⋯ }
-- Mathlib.Algebra.Module.Equiv.Opposite
MulOpposite.opLinearEquiv_symm_toAddEquiv : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (MulOpposite.opLinearEquiv R).symm.toAddEquiv = MulOpposite.opAddEquiv.symm
-- Batteries.Data.Vector.Lemmas
Vector.get_range : ∀ (n : ℕ) (i : Fin n), (Vector.range n).get i = ↑i
-- Lean.DocString.Links
_private.Lean.DocString.Links.0.Lean.fallbackManualRoot : String
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.toLinearExpr : Lean.Expr → Lean.Meta.Simp.Arith.Int.ToLinear.M Int.Internal.Linear.Expr
-- Batteries.Data.Char.Basic
Char.eq_false_of_any_eq_false : ∀ {p : Char → Bool}, Char.any p = false → ∀ (c : Char), p c = false
-- Mathlib.Data.Multiset.FinsetOps
Multiset.Nodup.ndinter : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} (t : Multiset α), s.Nodup → (s.ndinter t).Nodup
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : β k → β k},
      (t.modify k f).get? k' = if h : cmp k k' = Ordering.eq then cast ⋯ (Option.map f (t.get? k)) else t.get? k'
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_one : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M], ⇑1 = 1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.MatchResult.push : {α : Type} → Lean.Meta.RefinedDiscrTree.MatchResult α → ℕ → Array α → Lean.Meta.RefinedDiscrTree.MatchResult α