mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.rightUnitor_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).inv
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.eq_5 : ∀ (x x_1 : Lean.Grind.IntInterval),
  (∀ (a a_1 b b_1 : ℤ), x = Lean.Grind.IntInterval.co a a_1 → x_1 = Lean.Grind.IntInterval.co b b_1 → False) →
    (∀ (a b : ℤ), x = Lean.Grind.IntInterval.ci a → x_1 = Lean.Grind.IntInterval.ci b → False) →
      (∀ (a b : ℤ), x = Lean.Grind.IntInterval.io a → x_1 = Lean.Grind.IntInterval.io b → False) →
        (x = Lean.Grind.IntInterval.ii → x_1 = Lean.Grind.IntInterval.ii → False) →
          Lean.Grind.instBEqIntInterval.beq x x_1 = false
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.ι_mapBifunctorMap_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂}
  (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J)
  [inst_8 : TotalComplexShape c₁ c₂ c] [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : L₁.HasMapBifunctor L₂ F c]
  [inst_11 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j) {Z : D}
  (h_1 : (L₁.mapBifunctor L₂ F c).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.mapBifunctorMap f₁ f₂ F c).f j) h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂))
      (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂))
        (CategoryTheory.CategoryStruct.comp (L₁.ιMapBifunctor L₂ F c i₁ i₂ j h) h_1))
-- Mathlib.Data.TypeVec
/-- similar to `of_subtype` adapted to relations (i.e. predicate on product)  -/
TypeVec.ofSubtype' : {n : ℕ} →
  {α : TypeVec.{u} n} →
    (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) →
      (TypeVec.Subtype_ p).Arrow fun i => { x // TypeVec.ofRepeat (p i (TypeVec.prod.mk i x.1 x.2)) }
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.getKeyLE?.go : {α : Type u} → {β : α → Type v} → [Ord α] → α → Option α → Std.DTreeMap.Internal.Impl α β → Option α
-- Init.Data.SInt.Bitwise
Int8.ofBitVec_not : ∀ (a : BitVec 8), Int8.ofBitVec (~~~a) = ~~~Int8.ofBitVec a
-- Init.Data.Array.Lemmas
Array.size_swapAt : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {v : α} (hi : i < xs.size), (xs.swapAt i v hi).2.size = xs.size
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
/-- The natural morphism `colim_k (∏ᶜ s ↦ (F s).obj (k s)) ⟶ ∏ᶜ s ↦ colim_k (F s).obj (k s)`.
A category has the `IPC` property of shape `α` if this morphism is an isomorphism as long
as the indexing categories are filtered.  -/
CategoryTheory.Limits.colimitPointwiseProductToProductColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type u_1} →
      {I : α → Type u_2} →
        [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] →
          [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C] →
            (F : (i : α) → CategoryTheory.Functor (I i) C) →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasColimit (F i)] →
                [inst_4 :
                    CategoryTheory.Limits.HasColimit
                      ((CategoryTheory.Functor.pi F).comp (CategoryTheory.Limits.Pi.functor α))] →
                  CategoryTheory.Limits.colimit (CategoryTheory.Limits.pointwiseProduct F) ⟶
                    ∏ᶜ fun s => CategoryTheory.Limits.colimit (F s)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
CommMonCat.FilteredColimits.colimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommMonCat),
  CommMonCat.FilteredColimits.colimit F = CommMonCat.of ↑(CommMonCat.FilteredColimits.M F)
