mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.NhdsSet
hasBasis_nhdsSet_Iic_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] (a : α)
  [h : Nonempty ↑(Set.Ioi a)], (nhdsSet (Set.Iic a)).HasBasis (fun x => a < x) Set.Iio
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instBoundedOrder : {V : Type u} → {G : SimpleGraph V} → BoundedOrder G.Subgraph
-- Lean.DocString.Types
Lean.Doc.ListItem.mk.injEq : ∀ {α : Type u} (contents contents_1 : Array α),
  ({ contents := contents } = { contents := contents_1 }) = (contents = contents_1)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.linearMap_ext : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f g : MvPolynomial σ R →ₗ[R] M},
  (∀ (s : σ →₀ ℕ), f ∘ₗ MvPolynomial.monomial s = g ∘ₗ MvPolynomial.monomial s) → f = g
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instPartialOrderOpenAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenAddSubgroup.instPartialOrderOpenAddSubgroup = inferInstance
-- Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
/-- For a complete normed ring `R`, the embedding of the units `Rˣ` into `R` is a `C^n` map between
manifolds.  -/
Units.contMDiff_val : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {n : WithTop ℕ∞} {𝕜 : Type u_2}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAlgebra 𝕜 R],
  ContMDiff (modelWithCornersSelf 𝕜 R) (modelWithCornersSelf 𝕜 R) n Units.val
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailStateTOfNonempty : {σ : Type u} →
  {m : Type u → Type v} → [inst : Monad m] → [Lean.Order.MonadTail m] → [Nonempty σ] → Lean.Order.MonadTail (StateT σ m)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- Auxiliary function for `trans_refl_reparam`.  -/
Path.Homotopy.transReflReparamAux : ↑unitInterval → ℝ
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_leftUnitor_hom_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  (f : a ⟶ b), (CategoryTheory.Bicategory.leftUnitor f).hom.1 = (CategoryTheory.Bicategory.leftUnitor f.1).hom
-- Mathlib.Data.List.Chain
List.isChain_cons_pmap_of_isChain_cons : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {S : β → β → Prop} {p : α → Prop} {f : (a : α) → p a → β},
  (∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)) →
    ∀ {l : List α} {a : α} (ha : p a),
      List.IsChain R (a :: l) → ∀ (hl₂ : ∀ a ∈ l, p a), List.IsChain S (f a ha :: List.pmap f l hl₂)
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.unit_tensor_d₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_6 : AddMonoid I] {c : ComplexShape I} [inst_7 : c.TensorSigns] (K : HomologicalComplex C c)
  [inst_8 : DecidableEq I]
  [inst_9 :
    ∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  (i₁ i₂ j : I),
  HomologicalComplex.mapBifunctor.d₁ (HomologicalComplex.tensorUnit C c) K
      (CategoryTheory.MonoidalCategory.curriedTensor C) c i₁ i₂ j =
    0
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- This is a linear map version of `SeparatingDual.exists_ne_zero` in a projective module.  -/
Module.Projective.exists_dual_ne_zero : ∀ {V : Type uV} [inst : AddCommMonoid V] (R : Type u_1) [inst_1 : Semiring R] [inst_2 : Module R V]
  [Module.Projective R V] {x : V}, x ≠ 0 → ∃ f, f x ≠ 0
-- Mathlib.Analysis.Distribution.FourierMultiplier
/-- Fourier multiplier on tempered distributions.  -/
TemperedDistribution.fourierMultiplierCLM : {E : Type u_3} →
  (F : Type u_4) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : InnerProductSpace ℝ E] →
          [inst_3 : NormedSpace ℂ F] →
            [FiniteDimensional ℝ E] →
              [inst_5 : MeasurableSpace E] →
                [BorelSpace E] → (E → ℂ) → TemperedDistribution E F →L[ℂ] TemperedDistribution E F
-- Mathlib.Tactic.Linter.OldObtain
/-- The `oldObtain` linter emits a warning upon uses of the "stream-of-consciousness" variants
of the `obtain` tactic, i.e. with the proof postponed.  -/
Mathlib.Linter.Style.linter.oldObtain : Lean.Option Bool
-- Std.Data.ExtDTreeMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.getThenInsertIfNew? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        [Std.LawfulEqCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) → β a → Option (β a) × Std.ExtDTreeMap α β cmp
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.spine_spineToSimplex_apply : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (f : X.Path m),
  X.spine m h (sx.spineToSimplex m h f) = f
