mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Bounded
/-- The diameter of a ball of radius `r` is at most `2 r`.  -/
Metric.diam_ball : ∀ {α : Type u} {x : α} [inst : PseudoMetricSpace α] {r : ℝ}, 0 ≤ r → Metric.diam (Metric.ball x r) ≤ 2 * r
-- Mathlib.Order.Category.PartOrdEmb
/-- Given a functor `F : J ⥤ PartOrdEmb` and a colimit cocone `c` for
`F ⋙ forget _`, this is the type `c.pt` on which we define a partial order
which makes it the colimit of `F`.  -/
PartOrdEmb.Limits.CoconePt : {J : Type u} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J PartOrdEmb} →
      {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} →
        CategoryTheory.Limits.IsColimit c → Type u
-- Init.Data.Rat.Lemmas
Rat.divInt_mul_right : ∀ {n d a : ℤ}, a ≠ 0 → Rat.divInt (n * a) (d * a) = Rat.divInt n d
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Y Z : C}
  [inst_2 : CategoryTheory.HasLeftDual Z] (f : Y ⟶ ᘁZ),
  (CategoryTheory.tensorLeftHomEquiv Y (ᘁZ) Z (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) (ε_ (ᘁZ) Z)) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.rightUnitor ᘁZ).inv
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst_2 : MeasurableSpace E] [BorelSpace E],
  ProbabilityTheory.IsAEKolmogorovProcess X P p q M → ∀ (s : T), AEMeasurable (X s) P
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.universally_isZariskiLocalAtSource : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtSource P],
  AlgebraicGeometry.IsZariskiLocalAtSource P.universally
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.toContinuousMap : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f₀ f₁ : C(X, Y)} → f₀.Homotopy f₁ → C(↑unitInterval × X, Y)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Functor.pi.eq_1 : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i)),
  CategoryTheory.Functor.pi F =
    { obj := fun f i => (F i).obj (f i), map := fun {X Y} α i => (F i).map (α i), map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_ofSnowflaking_closedBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  {r : ℝ},
  0 ≤ r →
    ⇑Metric.Snowflaking.ofSnowflaking '' Metric.closedBall x r =
      Metric.closedBall (Metric.Snowflaking.ofSnowflaking x) (r ^ α⁻¹)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isPreconnected_nonempty_finite_subsets : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α},
  IsPreconnected s → IsPreconnected {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ s}
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_inv_right₀`. -/
Monovary.of_inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g : ι → β}, StrongLT 0 g → Monovary f g⁻¹ → Antivary f g
-- Init.Data.String.Basic
/-- Given a slice `s` and a position on `s.copy`, obtain the corresponding position on `s`.  -/
String.Pos.ofCopy : {s : String.Slice} → s.copy.Pos → s.Pos
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∉ t₁ → k ∉ t₁ ∩ t₂
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.instCommuteWith_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [inst_1 : CategoryTheory.Bicategory.HasAbsLeftKanLift f g] {x : B} (h : x ⟶ c),
  CategoryTheory.Bicategory.LanLift.CommuteWith f g h
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Trie to match next  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.PartialMatch.trie : Lean.Meta.RefinedDiscrTree.PartialMatch✝ → Lean.Meta.RefinedDiscrTree.TrieIndex
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.fixingSubgroup_union_to_fixingSubgroup_of_fixingSubgroup.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α},
  SubMulAction.fixingSubgroup_union_to_fixingSubgroup_of_fixingSubgroup =
    { toFun := fun m => ⟨⟨↑m, ⋯⟩, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_eq_index : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] (I : Ideal S),
  Ideal.absNorm I = (Submodule.toAddSubgroup I).index
-- Mathlib.Algebra.Group.Defs
npowRec'.eq_2 : ∀ {M : Type u_2} [inst : One M] [inst_1 : Mul M] (x : M), npowRec' 1 x = x
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- If `a ∈ P^i \ P^(i+1)` and `c ∈ P^i`, then `a * d + e = c` for `e ∈ P^(i+1)`.
`Ideal.mul_add_mem_pow_succ_unique` shows the choice of `d` is unique, up to `P`.
Inspired by [Neukirch], proposition 6.1  -/
Ideal.exists_mul_add_mem_pow_succ : ∀ {S : Type u_1} [inst : CommRing S] {P : Ideal S} [P_prime : P.IsPrime] [IsDedekindDomain S],
  P ≠ ⊥ → ∀ {i : ℕ} (a c : S), a ∈ P ^ i → a ∉ P ^ (i + 1) → c ∈ P ^ i → ∃ d, ∃ e ∈ P ^ (i + 1), a * d + e = c
-- Mathlib.Algebra.Group.Prod
AddEquiv.coe_prodAssoc_symm : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P], ⇑AddEquiv.prodAssoc.symm = ⇑(Equiv.prodAssoc M N P).symm
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_lt_div_of_pos_right : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  a < b → 0 < c → a / c < b / c
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_image : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] {s : Set α} {f : β → M} {g : α → β},
  Function.Injective g → ∀ {x : α}, (g '' s).mulIndicator f (g x) = s.mulIndicator (f ∘ g) x
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_inj : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {x y : β},
  CauSeq.const abv x = CauSeq.const abv y ↔ x = y
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.close : {β : Type} → Std.Http.Server.Connection.Recv✝ β
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.PreservesColimitPair.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G],
  (CategoryTheory.Limits.PreservesColimitPair.iso G X Y).hom = CategoryTheory.Limits.coprodComparison G X Y
-- Mathlib.RingTheory.IsAdjoinRoot
AdjoinRoot.isAdjoinRoot_map_eq_mkₐ : ∀ {R : Type u} [inst : CommRing R] (f : Polynomial R), (AdjoinRoot.isAdjoinRoot f).map = AdjoinRoot.mkₐ f
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.castOrderEmbedding.congr_simp : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : AddLeftMono α]
  [inst_3 : ZeroLEOneClass α] [inst_4 : CharZero α], Nat.castOrderEmbedding = Nat.castOrderEmbedding
-- Mathlib.Algebra.Order.Monoid.Lex
AddMonoidHom.fst_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddMonoid β] [inst_3 : Preorder β],
  Monotone ⇑(AddMonoidHom.fst α β)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- If a permutation is a cycle of `g`, then its support is invariant under `g`.  -/
Equiv.Perm.mem_cycleFactorsFinset_support : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g c : Equiv.Perm α},
  c ∈ g.cycleFactorsFinset → ∀ (a : α), g a ∈ c.support ↔ a ∈ c.support
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.forget_obj : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (X : FDRep k G),
  (TannakaDuality.FiniteGroup.forget k G).obj X = X.V
-- Init.Data.List.Impl
List.eraseIdx.eq_1 : ∀ {α : Type u} (x : ℕ), [].eraseIdx x = []
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.killCopies_bot : ∀ {V : Type u_1} {W : Type u_2} (G : SimpleGraph V), G.killCopies ⊥ = G
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.kerParam_apply : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α}
  {u : Equiv.Perm ↑(Function.fixedPoints ⇑g)} {v : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)} {x : α},
  ((Equiv.Perm.OnCycleFactors.kerParam g) (u, v)) x =
    if hx : g.cycleOf x ∈ g.cycleFactorsFinset then ↑(v ⟨g.cycleOf x, hx⟩) x else (Equiv.Perm.ofSubtype u) x
-- Init.Data.UInt.Lemmas
USize.ofFin_uint16ToFin : ∀ (n : UInt16), USize.ofFin (Fin.castLE UInt16.size_le_usizeSize n.toFin) = n.toUSize
-- Lean.Elab.Term.TermElabM
/-- Helper function for `elabTerm` that tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
an error is found.  -/
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.elabUsingElabFnsAux : Lean.Elab.Term.SavedState →
  Lean.Syntax →
    Option Lean.Expr →
      Bool → List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Term.TermElab) → Lean.Elab.TermElabM Lean.Expr
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.TerminationMeasure.structural : Lean.Elab.TerminationMeasure → Bool
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
mulintEquivOfZPowersEqTop_strictMono : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : CommGroup G] [inst_2 : PartialOrder G] [IsOrderedMonoid G] {g : G}
  (hg : Subgroup.zpowers g = ⊤), 1 < g → StrictMono ⇑(intEquivOfZPowersEqTop g hg)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.instEpiToCycles : ∀ {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) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ), CategoryTheory.Epi (X.toCycles f g fg h n)
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_inter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (m₁ ∩ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∉ m₂
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_nhds_top_iff_nnreal : ∀ {α : Type u_1} {m : α → ENNReal} {f : Filter α},
  Filter.Tendsto m f (nhds ⊤) ↔ ∀ (x : NNReal), ∀ᶠ (a : α) in f, ↑x < m a
-- Mathlib.Tactic.Sat.FromLRAT
/-- Construct the clause expression from the input list. For example `[1, -2]` is translated to
`Clause.cons (Literal.pos 1) (Clause.cons (Literal.neg 2) Clause.nil)`.  -/
Mathlib.Tactic.Sat.buildClause : Array ℤ → Lean.Expr
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The projection from `P` to the quotient by an open normal subgroup.  -/
ProfiniteAddGrp.proj : {P : ProfiniteAddGrp.{u}} → (U : OpenNormalAddSubgroup ↑P.toProfinite.toTop) → P ⟶ P.diagram.obj U
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.withSetOptionValueFnCore.insertOption : Lean.Syntax → Lean.DataValue → Lean.Parser.ParserContextCore → Lean.Parser.ParserContextCore
-- Init.Data.Char.Ordinal
_private.Init.Data.Char.Ordinal.0.Char.succ?.eq_def : ∀ (c : Char),
  c.succ? =
    if h₀ : c.val < 55295 then some { val := c.val + 1, valid := ⋯ }
    else
      if h₁ : c.val = 55295 then some { val := 57344, valid := Char.succ?._proof_2✝ }
      else if h₂ : c.val < 1114111 then some { val := c.val + 1, valid := ⋯ } else none
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.isoOfIso_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Mon C} {P Q : Bimod X Y} (f : P.X ≅ Q.X)
  (f_left_act_hom :
    CategoryTheory.CategoryStruct.comp P.actLeft f.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom) Q.actLeft)
  (f_right_act_hom :
    CategoryTheory.CategoryStruct.comp P.actRight f.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X) Q.actRight),
  (Bimod.isoOfIso f f_left_act_hom f_right_act_hom).hom.hom = f.hom
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.fst_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β], ⇑ContinuousMap.fst = Prod.fst
-- Mathlib.Topology.Separation.Basic
eventually_ne_nhdsWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {a b : X} {s : Set X},
  a ≠ b → ∀ᶠ (x : X) in nhdsWithin a s, x ≠ b
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms an array of mappings into a tree map.  -/
Std.DTreeMap.Raw.ofArray : {α : Type u} →
  {β : α → Type v} →
    Array ((a : α) × β a) →
      (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.ofArray._auto_1) → Std.DTreeMap.Raw α β cmp
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type E₈.

The corresponding Coxeter-Dynkin diagram is:
```
                o
                |
    o --- o --- o --- o --- o --- o --- o
