mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- The radical of a quadratic form `Q` on `M`.

This is the largest submodule `N` such that `Q` lifts to a quadratic form on `M ⧸ N`; see
`Submodule.le_radical_iff` for this characterization.

See also [elman-karpenko-merkurjev-2008], Chapter II, §7.  -/
QuadraticMap.radical : {R : Type u_1} →
  {M : Type u_2} →
    {P : Type u_4} →
      [inst : AddCommGroup M] →
        [inst_1 : AddCommGroup P] →
          [inst_2 : CommRing R] → [inst_3 : Module R M] → [inst_4 : Module R P] → QuadraticMap R M P → Submodule R M
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.union_ramifiedPlacesOver_unramifiedPlacesOver : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.ramifiedPlacesOver L v ∪ NumberField.InfinitePlace.unramifiedPlacesOver L v =
    NumberField.InfinitePlace.placesOver L v
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {n : ℕ} (xs : List.Vector α n) (f₁ : β → σ₁ → σ₁ × γ)
  {s : σ₁} (f₂ : α → β),
  List.Vector.mapAccumr f₁ (List.Vector.map f₂ xs) s = List.Vector.mapAccumr (fun x s => f₁ (f₂ x) s) xs s
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_snd : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.snd
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = false → t[a]? = none
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Ico_iff : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a₁ b₁ a₂ b₂ : α},
  a₁ < b₁ → (Finset.Ico a₁ b₁ ⊆ Finset.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)
-- Mathlib.Topology.Connected.Basic
/-- If any point of a set is joined to a fixed point by a preconnected subset,
then the original set is preconnected as well.  -/
isPreconnected_of_forall : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α} (x : α),
  (∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t) → IsPreconnected s
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.MapSubtype.orderIso_symm_apply : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (sH' : { H' // H' ≤ H }),
  (AddSubgroup.MapSubtype.orderIso H).symm sH' = (↑sH').addSubgroupOf H
-- Mathlib.Order.Sublattice
Sublattice.comap_equiv_eq_map_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : β ≃o α) (L : Sublattice α),
  Sublattice.comap { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L =
    Sublattice.map { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ } L
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.div_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  MonovaryOn f g₁ s → AntivaryOn f g₂ s → MonovaryOn f (g₁ / g₂) s
-- Std.Sat.AIG.LawfulOperator
/-- A function `f` that takes some `aig : AIG α` and an argument of type `β aig` is called a lawful
AIG operator if it only extends the `AIG` but never modifies already existing nodes.

This guarantees that applying such a function will not change the semantics of any existing parts
of the circuit, allowing us to perform local reasoning on the AIG.
 -/
Std.Sat.AIG.LawfulOperator : (α : Type) →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (β : Std.Sat.AIG α → Type) → ((aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α) → Prop
-- Batteries.Data.Array.Match
Array.PrefixTable.mk.inj : ∀ {α : Type u_1} {toArray : Array (α × ℕ)} {valid : ∀ {i : ℕ} (h : i < toArray.size), toArray[i].2 ≤ i}
  {toArray_1 : Array (α × ℕ)} {valid_1 : ∀ {i : ℕ} (h : i < toArray_1.size), toArray_1[i].2 ≤ i},
  { toArray := toArray, valid := valid } = { toArray := toArray_1, valid := valid_1 } → toArray = toArray_1
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_iff_tendsto'`. -/
Asymptotics.isLittleO_of_tendsto' : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜},
  (∀ᶠ (x : α) in l, g x = 0 → f x = 0) → Filter.Tendsto (fun x => f x / g x) l (nhds 0) → f =o[l] g
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Given a continuous linear map `f` from continuous multilinear maps on `n` variables to
continuous linear maps on `E 0`, construct the corresponding continuous multilinear map on `n+1`
variables obtained by concatenating the variables, given by `m ↦ f (init m) (m (last n))`.  -/
ContinuousMultilinearMap.uncurryRight : {𝕜 : Type u} →
  {n : ℕ} →
    {Ei : Fin n.succ → Type wEi} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  (Ei i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G) → ContinuousMultilinearMap 𝕜 Ei G
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  HasMFDerivAt[s] f x f' → s ∈ nhdsWithin x t → HasMFDerivAt[t] f x f'
-- Init.Data.Fin.Basic
/-- Extracts the underlying `Nat` value.

This function is a synonym for `Fin.val`, which is the simp normal form. `Fin.val` is also a
coercion, so values of type `Fin n` are automatically converted to `Nat`s as needed.
 -/
Fin.toNat : {n : ℕ} → Fin n → ℕ
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt
CategoryTheory.IsGrothendieckAbelian.hasExt : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.HasExt C
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.updateTypes : Lean.Expr →
  Lean.Expr → Array Lean.Meta.GeneralizeTelescope.Entry → ℕ → Lean.MetaM (Array Lean.Meta.GeneralizeTelescope.Entry)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_roo : ∀ {m n i : ℕ}, (m<...n).toArray[i]! = if i < n - (m + 1) then m + 1 + i else 0
-- Std.Data.DTreeMap.Internal.Def
/-- The "delta" parameter of the size-bounded tree. Controls how imbalanced the tree can be.  -/
Std.DTreeMap.Internal.delta : ℕ
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_negSucc : ∀ {a : ℤ} {b : ℕ}, a ∣ Int.negSucc b ↔ a ∣ ↑(b + 1)
-- Mathlib.FieldTheory.AbelRuffini
gal_X_isSolvable : ∀ {F : Type u_1} [inst : Field F], Group.IsSolvable Polynomial.X.Gal
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.congr_simp : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {f f_1 : ι → α → β} (e_f : f = f_1) {μ μ_1 : MeasureTheory.Measure α} (e_μ : μ = μ_1)
  (hf : ∀ (i : ι), AEMeasurable (f i) μ) (p p_1 : α → (ι → β) → Prop),
  p = p_1 → ∀ (a a_1 : ι), a = a_1 → ∀ (a_2 a_3 : α), a_2 = a_3 → aeSeq hf p a a_2 = aeSeq ⋯ p_1 a_1 a_3
-- Mathlib.Order.Category.PartOrdEmb
/-- The underlying partially ordered type.  -/
PartOrdEmb.carrier : PartOrdEmb → Type u_1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_le_rpow_of_exponent_le : ∀ {x : ENNReal} {y z : ℝ}, 1 ≤ x → y ≤ z → x ^ y ≤ x ^ z
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_sup : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S₁ S₂ : Subalgebra R Aᵐᵒᵖ), (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.Functor.preservesHomologyOfExact : ∀ {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] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits F]
  [CategoryTheory.Limits.PreservesFiniteColimits F], F.PreservesHomology
-- Mathlib.Computability.DFA
DFA.evalFrom_split : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) [inst : Fintype σ] {x : List α} {s t : σ},
  Fintype.card σ ≤ x.length →
    M.evalFrom s x = t →
      ∃ q a b c,
        x = a ++ b ++ c ∧
          a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
