mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_mul_of_isUnit_right : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a u : M}, IsUnit u → UniqueFactorizationMonoid.radical (a * u) = UniqueFactorizationMonoid.radical a
-- Init.Grind.AC
Lean.Grind.AC.Seq.var : Lean.Grind.AC.Var → Lean.Grind.AC.Seq
-- Init.Grind.Order
Lean.Grind.Order.eq_trans_true' : ∀ {p q : Prop}, p = q → p = True → q = True
-- Mathlib.CategoryTheory.Shift.Quotient
/-- The shift by a monoid `A` induced on a quotient category `Quotient r` when the
relation `r` is compatible with the shift.  -/
CategoryTheory.HasShift.quotient : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (r : HomRel C) →
      (A : Type w) →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] →
            [r.IsCompatibleWithShift A] → CategoryTheory.HasShift (CategoryTheory.Quotient r) A
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.contMDiffAt_finsum : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] {s : Set M}
  (f : SmoothPartitionOfUnity ι I M s) {n : ℕ∞} {x₀ : M} {g : ι → M → F},
  (∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I (modelWithCornersSelf ℝ F) (↑n) (g i) x₀) →
    ContMDiffAt I (modelWithCornersSelf ℝ F) (↑n) (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_zero_succ : ∀ {n : ℕ}, Fin.cons 0 Fin.succ = id
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.comm : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t : Set X}, Metric.AreSeparated s t ↔ Metric.AreSeparated t s
-- Mathlib.Analysis.Normed.Ring.Units
/-- In a normed ring with summable geometric series, an element `y` of distance less
than `‖x⁻¹‖⁻¹` from `x` is a unit. Here we construct its `Units` structure.  -/
Units.ofNearby : {R : Type u_1} → [inst : NormedRing R] → [HasSummableGeomSeries R] → (x : Rˣ) → (y : R) → ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹ → Rˣ
-- Mathlib.Order.Grade
isMax_grade_iff : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeMaxOrder 𝕆 α] {a : α},
  IsMax (grade 𝕆 a) ↔ IsMax a
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instModuleComplexOfHasDetOneFinOfNatNatReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → [Γ.HasDetOne] → Module ℂ (CuspForm Γ k)
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.monic_f : ∀ {R : Type u_1} [inst : CommRing R] (self : StandardEtalePair R), self.f.Monic
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_le_of_subset : ∀ {s t : Set Ordinal.{u}}, ¬BddAbove s → s ⊆ t → Ordinal.enumOrd t ≤ Ordinal.enumOrd s
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l : Filter α} (op₁ : γ → δ) (op₂ : β → γ) (f : l.Germ β),
  Filter.Germ.map op₁ (Filter.Germ.map op₂ f) = Filter.Germ.map (op₁ ∘ op₂) f
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.subsingleton : ∀ {R : Type u_1} [inst : CommRing R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsAdicComplete ⊤ M → Subsingleton M
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.isoOfComponents_inv_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : (i : ι) → C₁.X i ≅ C₂.X i)
  (hf :
    autoParam
      (∀ (i j : ι),
        c.Rel i j →
          CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) =
            CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom)
      HomologicalComplex.Hom.isoOfComponents._auto_1)
  (i : ι), (HomologicalComplex.Hom.isoOfComponents f hf).inv.f i = (f i).inv
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.hom_ext_iff : ∀ {M N : MagmaCat} {f g : M ⟶ N}, f = g ↔ MagmaCat.Hom.hom f = MagmaCat.Hom.hom g
-- Mathlib.Algebra.Ring.Prod
RingHom.prodMap_def : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [inst : NonAssocSemiring R]
  [inst_1 : NonAssocSemiring S] [inst_2 : NonAssocSemiring R'] [inst_3 : NonAssocSemiring S'] (f : R →+* R')
  (g : S →+* S'), f.prodMap g = (f.comp (RingHom.fst R S)).prod (g.comp (RingHom.snd R S))
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
/-- Eta-expanded form of `MeasureTheory.VectorMeasure.withDensity_zero` -/
MeasureTheory.VectorMeasure.withDensity_fun_zero : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.withDensity (fun x => 0) B = 0
-- Mathlib.Algebra.Group.Action.Prod
Prod.faithfulVAddRight : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd M β] [Nonempty α] [FaithfulVAdd M β],
  FaithfulVAdd M (α × β)
-- Std.Sync.Channel
Std.CloseableChannel.Error.ofNat : ℕ → Std.CloseableChannel.Error
-- Mathlib.Algebra.Group.Defs
LeftCancelMonoid.toMonoid : {M : Type u} → [self : LeftCancelMonoid M] → Monoid M
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.inr.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousAddMonoidHom.inr A B = ContinuousAddMonoidHom.prod 0 (ContinuousAddMonoidHom.id B)
-- Mathlib.Order.Interval.Set.Basic
IsBot.Ici_eq : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsBot a → Set.Ici a = Set.univ
-- Mathlib.Analysis.Matrix.Order
/-- A positive definite matrix `M` induces a norm on `Matrix n n 𝕜`
`‖x‖ = sqrt (x * M * xᴴ).trace`.  -/
Matrix.toMatrixSeminormedAddCommGroup : {𝕜 : Type u_1} →
  {n : Type u_2} →
    [inst : RCLike 𝕜] → [Fintype n] → (M : Matrix n n 𝕜) → M.PosSemidef → SeminormedAddCommGroup (Matrix n n 𝕜)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} {f : SmoothPartitionOfUnity ι I M s} {U : ι → Set M},
  f.toPartitionOfUnity.IsSubordinate U ↔ f.IsSubordinate U