```
 -/
CoxeterMatrix.E₈ : CoxeterMatrix (Fin 8)
-- Mathlib.Probability.Process.Filtration
/-- The canonical filtration on the product space `Π i, X i`, where `piLE i`
consists of measurable sets depending only on coordinates `≤ i`.  -/
MeasureTheory.Filtration.piLE : {ι : Type u_2} →
  [inst : Preorder ι] →
    {X : ι → Type u_4} → [inst_1 : (i : ι) → MeasurableSpace (X i)] → MeasureTheory.Filtration ι MeasurableSpace.pi
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Cancellation of a telescoping sum.  -/
List.sum_range_sub' : ∀ {G : Type u_7} [inst : AddGroup G] (n : ℕ) (f : ℕ → G),
  (List.map (fun k => f k - f (k + 1)) (List.range n)).sum = f 0 - f n
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.mconv.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M),
  μ.mconv ν = MeasureTheory.Measure.map (fun x => x.1 * x.2) (μ.prod ν)
-- Mathlib.Data.List.OfFn
/-- This breaks a list of `m*n` items into `m` groups each containing `n` elements.  -/
List.ofFn_mul : ∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α),
  List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
-- Mathlib.Tactic.ProxyType
/-- The term elaborator `proxy_equiv% α` for a type `α` elaborates to an equivalence `β ≃ α`
for a "proxy type" `β` composed out of basic type constructors `Unit`, `PLift`, `Sigma`,
`Empty`, and `Sum`.

This only works for inductive types `α` that are neither recursive nor have indices.
If `α` is an inductive type with name `I`, then as a side effect this elaborator defines
`I.proxyType` and `I.proxyTypeEquiv`.

The elaborator makes use of the expected type, so `(proxy_equiv% _ : _ ≃ α)` works.

For example, given this inductive type
```
inductive foo (n : Nat) (α : Type)
  | a
  | b : Bool → foo n α
  | c (x : Fin n) : Fin x → foo n α
  | d : Bool → α → foo n α
