mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.map_eq_natCast_iff : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : β → α} {n : ℕ} {a : WithTop β},
  WithTop.map f a = ↑n ↔ ∃ x, a = ↑x ∧ f x = ↑n
-- Mathlib.Data.Finmap
Finmap.ext_iff' : ∀ {α : Type u} {β : α → Type v} {s t : Finmap β}, s.entries = t.entries ↔ s = t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.getKey? t.minKey! = some t.minKey!
-- Mathlib.Data.Fin.Rev
Fin.predAbove_rev_right : ∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)), p.predAbove i.rev = (p.rev.predAbove i).rev
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∪ t₂).getKey! k = t₂.getKey! k
-- Mathlib.Order.WellFoundedSet
Set.isWF_union : ∀ {α : Type u_2} [inst : Preorder α] {s t : Set α}, (s ∪ t).IsWF ↔ s.IsWF ∧ t.IsWF
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInvEquiv.congr_simp : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M),
  S.leftInvEquiv hS = S.leftInvEquiv hS
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
Filter.EventuallyEq.lineDerivWithin_eq_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f f₁ : E → F}
  {s : Set E} {x v : E}, f₁ =ᶠ[nhds x] f → lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_7.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.mul_inv_le_of_mul_le : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, b < 0 → a * b ≤ c → c * b⁻¹ ≤ a
-- Mathlib.NumberTheory.Chebyshev
/-- Expresses the prime counting function `π` in terms of `θ` by using Abel summation.  -/
Chebyshev.primeCounting_eq_theta_div_log_add_integral : ∀ {x : ℝ},
  2 ≤ x →
    ↑⌊x⌋₊.primeCounting = Chebyshev.theta x / Real.log x + ∫ (t : ℝ) in 2..x, Chebyshev.theta t / (t * Real.log t ^ 2)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_comm : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] {μ : F} {f g : α → β}, f =ᵐ[μ] g ↔ g =ᵐ[μ] f
-- Mathlib.Algebra.Star.SelfAdjoint
/-- The skew-adjoint elements of a star additive group, as an additive subgroup.  -/
skewAdjoint : (R : Type u_1) → [inst : AddCommGroup R] → [StarAddMonoid R] → AddSubgroup R
-- Init.Data.Slice.List.Basic
instSliceableListNatListSlice_8 : {α : Type u} → Std.Rii.Sliceable (List α) ℕ (ListSlice α)
-- Mathlib.NumberTheory.Niven
/-- **Niven's theorem**: The only rational values of `cos` that occur at rational multiples of π
are `{-1, -1/2, 0, 1/2, 1}`.  -/
niven : ∀ {θ : ℝ}, (∃ r, θ = ↑r * Real.pi) → (∃ q, Real.cos θ = ↑q) → Real.cos θ ∈ {-1, -1 / 2, 0, 1 / 2, 1}
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.prelude.formatter : Lean.PrettyPrinter.Formatter
-- Plausible.Sampleable
Plausible.ULift.sampleableExt : {α : Type u_1} → [Plausible.SampleableExt α] → Plausible.SampleableExt (ULift.{u_3, u_1} α)
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Let `S` be an `S₀`-algebra. Then `S`-modules are modules over `S₀`.
 -/
SemimoduleCat.Algebra.instModuleCarrier : {S₀ : Type u₀} →
  [inst : CommSemiring S₀] →
    {S : Type u} → [inst_1 : Semiring S] → [Algebra S₀ S] → {M : SemimoduleCat S} → Module S₀ ↑M
-- Mathlib.Topology.Path
/-- The path 0 ⟶ 1 in `I`  -/
Path.id : Path 0 1
-- Mathlib.Data.EReal.Basic
EReal.toReal_top : ⊤.toReal = 0
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.mulAntidiagonal_mono_left : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO},
  u ⊆ s → Finset.mulAntidiagonal hu ht a ⊆ Finset.mulAntidiagonal hs ht a
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.induction_on : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {p : Turing.ListBlank Γ → Prop} (q : Turing.ListBlank Γ),
  (∀ (a : List Γ), p (Turing.ListBlank.mk a)) → p q
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.vadd_Lp_ae_eq : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)),
  ↑↑(c +ᵥ f) =ᵐ[μ] fun x => ↑↑f (DomAddAct.mk.symm c +ᵥ x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- ```
 X ⊞ Y --fst--> X
   |            |
  snd           0
   |            |
   v            v
   Y -----0---> 0
```
is a bi-Cartesian square.
 -/
CategoryTheory.BicartesianSq.of_is_biproduct₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.BicartesianSq b.fst b.snd 0 0
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheaf.coeFun : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            {M : Type u} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (N : Type u) →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H N] →
                                        (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) →
                                          CoeFun ((smoothSheaf IM I M N).presheaf.obj U) fun x => ↥(Opposite.unop U) → N