-- Mathlib.LinearAlgebra.Multilinear.TensorProduct
MultilinearMap.domCoprodDep'_apply : ∀ {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [inst : CommSemiring R] {N₁ : Type u_6} [inst_1 : AddCommMonoid N₁]
  [inst_2 : Module R N₁] {N₂ : Type u_7} [inst_3 : AddCommMonoid N₂] [inst_4 : Module R N₂] {N : ι₁ ⊕ ι₂ → Type u_8}
  [inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] [inst_6 : (i : ι₁ ⊕ ι₂) → Module R (N i)]
  (a : MultilinearMap R (fun i₁ => N (Sum.inl i₁)) N₁) (b : MultilinearMap R (fun i₂ => N (Sum.inr i₂)) N₂),
  MultilinearMap.domCoprodDep' (a ⊗ₜ[R] b) = a.domCoprodDep b
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instInv.eq_1 : ∀ {α : Type u}, FreeGroup.instInv = { inv := Quot.map FreeGroup.invRev ⋯ }
-- Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
/-- The projection from a trivial fiber bundle to its base is surjective.  -/
IsHomeomorphicTrivialFiberBundle.surjective_proj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B} [Nonempty F],
  IsHomeomorphicTrivialFiberBundle F proj → Function.Surjective proj
-- Mathlib.GroupTheory.ArchimedeanDensely
instLocallyFiniteOrderUnits : {X : Type u_2} → [inst : Preorder X] → [LocallyFiniteOrder X] → [inst_2 : Monoid X] → LocallyFiniteOrder Xˣ
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.ext_iff : ∀ {K : Type u} [inst : DivisionRing K] {S T : Subfield K}, S = T ↔ ∀ (x : K), x ∈ S ↔ x ∈ T
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaPairingExt_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  {x y : (CategoryTheory.yonedaPairing C).obj X}, x = y ↔ ∀ (Y : Cᵒᵖ), x.app Y = y.app Y
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerRight_inv_app : ∀ {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ₗ Gₗ : CategoryTheory.Functor C E} (α : Fₗ ≅ Gₗ)
  (H : CategoryTheory.Functor D E') (x : CategoryTheory.Join C D),
  (CategoryTheory.Join.mapIsoWhiskerRight α H).inv.app x =
    match x with
    | CategoryTheory.Join.left x => (CategoryTheory.Join.inclLeft E E').map (α.inv.app x)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right (H.obj x))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_prodMap : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {M₄ : Type u_5} [inst_10 : TopologicalSpace M₄] [inst_11 : AddCommMonoid M₄]
  [inst_12 : Module R M₄] (f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄), ↑(f₁.prodMap f₂) = (↑f₁).prodMap ↑f₂
-- Mathlib.Analysis.Complex.Hadamard
/-- The function `scale f l u` is `diffContOnCl`.  -/
Complex.HadamardThreeLines.scale_diffContOnCl : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {l u : ℝ},
  l < u →
    DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip l u) →
      DiffContOnCl ℂ (Complex.HadamardThreeLines.scale f l u) (Complex.HadamardThreeLines.verticalStrip 0 1)
-- Mathlib.Algebra.DualNumber
DualNumber.fst_eps : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R], TrivSqZeroExt.fst DualNumber.eps = 0
-- Mathlib.Combinatorics.Additive.Corner.Defs
isCorner_image : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommMonoid G] [inst_1 : AddCommMonoid H] {A : Set (G × G)} {s : Set G}
  {t : Set H} {f : G → H} {x₁ y₁ x₂ y₂ : G},
  IsAddFreimanIso 2 s t f →
    A ⊆ s ×ˢ s →
      x₁ ∈ s →
        y₁ ∈ s → x₂ ∈ s → y₂ ∈ s → (IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.map.eq_1 : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [inst_1 : Monad m] (f : β → γ)
  (it : Std.IterM m β), Std.IterM.map f it = Std.IterM.mapWithPostcondition (fun b => pure (f b)) it
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁),
  CategoryTheory.Epi (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).g
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.closure_le_centralizer_centralizer : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.closure s ≤ Subgroup.centralizer ↑(Subgroup.centralizer s)
-- Init.Data.SInt.Bitwise
Int16.not_not : ∀ {a : Int16}, ~~~~~~a = a
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.nullMeasurable_comp_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite μ] [NeZero ν] {f : α → γ},
  MeasureTheory.NullMeasurable (f ∘ Prod.fst) (μ.prod ν) ↔ MeasureTheory.NullMeasurable f μ
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.IsBase.isBase_insert_sdiff_of_mem_closure`. -/
Matroid.IsBase.isBase_insert_diff_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {e f : α} {B : Set α},
  M.IsBase B → e ∈ M.closure (insert f B \ {e}) → e ∈ insert f B → M.IsBase (insert f B \ {e})
-- Batteries.Classes.Order
Std.instLawfulOrdNat : Std.LawfulOrd ℕ
-- Mathlib.Computability.RegularExpressions
RegularExpression.epsilon : {α : Type u} → RegularExpression α
-- Mathlib.Algebra.Notation.Defs
Subsingleton.eq_one : ∀ {α : Type u} [inst : One α] [Subsingleton α] (a : α), a = 1
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
/-- The natural number `n` that defines the module as a quotient of `Fin n → R` (i.e. `R^n`).  -/
FGModuleRepr.n : {R : Type u} → [inst : Ring R] → FGModuleRepr R → ℕ
-- Mathlib.Data.Finset.Pi
/-- The diagonal of a finset `s : Finset α` as a finset of functions `ι → α`, namely the set of
constant functions valued in `s`.  -/
Finset.piDiag : {α : Type u_1} → Finset α → (ι : Type u_3) → [DecidableEq (ι → α)] → Finset (ι → α)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- Given a linear map `f : M →ₗ[R] A` into an `R`-algebra `A`, which satisfies the condition:
`cond : ∀ m : M, f m * f m = 0`, this is the canonical lift of `f` to a morphism of `R`-algebras
from `ExteriorAlgebra R M` to `A`.
 -/
ExteriorAlgebra.lift : (R : Type u1) →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {A : Type u_1} →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] → { f // ∀ (m : M), f m * f m = 0 } ≃ (ExteriorAlgebra R M →ₐ[R] A)
-- Init.Data.Subtype.Order
Subtype.instIsLinearOrder : ∀ {α : Type u} [inst : LE α] [Std.IsLinearOrder α] {P : α → Prop}, Std.IsLinearOrder (Subtype P)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α}
  {h₁ : a ∈ t.insert k}, (t.insert k).get a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.get a ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective.  -/
Subsemigroup.giMapComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] →
      [inst_1 : Mul N] →
        {f : M →ₙ* N} → Function.Surjective ⇑f → GaloisInsertion (Subsemigroup.map f) (Subsemigroup.comap f)
-- Mathlib.SetTheory.Ordinal.Arithmetic
_private.Mathlib.SetTheory.Ordinal.Arithmetic.0.Ordinal.sub_eq_zero_of_lt : ∀ {a b : Ordinal.{u_4}}, a < b → a - b = 0
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.ofEq.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y), AddActionHom.ofEq h f = { toFun := f.toFun, map_vadd' := ⋯ }
-- Init.Data.Slice.List.Lemmas
ListSlice.size_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.size (Std.Rco.Sliceable.mkSlice xs lo...hi) = min hi (Std.Slice.size xs) - lo
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhds_coe : ∀ {r : ℝ}, nhds ↑r = Filter.map Real.toEReal (nhds r)
-- Mathlib.Analysis.Normed.Ring.Units
NormedRing.inverse_one_sub : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (t : R) (h : ‖t‖ < 1),
  Ring.inverse (1 - t) = ↑(Units.oneSub t h)⁻¹
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.pOpcycles.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ),
  X.pOpcycles f g n = CategoryTheory.Limits.cokernel.π (X.δ f g (n - 1) n ⋯)
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.mkHomFromDouble_f₀_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} {f : X₀ ⟶ X₁} {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (h : i₀ ≠ i₁) {K : HomologicalComplex C c} (φ₀ : X₀ ⟶ K.X i₀) (φ₁ : X₁ ⟶ K.X i₁)
  (comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
  (hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0) {Z : C} (h_1 : K.X i₀ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HomologicalComplex.mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₀) h_1 =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.doubleXIso₀ f hi₀₁).hom
      (CategoryTheory.CategoryStruct.comp φ₀ h_1)
-- Mathlib.Probability.Kernel.RadonNikodym
/-- Auxiliary function used to define `ProbabilityTheory.Kernel.rnDeriv` and
`ProbabilityTheory.Kernel.singularPart`.

This has the properties we want for a Radon-Nikodym derivative only if `κ ≪ ν`. The definition of
`rnDeriv κ η` will be built from `rnDerivAux κ (κ + η)`.  -/
ProbabilityTheory.Kernel.rnDerivAux : {α : Type u_1} →
  {γ : Type u_2} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] →
          ProbabilityTheory.Kernel α γ → ProbabilityTheory.Kernel α γ → α → γ → ℝ
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.copy_toSubsemiring : ∀ {R : Type u} [inst : NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S),
  (S.copy s hs).toSubsemiring = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Data.Set.Defs
/-- The singleton of an element `a` is the set with `a` as a single element.

Note that you should **not** use this definition directly, but instead write `{a}`.  -/
Set.singleton : {α : Type u} → α → Set α
-- Mathlib.Analysis.Normed.Ring.Basic
NormOneClass.nontrivial : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] [inst_1 : One G] [NormOneClass G], Nontrivial G
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.HomologyMapData.natTransApp_right : ∀ {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 G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  [inst_6 : F.PreservesLeftHomologyOf S] [inst_7 : G.PreservesLeftHomologyOf S] [inst_8 : F.PreservesRightHomologyOf S]
  [inst_9 : G.PreservesRightHomologyOf S] (h : S.HomologyData) (τ : F ⟶ G),
  (CategoryTheory.ShortComplex.HomologyMapData.natTransApp h τ).right =
    CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h.right τ
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instAlgebra : (R : Type u_1) →
  (X : Type u_2) →
    [inst : CommSemiring R] → {A : Type u_3} → [inst_1 : CommSemiring A] → [Algebra R A] → Algebra R (FreeAlgebra A X)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.instMulActionProd : (D : Type u_1) →
  (Q : Type u_2) → [inst : Group D] → [inst_1 : Group Q] → (Λ : Type u_3) → [MulAction D Λ] → MulAction (D ≀ᵣ Q) (Λ × Q)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insertIfNew!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k}, Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.insertIfNew! k v t) = true
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonHashSet : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → [Lean.ToJson α] → Lean.ToJson (Std.HashSet α)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
Finset.instFintypeSubtypeMemSubgroupInvMulSubgroup : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : DecidableEq G] → (A : Finset G) → (h : ↑(A * A).card < 3 / 2 * ↑A.card) → Fintype ↥(A.invMulSubgroup h)
-- Mathlib.Order.Filter.FilterProduct
_private.Mathlib.Order.Filter.FilterProduct.0.Filter.Germ.«termβ*» : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.inj.inj : ∀ {origin origin_1 : Lean.Meta.Grind.Origin},
  Lean.Meta.Grind.SplitSource.inj origin = Lean.Meta.Grind.SplitSource.inj origin_1 → origin = origin_1
-- Mathlib.Topology.Compactness.Lindelof
LindelofSpace.elim_nhds_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] [LindelofSpace X] (U : X → Set X),
  (∀ (x : X), U x ∈ nhds x) → ∃ t, t.Countable ∧ ⋃ x ∈ t, U x = Set.univ
-- Init.Data.UInt.Bitwise
UInt8.shiftLeft_xor : ∀ {a b c : UInt8}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Init.Data.Nat.Basic
Nat.pred_lt_of_lt : ∀ {n m : ℕ}, m < n → n.pred < n
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_umod : ∀ {w i : ℕ} {n d : BitVec w},
  (n % d).getLsbD i =
    if d = 0#w then n.getLsbD i else (BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w)).r.getLsbD i
-- Init.Data.SInt.Lemmas
Int64.zero_mul : ∀ {a : Int64}, 0 * a = 0
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.incl_eq_val : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), ⇑N.incl = Subtype.val
-- Init.Data.UInt.Lemmas
USize.ofNatLT_lt_iff_lt : ∀ {a b : ℕ} (ha : a < USize.size) (hb : b < USize.size), USize.ofNatLT a ha < USize.ofNatLT b hb ↔ a < b
-- Mathlib.Algebra.GroupWithZero.Defs
/-- If `α` has no zero divisors, then for elements `a, b : α`, `a * b` equals zero iff so is
`b * a`.  -/
mul_eq_zero_comm : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ b * a = 0
-- Lean.Data.Name
Lean.Name.eqStr : Lean.Name → String → Bool
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.norm : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : SeminormedAddCommGroup β]
  {f : α → β}, MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => ‖f x‖) μ
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_X_pow_char_sub_C_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ} [inst_2 : ExpChar R p] [inst_3 : PerfectRing R p]
  {y : R} {m : ℕ}, ((Polynomial.X ^ p - Polynomial.C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}
-- Mathlib.Order.RelIso.Basic
/-- Transport a `RelIso` across a pair of `RelIso`s, by pre- and post-composition.

This is `Equiv.equivCongr` for `RelIso`.  -/
RelIso.relIsoCongr : {α₁ : Type u_5} →
  {β₁ : Type u_6} →
    {α₂ : Type u_7} →
      {β₂ : Type u_8} →
        {r₁ : α₁ → α₁ → Prop} →
          {s₁ : β₁ → β₁ → Prop} →
            {r₂ : α₂ → α₂ → Prop} → {s₂ : β₂ → β₂ → Prop} → r₁ ≃r r₂ → s₁ ≃r s₂ → r₁ ≃r s₁ ≃ (r₂ ≃r s₂)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of colimits along a natural isomorphism in the shape.  -/
CategoryTheory.Limits.preservesColimit_of_iso_diagram : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K₁ K₂ : CategoryTheory.Functor J C}
  (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.PreservesColimit K₁ F],
  CategoryTheory.Limits.PreservesColimit K₂ F
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.ext : ∀ {R : Type u_1} {M : Type u_2} {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  {Q : QuadraticForm R M} {A : Type u_3} {inst_3 : Ring A} {inst_4 : Algebra R A} {x y : CliffordAlgebra.EvenHom Q A},
  x.bilin = y.bilin → x = y
-- Init.Data.Array.MapIdx
Array.toList_zipIdx : ∀ {α : Type u_1} {xs : Array α} {k : ℕ}, (xs.zipIdx k).toList = xs.toList.zipIdx k
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → (cmp t.minKey! k).isLE = true