-- Mathlib.Order.Fin.SuccAboveOrderIso
/-- Given `i : Fin (n + 2)`, this is the order isomorphism
between `Fin (n + 1)` and the finite set `{i}ᶜ`.  -/
Fin.succAboveOrderIso : {n : ℕ} → (i : Fin (n + 2)) → Fin (n + 1) ≃o ↥{i}ᶜ
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_op : ∀ {M : Type u_2} [inst : Mul M] (S : Subsemigroup M), S.op.unop = S
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.le_traceDual : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] {I J : Submodule B L},
  I ≤ Submodule.traceDual A K J ↔ I * J ≤ Submodule.traceDual A K 1
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.state : Std.Http.Body.Stream → Std.Mutex Std.Http.Body.Channel.State✝
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- **Alias** of `SimpleGraph.isBridge_iff_forall_cycle_notMem`. -/
SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem : ∀ {V : Type u} {G : SimpleGraph V} {e : Sym2 V},
  e ∈ G.edgeSet → (G.IsBridge e ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges)
-- Aesop.Util.EqualUpToIds
_private.Aesop.Util.EqualUpToIds.0.Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂.printExpr : Lean.MetavarContext → Lean.LocalContext → Lean.LocalInstances → Lean.Expr → Lean.MetaM Lean.MessageData
-- Mathlib.AlgebraicGeometry.Scheme
/-- The structure sheaf of a scheme.  -/
AlgebraicGeometry.Scheme.sheaf : (X : AlgebraicGeometry.Scheme) → TopCat.Sheaf CommRingCat ↑X.toPresheafedSpace
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the forward direction of `isExtrFilter_dual_iff`. -/
IsExtrFilter.undual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter (⇑OrderDual.toDual ∘ f) l a → IsExtrFilter f l a
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimage.match_5.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive Nat.zero) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Topology.EMetricSpace.Basic
/-- In a pseudoemetric space, Cauchy sequences are characterized by the fact that, eventually,
the pseudoedistance between its elements is arbitrarily small  -/
EMetric.cauchySeq_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {u : β → α},
  CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (u m) (u n) < ε
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.assoc_tensor : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {Q : Type u_8} {S : Type u_9}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid Q] [inst_4 : AddCommMonoid S]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R S],
  TensorProduct.assoc R (TensorProduct R M N) Q S =
    LinearEquiv.rTensor S (TensorProduct.assoc R M N Q) ≪≫ₗ TensorProduct.assoc R M (TensorProduct R N Q) S ≪≫ₗ
        LinearEquiv.lTensor M (TensorProduct.assoc R N Q S) ≪≫ₗ
      (TensorProduct.assoc R M N (TensorProduct R Q S)).symm
-- Lean.Parser.Basic
Lean.Parser.mkAtomicInfo : String → Lean.Parser.ParserInfo
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    ∀ [Algebra.IsAlgebraic F ↥A],
      Cardinal.lift.{w, v} (Module.rank ↥A ↥(IntermediateField.extendScalars ⋯)) =
        Cardinal.lift.{v, w} (Module.rank F L)
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.trans : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep ep' : Equiv.Perm { a // p a })
  (en en' : Equiv.Perm { a // ¬p a }),
  Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en') =
    Equiv.Perm.subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.tAux.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J] (i j : J),
  AlgebraicGeometry.Scheme.IsLocallyDirected.tAux F i j = AlgebraicGeometry.Scheme.IsLocallyDirected.tAux F i j
-- Mathlib.Order.Category.OmegaCompletePartialOrder
/-- The equalizer fork is a limit.  -/
ωCPO.HasEqualizers.isEqualizer : {X Y : ωCPO} → (f g : X ⟶ Y) → CategoryTheory.Limits.IsLimit (ωCPO.HasEqualizers.equalizer f g)
-- Init.Data.Array.Basic
/-- Combines two arrays into an array of pairs in which the first and second components are the
corresponding elements of each input array. The resulting array is the length of the shorter of the
input arrays.

Examples:
* `#["Mon", "Tue", "Wed"].zip #[1, 2, 3] = #[("Mon", 1), ("Tue", 2), ("Wed", 3)]`
* `#["Mon", "Tue", "Wed"].zip #[1, 2] = #[("Mon", 1), ("Tue", 2)]`
* `#[x₁, x₂, x₃].zip #[y₁, y₂, y₃, y₄] = #[(x₁, y₁), (x₂, y₂), (x₃, y₃)]`
 -/