-- Init.Data.Range.Polymorphic.Iterators
/-- Internal function that constructs an iterator for a closed range `lo...hi`.
This is an internal function.
Use `Rco.iter` instead, which requires
importing `Std.Data.Iterators`.
 -/
Std.Rco.Internal.iter : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Rco α → Std.Iter α
-- Mathlib.Data.Nat.Prime.Basic
Nat.coprime_or_dvd_of_prime : ∀ {p : ℕ}, Nat.Prime p → ∀ (i : ℕ), p.Coprime i ∨ p ∣ i
-- Mathlib.Order.Filter.Prod
Filter.prod_pure : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {b : β}, f ×ˢ pure b = Filter.map (fun a => (a, b)) f
-- Mathlib.Analysis.Convex.Quasiconvex
/-- A function is quasiconcave if all its superlevels are convex.
This means that, for all `r`, `{x ∈ s | r ≤ f x}` is `𝕜`-convex.  -/
QuasiconcaveOn : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {β : Type u_3} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [LE β] → [SMul 𝕜 E] → Set E → (E → β) → Prop
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.mem_of_eqOnSource : ∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H) {e e' : OpenPartialHomeomorph H H},
  e ∈ G → e' ≈ e → e' ∈ G
-- Mathlib.GroupTheory.OreLocalization.Cardinality
AddOreLocalization.cardinalMk_le_lift_cardinalMk_of_addCommute : ∀ {R : Type u} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] (X : Type v)
  [inst_2 : AddAction R X],
  (∀ (s s' : ↥S), AddCommute s s') → Cardinal.mk (AddOreLocalization S X) ≤ Cardinal.lift.{u, v} (Cardinal.mk X)
-- Mathlib.Topology.Inseparable
/-- **Alias** of the forward direction of `specializingMap_iff_closure_singleton_subset`. -/
SpecializingMap.closure_singleton_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  SpecializingMap f → ∀ (x : X), closure {f x} ⊆ f '' closure {x}
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le : ∀ {u v : ℕ → EReal},
  (∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ v n) → LinearGrowth.linearGrowthInf u ≤ LinearGrowth.linearGrowthSup v
-- Std.Time.Format.Modifier
Std.Time.Modifier.w.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.w presentation) = 1 + sizeOf presentation
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Configuration for `MetaM` used to process global simp theorems
 -/
Lean.Meta.simpGlobalConfig : Lean.Meta.ConfigWithKey
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → Std.DTreeMap.Raw.Const.get? (m₁ \ m₂) k = none
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_pow_of_smul_comm' : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (n : ℕ),
  MulOpposite.op x.fst • x.snd = x.fst • x.snd → (x ^ n).snd = n • MulOpposite.op (x.fst ^ n.pred) • x.snd
