mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.factorPowSucc_comp_fontaineThetaModPPow : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ),
  (Ideal.Quotient.factorPowSucc (Ideal.span {↑p}) (n + 1)).comp (WittVector.fontaineThetaModPPow R p (n + 1)) =
    WittVector.fontaineThetaModPPow R p n
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_mul_of_invertible : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [Invertible A], A⁻¹ * A = 1
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
/-- The Jordan decomposition of `μ.toSignedMeasure - ν.toSignedMeasure` is `(μ - ν, ν - μ)`.  -/
MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν],
  (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition = μ.jordanDecompositionOfToSignedMeasureSub ν
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- Notation for the identity prefunctor on a reflexive quiver.  -/
CategoryTheory.ReflPrefunctor.«term𝟭rq» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `MonoidHomClass.isometry_iff_norm`. -/
MonoidHomClass.isometry_of_norm : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕), (∀ (x : E), ‖f x‖ = ‖x‖) → Isometry ⇑f
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.congr : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_2, u, u} k G}
  {B : Rep.{u_2, u, u} k H} {f₁ f₂ : G →* H} (h : f₁ = f₂) {φ : A ⟶ Rep.res f₁ B} {T : Type u_1}
  (F : (f : G →* H) → (A ⟶ Rep.res f B) → T), F f₁ φ = F f₂ (h ▸ φ)
-- Init.Data.Int.Order
Int.max_eq_left_iff : ∀ {a b : ℤ}, max a b = a ↔ b ≤ a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- A homotopy between two morphisms of short complexes `S₁ ⟶ S₂` consists of various
maps and conditions which will be sufficient to show that they induce the same morphism
in homology.  -/
CategoryTheory.ShortComplex.Homotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → (S₁ ⟶ S₂) → (S₁ ⟶ S₂) → Type v_1
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryBiproductTriangle_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).obj₁ = X₁
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.Entry.mk.inj : ∀ {name : Aesop.RuleName} {pattern : Aesop.RulePattern} {name_1 : Aesop.RuleName} {pattern_1 : Aesop.RulePattern},
  { name := name, pattern := pattern } = { name := name_1, pattern := pattern_1 } → name = name_1 ∧ pattern = pattern_1
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.holder_coe : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal)
  [hpqr : p.HolderTriple q r] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ} (hBK : ∀ (i : ι), ‖B i‖ ≤ K)
  (e : ↥(lp E p)) (f : ↥(lp F q)) (i : ι), ↑(lp.holder r B hBK e f) i = ((B i) (↑e i)) (↑f i)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.piLIE_symm_apply_apply : ∀ (𝕜 : Type u) (E : Type wE) {ι : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : Fintype ι] {ι' : Type u_1} [inst_4 : Fintype ι'] {F : ι' → Type u_2}
  [inst_5 : (i' : ι') → SeminormedAddCommGroup (F i')] [inst_6 : (i' : ι') → NormedSpace 𝕜 (F i')]
  (a : E [⋀^ι]→L[𝕜] ((i : ι') → F i)) (i : ι') (a_1 : (i : ι) → (fun x => E) i),
  ((ContinuousAlternatingMap.piLIE 𝕜 E).symm a i) a_1 = a a_1 i
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousWithinAt.cpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ℂ} {s : Set α} {a : α},
  ContinuousWithinAt f s a →
    ContinuousWithinAt g s a → f a ∈ Complex.slitPlane → ContinuousWithinAt (fun x => f x ^ g x) s a
-- Mathlib.NumberTheory.Dioph
Poly.instInhabited : (α : Type u_3) → Inhabited (Poly α)
-- Mathlib.Topology.Algebra.Group.Extension
/-- A predicate stating that `φ` and `ψ` define a short exact sequence of topological groups.  -/
TopologicalAddGroup.IsSES : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : AddGroup A] →
        [inst_1 : AddGroup B] →
          [inst_2 : AddGroup C] →
            [TopologicalSpace A] → [TopologicalSpace B] → [TopologicalSpace C] → (A →+ B) → (B →+ C) → Prop
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonDiagnosticWith : {α : Type} → [Lean.ToJson α] → Lean.ToJson (Lean.Lsp.DiagnosticWith α)
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B)
  (x : f.ValueGroup₀),
  x = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), x = ↑(MonoidWithZeroHom.valueGroup.mk f r s hr hs)
