mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.CodeActions.Attr
/-- The list of command code actions to apply on any command.  -/
Lean.CodeAction.CommandCodeActions.onAnyCmd : Lean.CodeAction.CommandCodeActions → Array Lean.CodeAction.CommandCodeAction
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomposingCat_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b c : B) {X Y : b ⟶ c} (η : X ⟶ Y),
  (CategoryTheory.Bicategory.postcomposingCat a b c).map η =
    CategoryTheory.NatTrans.toCatHom₂ ((CategoryTheory.Bicategory.postcomposing a b c).map η)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instInhabitedCustomEliminator : Inhabited Lean.Meta.CustomEliminator
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.ind.congr_simp : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f f_1 : BumpCovering ι X s),
  f = f_1 → ∀ (x x_1 : X) (e_x : x = x_1) (hx : x ∈ s), f.ind x hx = f_1.ind x_1 ⋯
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_sub_negPart : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (IsSelfAdjoint a) CFC.posPart_sub_negPart._auto_1 → a⁺ - a⁻ = a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k a fallback : α} {v : β k},
  (t.insertIfNew k v).getKeyD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKeyD a fallback
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  (t.truncLT n).map ((t.truncLTι n).app X) = (t.truncLTι n).app ((t.truncLT n).obj X)
-- Lean.Meta.Tactic.Grind.Split
/-- Given `c`, the condition of an `if-then-else`, check whether we need to case-split on the `if-then-else` or not  -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.checkIteCondStatus : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitStatus
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `PadicAlgCl p` is nontrivial.  -/
PadicAlgCl.nontriviallyNormedField : (p : ℕ) → [hp : Fact (Nat.Prime p)] → NontriviallyNormedField (PadicAlgCl p)
-- Mathlib.Order.Filter.Interval
Filter.TendstoIxxClass.mk : ∀ {α : Type u_1} {Ixx : α → α → Set α} {l₁ : Filter α} {l₂ : outParam (Filter α)},
  Filter.Tendsto (fun p => Ixx p.1 p.2) (l₁ ×ˢ l₁) l₂.smallSets → Filter.TendstoIxxClass Ixx l₁ l₂
-- Mathlib.Data.Set.Lattice
Set.iUnion_option : ∀ {α : Type u_1} {ι : Type u_12} (s : Option ι → Set α), ⋃ o, s o = s none ∪ ⋃ i, s (some i)
-- Std.Time.Time.Unit.Nanosecond
/-- `Ordinal` represents a bounded value for nanoseconds in a day, which ranges between 0 and 86400000000000.
 -/
Std.Time.Nanosecond.Ordinal.OfDay : Type
-- Mathlib.Tactic.CancelDenoms.Core
/-- `mkProdPrf α sα v v' tr e` produces a proof of `v'*e = e'`, where numeric denominators have been
canceled in `e'`, distributing `v` proportionally according to the tree `tr` computed
by `findCancelFactor`.

The `v'` argument is a numeral expression corresponding to `v`, which we need in order to state
the return type accurately.
 -/
Mathlib.Tactic.CancelDenoms.mkProdPrf : {u : Lean.Level} →
  (α : Q(Type u)) →
    (sα : Q(Field «$α»)) →
      ℕ →
        (v' : Q(«$α»)) →
          BinaryTree ℕ → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Tactic.CancelDenoms.CancelResult q(inferInstance) e v')
-- Std.Time.DateTime.PlainDateTime
/-- Adds an `Hour.Offset` to a `PlainDateTime`, adjusting the date if the hour overflows.
 -/
Std.Time.PlainDateTime.addHours : Std.Time.PlainDateTime → Std.Time.Hour.Offset → Std.Time.PlainDateTime
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isBigO_atBot_of_degree_le : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜], P.degree ≤ Q.degree → (fun x => Polynomial.eval x P) =O[Filter.atBot] fun x => Polynomial.eval x Q
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Functor.mapCone₂_π_app : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  {K₁ : CategoryTheory.Functor J₁ C₁} {K₂ : CategoryTheory.Functor J₂ C₂} (c₁ : CategoryTheory.Limits.Cone K₁)
  (c₂ : CategoryTheory.Limits.Cone K₂) (x : J₁ × J₂),
  (G.mapCone₂ c₁ c₂).π.app x =
    CategoryTheory.CategoryStruct.comp ((G.map (c₁.π.app x.1)).app c₂.pt) ((G.obj (K₁.obj x.1)).map (c₂.π.app x.2))
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt16.size ≤ n → (UInt16.ofNatClamp n).toBitVec = (UInt16.size - 1)#'UInt16.toBitVec_ofNatClamp_of_le._proof_1
-- Mathlib.Order.KrullDimension
LTSeries.map.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (p p_1 : LTSeries α),
  p = p_1 → ∀ (f f_1 : α → β) (e_f : f = f_1) (hf : StrictMono f), p.map f hf = p_1.map f_1 ⋯