Array.zip : {α : Type u} → {β : Type u_1} → Array α → Array β → Array (α × β)
-- Mathlib.Order.Filter.ListTraverse
Filter.mem_traverse_iff : ∀ {α β : Type u} {f : β → Filter α} (fs : List β) (t : Set (List α)),
  t ∈ traverse f fs ↔ ∃ us, List.Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
-- Mathlib.NumberTheory.LSeries.SumCoeff
_private.Mathlib.NumberTheory.LSeries.SumCoeff.0.LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₁ : ∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => (∑ k ∈ Finset.Icc 1 n, f k) / ↑n) Filter.atTop (nhds l) →
    ∀ {ε : ℝ}, 0 < ε → ∀ᶠ (t : ℝ) in Filter.atTop, ‖∑ k ∈ Finset.Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t
-- Init.System.ST
EST.Out.error : {ε σ α : Type} → ε → Void σ → EST.Out ε σ α
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddGroup.induced.eq_1 : ∀ {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [inst : FunLike 𝓕 E F] [inst_1 : AddGroup E] [inst_2 : NormedAddGroup F]
  [inst_3 : AddMonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f),
  NormedAddGroup.induced E F f h =
    { norm := fun a => ‖f a‖, toAddGroup := inst_1, dist := fun a a_1 => dist (f a) (f a_1), dist_self := ⋯,
      dist_comm := ⋯, dist_triangle := ⋯, edist := fun a a_1 => PseudoMetricSpace.edist (f a) (f a_1), edist_dist := ⋯,
      toUniformSpace :=
        { toTopologicalSpace := TopologicalSpace.induced (⇑f) PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          uniformity := Filter.comap (fun p => (f p.1, f p.2)) (uniformity F), symm := ⋯, comp := ⋯,
          nhds_eq_comap_uniformity := ⋯ },
      uniformity_dist := ⋯, toBornology := { cobounded := Filter.comap (⇑f) (Bornology.cobounded F), le_cofinite := ⋯ },
      cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.Topology.Separation.GDelta
PerfectlyNormalSpace.closed_gdelta : ∀ {X : Type u} {inst : TopologicalSpace X} [self : PerfectlyNormalSpace X] ⦃h : Set X⦄, IsClosed h → IsGδ h
-- Mathlib.LinearAlgebra.Matrix.Permutation
Matrix.permMatrix_refl : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] [inst_1 : Zero R] [inst_2 : One R],
  Equiv.Perm.permMatrix R (Equiv.refl n) = 1
-- Mathlib.Tactic.MinImports
/-- `getDeclName cmd id` takes a `Syntax` input `cmd` and returns the `Name` of the declaration defined
by `cmd`.
 -/
Mathlib.Command.MinImports.getDeclName : Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Name
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_mem : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m),
  0 < m →
    ∀
      (q :
        ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace),
      0 ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.lintegral_eq_lintegral_of_isPiSystem : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)} {f g : α → ENNReal},
  m0 = MeasurableSpace.generateFrom s →
    IsPiSystem s →
      (∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ) →
        ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ →
          ∫⁻ (x : α), f x ∂μ ≠ ⊤ → ∀ (t : Set α), MeasurableSet t → ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one_notMem_inv_mul_iff : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, 1 ∉ t⁻¹ * s ↔ Disjoint s t
-- Mathlib.Probability.Process.Filtration
MeasureTheory.SigmaFiniteFiltration.mk : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {μ : MeasureTheory.Measure Ω}
  {f : MeasureTheory.Filtration ι m},
  (∀ (i : ι), MeasureTheory.SigmaFinite (μ.trim ⋯)) → MeasureTheory.SigmaFiniteFiltration μ f
-- Std.Time.Format.Modifier
/-- `n`: Nanosecond of second (e.g., 987654321).
 -/
