mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Basic
right_ne_zero_of_mul : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] {a b : M₀}, a * b ≠ 0 → b ≠ 0
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mul_mono : ∀ {M : Type u_1} [inst : CommMonoid M] {a b c d : Associates M}, a ≤ b → c ≤ d → a * c ≤ b * d
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s)
  [inst_6 : T2Space M] [inst_7 : IsManifold I (↑⊤) M] (i : ι) (x : M),
  ∃ t, ⇑(fs.toSmoothPartitionOfUnity i) =ᶠ[nhds x] ↑(fs.toFun i) * ∏ j ∈ t with WellOrderingRel j i, (1 - ↑(fs.toFun j))
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_comp : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup P] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : LieRingModule L M] [inst_9 : LieRingModule L N]
  [inst_10 : LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_filterMap_eq_size_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).size = (↑m).size ↔
      ∀ (a : α) (h : m.contains a = true),
        (f (m.getKey a h) (Std.DHashMap.Internal.Raw₀.Const.get m a h)).isSome = true)
-- Aesop.Rule
Aesop.NormSimpRule.mk.sizeOf_spec : ∀ (name : Aesop.RuleName) (entries : Array Lean.Meta.SimpEntry),
  sizeOf { name := name, entries := entries } = 1 + sizeOf name + sizeOf entries
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c),
  CategoryTheory.CategoryStruct.comp (t.natTransTruncLTOfLE a b hab) (t.natTransTruncLTOfLE b c hbc) =
    t.natTransTruncLTOfLE a c ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHom : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (d : D) {c c' : C} (f : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom (CategoryTheory.CategoryStruct.id d) f =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toLinearMap_symm : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ),
  ↑↑φ.symm.toContinuousLinearEquiv = ↑(↑φ.toContinuousLinearEquiv).symm
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_eq_zero_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (s : ↥M), IsLocalization.mk' S x s = 0 ↔ ∃ m, ↑m * x = 0
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.mk.injEq : ∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (tosInfHom : sInfHom α β)
  (map_sSup' : ∀ (s : Set α), tosInfHom.toFun (sSup s) = sSup (tosInfHom.toFun '' s)) (tosInfHom_1 : sInfHom α β)
  (map_sSup'_1 : ∀ (s : Set α), tosInfHom_1.toFun (sSup s) = sSup (tosInfHom_1.toFun '' s)),
  ({ tosInfHom := tosInfHom, map_sSup' := map_sSup' } = { tosInfHom := tosInfHom_1, map_sSup' := map_sSup'_1 }) =
    (tosInfHom = tosInfHom_1)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- For `B : BoxIntegral.Box`, the `TaggedPrepartition` formed by the set of all
`unitPartition.box` whose index is `B`-admissible.  -/
BoxIntegral.unitPartition.prepartition : {ι : Type u_1} → (n : ℕ) → [NeZero n] → [Fintype ι] → (B : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition B
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.pointwise_isCentralScalar : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A]
  [inst_3 : DistribMulAction Mᵐᵒᵖ A] [IsCentralScalar M A], IsCentralScalar M (AddSubmonoid A)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_div_right_image : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, ⋃ a ∈ t, (fun x => x / a) '' s = s / t
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.hasGaussianLaw_iff_charFun_map_eq : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [CompleteSpace E] [inst_4 : InnerProductSpace ℝ E]
  [MeasureTheory.IsFiniteMeasure P],
  AEMeasurable X P →
    (ProbabilityTheory.HasGaussianLaw X P ↔
      ∀ (t : E),
        MeasureTheory.charFun (MeasureTheory.Measure.map X P) t =
          Complex.exp
            (↑(∫ (x : Ω), (fun ω => inner ℝ t (X ω)) x ∂P) * Complex.I -
              ↑(ProbabilityTheory.variance (fun ω => inner ℝ t (X ω)) P) / 2))
-- Mathlib.Data.Fin.VecNotation
/-- Unexpander for the `![]` notation.  -/
Matrix.vecEmptyUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Data.EReal.Operations
EReal.top_sub : ∀ {x : EReal}, x ≠ ⊤ → ⊤ - x = ⊤
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Cache for iterated `stepEntry` certificates, keyed by step and matrix indices.  -/
Mathlib.Tactic.Determinant.CertCache.iterStepEntryCache : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Mathlib.Tactic.Determinant.CertCache rα → Std.HashMap (ℕ × ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.Data.List.Lattice
List.suffix_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] (l₁ l₂ : List α), l₂ <:+ l₁ ∪ l₂
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Notation for `tensorObj`, the tensor product of objects in a monoidal category  -/
CategoryTheory.MonoidalCategory.«term_⊗_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    {F : CategoryTheory.Functor J MonCat} →
      {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop} →
        {a a_1 : MonCat.Colimits.Prequotient F} → MonCat.Colimits.Relation F a a_1 → Prop
-- Mathlib.Order.Monotone.Monovary
antivaryOn_toDual_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn (⇑OrderDual.toDual ∘ f) g s ↔ MonovaryOn f g s
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_not_contains_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  l₂.contains k = true → Std.Internal.List.containsKey k (List.filter (fun p => !l₂.contains p.fst) l₁) = false
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.dite : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : (x : α) → Decidable (x ∈ s)] {f : ↑s → β},
  MeasureTheory.StronglyMeasurable f →
    ∀ {g : ↑sᶜ → β},
      MeasureTheory.StronglyMeasurable g →
        MeasurableSet s → MeasureTheory.StronglyMeasurable fun x => if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩
-- Mathlib.Data.Set.Function
Set.LeftInvOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g : β → γ} {f' : β → α}
  {g' : γ → β}, Set.LeftInvOn f' f s → Set.LeftInvOn g' g t → Set.MapsTo f s t → Set.LeftInvOn (f' ∘ g') (g ∘ f) s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Rat.borelSpace : BorelSpace ℚ
-- Lean.Util.Diff
/-- Finds the least common subsequence of two arrays using a variant of jgit's histogram diff algorithm.

Unlike jgit's implementation, this one does not perform a cutoff on histogram bucket sizes, nor does
it fall back to the Myers diff algorithm. This means that it has quadratic worst-case complexity.
Empirically, however, even quadratic cases of this implementation can handle hundreds of megabytes
in a second or so, and it is intended to be used for short strings like error messages. Be
cautious when applying it to larger workloads.
 -/
Lean.Diff.lcs : {α : Type} → [BEq α] → [Hashable α] → Subarray α → Subarray α → Array α
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
/-- The space of affine maps between two normed spaces is linearly isometric to the product of the
codomain with the space of linear maps, by taking the value of the affine map at `(0 : V)` and the
linear part.  -/
ContinuousAffineMap.toConstProdContinuousLinearMap : (𝕜 : Type u_1) →
  (V : Type u_3) →
    (W : Type u_4) →
      [inst : SeminormedAddCommGroup V] →
        [inst_1 : SeminormedAddCommGroup W] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedSpace 𝕜 V] → [inst_4 : NormedSpace 𝕜 W] → (V →ᴬ[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_le_nat_iff : ∀ {a : Cardinal.{u}} {n : ℕ}, Cardinal.lift.{v, u} a ≤ ↑n ↔ a ≤ ↑n
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.instBEqGoTo : BEq ExistsAndEq.GoTo
-- Mathlib.Data.Nat.SuccPred
Nat.forall_ne_zero_iff : ∀ (P : ℕ → Prop), (∀ (i : ℕ), i ≠ 0 → P i) ↔ ∀ (i : ℕ), P (i + 1)
-- Mathlib.Order.Filter.Pointwise
Filter.bot_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {g : Filter β}, ⊥ -ᵥ g = ⊥
-- Init.Data.Int.Pow
Int.natCast_pow : ∀ (m n : ℕ), ↑(m ^ n) = ↑m ^ n
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.rTensor_nontrivial : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [fl : Module.FaithfullyFlat R M] (N : Type u_1) [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Nontrivial N],
  Nontrivial (TensorProduct R N M)
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkHCongrProofHelper : Lean.Meta.CongrTheorem → Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.isEventuallyConstant_of_isArtinianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.IsArtinianObject X]
  (F : CategoryTheory.Functor ℕ (CategoryTheory.MonoOver X)ᵒᵖ), CategoryTheory.IsFiltered.IsEventuallyConstant F
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {kmi : α}, (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.ObjectProperty.FullSubcategory.mk.hcongr_5 : ∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (P : CategoryTheory.ObjectProperty C) (P' : CategoryTheory.ObjectProperty C'),
          P ≍ P' →
            ∀ (obj : C) (obj' : C'),
              obj ≍ obj' →
                ∀ (property : P obj) (property' : P' obj'),
                  property ≍ property' → { obj := obj, property := property } ≍ { obj := obj', property := property' }
-- Std.Http.Data.Chunk
/-- The trailer header fields as key-value pairs.
 -/
Std.Http.Trailer.headers : Std.Http.Trailer → Std.Http.Headers
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.Transported.instMonoidalCategoryStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          (e : C ≌ D) → CategoryTheory.MonoidalCategoryStruct (CategoryTheory.Monoidal.Transported e)
-- Mathlib.Algebra.FreeMonoid.Basic
/-- If `α` is a type, then `FreeMonoid α` is the free monoid generated by `α`.
This is a monoid equipped with a function `FreeMonoid.of : α → FreeMonoid α` which has
the following universal property: if `M` is any monoid, and `f : α → M` is any function,
then this function is the composite of `FreeMonoid.of` and a unique monoid homomorphism
`FreeMonoid.lift f : FreeMonoid α →* M`.

A typical element of `FreeMonoid α` is a formal product of elements of `α`.
For example if `x` and `y` are terms of type `α` then `x * y * y * x` is a
"typical" element of `FreeMonoid α`. In particular if `α` is empty
then `FreeMonoid α` is isomorphic to the trivial monoid, and if `α` has one term
then `FreeMonoid α` is isomorphic to `Multiplicative ℕ`.
If `α` has two or more terms then `FreeMonoid α` is not commutative.
One can think of `FreeMonoid α` as the type of lists of `α`, with multiplication
given by concatenation.
 -/
FreeMonoid : Type u_6 → Type u_6
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toContinuousMap : {α : Type u_5} →
  {β : Type u_6} →
    [inst : TopologicalSpace α] →
      [inst_1 : Zero β] → [inst_2 : TopologicalSpace β] → CompactlySupportedContinuousMap α β → C(α, β)
-- Init.Data.List.Perm
List.Perm.singleton_eq : ∀ {α : Type u_1} {a : α} {l : List α}, [a].Perm l → [a] = l
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Slot.value : {α : Type} → Std.Slot✝ α → Option α
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift.eq_1 : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {I : Ideal A} (hI : DividedPowers I) (g : M →ₗ[R] A)
  (hg : ∀ (m : M), g m ∈ I), DividedPowerAlgebra.lift hI g hg = DividedPowerAlgebra.lift' ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.wEquiv_map : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α β : TypeVec.{u} n} (g : α.Arrow β)
  (x y : (MvQPF.P F).W α), MvQPF.WEquiv x y → MvQPF.WEquiv (MvFunctor.map g x) (MvFunctor.map g y)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAtChain.below.nil : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {a : s.Pos}
  {motive : (a_1 : s.Pos) → String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat a a_1 → Prop},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain.below ⋯
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.forM : {m : Type → Type u_1} →
  {pu : Lean.Compiler.LCNF.Purity} →
    [Monad m] → Lean.Compiler.LCNF.Code pu → (Lean.Compiler.LCNF.Code pu → m Unit) → m Unit
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
add_le_mul : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ZeroLEOneClass R] [NeZero 1] [MulPosStrictMono R]
  [PosMulStrictMono R] [AddLeftMono R], 2 ≤ a → 2 ≤ b → a + b ≤ a * b
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- The norm of the tensor product of a scalar linear map and of an element of a normed space
is the product of the norms.  -/
ContinuousLinearMap.norm_smulRight_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (c : StrongDual 𝕜 E)
  (f : Fₗ), ‖ContinuousLinearMap.smulRight c f‖ = ‖c‖ * ‖f‖
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.toSubfunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S : CategoryTheory.SubmonoidFunctor M) (x : C), S.toSubfunctor.obj x = (S.obj x).carrier
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- A subgroup of a seminormed group is also a seminormed group,
with the restriction of the norm.  -/
SubgroupClass.seminormedGroup : {E : Type u_1} →
  [inst : SeminormedGroup E] →
    {S : Type u_2} → [inst_1 : SetLike S E] → [SubgroupClass S E] → (s : S) → SeminormedGroup ↥s
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.homology₀Iso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C],
  X.homology₀Iso R =
    CategoryTheory.ShortComplex.homologyMapIso
        (HomologicalComplex.isoSc' (X.chainComplex R) 1 0 0 SSet.homology₀Iso._proof_1 SSet.homology₀Iso._proof_2) ≪≫
      (X.homologyData₀ R).left.homologyIso
-- Mathlib.Algebra.Lie.Weights.Cartan
/-- Given a nilpotent Lie subalgebra `H ⊆ L` together with `χ₁ χ₂ : H → R`, there is a natural
`R`-bilinear product of root vectors and weight vectors, compatible with the actions of `H`.  -/
LieAlgebra.rootSpaceWeightSpaceProduct : (R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (H : LieSubalgebra R L) →
            [inst_3 : LieRing.IsNilpotent ↥H] →
              (M : Type u_3) →
                [inst_4 : AddCommGroup M] →
                  [inst_5 : Module R M] →
                    [inst_6 : LieRingModule L M] →
                      [inst_7 : LieModule R L M] →
                        (χ₁ χ₂ χ₃ : ↥H → R) →
                          χ₁ + χ₂ = χ₃ →
                            TensorProduct R ↥(LieAlgebra.rootSpace H χ₁) ↥(LieModule.genWeightSpace M χ₂) →ₗ⁅R,↥H⁆
                              ↥(LieModule.genWeightSpace M χ₃)
-- Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Algebra.IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct : ∀ {R : Type u_3} {A : Type u_4} {inst : CommRing R} {inst_1 : Ring A} {inst_2 : Algebra R A}
  [self : Algebra.IsGeometricallyReduced R A] (p : Ideal R) [inst_3 : p.IsPrime],
  IsReduced (TensorProduct R (AlgebraicClosure p.ResidueField) A)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.IsSymm.inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A : Matrix n n α},
  A.IsSymm → A⁻¹.IsSymm
-- Mathlib.Order.Types.Defs
OrderType.instNeZeroOfNat : NeZero 1
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.Tendsto.uniformity_neg : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f : ι → α × α}
  {l : Filter ι}, Filter.Tendsto f l (uniformity α) → Filter.Tendsto (-f) l (uniformity α)
-- ImportGraph.Tools.FindHome
/-- Tries to resolve the module `modName` to a source file URI.
This has to be done in the Lean server
since the `Environment` does not keep track of source URIs.  -/
getModuleUri : Lean.Name → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.DocumentUri)
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Calls `cases` on `h` (assumed to be a binary sum) `n` times, and returns
the resulting subgoals and their corresponding new hypotheses.
 -/
Mathlib.Tactic.MkIff.nCasesSum : ℕ → Lean.MVarId → Lean.FVarId → Lean.MetaM (List (Lean.FVarId × Lean.MVarId))
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mk : {R : Type u} →
  [inst : NonUnitalNonAssocSemiring R] →
    (toAddSubmonoid : AddSubmonoid R) →
      (∀ {a b : R}, a ∈ toAddSubmonoid.carrier → b ∈ toAddSubmonoid.carrier → a * b ∈ toAddSubmonoid.carrier) →
        NonUnitalSubsemiring R
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sheaf.pushforwardOverMapIso_hom_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] (F : CategoryTheory.Sheaf J A) {X Y : C} (f : X ⟶ Y)
  (X_1 : (CategoryTheory.Over X)ᵒᵖ),
  (F.pushforwardOverMapIso f).hom.hom.app X_1 =
    CategoryTheory.CategoryStruct.id (F.obj.obj (Opposite.op (Opposite.unop X_1).left))
