mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformationLabel.name.sizeOf_spec : ∀ (name : String), sizeOf (Lean.Lsp.ParameterInformationLabel.name name) = 1 + sizeOf name
-- Mathlib.Algebra.Module.Torsion.Free
smul_ne_zero : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m : M}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], r ≠ 0 → m ≠ 0 → r • m ≠ 0
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.pairingIn_neg_one_neg_four_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) (S : Type u_5)
  (i j : ι) [Finite ι] [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [inst_9 : CommRing S]
  [inst_10 : Algebra S R] [FaithfulSMul S R] [inst_12 : P.IsValuedIn S] [Module.IsTorsionFree R N],
  P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.root j = -2 • P.root i
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.induction_on : ∀ {α : Type u} [inst : Add α] {C : AddMagma.FreeAddSemigroup α → Prop} (x : AddMagma.FreeAddSemigroup α),
  (∀ (x : α), C (AddMagma.FreeAddSemigroup.of x)) → C x
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_singleton_of_not_subset : ∀ {ι : Type u_1} {u : Set ι} [Countable ι] {s : Set ι} (p : ↑unitInterval),
  ¬s ⊆ u → (ProbabilityTheory.setBernoulli u p) {s} = 0
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- If `R` is of characteristic zero, then `ζ` is a root of `cyclotomic n R` if and only if it is a
primitive `n`-th root of unity.  -/
Polynomial.isRoot_cyclotomic_iff_charZero : ∀ {n : ℕ} {R : Type u_2} [inst : CommRing R] [IsDomain R] [CharZero R] {μ : R},
  0 < n → ((Polynomial.cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n)
-- Mathlib.Data.Finset.Dedup
List.toFinset.ext : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α}, (∀ (x : α), x ∈ l ↔ x ∈ l') → l.toFinset = l'.toFinset
-- Qq.Macro
Qq.Impl.ExprBackSubstResult.unquoted.inj : ∀ {e e_1 : Lean.Expr}, Qq.Impl.ExprBackSubstResult.unquoted e = Qq.Impl.ExprBackSubstResult.unquoted e_1 → e = e_1
-- Lean.Elab.Tactic.Try
/-- Elaborate `register_try?_tactic` command  -/
Lean.Elab.Tactic.Try.elabRegisterTryTactic : Lean.Elab.Command.CommandElab
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.InjectionAnyResult.failed : Lean.Meta.Match.InjectionAnyResult✝
-- Init.Data.Nat.Fold
/-- Iterates the application of a function `f` to a starting value `init`, `n` times. At each step, `f`
is applied to the current value and to the next natural number less than `n`, in decreasing order.

Examples:
* `Nat.foldRev 3 f init = (f 0 (by simp) <| f 1 (by simp) <| f 2 (by simp) init)`
* `Nat.foldRev 4 (fun i _ xs => xs.push i) #[] = #[3, 2, 1, 0]`
* `Nat.foldRev 0 (fun i _ xs => xs.push i) #[] = #[]`
 -/
Nat.foldRev : {α : Type u} → (n : ℕ) → ((i : ℕ) → i < n → α → α) → α → α
-- Mathlib.Util.Export
Lean.Export.Entry.defn.sizeOf_spec : ∀ (n : Lean.Name), sizeOf (Lean.Export.Entry.defn n) = 1 + sizeOf n
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.hasBasis_nhds_zero_of_basis : ∀ {𝕜 : 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] {ι' : Type u_5} {p : ι' → Prop} {b : ι' → Set F},
  (nhds 0).HasBasis p b →
    (nhds 0).HasBasis (fun Si => Bornology.IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si => {f | Set.MapsTo (⇑f) Si.1 (b Si.2)}
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Mk₁.map.match_1.eq_1 : ∀ (motive : (x x_1 : Fin 2) → x ≤ x_1 → Sort u_1) (isLt isLt_1 : 0 < 2) (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩)
  (h_1 : (isLt isLt_2 : 0 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_2⟩ x)
  (h_2 : (isLt : 0 < 2) → (isLt_2 : 1 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_2⟩ x)
  (h_3 : (isLt isLt_2 : 1 < 2) → (x : ⟨1, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨1, isLt⟩ ⟨1, isLt_2⟩ x),
  (match ⟨0, isLt⟩, ⟨0, isLt_1⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_2⟩, x => h_1 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨1, isLt_2⟩, x => h_2 isLt isLt_2 x
    | ⟨1, isLt⟩, ⟨1, isLt_2⟩, x => h_3 isLt isLt_2 x) =
    h_1 isLt isLt_1 x
-- Mathlib.Tactic.Sat.FromLRAT
/-- Negation turns OR into AND, so `¬⟦l ∨ c⟧_v ≡ ¬⟦l⟧_v ∧ ¬⟦c⟧_v`.  -/
Sat.Clause.reify_and : ∀ {v : Sat.Valuation} {l : Sat.Literal} {a : Prop} {c : Sat.Clause} {b : Prop},
  Sat.Literal.reify v l a → Sat.Clause.reify v c b → Sat.Clause.reify v (Sat.Clause.cons l c) (a ∧ b)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.comp_map : ∀ {X Y Z : CategoryTheory.ReflQuiv} (f : X ⟶ Y) (g : Y ⟶ Z) {x y : ↑X} (a : x ⟶ y),
  (CategoryTheory.CategoryStruct.comp f g).map a = g.map (f.map a)
-- Aesop.RuleTac.Tactic
Aesop.RuleTac.tacticMImpl : Lean.Name → Aesop.RuleTac
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.tendsto_nhds_infty' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_3} {f : OnePoint X → α} {l : Filter α},
  Filter.Tendsto f (nhds OnePoint.infty) l ↔
    Filter.Tendsto f (pure OnePoint.infty) l ∧ Filter.Tendsto (f ∘ OnePoint.some) (Filter.coclosedCompact X) l
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- This lemma is meant to be used with `nullHomotopicMap'_f_of_not_rel_left`  -/
AlgebraicTopology.DoldKan.cs_down_0_not_rel_left : ∀ (j : ℕ), ¬AlgebraicTopology.DoldKan.c.Rel 0 j
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.zero : {J : Type w} → CategoryTheory.Limits.WalkingParallelFamily J
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `rearrangeComparison e` takes a proof `e` of an equality, inequality, or negation thereof,
and turns it into a proof of a comparison `_ R 0`, where `R ∈ {=, ≤, <}`.
 -/
Mathlib.Tactic.Linarith.rearrangeComparison? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Data.Stream.Defs
/-- A stream `Stream' α` is an infinite sequence of elements of `α`.  -/
Stream' : Type u → Type u
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) {Z : C} (h : s.N (Opposite.unop A.fst).len ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (s.πSummand A) h) = h
-- Lean.Parser.Do
Lean.Parser.Term.doHave.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Basic
zero_add_eq_id : ∀ {M : Type u_4} [inst : AddZeroClass M], (fun x => 0 + x) = id
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.brecOn.go : {α : Type u} →
  {motive_1 : Lean.Widget.TaggedText α → Sort u_1} →
    {motive_2 : Array (Lean.Widget.TaggedText α) → Sort u_1} →
      {motive_3 : List (Lean.Widget.TaggedText α) → Sort u_1} →
        (t : Lean.Widget.TaggedText α) →
          ((t : Lean.Widget.TaggedText α) → t.below → motive_1 t) →
            ((t : Array (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_1 t → motive_2 t) →
              ((t : List (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_2 t → motive_3 t) →
                motive_1 t ×' t.below
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.of_forall_contains_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {t₁ t₂ : Std.TreeMap.Raw α Unit cmp},
  t₁.WF → t₂.WF → (∀ (k : α), t₁.contains k = t₂.contains k) → t₁.Equiv t₂
-- Mathlib.Data.Nat.Find
Nat.findGreatest_of_ne_zero : ∀ {m : ℕ} {P : ℕ → Prop} [inst : DecidablePred P] {n : ℕ}, Nat.findGreatest P n = m → m ≠ 0 → P m
-- Mathlib.Combinatorics.Graph.Basic
Graph.banana_isNonloopAt : ∀ {α : Type u_1} {β : Type u_2} {x u v : α} {e : β} {edgeSet : Set β},
  (Graph.banana u v edgeSet).IsNonloopAt e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v
-- Mathlib.CategoryTheory.Yoneda
/-- Version of the Coyoneda lemma where the presheaf is fixed but the argument varies.  -/
CategoryTheory.coyonedaCompYonedaObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor C (Type v₁)) →
      CategoryTheory.coyoneda.rightOp.comp (CategoryTheory.yoneda.obj P) ≅ P.comp CategoryTheory.uliftFunctor.{u₁, v₁}
-- Mathlib.Order.Filter.Ker
Filter.ker_iInf : ∀ {ι : Sort u_1} {α : Type u_2} (f : ι → Filter α), (⨅ i, f i).ker = ⋂ i, (f i).ker
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- `C_c(α, β)` is the type of continuous functions `α → β` with compact support from a topological
space to a topological space with a zero element.

When possible, instead of parametrizing results over `f : C_c(α, β)`,
you should parametrize over `{F : Type*} [CompactlySupportedContinuousMapClass F α β] (f : F)`.

When you extend this structure, make sure to extend `CompactlySupportedContinuousMapClass`.  -/
CompactlySupportedContinuousMap : (α : Type u_5) → (β : Type u_6) → [TopologicalSpace α] → [Zero β] → [TopologicalSpace β] → Type (max u_5 u_6)
-- Mathlib.Algebra.Order.Field.Basic
/-- **Alias** of the reverse direction of `mul_sub_mul_div_mul_neg_iff`. -/
mul_sub_mul_div_mul_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b c d : α},
  c ≠ 0 → d ≠ 0 → a / c < b / d → (a * d - b * c) / (c * d) < 0
-- Init.Data.Rat.Lemmas
Rat.num_intCast : ∀ (a : ℤ), (↑a).num = a
-- Mathlib.Data.Fin.Basic
Fin.natCast_eq_mk : ∀ {m n : ℕ} (h : m < n),
  have this := ⋯;
  ↑m = ⟨m, h⟩
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- If `f : Filter α` is an atom, then it is an ultrafilter.  -/
Ultrafilter.ofAtom : {α : Type u} → (f : Filter α) → IsAtom f → Ultrafilter α
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (d : D) (x x_1 : Cᴹᵒᵖ) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.unmop d
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangle.obj₁ = (DerivedCategory.singleFunctor C 0).obj S.X₁
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.smallCategory : CategoryTheory.SmallCategory SemiSimplexCategory
-- Mathlib.Order.Defs.Unbundled
/-- An upper set in an order `α` is a set such that any element greater than one of its members is
also a member. Also called up-set, upward-closed set.  -/
UpperSet : (α : Type u_1) → [LE α] → Type u_1
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Left homotopy is a transitive relation.  -/
CategoryTheory.Arrow.LeftHomotopy.trans : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {e f g : u ⟶ v} →
          CategoryTheory.Arrow.LeftHomotopy e f →
            CategoryTheory.Arrow.LeftHomotopy f g → CategoryTheory.Arrow.LeftHomotopy e g
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.comp_toPrefunctor : ∀ {B : Type u₁} [inst : Quiver B] [inst_1 : (a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [inst_2 : Quiver C]
  [inst_3 : (a b : C) → Quiver (a ⟶ b)] {D : Type u₃} [inst_4 : Quiver D] [inst_5 : (a b : D) → Quiver (a ⟶ b)]
  (F : CategoryTheory.PrelaxFunctorStruct B C) (G : CategoryTheory.PrelaxFunctorStruct C D),
  (F.comp G).toPrefunctor = F.toPrefunctor ⋙q G.toPrefunctor
-- Mathlib.Topology.LocallyConstant.Algebra
/-- The constant-function embedding, as an additive monoid hom.  -/
LocallyConstant.constAddMonoidHom : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : AddZeroClass Y] → Y →+ LocallyConstant X Y
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.inv_def : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (e : E ≃ₗᵢ[R] E), e⁻¹ = e.symm
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReprPoly.repr : Lean.Grind.CommRing.Poly → ℕ → Std.Format
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (X : CategoryTheory.Grp C),
  (CategoryTheory.Functor.mapGrpCompIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'_bot : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Ideal S)
  [Nontrivial R] [IsDomain S] [Algebra.IsIntegral R S] [hP : P.LiesOver ⊥], ⊥.inertiaDeg' P = Module.finrank R S
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictAnti.mul_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
  [MulRightStrictMono α], StrictAnti f → ∀ (c : α), StrictAnti fun x => f x * c
-- Mathlib.NumberTheory.Real.Irrational
irrational_ratCast_div_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (↑q / x) ↔ q ≠ 0 ∧ Irrational x
-- Mathlib.Data.Finset.NAry
Finset.image_uncurry_product : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β),
  Finset.image (Function.uncurry f) (s ×ˢ t) = Finset.image₂ f s t
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_natCast_cpow_pos_of_pos : ∀ {n : ℕ}, 0 < n → ∀ (s : ℂ), 0 < ‖↑n ^ s‖
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.finset.injEq : ∀ (s s_1 : Lean.Term), (BigOperators.FinsetResult.finset✝ s = BigOperators.FinsetResult.finset✝ s_1) = (s = s_1)
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterStep.restrict_bundle : ∀ {α₁ : Type u_1} {m : Type u_1 → Type u_2} {β α₂ : Type u_1} [inst : Std.Iterator α₁ m β]
  [inst_1 : Std.Iterator α₂ m β] [inst_2 : Monad m] [inst_3 : LawfulMonad m] {ita : Std.IterM m β}
  {step : Std.IterStep (Std.IterM m β) β} {h : ∃ s, step.bundledQuotient = (↑s).bundledQuotient},
  Std.IterM.QuotStep.restrict ⟨step.bundledQuotient, h⟩ =
    Quot.mk (fun s₁ s₂ => (↑s₁).bundledQuotient = (↑s₂).bundledQuotient) h.choose
-- Init.Conv
Lean.Parser.Tactic.Conv.enterArg : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.copy.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = ↑p),
  p.copy s hs = { carrier := s, smul_mem' := ⋯ }
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.mem_toList_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {p : Equiv.Perm α} {x y : α},
  y ∈ p.toList x ↔ p.SameCycle x y ∧ x ∈ p.support
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_inter_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a homology data `h` of a short complex `S` is such that both `h.left` and
`h.right` are preserved by a functor `F`, this is the induced homology data
`h.map F` for the short complex `S.map F`.  -/
CategoryTheory.ShortComplex.HomologyData.map : {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} →
              (h : S.HomologyData) →
                (F : CategoryTheory.Functor C D) →
                  [inst_4 : F.PreservesZeroMorphisms] →
                    [h.left.IsPreservedBy F] → [h.right.IsPreservedBy F] → (S.map F).HomologyData
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Given a function `f : ι → M` and a multiset `t : Multiset ι`, we can always find `i : ι`, belonging
to `t` if `t` is nonempty, such that `‖(s.map f).prod‖ ≤ ‖f i‖`.
 -/
IsUltrametricDist.exists_norm_multiset_prod_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] (s : Multiset ι) [Nonempty ι]
  {f : ι → M}, ∃ i, (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖
-- Init.Data.Array.Zip
Array.map_zip_eq_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {as : Array α} {bs : Array β},
  Array.map f (as.zip bs) = Array.zipWith (Function.curry f) as bs
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerveFunctor_obj : ∀ (C : CategoryTheory.Cat), CategoryTheory.nerveFunctor.obj C = CategoryTheory.nerve ↑C
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- **Alias** of `MeasureTheory.integrable_finsetSum`. -/
MeasureTheory.integrable_finset_sum : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_8} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] [ContinuousAdd ε'] {ι : Type u_9} (s : Finset ι) {f : ι → α → ε'},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) → MeasureTheory.Integrable (fun a => ∑ i ∈ s, f i a) μ
-- Init.Data.Slice.Array.Lemmas
Subarray.size_mkSlice_roc : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.size (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = min (hi + 1) (Std.Slice.size xs) - (lo + 1)
-- Lean.Parser.Syntax
Lean.Parser.Command.macro_rules.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.StrongHomClass.theory_model : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {T : L.Theory}
  {F : Type u_4} [inst_2 : EquivLike F M N] [L.StrongHomClass F M N] (g : F) [M ⊨ T], N ⊨ T
-- Mathlib.Algebra.Group.Graph
/-- **Goursat's lemma** for monoid isomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that the natural maps from `G` to
both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃* I`.  -/
Subgroup.exists_mulEquiv_eq_graph : ∀ {H : Type u_2} {I : Type u_3} [inst : Group H] [inst_1 : Group I] {G : Subgroup (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) → Function.Bijective (Prod.snd ∘ ⇑G.subtype) → ∃ e, G = e.toMonoidHom.graph
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- For `x : prime ideal of A` and any `p : NumDenSameDeg 𝒜 x`, or equivalent a numerator and a
denominator of the same degree, we get an element `p.num / p.den` of `Aₓ`.
 -/
HomogeneousLocalization.NumDenSameDeg.embedding : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          (𝒜 : ι → σ) → (x : Submonoid A) → HomogeneousLocalization.NumDenSameDeg 𝒜 x → Localization x
-- Mathlib.Algebra.Order.Group.Lattice
neg_sup : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a b : α), -(a ⊔ b) = -a ⊓ -b
-- Mathlib.Algebra.Free
FreeAddSemigroup.traverse_eq : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : FreeAddSemigroup α),
  FreeAddSemigroup.traverse F x = traverse F x
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.instIsScalarTowerForall : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : DistribSMul S R] [IsScalarTower S R R], IsScalarTower S (Matrix n n R) (n → R)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.const_smul_mem_Lp : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] (c : 𝕜)
  (f : ↥(MeasureTheory.Lp E p μ)), c • ↑f ∈ MeasureTheory.Lp E p μ
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.ghostComponent_frobenius : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (n : ℕ) (x : WittVector p R),
  (WittVector.ghostComponent n) (WittVector.frobenius x) = (WittVector.ghostComponent (n + 1)) x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_right_Q : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.HomologyData.canonical S).right.Q = S.opcycles
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The vector from any point to the centroid is the average of vectors to the simplex vertices.  -/
Affine.Simplex.centroid_vsub_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [CharZero k] (s : Affine.Simplex k P n) (p : P),
  s.centroid -ᵥ p = (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ p)
-- Mathlib.Analysis.Convex.Cone.Closure
ConvexCone.mem_closure : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] {E : Type u_2} [inst_2 : AddCommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : SMul 𝕜 E] [inst_6 : ContinuousConstSMul 𝕜 E]
  {K : ConvexCone 𝕜 E} {a : E}, a ∈ K.closure ↔ a ∈ closure ↑K
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_smul_of_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : ℝ},
  0 ≤ r → ∀ {a : A}, (r • a)⁺ = r • a⁺
-- Mathlib.Data.Int.GCD
pow_mem_range_pow_of_coprime : ∀ {α : Type u_1} [inst : CommGroupWithZero α] {m n : ℕ},
  m.Coprime n → ∀ (a : α), (a ^ m ∈ Set.range fun x => x ^ n) ↔ a ∈ Set.range fun x => x ^ n
-- Init.Data.Int.Lemmas
Int.negSucc_sub_one : ∀ (n : ℕ), Int.negSucc n - 1 = Int.negSucc (n + 1)
-- Mathlib.Condensed.TopCatAdjunction
/-- The adjunction `condensedSetToTopCat ⊣ topCatToCondensedSet`  -/
CondensedSet.topCatAdjunction : condensedSetToTopCat ⊣ topCatToCondensedSet
-- Init.Data.Iterators.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.eq_3 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done),
  Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.IterStep.done, property⟩ = Std.IterStep.done
-- Init.Data.SInt.Lemmas
Int32.sub_neg : ∀ {a b : Int32}, a - -b = a + b
-- Mathlib.Algebra.Order.Floor.Defs
Nat.ceil_pos : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a : α}, 0 < ⌈a⌉₊ ↔ 0 < a
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.mk : ∀ {K : Type u_1} [inst : Field K], (∀ (v : NumberField.InfinitePlace K), v.IsReal) → NumberField.IsTotallyReal K