Std.Time.Modifier.n : Std.Time.Number → Std.Time.Modifier
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_rpow_left_iff : ∀ {x y z : ℝ}, 1 < x → (x ^ y < x ^ z ↔ y < z)
-- Mathlib.RingTheory.Algebraic.Integral
/-- If `K` is a field, `r : A` and `f : K[X]`, then `Polynomial.aeval r f` is
transcendental over `K` if and only if `r` and `f` are both transcendental over `K`.
See also `Transcendental.aeval_of_transcendental` and `Transcendental.of_aeval`.  -/
transcendental_aeval_iff : ∀ {K : Type u_1} {A : Type u_4} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A] {r : A} {f : Polynomial K},
  Transcendental K ((Polynomial.aeval r) f) ↔ Transcendental K r ∧ Transcendental K f
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.𝔾ₐ_toPowerSeries : ∀ {R : Type u_1} [inst : CommRing R], FormalGroup.𝔾ₐ.toPowerSeries = MvPowerSeries.X 0 + MvPowerSeries.X 1
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.mulSupport.eq_1 : ∀ {G : Type u_1} [inst : Group G] (M : Submonoid G), M.mulSupport = { toSubmonoid := M ⊓ M⁻¹, inv_mem' := ⋯ }
-- Mathlib.Topology.Algebra.Monoid
Prod.separatelyContinuousAdd : ∀ {M : Type u_6} {N : Type u_7} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M]
  [inst_3 : TopologicalSpace N] [inst_4 : Add N] [SeparatelyContinuousAdd N], SeparatelyContinuousAdd (M × N)
-- Mathlib.FieldTheory.KrullTopology
/-- For a field extension `L/K`, the Krull topology on `Gal(L/K)` makes it a topological group.  -/
instIsTopologicalGroupAlgEquiv : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L], IsTopologicalGroup Gal(L/K)
-- Init.Data.SInt.Lemmas
Int8.mod_one : ∀ {a : Int8}, a % 1 = 0
-- Mathlib.Topology.Sheaves.Alexandrov
/-- The right Kan extension of `F` along `X ⥤ (Opens X)ᵒᵖ`.  -/
Alexandrov.principalsKanExtension : {X : Type v} →
  [inst : TopologicalSpace X] →
    [inst_1 : Preorder X] →
      [Topology.IsUpperSet X] →
        {C : Type u} →
          [inst_3 : CategoryTheory.Category.{v, u} C] →
            [CategoryTheory.Limits.HasLimits C] →
              CategoryTheory.Functor X C → CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ C
-- Mathlib.Data.Fin.Tuple.Finset
Fin.insertNth_mem_piFinset_insertNth : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {p : Fin (n + 1)} {x_pivot : α p} {x_remove : (i : Fin n) → α (p.succAbove i)}
  {s_pivot : Finset (α p)} {s_remove : (i : Fin n) → Finset (α (p.succAbove i))},
  p.insertNth x_pivot x_remove ∈ Fintype.piFinset (p.insertNth s_pivot s_remove) ↔
    x_pivot ∈ s_pivot ∧ x_remove ∈ Fintype.piFinset s_remove
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : K.opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.sc' i j k).pOpcycles
      (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv h) =
    CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h
-- Mathlib.Topology.Bases
/-- The product of two separable spaces is a separable space.  -/
TopologicalSpace.instSeparableSpaceProd : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] [TopologicalSpace.SeparableSpace α]
  [TopologicalSpace.SeparableSpace β], TopologicalSpace.SeparableSpace (α × β)