```
the proxy type it generates is `Unit ⊕ Bool ⊕ (x : Fin n) × Fin x ⊕ (_ : Bool) × α` and
in particular we have that
```
proxy_equiv% (foo n α) : Unit ⊕ Bool ⊕ (x : Fin n) × Fin x ⊕ (_ : Bool) × α ≃ foo n α
```
 -/
Mathlib.ProxyType.proxy_equiv : Lean.ParserDescr
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.map_bijective : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] {f : M →+ N},
  Function.Bijective ⇑f → Function.Bijective ⇑(AddUnits.map f)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.ofHom₂_hom₂ : ∀ {R : Type u_1} [inst : CommRing R] {M N P : ModuleCat R} (f : M ⟶ ModuleCat.of R (N ⟶ P)),
  ModuleCat.ofHom₂ (ModuleCat.Hom.hom₂ f) = f
-- Mathlib.Algebra.DualNumber
DualNumber.snd_eps : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R], TrivSqZeroExt.snd DualNumber.eps = 1
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derived'_counit : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂) [inst_4 : L₁.IsLocalization W₁]
  [inst_5 : L₂.IsLocalization W₂] {G' : CategoryTheory.Functor D₁ D₂} {F' : CategoryTheory.Functor D₂ D₁}
  (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [inst_6 : G'.IsLeftDerivedFunctor α W₁]
  [inst_7 : F'.IsRightDerivedFunctor β W₂] (η : CategoryTheory.Functor.id D₁ ⟶ G'.comp F')
  (ε : F'.comp G' ⟶ CategoryTheory.Functor.id D₂)
  (hη :
    autoParam
      (∀ (X₁ : C₁),
        CategoryTheory.CategoryStruct.comp (η.app (L₁.obj X₁)) (F'.map (α.app X₁)) =
          CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (β.app (G.obj X₁)))
      CategoryTheory.Adjunction.derived'._auto_1)
  (hε :
    autoParam
      (∀ (X₂ : C₂),
        CategoryTheory.CategoryStruct.comp (G'.map (β.app X₂)) (ε.app (L₂.obj X₂)) =
          CategoryTheory.CategoryStruct.comp (α.app (F.obj X₂)) (L₂.map (adj.counit.app X₂)))
      CategoryTheory.Adjunction.derived'._auto_3),
  (adj.derived' W₁ W₂ α β η ε hη hε).counit = ε
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.pageFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  (c : ℤ → ComplexShape κ) (r₀ r : ℤ) (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.pageFunctor._auto_1)
  {X Y : CategoryTheory.SpectralSequence C c r₀} (f : X ⟶ Y),
  (CategoryTheory.SpectralSequence.pageFunctor C c r₀ r hr).map f = f.hom r ⋯
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- The mates equivalence commutes with composition of a square of squares. These results form the
basis for an isomorphism of double categories to be proven later.
 -/
CategoryTheory.Bicategory.mateEquiv_square : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f x y z : B} {g₁ : a ⟶ d} {h₁ : b ⟶ e} {k₁ : c ⟶ f}
  {g₂ : d ⟶ x} {h₂ : e ⟶ y} {k₂ : f ⟶ z} {l₁ : a ⟶ b} {r₁ : b ⟶ a} {l₂ : b ⟶ c} {r₂ : c ⟶ b} {l₃ : d ⟶ e} {r₃ : e ⟶ d}
  {l₄ : e ⟶ f} {r₄ : f ⟶ e} {l₅ : x ⟶ y} {r₅ : y ⟶ x} {l₆ : y ⟶ z} {r₆ : z ⟶ y}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃) (adj₄ : CategoryTheory.Bicategory.Adjunction l₄ r₄)
  (adj₅ : CategoryTheory.Bicategory.Adjunction l₅ r₅) (adj₆ : CategoryTheory.Bicategory.Adjunction l₆ r₆)
  (α : CategoryTheory.CategoryStruct.comp g₁ l₃ ⟶ CategoryTheory.CategoryStruct.comp l₁ h₁)
  (β : CategoryTheory.CategoryStruct.comp h₁ l₄ ⟶ CategoryTheory.CategoryStruct.comp l₂ k₁)
  (γ : CategoryTheory.CategoryStruct.comp g₂ l₅ ⟶ CategoryTheory.CategoryStruct.comp l₃ h₂)
  (δ : CategoryTheory.CategoryStruct.comp h₂ l₆ ⟶ CategoryTheory.CategoryStruct.comp l₄ k₂),
  (CategoryTheory.Bicategory.mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆))
      (CategoryTheory.Bicategory.leftAdjointSquare.comp α β γ δ) =
    CategoryTheory.Bicategory.rightAdjointSquare.comp ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₃) α)
      ((CategoryTheory.Bicategory.mateEquiv adj₂ adj₄) β) ((CategoryTheory.Bicategory.mateEquiv adj₃ adj₅) γ)
      ((CategoryTheory.Bicategory.mateEquiv adj₄ adj₆) δ)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.mapArrowHom.congr_simp : ∀ {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] {F' G' : HomologicalComplex C c} (φ' : F' ⟶ G')
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ'] (H : ∀ (j : ι), ∃ i, c.Rel i j)
  (α α_1 : CategoryTheory.Arrow.mk φ ⟶ CategoryTheory.Arrow.mk φ'),
  α = α_1 →
    HomologicalComplex.homotopyCofiber.mapArrowHom φ φ' H α = HomologicalComplex.homotopyCofiber.mapArrowHom φ φ' H α_1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.curriedAssociatorNatIso_inv_app_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X X_1 X_2 : C),
  (((CategoryTheory.MonoidalCategory.curriedAssociatorNatIso C).inv.app X).app X_1).app X_2 =
    (CategoryTheory.MonoidalCategoryStruct.associator X X_1 X_2).inv
-- Mathlib.Order.RelIso.Basic
RelEmbedding.coe_toEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : r ↪r s}, ⇑f.toEmbedding = ⇑f
-- Lean.Message
/-- The message kind (i.e., the top-level tag).  -/
Lean.SerialMessage.kind : Lean.SerialMessage → Lean.Name
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_diseq_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.Computability.RecursiveIn
/-- If a function is recursive in a constant partial function, then it is partial recursive.  -/
RecursiveIn.partrec_of_const : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ} {s : Part ℕ},
  RecursiveIn {fun x => s} f → Partrec f
-- Mathlib.LinearAlgebra.Dimension.Finite
finrank_eq_zero_of_not_exists_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  (¬∃ s, Nonempty (Module.Basis (↑↑s) R M)) → Module.finrank R M = 0
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂],
  Module.finrank K V = Module.finrank K V₂ → ∀ {f : V →ₗ[K] V₂}, f.ker = ⊥ ↔ f.range = ⊤
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.toMonObj : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} →
      {X : C} → [self : CategoryTheory.GrpObj X] → CategoryTheory.MonObj X
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.isAlphanumAscii : UInt8 → Bool
-- Mathlib.Data.Finsupp.Defs
Finsupp.notMem_support_iff : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f : α →₀ M} {a : α}, a ∉ f.support ↔ f a = 0
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Cell.getEntry?.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → (Unit → motive none) → ((p : (a : α) × β a) → motive (some p)) → motive x
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.absolutelyContinuous_of_eq : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ = ν → μ.AbsolutelyContinuous ν
-- Std.Data.String.ToInt
String.Slice.isSome_toInt? : ∀ {s : String.Slice}, s.toInt?.isSome = s.isInt