-- Mathlib.Topology.Category.TopPair
/-- Construct a topological pair from its components.  -/
TopPair.of : {A X : TopCat} → (f : A ⟶ X) → Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → TopPair
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_mul_aux : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {M N : Matrix n n R}
  {p : n → n}, ¬Function.Bijective p → ∑ σ, ↑↑(Equiv.Perm.sign σ) * ∏ x, M (σ x) (p x) * N (p x) x = 0
-- Mathlib.CategoryTheory.Limits.MonoCoprod
/-- the left inclusion of a colimit binary cofan is mono  -/
CategoryTheory.Limits.MonoCoprod.binaryCofan_inl : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Limits.MonoCoprod C] ⦃A B : C⦄
  (c : CategoryTheory.Limits.BinaryCofan A B) (x : CategoryTheory.Limits.IsColimit c), CategoryTheory.Mono c.inl
-- Mathlib.Algebra.Ring.Equiv
RingEquivClass.toAddEquivClass : ∀ {F : Type u_1} {R : Type u_4} {S : Type u_5} [inst : EquivLike F R S] [inst_1 : Mul R] [inst_2 : Add R]
  [inst_3 : Mul S] [inst_4 : Add S] [h : RingEquivClass F R S], AddEquivClass F R S
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- The representative is isomorphic to the original module.  -/
Module.Finite.reprEquiv : (R : Type u) →
  (M : Type u_1) →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [inst_3 : Module.Finite R M] → Module.Finite.repr R M ≃ₗ[R] M
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.instCanLiftENatOfENatLeAleph0 : CanLift Cardinal.{u_1} ℕ∞ Cardinal.ofENat fun x => x ≤ Cardinal.aleph0
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPair_map_inclLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ : CategoryTheory.Functor C E) (Fᵣ : CategoryTheory.Functor D E')
  {c c' : C} (f : c ⟶ c'),
  (CategoryTheory.Join.mapPair Fₗ Fᵣ).map ((CategoryTheory.Join.inclLeft C D).map f) =
    (CategoryTheory.Join.inclLeft E E').map (Fₗ.map f)
-- Mathlib.RingTheory.Artinian.Instances
IsArtinianRing.instDecompositionMonoidPolynomial : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R] [IsReduced R], DecompositionMonoid (Polynomial R)
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
/-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` ∈ `S`, and `S'` a subalgebra of `S` that contains
`lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
`sᵢ ^ n • x ∈ S'` for some `n` for each `sᵢ`.  -/
Subalgebra.mem_of_finsetSum_eq_one_of_pow_smul_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (S' : Subalgebra R S) {ι : Type u_3} (ι' : Finset ι) (s l : ι → S),
  ∑ i ∈ ι', l i * s i = 1 →
    (∀ (i : ι), s i ∈ S') → (∀ (i : ι), l i ∈ S') → ∀ (x : S), (∀ (i : ι), ∃ n, s i ^ n • x ∈ S') → x ∈ S'
-- Mathlib.RingTheory.Unramified.Basic
/-- Unramified is stable under composition.  -/
Algebra.Unramified.comp : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [Algebra.Unramified R A]
  [Algebra.Unramified A B], Algebra.Unramified R B
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.forIn.visit.match_1.splitter : {α : Type u_1} →
  {σ : Type u_3} →
    (motive : RBTree.RBNode α → σ → Sort u_2) →
      (x : RBTree.RBNode α) →
        (x_1 : σ) →
          ((b : σ) → motive RBTree.RBNode.nil b) →
            ((c : RBTree.RBColor) →
                (l : RBTree.RBNode α) →
                  (v : α) → (r : RBTree.RBNode α) → (b : σ) → motive (RBTree.RBNode.node c l v r) b) →
              motive x x_1
-- Std.Async.ContextAsync
/-- Runs all computations concurrently and collects results in the same order. Each runs in its own child context;
if any computation fails, all others are cancelled and the exception is propagated.
 -/
Std.Async.ContextAsync.concurrentlyAll : {α : Type} →
  Array (Std.Async.ContextAsync α) → optParam Task.Priority Task.Priority.default → Std.Async.ContextAsync (Array α)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.instMonoF' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData' C) (i j : D.J),
  CategoryTheory.Mono (D.f' i j)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The range of a surjective `MonoidHom` is the whole of the codomain.  -/
MonoidHom.mrange_eq_top_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F), Function.Surjective ⇑f → MonoidHom.mrange f = ⊤
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_anti_mono_ideal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {s t : Ideal A}, s ≤ t → ProjectiveSpectrum.zeroLocus 𝒜 ↑t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 ↑s
-- Init.Data.BitVec.Lemmas
/-- Get the most significant bit after `extractLsb'`. With `extractLsb'`, we extract
a `BitVec len` `x'` with length `len` from `BitVec w` `x`, starting from the
element at position `start`. The function `getMsb` extracts a bit counting from
the most significant bit. Assuming certain conditions,
`(@extractLsbD' w x start len).getMsbD i` is equal to
`@getMsbD w x (w - (start + len - i))`.

Example (w := 10, start := 3, len := 4):

                                |---| = w - (start + len) = 3
                                      |start + len|       = 7
                                            |start|       = 3
                                      | len |             = 4
let x                       =   9 8 7 6 5 4 3 2 1 0
let x' = x.extractLsb' 3 4  =         6 5 4 3
                                      | |
                                      | x'.getMsbD 1 =
                                        x.getMsbD (i := w - (start + len - i) = 10 - (3 + 4 - 1) = 4)
                                      |
                                      x'.getMsbD 0 =
                                      x.getMsbD (i := w - (start + len - i) = 10 - (3 + 4 - 0) = 3)

# Condition 1: `i < len`

The index `i` must be within the range of `len`.

# Condition 2: `start + len - i ≤ w`

If `start + len` is larger than `w`, the high bits at `i` with `w ≤ i` are filled with 0,
meaning that `getMsbD[i] = false` for these `i`.
If `i` is large enough, `getMsbD[i]` is again within the bounds `x`.
The precise condition is:

  `start + len - i ≤ w`

Example (w := 10, start := 7, len := 5):

                                    |= w - (start + len)    = 0
                                |      start + len    |     = 12
                                        |    start    |     = 7
                                |  len  |                   = 5
let x                       =       9 8 7 6 5 4 3 2 1 0
let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
                                |   |
                                |   x'.getMsbD (i := 2) =
                                |   x.getMsbD (i := w - (start + len - i) = 10 - (7 + 5 - 2)) =
                                |   x.getMsbD 0
                                |   ✅ start + len - i ≤ w
                                |        7 + 5 - 2 = 10 ≤ 10
                                |
                                x'.getMsbD (i := 0) =
                                x.getMsbD (i := w - (start + len - i) = 10 - (7 + 5 - 0)) =
                                x.getMsbD (i := w - (start + len - i) = x.getMsbD (i := -2) -- in Nat becomes 0
                                ❌ start + len - i ≤ w
                                     7 + 5 - 0 ≤ w
 -/
BitVec.getMsbD_extractLsb' : ∀ {w start len : ℕ} {x : BitVec w} {i : ℕ},
  (BitVec.extractLsb' start len x).getMsbD i =
    (decide (i < len) && (decide (start + len - i ≤ w) && x.getMsbD (w - (start + len - i))))
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `Measurable.smul` -/
Measurable.fun_smul : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {f : α → M} {g : α → X} [inst_2 : MeasurableSpace M] [MeasurableSMul₂ M X],
  Measurable f → Measurable g → Measurable fun i => f i • g i
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.bind_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : α → β) (q : β → PMF γ),
  (PMF.map f p).bind q = p.bind (q ∘ f)
-- Std.Internal.Do.Order.Basic
Lean.Order.le_of_imp_top_le : ∀ (x y : Prop), (x → Lean.Order.PartialOrder.rel Lean.Order.top y) → Lean.Order.PartialOrder.rel x y
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqns.splitterName : Lean.Meta.Match.MatchEqns → Lean.Name
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.map_sup : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : NonUnitalSemiring B]
  [inst_6 : StarRing B] [inst_7 : Module R B] [inst_8 : FunLike F A B] [inst_9 : NonUnitalAlgHomClass F R A B]
  [inst_10 : StarHomClass F A B] [inst_11 : IsScalarTower R A A] [inst_12 : SMulCommClass R A A]
  [inst_13 : StarModule R A] [inst_14 : IsScalarTower R B B] [inst_15 : SMulCommClass R B B] [inst_16 : StarModule R B]
  (f : F) (S T : NonUnitalStarSubalgebra R A),
  NonUnitalStarSubalgebra.map f (S ⊔ T) = NonUnitalStarSubalgebra.map f S ⊔ NonUnitalStarSubalgebra.map f T
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerLeft_comp_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H K : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ K),
  CategoryTheory.CategoryStruct.comp (F.whiskerLeft β) (CategoryTheory.Functor.whiskerRight α K) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α H) (G.whiskerLeft β)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.zero_powerlt : ∀ {a : Cardinal.{u_1}}, a ≠ 0 → 0 ^< a = 1