-- Mathlib.Order.Category.BddLat
BddLat.coe_forget_to_lat : ∀ (X : BddLat), ↑((CategoryTheory.forget₂ BddLat Lat).obj X) = ↑X.toLat
-- Init.Grind.Interactive
/-- Shows equivalence classes of terms.  -/
Lean.Parser.Tactic.Grind.showEqcs : Lean.ParserDescr
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f g) f =
    CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) g
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeans.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_eq_ofNat : ∀ {o : Ordinal.{u_1}} {n : ℕ} [inst : n.AtLeastTwo], o.card = OfNat.ofNat n ↔ o = OfNat.ofNat n
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_iSup₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → LowerSet α),
  (⨆ i, ⨆ j, f i j).compl = ⨆ i, ⨆ j, (f i j).compl
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.associator_hom_app_apply : ∀ (K L M : SSet) {Δ : SimplexCategoryᵒᵖ}
  (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj K L) M).obj Δ),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.associator (K.obj Δ) (L.obj Δ) (M.obj Δ)).hom)
      x =
    (x.1.1, x.1.2, x.2)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- **Alias** of `Function.Bijective.finsetProd`.

---

**Alias** of `Fintype.prod_bijective`.

---

`Fintype.prod_bijective` is a variant of `Finset.prod_bij` that accepts `Function.Bijective`.

See `Function.Bijective.prod_comp` for a version without `h`.  -/
Function.Bijective.finset_prod : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  (e : ι → κ), Function.Bijective e → ∀ (f : ι → M) (g : κ → M), (∀ (x : ι), f x = g (e x)) → ∏ x, f x = ∏ x, g x
-- Lean.Elab.PreDefinition.WF.Fix
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.replaceRecApps.containsRecFn : (recFnName : Lean.Name) → Lean.Expr → Lean.Elab.WF.RecM✝ recFnName Bool
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.TopSort.State.mk.injEq : ∀ (visitedFVars : Lean.FVarIdSet) (visitedMVars : Lean.MVarIdSet) (result : Array Lean.Expr)
  (visitedFVars_1 : Lean.FVarIdSet) (visitedMVars_1 : Lean.MVarIdSet) (result_1 : Array Lean.Expr),
  ({ visitedFVars := visitedFVars, visitedMVars := visitedMVars, result := result } =
      { visitedFVars := visitedFVars_1, visitedMVars := visitedMVars_1, result := result_1 }) =
    (visitedFVars = visitedFVars_1 ∧ visitedMVars = visitedMVars_1 ∧ result = result_1)
-- Mathlib.Algebra.Lie.OfAssociative
Module.End.instLieRingModule : {R : Type u} →
  [inst : CommRing R] →
    {M : Type w} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → LieRingModule (Module.End R M) M
-- Mathlib.Algebra.Category.Semigrp.Basic
MulEquiv.toMagmaCatIso_inv : ∀ {X Y : Type u} [inst : Mul X] [inst_1 : Mul Y] (e : X ≃* Y), e.toMagmaCatIso.inv = MagmaCat.ofHom e.symm.toMulHom
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_mul : ∀ {m n : ℕ},
  m ≠ 0 →
    n ≠ 0 → ArithmeticFunction.cardFactors (m * n) = ArithmeticFunction.cardFactors m + ArithmeticFunction.cardFactors n
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n : ℕ),
  S.toBiprod F n =
    CategoryTheory.Limits.biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)