-- Mathlib.Analysis.Normed.Module.Basic
norm_natCast_eq_mul_norm_one : ∀ (α : Type u_6) [inst : SeminormedRing α] [NormSMulClass ℤ α] (n : ℕ), ‖↑n‖ = ↑n * ‖1‖
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.probabilitymeasure_of_probabilitymeasures_mconv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M) [MeasurableMul₂ M]
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν],
  MeasureTheory.IsProbabilityMeasure (μ.mconv ν)
-- Mathlib.Data.Nat.Order.Lemmas
Nat.Subtype.orderBot : (s : Set ℕ) → [DecidablePred fun x => x ∈ s] → [h : Nonempty ↑s] → OrderBot ↑s
-- Mathlib.Topology.MetricSpace.Holder
/-- **Alias** of the reverse direction of `HolderWith.restrict_iff`. -/
HolderOnWith.holderWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C r f s → HolderWith C r (s.domRestrict f)
-- Mathlib.NumberTheory.Pell
/-- A power of a fundamental solution is never equal to the negative of a power of this
fundamental solution.  -/
Pell.IsFundamental.zpow_ne_neg_zpow : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → ∀ {n n' : ℤ}, a ^ n ≠ -a ^ n'
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.commShiftIso_add : ∀ {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} (F : CategoryTheory.Functor C D) {A : Type u_6} {inst_2 : AddMonoid A}
  {inst_3 : CategoryTheory.HasShift C A} {inst_4 : CategoryTheory.HasShift D A} [self : F.CommShift A] (a b : A),
  CategoryTheory.Functor.commShiftIso F (a + b) =
    CategoryTheory.Functor.CommShift.isoAdd (CategoryTheory.Functor.commShiftIso F a)
      (CategoryTheory.Functor.commShiftIso F b)
-- Mathlib.Order.Disjoint
IsCompl.le_left_iff : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl x y → (z ≤ x ↔ Disjoint z y)
-- Mathlib.Data.Matrix.Mul
Matrix.submatrix_vecMul_equiv : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : l → α) (e₁ : l ≃ m) (e₂ : o → n),
  Matrix.vecMul v (M.submatrix (⇑e₁) e₂) = Matrix.vecMul (v ∘ ⇑e₁.symm) M ∘ e₂
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.prod_mk : ∀ {α : Type u_4} {β : Type u_5} [inst : Monoid α] [inst_1 : Monoid β] {a : α} {b : β},
  IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.foldM_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Monad o] [LawfulMonad o] [inst_10 : Std.IteratorLoop α m n]
  [inst_11 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o]
  [inst_14 : MonadLiftT m n] [inst_15 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n γ}
  {g : δ → γ → o δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.foldM g init (Std.IterM.mapM f it) =
    Std.IterM.foldM
      (fun d b => do
        let c ← liftM (f b)
        g d c)
      init it
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (V W : E → E) (s : Set E) (x : E),
  VectorField.lieBracketWithin 𝕜 V W s x = (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x)
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
rieszContentAux.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  (K : TopologicalSpace.Compacts X), rieszContentAux Λ K = sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inl_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.CategoryStruct.comp self.inl self.snd = 0
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_setOfPred_prime : schnirelmannDensity (Set.ofPred Nat.Prime) = 0
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_pow_eq_top : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [I.IsTwoSided] {n : ℕ}, I ⊔ J = ⊤ → I ⊔ J ^ n = ⊤
-- Mathlib.NumberTheory.NumberField.House
NumberField.house.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α α_1 : K),
  α = α_1 → NumberField.house α = NumberField.house α_1