-- Mathlib.Data.Finset.Card
Finset.card_ne_zero_of_mem : ∀ {α : Type u_1} {s : Finset α} {a : α}, a ∈ s → s.card ≠ 0
-- Init.Data.List.Attach
List.reverse_wfParam : ∀ {α : Type u_1} {xs : List α}, (wfParam xs).reverse = xs.attach.unattach.reverse
-- Mathlib.Topology.Algebra.Ring.Real
ENNReal.nhds_coe_coe : ∀ {r p : NNReal}, nhds (↑r, ↑p) = Filter.map (fun p => (↑p.1, ↑p.2)) (nhds (r, p))
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_neg : ∀ {K : Type u} [inst : CommRing K] (p : FractionRing (Polynomial K)),
  { toFractionRing := -p } = -{ toFractionRing := p }
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.mul_le_nndist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (x y : α), K⁻¹ * nndist x y ≤ nndist (f x) (f y)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.smul_single : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {S : Type u_3} [inst_1 : SMulZeroClass S k] (s : S) (a : G)
  (b : k), s • SkewMonoidAlgebra.single a b = SkewMonoidAlgebra.single a (s • b)
-- Batteries.Data.List.Perm
List.Perm.inter_right : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] (t₁ : List α), l₁.Perm l₂ → (l₁ ∩ t₁).Perm (l₂ ∩ t₁)
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The relation 'in the same orbit'.  -/
MulAction.orbitRel : (G : Type u_1) → (α : Type u_2) → [inst : Group G] → [MulAction G α] → Setoid α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] [inst_1 : Inhabited γ] {f : α → β → Option γ} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl k =
    ((Std.DTreeMap.Internal.Impl.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.HasDimensionLT.mk : ∀ {X : SSet} {d : ℕ}, (∀ (n : ℕ), d ≤ n → X.degenerate n = ⊤) → X.HasDimensionLT d
-- Mathlib.Algebra.Exact.Basic
LinearMap.exact_subtype_mkQ : ∀ {R : Type u_8} {N : Type u_10} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] (Q : Submodule R N),
  Function.Exact ⇑Q.subtype ⇑Q.mkQ
-- Mathlib.Algebra.Group.Action.Defs
IsCentralVAdd.unop_vadd_eq_vadd : ∀ {M : Type u_9} {α : Type u_10} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] (m : Mᵃᵒᵖ) (a : α),
  AddOpposite.unop m +ᵥ a = m +ᵥ a
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- Restrict the support of a multivariate power series to a finite set of monomials and
obtain a multivariate polynomial.  -/
MvPowerSeries.truncFinset : {σ : Type u_1} → (R : Type u_4) → [inst : CommSemiring R] → Finset (σ →₀ ℕ) → MvPowerSeries σ R →ₗ[R] MvPolynomial σ R
-- Mathlib.Topology.Closure
closure_eq_iff_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, closure s = s ↔ IsClosed s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse.map_one : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, CliffordAlgebra.reverse 1 = 1
-- Mathlib.Analysis.Complex.Hadamard
/-- If `f` is bounded on the unit vertical strip, then `f` is bounded by `sSupNormIm` there.  -/
Complex.HadamardThreeLines.norm_le_sSupNormIm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E),
  ∀ z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1,
    BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
      ‖f z‖ ≤ Complex.HadamardThreeLines.sSupNormIm f z.re
-- Mathlib.GroupTheory.Commutator.Finite
/-- The commutator of a finite direct product is contained in the direct product of the commutators.
 -/
Subgroup.commutator_pi_pi_of_finite : ∀ {η : Type u_2} [Finite η] {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] (H K : (i : η) → Subgroup (Gs i)),
  ⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ = Subgroup.pi Set.univ fun i => ⁅H i, K i⁆