-- Batteries.Data.List.Lemmas
List.getElem_getElem_findIdxs : ∀ {i : ℕ} {α : Type u_1} {xs : List α} {p : α → Bool} (h : i < (List.findIdxs p xs).length),
  p xs[(List.findIdxs p xs)[i]] = true
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Pass.mk.inj : ∀ {toConfig : Mathlib.TacticAnalysis.Config} {opt : Option (Lean.Option Bool)}
  {toConfig_1 : Mathlib.TacticAnalysis.Config} {opt_1 : Option (Lean.Option Bool)},
  { toConfig := toConfig, opt := opt } = { toConfig := toConfig_1, opt := opt_1 } → toConfig = toConfig_1 ∧ opt = opt_1
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittAdd.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittAdd p = wittStructureInt p (MvPolynomial.X 0 + MvPolynomial.X 1)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_union_le : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s s' : Set α),
  μ.restrict (s ∪ s') ≤ μ.restrict s + μ.restrict s'
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_neg_pos_neg_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {K : ℝ},
  ↑(A ^ 3).card ≤ K * ↑A.card → ↑(A⁻¹ * A * A⁻¹).card ≤ K ^ 3 * ↑A.card
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrTheorem.proof : Lean.Meta.CongrTheorem → Lean.Expr
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.cons_sub : ∀ {α : Type u_1} {n : ℕ} [inst : Sub α] (x : α) (v : Fin n → α) (w : Fin n.succ → α),
  Matrix.vecCons x v - w = Matrix.vecCons (x - Matrix.vecHead w) (v - Matrix.vecTail w)
-- Init.PropLemmas
forall_apply_eq_imp_iff₂ : ∀ {α : Sort u_2} {β : Sort u_1} {f : α → β} {p : α → Prop} {q : β → Prop},
  (∀ (b : β) (a : α), p a → f a = b → q b) ↔ ∀ (a : α), p a → q (f a)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_mono_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q Q' : l},
  Lean.Order.PartialOrder.rel Q Q' → Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet P Q')
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_add_adjacent_intervals : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b →
    IntervalIntegrable f μ b c → ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ = ∫ (x : ℝ) in a..c, f x ∂μ
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.direction_smul : ∀ {k : Type u_2} {V : Type u_3} [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {a : k},
  a ≠ 0 → ∀ (s : AffineSubspace k V), (a • s).direction = s.direction
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.comp_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {X Y Z : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left
-- Mathlib.Order.UpperLower.Basic
Set.monotone_mem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, (Monotone fun x => x ∈ s) ↔ IsUpperSet s
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.le_pushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C), P ≤ P.pushouts
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The duality equivalence `WalkingSpanᵒᵖ ≌ WalkingCospan`  -/
CategoryTheory.Limits.walkingSpanOpEquiv : CategoryTheory.Limits.WalkingSpanᵒᵖ ≌ CategoryTheory.Limits.WalkingCospan
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.IsBipartiteWith.mk : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V},
  Disjoint s t → (∀ ⦃v w : V⦄, G.Adj v w → v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s) → G.IsBipartiteWith s t
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.sectionsAddGroup : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddGrpCat) → AddGroup ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_of_arrow_mk_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ S₄ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [inst_4 : S₃.HasHomology] [inst_5 : S₄.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₃ ⟶ S₄)
  (e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ') [hφ : CategoryTheory.ShortComplex.QuasiIso φ],
  CategoryTheory.ShortComplex.QuasiIso φ'
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.ofHom_hom : ∀ {X Y : Type u} (f : X ⟶ Y), TypeCat.ofHom ⇑(TypeCat.Hom.hom f) = f
-- Mathlib.RingTheory.Jacobson.Ring
isJacobsonRing_of_isIntegral : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] [IsJacobsonRing R], IsJacobsonRing S
-- Mathlib.NumberTheory.Real.Irrational
one_lt_natDegree_of_irrational_root : ∀ (x : ℝ) (p : Polynomial ℤ), Irrational x → p ≠ 0 → (Polynomial.aeval x) p = 0 → 1 < p.natDegree
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.NatTrans.mapHomologicalComplex_comp : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (c : ComplexShape ι) {F G H : CategoryTheory.Functor W₁ W₂}
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms] [inst_6 : H.PreservesZeroMorphisms]
  (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.comp α β) c =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.mapHomologicalComplex α c)
      (CategoryTheory.NatTrans.mapHomologicalComplex β c)
-- Mathlib.RingTheory.Spectrum.Prime.Defs
/-- The prime spectrum of a commutative (semi)ring `R` is the type of all prime ideals of `R`.

It is naturally endowed with a topology (the Zariski topology),
and a sheaf of commutative rings (see `Mathlib/AlgebraicGeometry/StructureSheaf.lean`).
It is a fundamental building block in algebraic geometry.  -/
PrimeSpectrum : (R : Type u_1) → [CommSemiring R] → Type u_1
-- Std.Sat.AIG.Basic
/-- A `RefVec` to be extended to `newWidth`.
 -/