-- Mathlib.Computability.RecursiveIn
/-- A binary total function is computable in `O`.  -/
ComputableIn₂ : {α : Type u_5} →
  {β : Type u_6} →
    {σ : Type u_7} → [Primcodable α] → [Primcodable β] → [Primcodable σ] → Set (ℕ →. ℕ) → (α → β → σ) → Prop
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_empty_right : ∀ {α : Type u_2} (s : Finset α), Disjoint s ∅
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPPrepend.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (acc : List α) (h_1 : (acc : List α) → motive [] acc)
  (h_2 : (a : α) → (t acc : List α) → motive (a :: t) acc),
  (match [], acc with
    | [], acc => h_1 acc
    | a :: t, acc => h_2 a t acc) =
    h_1 acc
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.cosZeta_eq : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.cosZeta a s = (HurwitzZeta.expZeta a s + HurwitzZeta.expZeta (-a) s) / 2
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.ulift : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Flat R M],
  Module.Flat R (ULift.{v', v} M)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.uncurry_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C × D),
  (CategoryTheory.Functor.uncurry.obj F).obj X = (F.obj X.1).obj X.2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂)[k] = m₁[k]
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda₀_mapComp_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b c : Bᵒᵖ} (f : a ⟶ b) (g : b ⟶ c)
  (X : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda₀ x).mapComp f g).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop f.unop X).hom
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
SeparationQuotient.liftNormedAddGroupHom_normNoninc : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (f : NormedAddGroupHom M N) (hf : ∀ (s : M), ‖s‖ = 0 → f s = 0),
  f.NormNoninc → (SeparationQuotient.liftNormedAddGroupHom f hf).NormNoninc