-- Mathlib.Data.Subtype
Subtype.equiv_iff : ∀ {α : Sort u_1} [inst : HasEquiv α] {p : α → Prop} {s t : Subtype p}, s ≈ t ↔ ↑s ≈ ↑t
-- Init.Data.Array.Bootstrap
Array.toListImpl_eq : ∀ {α : Type u_1} {xs : Array α}, xs.toListImpl = xs.toList
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_eq_toBitVec : ∀ (a : USize) (h : System.Platform.numBits = 64), a.toBitVec64 h = BitVec.cast h a.toBitVec
-- Mathlib.Analysis.Normed.Group.Uniform
Isometry.nnnorm_map_of_map_one : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F},
  Isometry f → f 1 = 1 → ∀ (x : E), ‖f x‖₊ = ‖x‖₊
-- Mathlib.Data.Seq.Defs
/-- Coinductive principle for equality on sequences.
This is a version of `eq_of_bisim` that looks more like an induction principle.  -/
Stream'.Seq.eq_of_bisim' : ∀ {α : Type u} {s₁ s₂ : Stream'.Seq α} (motive : Stream'.Seq α → Stream'.Seq α → Prop),
  motive s₁ s₂ →
    (∀ (s₁ s₂ : Stream'.Seq α),
        motive s₁ s₂ →
          s₁ = Stream'.Seq.nil ∧ s₂ = Stream'.Seq.nil ∨
            ∃ x s₁' s₂', s₁ = Stream'.Seq.cons x s₁' ∧ s₂ = Stream'.Seq.cons x s₂' ∧ motive s₁' s₂') →
      s₁ = s₂
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- An additive submagma of an additive magma inherits an addition.  -/
AddMemClass.add : {M : Type u_1} → {A : Type u_3} → [inst : Add M] → [inst_1 : SetLike A M] → [hA : AddMemClass A M] → (S' : A) → Add ↥S'
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae_ennreal_smul_measure_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {c : ENNReal} {p : α → Prop},
  c ≠ 0 → ∀ {μ : MeasureTheory.Measure α}, (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x
-- Init.Data.UInt.Lemmas
UInt32.toUInt32_toUInt64 : ∀ (n : UInt32), n.toUInt64.toUInt32 = n
-- Mathlib.Algebra.Group.Pi.Basic
Pi.invOneClass.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → InvOneClass (f i)],
  Pi.invOneClass = { toOne := Pi.instOne, toInv := Pi.instInv, inv_one := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β},
  (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.isSimpleModule_weylGroupRootRep_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Nontrivial M],
  IsSimpleModule (MonoidAlgebra R ↥P.weylGroup) P.weylGroupRootRep.asModule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
-- Mathlib.Order.WithBot
WithTop.untop_lt_untop_iff : ∀ {α : Type u_1} [inst : LT α] {x y : WithTop α} (hy : y ≠ ⊤) (hx : x ≠ ⊤), y.untop hy < x.untop hx ↔ y < x
-- Lean.Expr
Lean.Int.mkInstPow : Lean.Expr
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  ‖MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT‖ ≤ max C 0
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.instUniqueOne : Unique (OrderedFinpartition 1)
-- Mathlib.RepresentationTheory.Rep.Basic
Representation.equivOfIso_toFun : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (i : A ≅ B) (a : ↑A),
  (Representation.equivOfIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a
-- Batteries.Recycling.RBTree.Lemmas
/-- The set `{x | cut x = .lt}` is downward-closed.  -/
RBTree.RBNode.IsCut.le_lt_trans : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} [self : RBTree.RBNode.IsCut cmp cut] {x y : α}
  [Std.TransCmp cmp], cmp x y ≠ Ordering.gt → cut x = Ordering.lt → cut y = Ordering.lt
-- Aesop.Rule
Aesop.NormRule : Type
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ) {Z : C}
  (h :
    (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).obj
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((DerivedCategory.homologyFunctorFactorsh C n).hom.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K))
      h =
    CategoryTheory.CategoryStruct.comp
      ((DerivedCategory.homologyFunctor C n).map ((DerivedCategory.quotientCompQhIso C).hom.app K))
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n).hom.app K)
        (CategoryTheory.CategoryStruct.comp
          ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n).inv.app K) h))
-- Mathlib.Computability.Primrec.List
Primrec.optionToList : ∀ {α : Type u_1} [inst : Primcodable α], Primrec Option.toList
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_inter_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (a_1 : a ⟶ b) {a_2 b_1 : Bᵒᵖ} (g : a_2 ⟶ b_1)
  (X : ↑(CategoryTheory.Cat.of (Opposite.unop a_2 ⟶ a))),
  ((CategoryTheory.Bicategory.yoneda.map a_1).naturality g).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop X a_1).hom
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurableSet_ball : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {x : α} {ε : ℝ},
  MeasurableSet (Metric.ball x ε)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