Std.Sat.AIG.ExtendTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_min_le : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : LinearOrder M] [IsOrderedMonoid M] {f g : ι → M}
  {s : Finset ι}, ∏ i ∈ s, min (f i) (g i) ≤ min (s.prod f) (s.prod g)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.mem_carrier : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] {p : SubAddAction R M} {x : M}, x ∈ p.carrier ↔ x ∈ ↑p
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.processNewFacts : Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.AddConstMap.Equiv
/-- Inverse map of an `AddConstEquiv`, as an `AddConstEquiv`.  -/
AddConstEquiv.symm : {G : Type u_1} →
  {H : Type u_2} → [inst : Add G] → [inst_1 : Add H] → {a : G} → {b : H} → AddConstEquiv G H a b → AddConstEquiv H G b a
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.levelNames : Lean.Elab.Command.InductiveView → List Lean.Name
-- Mathlib.Data.Opposite
/-- The canonical map `αᵒᵖ → α`.  -/
Opposite.unop : {α : Sort u} → αᵒᵖ → α
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.naturality_1'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x : CategoryTheory.IsIso (α.app X)} {Z : D}
  (h : G.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app X))
      (CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (α.app Y) h)) =
    CategoryTheory.CategoryStruct.comp (G.map f) h
-- Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
/-- Shows that `Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂`.  -/
GenContFract.dens_recurrence : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K] {gp : GenContFract.Pair K} {ppredB predB : K},
  g.s.get? (n + 1) = some gp →
    g.dens n = ppredB → g.dens (n + 1) = predB → g.dens (n + 2) = gp.b * predB + gp.a * ppredB
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : Group X] [IsTopologicalGroup X]
  [inst_3 : UniformSpace Y] [inst_4 : CommGroup Y] [IsUniformGroup Y] [T0Space Y] [CompactSpace Y] (U : Set X)
  (V : Set Y), IsCompact U → V ∈ nhds 1 → EquicontinuousAt (fun f => ⇑↑f) 1 → LocallyCompactSpace (X →ₜ* Y)
-- Mathlib.GroupTheory.Submonoid.Center
/-- For a monoid, the units of the center inject into the center of the units. This is not an
equivalence in general; one case where this holds is for groups with zero, which is covered in
`centerUnitsEquivUnitsCenter`.  -/
unitsCenterToCenterUnits : (M : Type u_1) → [inst : Monoid M] → (↥(Submonoid.center M))ˣ →* ↥(Submonoid.center Mˣ)
-- Mathlib.Analysis.Calculus.Deriv.Add
HasStrictDerivAt.neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasStrictDerivAt f f' x → HasStrictDerivAt (-f) (-f') x
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.nnnorm_comm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (x : TensorProduct 𝕜 E F), ‖(TensorProduct.comm 𝕜 E F) x‖₊ = ‖x‖₊
-- Lean.PrettyPrinter.Delaborator.Metavariable
_private.Lean.PrettyPrinter.Delaborator.Metavariable.0.Lean.PrettyPrinter.Delaborator.describeMVar : Lean.MVarId → ℕ → optParam Bool false → Lean.MetaM String
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.toLinearMap_injective : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {F : Type u_14} [inst_6 : FunLike F M M₃] [inst_7 : SemilinearMapClass F σ M M₃] {f g : F}, ↑f = ↑g → f = g
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Canon.State : Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_key : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.containsKey k (List.filter (fun p => f p.fst) l) = true ↔
      ∃ (h : Std.Internal.List.containsKey k l = true), f (Std.Internal.List.getKey k l h) = true)
-- Mathlib.Topology.Category.Stonean.Basic
/-- `Projective` implies `ExtremallyDisconnected`.  -/
CompHaus.instExtremallyDisconnectedCarrierToTopTrueOfProjective : ∀ (X : CompHaus) [CategoryTheory.Projective X], ExtremallyDisconnected ↑X.toTop
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.inr_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⨿ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) h) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
AlgHom.toContinuousLinearMap.congr_simp : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [inst_3 : CompleteSpace A] (φ φ_1 : A →ₐ[𝕜] 𝕜), φ = φ_1 → φ.toContinuousLinearMap = φ_1.toContinuousLinearMap
-- Init.Data.Rat.Lemmas
Rat.zpow_pos : ∀ {a : ℚ} {n : ℤ}, 0 < a → 0 < a ^ n
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.MergeSort.Internal.splitInTwo.eq_1 : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  List.MergeSort.Internal.splitInTwo l =
    (⟨(List.splitAt ((n + 1) / 2) ↑l).1, ⋯⟩, ⟨(List.splitAt ((n + 1) / 2) ↑l).2, ⋯⟩)
-- Mathlib.NumberTheory.Niven
/-- `exp(-(q * π) * I)` for `q : ℚ` is integral over `ℤ`.  -/
Complex.isIntegral_exp_neg_rat_mul_pi_mul_I : ∀ (q : ℚ), IsIntegral ℤ (Complex.exp (-(↑q * ↑Real.pi) * Complex.I))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.instHasKernelSnd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.HasKernel CategoryTheory.Limits.biprod.snd