-- Init.Data.Range.Polymorphic.Basic
/-- Returns the number of elements starting from `lo` that satisfy the given upper bound.  -/
Std.Rxc.HasSize.size : {α : Type u} → [self : Std.Rxc.HasSize α] → α → α → ℕ
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSMul : {β : Type u_2} → {α : Type u_1} → [SMul β α] → SMul β (Colex α)
-- Mathlib.Algebra.Lie.InvariantForm
/-- A bilinear form on a Lie module `M` of a Lie algebra `L` is *invariant* if
for all `x : L` and `y z : M` the condition `Φ ⁅x, y⁆ z = -Φ y ⁅x, z⁆` holds.
 -/
LinearMap.BilinForm.lieInvariant : {R : Type u_1} →
  (L : Type u_2) →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [LieRingModule L M] → LinearMap.BilinForm R M → Prop
-- Std.Data.String.ToInt
Int.repr_injective : ∀ {a b : ℤ}, a.repr = b.repr → a = b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_filterMap_iff : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)},
  t.WF → ((Std.DTreeMap.Raw.filterMap f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = none)
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.hasSum_eval : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] {α : Type u_5}
  {p : α → E [⋀^ι]→L[𝕜] F} {q : E [⋀^ι]→L[𝕜] F}, HasSum p q → ∀ (m : ι → E), HasSum (fun a => (p a) m) (q m)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_eq_one_iff : ∀ {V : Type u} {G : SimpleGraph V}, G.chromaticNumber = 1 ↔ G = ⊥ ∧ Nonempty V
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.comp_f₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃),
  (CategoryTheory.CategoryStruct.comp f g).f₃ = CategoryTheory.CategoryStruct.comp f.f₃ g.f₃
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology LightProfinite) (Type u)).Faithful
-- Lean.Elab.Import
/-- Elaborates the given header syntax into an environment.

If `mainModule` is not given, `Environment.setMainModule` should be called manually. This is a
backwards compatibility measure not compatible with the module system.
 -/
Lean.Elab.processHeader : Lean.Elab.HeaderSyntax →
  Lean.Options →
    Lean.MessageLog →
      Lean.Parser.InputContext →
        optParam UInt32 0 →
          optParam (Array Lean.Plugin) #[] →
            optParam Bool false → optParam Lean.Name Lean.Name.anonymous → IO (Lean.Environment × Lean.MessageLog)
-- Lean.KeyedDeclsAttribute
/-- Convert `Syntax` into a `Key`, the default implementation expects an identifier.  -/
Lean.KeyedDeclsAttribute.Def.evalKey : {γ : Type} → Lean.KeyedDeclsAttribute.Def γ → Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key
-- Init.Data.Order.Ord
Array.instLawfulBEqCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [inst : BEq α] [Std.LawfulBEqCmp cmp], Std.LawfulBEqCmp (Array.compareLex cmp)
-- Mathlib.GroupTheory.Coset.Card
QuotientGroup.card_quotient_rightRel : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) [inst_1 : Fintype (α ⧸ s)],
  Fintype.card (Quotient (QuotientGroup.rightRel s)) = Fintype.card (α ⧸ s)
-- Mathlib.Algebra.Group.Defs
left_inv_eq_right_inv : ∀ {M : Type u_2} [inst : Monoid M] {a b c : M}, b * a = 1 → a * c = 1 → b = c
-- Mathlib.Analysis.Normed.Module.Basic
PUnit.normedAlgebra : (𝕜 : Type u_1) → [inst : NormedField 𝕜] → NormedAlgebra 𝕜 PUnit.{u_6 + 1}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Convert a `BinaryBicone` into a `Bicone` over a pair.  -/
CategoryTheory.Limits.BinaryBicone.toBiconeFunctor : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        CategoryTheory.Functor (CategoryTheory.Limits.BinaryBicone X Y)
          (CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y))
-- Init.Data.Option.Lemmas
Option.isNone_join : ∀ {α : Type u_1} {x : Option (Option α)}, x.join.isNone = Option.all Option.isNone x
-- Mathlib.LinearAlgebra.Complex.Module
Complex.isSelfAdjoint_I_smul_iff_mem_skewAdjoint : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [StarModule ℂ A] {a : A},
  IsSelfAdjoint (Complex.I • a) ↔ a ∈ skewAdjoint A