/-- Pull an additive subgroup back to an opposite additive subgroup along `AddOpposite.unop`  -/
AddSubgroup.op : {G : Type u_2} → [inst : AddGroup G] → AddSubgroup G → AddSubgroup Gᵃᵒᵖ
-- Batteries.Data.Char.AsciiCasing
/-- Setoid structure on `Char` using `beqCaseInsensitiveAsciiOnly`
 -/
Char.beqCaseInsensitiveAsciiOnly.isSetoid : Setoid Char
-- Lean.Environment
Lean.Environment.realizingStack : Lean.Environment → List Lean.Name
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- If two normal subgroups `M` and `N` of `G` are the same, their quotient groups are
isomorphic.  -/
QuotientGroup.quotientMulEquivOfEq : {G : Type u} →
  [inst : Group G] → {M N : Subgroup G} → [inst_1 : M.Normal] → [inst_2 : N.Normal] → M = N → G ⧸ M ≃* G ⧸ N
-- Mathlib.Order.Defs.Unbundled
IsStrictTotalOrder.toIsStrictOrder : ∀ {α : Sort u_1} {lt : α → α → Prop} [self : IsStrictTotalOrder α lt], IsStrictOrder α lt
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_le : ∀ {a b : ℝ}, a ≤ b → unitInterval.sigmoid a ≤ unitInterval.sigmoid b
-- Aesop.Frontend.Tactic
_private.Aesop.Frontend.Tactic.0.Aesop.Frontend.elabOptions.unsafe_1 : Lean.Syntax → Lean.Elab.TermElabM Aesop.Options
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher : {ρ : Type} → ρ → String.Slice → Type
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link2.match_5.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.Balanced → Sort u_3)
  (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (szr : ℕ) →
      (k'' : α) →
        (v'' : β k'') →
          (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) →
              Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' →
                motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') hr),
  (match hr' : Std.DTreeMap.Internal.Impl.leaf, hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr hr'
    | Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', hr => h_2 szr k'' v'' l'' r'' hr hr') =
    h_1 hr ⋯
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instEssentiallySmallHasCardinalLTWithTerminal : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular],
  CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1}
    (CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminal κ)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq : ∀ (x : ℝ), Real.cos x ≠ -1 → Real.cos x = (1 - Real.tan (x / 2) ^ 2) / (1 + Real.tan (x / 2) ^ 2)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.toMulEquiv_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), f.toMulEquiv = ↑f
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.singleton_eq_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {p : α}, {p} = ∅.insert p
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs.injEq : ∀ (c c_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs c = Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs c_1) = (c = c_1)
-- Mathlib.Testing.Plausible.Sampleable
Plausible.Rat.sampleableExt : Plausible.SampleableExt ℚ
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_sq_re_conj_add : ∀ {K : Type u_1} [inst : RCLike K] (x : K), ‖(starRingEnd K) x + x‖ ^ 2 = RCLike.re ((starRingEnd K) x + x) ^ 2
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Localization.instCommMonoidWithZero : {M : Type u_1} → [inst : CommMonoidWithZero M] → {S : Submonoid M} → CommMonoidWithZero (Localization S)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.norm : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {l : Filter α} {f : α → E},
  MeasureTheory.IntegrableAtFilter f l μ → MeasureTheory.IntegrableAtFilter (fun x => ‖f x‖) l μ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RciSliceData.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Rci α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β) (range_1 : Std.Rci α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Complete matches of unsafe rules.  -/
Aesop.ForwardRuleMatches.unsafeMatches : Aesop.ForwardRuleMatches → Lean.PHashSet Aesop.ForwardRuleMatch
-- Mathlib.Data.Set.Image
Set.image_preimage_eq_of_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, s ⊆ Set.range f → f '' f ⁻¹' s = s
-- Mathlib.MeasureTheory.Measure.Doubling
/-- A doubling constant for a uniformly locally doubling measure.

See also `IsUnifLocDoublingMeasure.scalingConstantOf`.  -/
IsUnifLocDoublingMeasure.doublingConstant : {α : Type u_1} →
  [inst : PseudoMetricSpace α] →
    [inst_1 : MeasurableSpace α] → (μ : MeasureTheory.Measure α) → [IsUnifLocDoublingMeasure μ] → NNReal
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k fallback : α},
  t.WF → (Std.DTreeMap.Raw.map f t).getKeyD k fallback = t.getKeyD k fallback
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Function index of caller  -/
Lean.Elab.WF.GuessLex.RecCallWithContext.caller : Lean.Elab.WF.GuessLex.RecCallWithContext → ℕ