-- Mathlib.Data.ENNReal.Inv
/-- The birational order isomorphism between `ℝ≥0∞` and the unit interval `Set.Iic (1 : ℝ≥0∞)`.  -/
ENNReal.orderIsoIicOneBirational : ENNReal ≃o ↑(Set.Iic 1)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- The truncated cast `ENNReal.truncateToReal t : ℝ≥0∞ → ℝ` is continuous when `t ≠ ∞`.  -/
ENNReal.continuous_truncateToReal : ∀ {t : ENNReal}, t ≠ ⊤ → Continuous t.truncateToReal
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_eq_maxD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.max! = t.maxD default
-- Lean.ToExpr
_private.Lean.ToExpr.0.Lean.Name.toExprAux : Lean.Name → Lean.Expr
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Reformulation of `hasSum_nat_cosZeta` using `LSeriesHasSum`.  -/
HurwitzZeta.LSeriesHasSum_cos : ∀ (a : ℝ) {s : ℂ}, 1 < s.re → LSeriesHasSum (fun x => ↑(Real.cos (2 * Real.pi * a * ↑x))) s (HurwitzZeta.cosZeta (↑a) s)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
/-- Note that this is not trivial as we don't assume that `f` is integrable.  -/
MeasureTheory.setIntegral_condExp_le_of_ae_restrict_nonneg : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ {f : α → ℝ}, 0 ≤ᵐ[μ.restrict s] f → ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ
-- Mathlib.Analysis.Complex.Exponential
Real.exp_monotone : Monotone Real.exp
-- Mathlib.Order.SuccPred.Basic
Order.succ_eq_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α),
  Order.succ a = sInf (Set.Ioi a)