-- Mathlib.GroupTheory.Torsion
/-- For prime `p`, `g` lies in the additive `p`-primary component iff its additive
order is a power of `p`.  -/
AddCommMonoid.mem_primaryComponent_iff_addOrderOf : ∀ {G : Type u_1} [inst : AddCommMonoid G] {p : ℕ} [Fact (Nat.Prime p)] {g : G},
  g ∈ AddCommMonoid.primaryComponent G p ↔ ∃ n, addOrderOf g = p ^ n
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α), MeasureTheory.Measure.singularPart 0 ν = 0
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.exists_edist_lt_of_hausdorffEDist_lt`.

---

If the Hausdorff distance is `< r`, then any point in one of the sets has
a corresponding point at distance `< r` in the other set.  -/
EMetric.exists_edist_lt_of_hausdorffEdist_lt : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α} {r : ENNReal},
  x ∈ s → Metric.hausdorffEDist s t < r → ∃ y ∈ t, edist x y < r
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.nonsing_inv_mul_cancel_right : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) (B : Matrix m n α), IsUnit A.det → B * A⁻¹ * A = B
-- Mathlib.Data.Seq.Computation
Computation.liftRel_mem_cases : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β},
  (∀ a ∈ ca, Computation.LiftRel R ca cb) → (∀ b ∈ cb, Computation.LiftRel R ca cb) → Computation.LiftRel R ca cb
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.instFullSubterminalsSubterminalInclusion : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.subterminalInclusion C).Full
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.finite_of_finite : ∀ {α : Type u_1} {M : Matroid α} {B B' : Set α}, M.IsBase B → B.Finite → M.IsBase B' → B'.Finite
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The morphism `K.truncLE e ⟶ L.truncLE e` induced by a morphism `K ⟶ L`.  -/
HomologicalComplex.truncLEMap : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              {K L : HomologicalComplex C c'} →
                (K ⟶ L) →
                  (e : c.Embedding c') →
                    [inst_2 : e.IsTruncLE] →
                      [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                        [inst_4 : ∀ (i' : ι'), L.HasHomology i'] →
                          [inst_5 : CategoryTheory.Limits.HasZeroObject C] → K.truncLE e ⟶ L.truncLE e
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_inter_eq_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (∀ a ∈ m₁, a ∈ m₂) → (m₁ ∩ m₂).size = m₁.size
-- Mathlib.Tactic.NormNum.NatFib
Mathlib.Meta.NormNum.isFibAux_two_mul_add_one : ∀ {n a b n' a' b' : ℕ},
  Mathlib.Meta.NormNum.IsFibAux n a b →
    2 * n + 1 = n' → a * a + b * b = a' → b * (2 * a + b) = b' → Mathlib.Meta.NormNum.IsFibAux n' a' b'
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.lipschitzOnWith_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] [inst_1 : PseudoEMetricSpace β]
  {f : γ → UniformFun α β} {K : NNReal} {s : Set γ},
  LipschitzOnWith K f s ↔ ∀ (c : α), LipschitzOnWith K (fun x => UniformFun.toFun (f x) c) s
-- Init.Data.Array.Basic
Array.pop.eq_1 : ∀ {α : Type u} (xs : Array α), xs.pop = { toList := xs.toList.dropLast }
-- Mathlib.Topology.Order.Hom.Basic
/-- The type of continuous monotone maps from `α` to `β`, aka Priestley homomorphisms.  -/
ContinuousOrderHom : (α : Type u_6) →
  (β : Type u_7) → [Preorder α] → [Preorder β] → [TopologicalSpace α] → [TopologicalSpace β] → Type (max u_6 u_7)
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.mass_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β), (μ.prod ν).mass = μ.mass * ν.mass
-- Mathlib.GroupTheory.OrderOfElement
Prod.orderOf : ∀ {α : Type u_4} {β : Type u_5} [inst : Monoid α] [inst_1 : Monoid β] (x : α × β),
  orderOf x = (orderOf x.1).lcm (orderOf x.2)
-- Mathlib.Algebra.Group.Basic
/-- Version of `mul_right_iterate` that is fully applied, for `rw`.  -/
mul_right_iterate_apply : ∀ {M : Type u_4} [inst : Monoid M] {n : ℕ} (a b : M), (fun x => x * a)^[n] b = b * a ^ n
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The proof of the rewrite  -/
Mathlib.Tactic.LibraryRewrite.Rewrite.proof : Mathlib.Tactic.LibraryRewrite.Rewrite → Lean.Expr
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_eq_of_isMaxOn : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {p : AddMonoidAlgebra R A} {a : A},
  a ∈ p.coeff.support → IsMaxOn D (↑p.coeff.support) a → AddMonoidAlgebra.supDegree D p = D a
-- Mathlib.Data.Set.Card
Set.map_eq_of_subset : ∀ {α : Type u_1} {s : Set α} {f : α ↪ α}, ⇑f '' s ⊆ s → autoParam s.Finite Set.map_eq_of_subset._auto_1 → ⇑f '' s = s
-- Mathlib.Data.NNReal.Defs
/-- **Alias** of the reverse direction of `Real.nnabs_pos`. -/
Mathlib.Meta.Positivity.nnabs_pos_of_pos : ∀ {x : ℝ}, x ≠ 0 → 0 < Real.nnabs x
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.mk.inj : ∀ {X : SSet} {dim : ℕ} {simplex : X.obj (Opposite.op { len := dim })} {dim_1 : ℕ}
  {simplex_1 : X.obj (Opposite.op { len := dim_1 })},
  { dim := dim, simplex := simplex } = { dim := dim_1, simplex := simplex_1 } → dim = dim_1 ∧ simplex ≍ simplex_1
-- Mathlib.Topology.FiberBundle.Basic
/-- This structure permits to define a fiber bundle when trivializations are given as local
equivalences but there is not yet a topology on the total space. The total space is hence given a
topology in such a way that there is a fiber bundle structure for which the partial equivalences
are also open partial homeomorphisms and hence local trivializations.  -/
FiberPrebundle : {B : Type u_2} →
  (F : Type u_3) →
    (E : B → Type u_5) →
      [TopologicalSpace B] → [TopologicalSpace F] → [(x : B) → TopologicalSpace (E x)] → Type (max (max u_2 u_3) u_5)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_insert_le_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {he : t.isEmpty = false}, (cmp ((t.insert k v).minKey ⋯) (t.minKey he)).isLE = true
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mem_toSubsemigroup : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : NonUnitalSubsemiring R} {x : R}, x ∈ s.toSubsemigroup ↔ x ∈ s
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.id : ∀ {α : Type u_1}, Filter.TendstoCofinite id
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.isoLimitCone_inv_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.LimitCone F)
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).inv
      (CategoryTheory.Limits.limit.π F j) =
    t.cone.π.app j
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHAddDuration : HAdd Std.Time.PlainDateTime Std.Time.Duration Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.initialMonoClass : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.InitialMonoClass C
-- Mathlib.Algebra.Order.Monoid.Lex
AddMonoidHom.inl_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddMonoid β] [inst_3 : Preorder β],
  Monotone ⇑(AddMonoidHom.inl α β)
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.powerSeriesAlgebra : (Γ : Type u_1) →
  (R : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring Γ] →
        [inst_2 : PartialOrder Γ] →
          [inst_3 : IsStrictOrderedRing Γ] →
            {S : Type u_4} → [inst_4 : CommSemiring S] → [Algebra S (PowerSeries R)] → Algebra S (HahnSeries Γ R)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → Bool} {k : α}, m.WF → k ∈ Std.DHashMap.Raw.filter f m → k ∈ m
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.RelativeMorphism.mk.congr_simp : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (map map_1 : X ⟶ Y) (e_map : map = map_1)
  (comm : CategoryTheory.CategoryStruct.comp A.ι map = CategoryTheory.CategoryStruct.comp φ B.ι),
  { map := map, comm := comm } = { map := map_1, comm := ⋯ }
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsMulApply.mul_apply`. -/
mul_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Mul β}
  {inst_2 : Mul F} [self : IsMulApply F α β] (f g : F) (x : α), (f * g) x = f x * g x
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.mul_left_strictMono : ∀ {A : Type u_2} (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K] {I : FractionalIdeal (nonZeroDivisors A) K}, I ≠ 0 → StrictMono fun x => x * I