-- Mathlib.NumberTheory.Divisors
Nat.one_lt_div_of_mem_properDivisors : ∀ {m n : ℕ}, m ∈ n.properDivisors → 1 < n / m
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.term𝕢_ : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {fallback : α}, t.getKeyD (t.minKey he) fallback = t.minKey he
-- Mathlib.Data.Multiset.NatAntidiagonal
Multiset.Nat.antidiagonal.eq_1 : ∀ (n : ℕ), Multiset.Nat.antidiagonal n = ↑(List.Nat.antidiagonal n)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.map_comp_map : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} {P : Type u_4} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R' P] [inst_11 : Module R'ᵐᵒᵖ P] [inst_12 : IsCentralScalar R' P] (f : M →ₗ[R'] N) (g : N →ₗ[R'] P),
  TrivSqZeroExt.map (g ∘ₗ f) = (TrivSqZeroExt.map g).comp (TrivSqZeroExt.map f)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
NNReal.continuousAt_rpow_const : ∀ {x : NNReal} {y : ℝ}, x ≠ 0 ∨ 0 ≤ y → ContinuousAt (fun z => z ^ y) x
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [CompactSpace M], CompactSpace Mᵈᵐᵃ
-- Mathlib.SetTheory.ZFC.Class
Class.mem_def : ∀ (A B : Class.{u}), A ∈ B ↔ ∃ x, ↑x = A ∧ B x
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivary_neg`. -/
Antivary.neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β},
  Antivary f g → Antivary (-f) (-g)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.tsum_add_tsum_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [T2Space α]
  [ContinuousAdd α] {s : Set β},
  Summable (f ∘ Subtype.val) → Summable (f ∘ Subtype.val) → ∑' (x : ↑s), f ↑x + ∑' (x : ↑sᶜ), f ↑x = ∑' (x : β), f x
-- Mathlib.Analysis.Asymptotics.Defs
/-- We say that `f` is `Θ(g)` along a filter `l` (notation: `f =Θ[l] g`) if `f =O[l] g` and
`g =O[l] f`.  -/
Asymptotics.IsTheta : {α : Type u_1} → {E : Type u_3} → {F : Type u_4} → [Norm E] → [Norm F] → Filter α → (α → E) → (α → F) → Prop
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- An Unoriented angle is unchanged by replacing the first point by one weakly further away on the
same ray.  -/
Wbtw.angle_eq_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p p₂ : P} (p₃ : P),
  Wbtw ℝ p₂ p₁ p → p₁ ≠ p₂ → EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p p₂ p₃
-- Mathlib.Data.Fintype.Lattice
Finset.fold_inf_univ : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : SemilatticeInf α] [inst_2 : OrderBot α] (a : α),
  Finset.fold min a (fun x => x) Finset.univ = ⊥
-- Mathlib.Data.Finsupp.Sigma
Finsupp.embSigma_eq_zero : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k : κ} {f : ι k →₀ M}, f.embSigma = 0 ↔ f = 0