-- Mathlib.Analysis.Convex.Intrinsic
AffineIsometry.intrinsicClosure_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : SeminormedAddCommGroup W] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : MetricSpace P] [inst_6 : PseudoMetricSpace Q] [inst_7 : NormedAddTorsor V P]
  [inst_8 : NormedAddTorsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : Set P), intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 s
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.add_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Add A] (M N : CStarMatrix m n A) (i : m) (j : n),
  (M + N) i j = M i j + N i j
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- The `support` of a walk is the list of vertices it visits in order.  -/
SimpleGraph.Walk.support : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → List V
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.aestronglyMeasurable_condExpL1CLM : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  [inst_3 : CompleteSpace F'] (f : ↥(MeasureTheory.Lp F' 1 μ)),
  MeasureTheory.AEStronglyMeasurable (↑↑((MeasureTheory.condExpL1CLM F' hm μ) f)) μ
-- Mathlib.SetTheory.Cardinal.Arithmetic
/-- This lemma makes lemmas assuming `Infinite α` applicable to the situation where we have
`Infinite β` instead.  -/
Cardinal.mk_equiv_comm : ∀ {α : Type u} {β' : Type v}, Cardinal.mk (α ≃ β') = Cardinal.mk (β' ≃ α)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Build an isomorphism in the category `AddGrpCat` from an `AddEquiv` between `AddGroup`s.  -/
AddEquiv.toAddGrpIso : {X Y : AddGrpCat} → ↑X ≃+ ↑Y → (X ≅ Y)
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series of `f`
converges everywhere pointwise to `f`.  -/
UnitAddTorus.hasSum_mFourier_series_apply_of_summable : ∀ {d : Type u_1} [inst : Fintype d] {f : C(UnitAddTorus d, ℂ)},
  Summable (UnitAddTorus.mFourierCoeff ⇑f) →
    ∀ (x : UnitAddTorus d), HasSum (fun i => UnitAddTorus.mFourierCoeff (⇑f) i • (UnitAddTorus.mFourier i) x) (f x)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_subset_Ioo_right : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₂ < a₁ → Set.Ioc b a₂ ⊆ Set.Ioo b a₁
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opUnopEquiv_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Functor.opUnopEquiv C D).functor = CategoryTheory.Functor.opHom C D
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.not_boundaryLE_prev : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff]
  {i j : ι}, c.Rel i j → ¬e.BoundaryLE i
-- Mathlib.Order.Lattice
inf_sup_le : ∀ {α : Type u} [inst : DistribLattice α] {x y z : α}, x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ x ⊓ z
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.instEpiMapFourδ₄Toδ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ : ι}
  (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₁ n₂ n₃ : ℤ) (hn₂ : n₁ + 1 = n₂) (hn₃ : n₂ + 1 = n₃),
  CategoryTheory.Epi
    (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Flat R ↥A],
      (∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b) → Function.Injective ⇑(algebraMap R S) → Module.rank R ↥(A ⊓ B) = 1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_bot : ∀ {V : Type u_1}, ⊥.edgeFinset = ∅
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_f : ∀ (X : AlgebraicGeometry.Scheme) (U : X.AffineZariskiSite),
  (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X).f U = (↑U).ι
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.extraction_of_eventually_atTop : ∀ {P : ℕ → Prop}, (∀ᶠ (n : ℕ) in Filter.atTop, P n) → ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
-- Mathlib.Algebra.Module.FinitePresentation
instFinitePresentationLocalizationLocalizedModule : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submonoid R)
  [Module.FinitePresentation R M], Module.FinitePresentation (Localization S) (LocalizedModule S M)
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.of_dense : ∀ {α : Type u_1} [inst : LT α] [DenselyOrdered α] (a : α), Order.IsPredPrelimit a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.diff_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ m₄ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ \ m₂).Equiv (m₃ \ m₄)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Eta-expanded form of `contDiffWithinAt_id` -/
contDiffWithinAt_fun_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {s : Set E} {x : E}, ContDiffWithinAt 𝕜 n (fun x => x) s x
-- Mathlib.RingTheory.RingInvo
RingInvo.involution : ∀ {R : Type u_2} [inst : Semiring R] (f : RingInvo R) (x : R), MulOpposite.unop (f (MulOpposite.unop (f x))) = x
-- Init.Data.List.MapIdx
List.mapIdx_eq_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β}, List.mapIdx f l = l.mapFinIdx fun i a x => f i a
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- `Over.map f` is left adjoint to `Over.pullback f`.  -/
CategoryTheory.Over.mapPullbackAdj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f] →
          CategoryTheory.Over.map f ⊣ CategoryTheory.Over.pullback f
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.pred_succ : ∀ (o : Ordinal.{u_4}), (Order.succ o).pred = o
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.update_zero_eq_erase : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α),
  f.update a 0 = (SkewMonoidAlgebra.erase a) f
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_append_toList_roc : ∀ {l m n : ℤ}, l ≤ m → m ≤ n → (l<...=m).toList ++ (m<...=n).toList = (l<...=n).toList
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.isBasis' : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → M.IsBasis' I X
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_zpow : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Group (G i)] [inst_3 : ∀ (i : ι), SubgroupClass (S i) (G i)] (i : ι)
  (r : G i) (n : ℤ), RestrictedProduct.mulSingle A i (r ^ n) = RestrictedProduct.mulSingle A i r ^ n
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.prod_obj : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) (Δ : SimplexCategoryᵒᵖ),
  (A.prod B).obj Δ = (A.obj Δ).prod (B.obj Δ)
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.mk : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ⊤.FG → Algebra.FiniteType R A
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.orthogonal_eq_top_iff : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V} {W : Submodule K V},
  B.IsRefl → (B.restrict W).Nondegenerate → (B.orthogonal W = ⊤ ↔ W = ⊥)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.toPiLocalizationEquiv_apply_apply : ∀ (R : Type u) [inst : CommSemiring R] [inst_1 : DiscreteTopology (PrimeSpectrum R)] (x : R) (I : PrimeSpectrum R),
  (PrimeSpectrum.toPiLocalizationEquiv R) x I = (algebraMap R (Localization I.asIdeal.primeCompl)) x
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.RestrictScalars.instLieRingRestrictScalars : (R : Type u_1) → (A : Type u_2) → (L : Type u_3) → [h : LieRing L] → LieRing (RestrictScalars R A L)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- `M →ₗ[R] N` is the type of `R`-linear maps from `M` to `N`.  -/
«term_→ₗ[_]_» : Lean.TrailingParserDescr
-- Init.Classical
Classical.choose_spec : ∀ {α : Sort u} {p : α → Prop} (h : ∃ x, p x), p (Classical.choose h)
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.leftUnitor'_inv_comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_6 : AddMonoid I] {c : ComplexShape I} [inst_7 : c.TensorSigns] (K : HomologicalComplex C c)
  [inst_8 : DecidableEq I]
  [inst_9 :
    ∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  (i j : I),
  CategoryTheory.CategoryStruct.comp (K.leftUnitor'.inv i) (((HomologicalComplex.tensorUnit C c).tensorObj K).d i j) =
    CategoryTheory.CategoryStruct.comp (K.d i j) (K.leftUnitor'.inv j)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S.eq_1 : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F) (f : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.SimpleFunc.setToL1S T f =
    MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- The localization functor `HomotopyCategory.Plus C ⥤ DerivedCategory.Plus C`.  -/
DerivedCategory.Plus.Qh : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Functor (HomotopyCategory.Plus C) (DerivedCategory.Plus C)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNeg.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Neg Y],
  LocallyConstant.instNeg = { neg := fun f => { toFun := -⇑f, isLocallyConstant := ⋯ } }