-- Init.Data.UInt.Bitwise
UInt8.xor_assoc : ∀ (a b c : UInt8), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inr_mapHomologicalComplexObjIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)],
  CategoryTheory.CategoryStruct.comp ((H.mapHomologicalComplex c).map (HomologicalComplex.homotopyCofiber.inr φ))
      (HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjIso φ H).hom =
    HomologicalComplex.homotopyCofiber.inr ((H.mapHomologicalComplex c).map φ)
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.instIsMarkovKernelProdParallelComp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel γ δ} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η],
  ProbabilityTheory.IsMarkovKernel (κ.parallelComp η)
-- Init.Data.List.Scan.Lemmas
List.getElem?_scanr_zero : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β}, (List.scanr f b l)[0]? = some (List.foldr f b l)
-- Std.Data.HashMap.Lemmas
/-- Simpler variant of `getElem!_filterMap` when `LawfulBEq` is available.  -/
Std.HashMap.getElem!_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α]
  [inst : Inhabited γ] {f : α → β → Option γ} {k : α}, (Std.HashMap.filterMap f m)[k]! = (m[k]?.bind (f k)).get!
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk.congr_simp : ∀ {M : Type u_3} [inst : MulOneClass M] (toSubsemigroup toSubsemigroup_1 : Subsemigroup M)
  (e_toSubsemigroup : toSubsemigroup = toSubsemigroup_1) (one_mem' : 1 ∈ toSubsemigroup.carrier),
  { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = { toSubsemigroup := toSubsemigroup_1, one_mem' := ⋯ }
-- Mathlib.Data.Matrix.Basic
LinearMap.mapMatrix_id : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α], LinearMap.id.mapMatrix = LinearMap.id
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.connected_bot_iff : ∀ {V : Type u}, ⊥.Connected ↔ Subsingleton V ∧ Nonempty V
-- Init.Data.List.Sublist
List.prefix_filterMap_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l₁ : List α} {l₂ : List β},
  l₂ <+: List.filterMap f l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = List.filterMap f l
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.le_multiplicity_of_δ_of_fin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] {n : ℕ}
  (f : Fin n → E),
  (∀ (i : Fin n), ‖f i‖ ≤ 2) →
    (Pairwise fun i j => 1 - Besicovitch.goodδ E ≤ ‖f i - f j‖) → n ≤ Besicovitch.multiplicity E
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- Families of `PowerSeries` that can be substituted, as an `Ideal`.  -/
PowerSeries.HasSubst.ideal : {τ : Type u_3} → {S : Type u_4} → [inst : CommRing S] → Ideal (MvPowerSeries τ S)
-- Std.Data.HashMap.Raw
/-- Transforms the hash map into a list of mappings in some order.  -/
Std.HashMap.Raw.toList : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → List (α × β)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.congr_right : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g₁ g₂ : α → F} {l : Filter α},
  f =O[𝕜; l] g₁ → (∀ (x : α), g₁ x = g₂ x) → f =O[𝕜; l] g₂
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_toList_iff_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α} {v : β}, (k, v) ∈ m.toList ↔ m[k]? = some v
-- Init.Data.Int.Order
Int.toNat_of_nonneg : ∀ {a : ℤ}, 0 ≤ a → ↑a.toNat = a
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentationCore.mk.injEq : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M}
  (desc : {N : Type w'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → relations.Solution N → M →ₗ[A] N)
  (postcomp_desc :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N),
      solution.postcomp (desc s) = s)
  (postcomp_injective :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] {f f' : M →ₗ[A] N},
      solution.postcomp f = solution.postcomp f' → f = f')
  (desc_1 : {N : Type w'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → relations.Solution N → M →ₗ[A] N)
  (postcomp_desc_1 :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N),
      solution.postcomp (desc_1 s) = s)
  (postcomp_injective_1 :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] {f f' : M →ₗ[A] N},
      solution.postcomp f = solution.postcomp f' → f = f'),
  ({ desc := desc, postcomp_desc := postcomp_desc, postcomp_injective := postcomp_injective } =
      { desc := desc_1, postcomp_desc := postcomp_desc_1, postcomp_injective := postcomp_injective_1 }) =
    (desc = desc_1)
-- Mathlib.FieldTheory.Perfect
Polynomial.rootsExpandToRoots_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p : ℕ) [inst_2 : ExpChar R p] (f : Polynomial R)
  [inst_3 : DecidableEq R] (x : ↥((Polynomial.expand R p) f).roots.toFinset),
  ↑((Polynomial.rootsExpandToRoots p f) x) = ↑x ^ p
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mem_carrier : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M)
  {x : M}, x ∈ p.carrier ↔ x ∈ ↑p