-- Mathlib.LinearAlgebra.Dual.Basis
/-- The linear map from a vector space equipped with basis to its dual vector space,
taking basis elements to corresponding dual basis elements.  -/
Module.Basis.toDual : {R : Type uR} →
  {M : Type uM} →
    {ι : Type uι} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [DecidableEq ι] → Module.Basis ι R M → M →ₗ[R] Module.Dual R M
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inrₗ.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β],
  OrderAddMonoidHom.inrₗ α β =
    { toFun := (Prod.Lex.toLexOrderHom.comp ↑(OrderAddMonoidHom.inr α β)).toFun, map_zero' := ⋯, map_add' := ⋯,
      monotone' := ⋯ }
-- Mathlib.LinearAlgebra.Prod
/-- `M` as a submodule of `M × N`.  -/
Submodule.fst : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → Submodule R (M × M₂)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The diagram `S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃` is exact
for any `S : SnakeInput C`.  -/
CategoryTheory.ShortComplex.SnakeInput.snake_lemma : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.composableArrows.Exact
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.toTree.eq_1 : ∀ (p : DyckWord),
  p.toTree = if p = 0 then BinaryTree.nil else BinaryTree.node () p.insidePart.toTree p.outsidePart.toTree
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioc_of_Ioc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun i => Set.Ioc (a i) (b i)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_inv_comp_biproduct_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C) (j : J)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) h
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.mk.inj : ∀ {ref : Lean.Syntax} {kind : Lean.Elab.DefKind} {levelParams : List Lean.Name} {modifiers : Lean.Elab.Modifiers}
  {declName : Lean.Name} {binders : Lean.Syntax} {numSectionVars : ℕ} {type value : Lean.Expr}
  {termination : Lean.Elab.TerminationHints} {ref_1 : Lean.Syntax} {kind_1 : Lean.Elab.DefKind}
  {levelParams_1 : List Lean.Name} {modifiers_1 : Lean.Elab.Modifiers} {declName_1 : Lean.Name}
  {binders_1 : Lean.Syntax} {numSectionVars_1 : ℕ} {type_1 value_1 : Lean.Expr}
  {termination_1 : Lean.Elab.TerminationHints},
  { ref := ref, kind := kind, levelParams := levelParams, modifiers := modifiers, declName := declName,
        binders := binders, numSectionVars := numSectionVars, type := type, value := value,
        termination := termination } =
      { ref := ref_1, kind := kind_1, levelParams := levelParams_1, modifiers := modifiers_1, declName := declName_1,
        binders := binders_1, numSectionVars := numSectionVars_1, type := type_1, value := value_1,
        termination := termination_1 } →
    ref = ref_1 ∧
      kind = kind_1 ∧
        levelParams = levelParams_1 ∧
          modifiers = modifiers_1 ∧
            declName = declName_1 ∧
              binders = binders_1 ∧
                numSectionVars = numSectionVars_1 ∧ type = type_1 ∧ value = value_1 ∧ termination = termination_1
-- Mathlib.Tactic.Positivity.Core
/-- An extension for `positivity`.  -/
Mathlib.Meta.Positivity.PositivityExt : Type
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- The environment extension that contains a simp set, returned by `Lean.Meta.registerSimpAttr`.

Use the simp set's attribute or `Lean.Meta.addSimpTheorem` to add theorems to the simp set. Use
`Lean.Meta.SimpExtension.getTheorems` to get the contents.
 -/
Lean.Meta.SimpExtension : Type
-- Mathlib.RingTheory.Perfection
/-- A perfection map to a ring of characteristic `p` is a map that is isomorphic
to its perfection.  -/
PerfectionMap : (p : ℕ) →
  [Fact (Nat.Prime p)] →
    {R : Type u₁} →
      [inst : CommSemiring R] →
        [CharP R p] → {P : Type u₂} → [inst_2 : CommSemiring P] → [CharP P p] → [PerfectRing P p] → (P →+* R) → Prop
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- Given all finite wide pullbacks in `C`, construct finite products in `C/B`.  -/
CategoryTheory.Over.ConstructProducts.over_finiteProducts_of_finiteWidePullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] {B : C},
  CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Over B)
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.map.congr_simp : ∀ {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 S_1 : CategoryTheory.ShortComplex C),
  S = S_1 →
    ∀ (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1) [inst_4 : F.PreservesZeroMorphisms], S.map F = S_1.map F_1