mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Init
/-- Define a linter set of all mathlib syntax linters which are enabled by default.

Projects depending on mathlib can use `set_option linter.mathlibStandardSet true` to enable
all these linters, or add the `weak.linter.mathlibStandardSet` option to their lakefile.
 -/
linter.mathlibStandardSet : Lean.Option Bool
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.inf_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S T : CategoryTheory.SubmonoidFunctor M) (x : C), (Lattice.inf S T).obj x = S.obj x ⊓ T.obj x
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.instInhabitedQuotientSubgroup.eq_1 : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), QuotientGroup.instInhabitedQuotientSubgroup s = { default := ↑1 }
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- Finite inductive type extending `Mathlib.Ineq`: a type of inequality (`eq`, `le` or `lt`),
together with, in the case of `lt`, a Boolean, typically representing the strictness (< or ≤) of
some other inequality.  -/
Mathlib.Ineq.WithStrictness : Type
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_ofNonUnitalStarAlgHom : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁]
  [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁] [inst_4 : NonUnitalNonAssocSemiring A₂]
  [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂] (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁)
  (h₁ : g.comp f = NonUnitalStarAlgHom.id R A₁) (h₂ : f.comp g = NonUnitalStarAlgHom.id R A₂),
  (StarAlgEquiv.ofNonUnitalStarAlgHom f g h₁ h₂).symm = StarAlgEquiv.ofNonUnitalStarAlgHom g f h₂ h₁
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k : α} {v : β}, Std.ExtDTreeMap.Const.get! (t.insert k v) k = v
-- Mathlib.RingTheory.DividedPowers.Basic
/-- The canonical `DividedPowers` structure on the zero ideal  -/
dividedPowersBot : (A : Type u_1) → [inst : CommSemiring A] → DividedPowers ⊥
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- The function given in the definition of `torusIntegral` is integrable.  -/
TorusIntegrable.function_integrable : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ}
  [inst_1 : NormedSpace ℂ E],
  TorusIntegrable f c R →
    MeasureTheory.IntegrableOn
      (fun θ => (∏ i, ↑(R i) * Complex.exp (↑(θ i) * Complex.I) * Complex.I) • f (torusMap c R θ))
      (Set.Icc 0 fun x => 2 * Real.pi) MeasureTheory.volume
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_ofNat_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocMod hp (a - OfNat.ofNat m * p) b = toIocMod hp a b - OfNat.ofNat m * p
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.Nondegenerate.mul_iff_right : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : CommRing A] [IsDomain A] {M N : Matrix n n A},
  N.Nondegenerate → ((M * N).Nondegenerate ↔ M.Nondegenerate)
-- Mathlib.NumberTheory.LSeries.RiemannZeta
completedRiemannZeta.eq_1 : ∀ (s : ℂ), completedRiemannZeta s = HurwitzZeta.completedHurwitzZetaEven 0 s
-- Mathlib.CategoryTheory.Sites.Point.Conservative
/-- Let `P : ObjectProperty J.Point` a family of points of a
site `(C, J)`). We say that it is a conservative family of points
if the corresponding fiber functors `Sheaf J (Type w) ⥤ Type w`
jointly reflect isomorphisms.  -/
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → CategoryTheory.ObjectProperty J.Point → Prop
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Ordered.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering), RBTree.RBNode.Path.Ordered cmp RBTree.RBNode.Path.root = True
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
/-- Given a family of objects `U : ι → C`, this is the Cech complex functor
`(Cᵒᵖ ⥤ A) ⥤ CochainComplex A ℕ` which sends a presheaf `P : Cᵒᵖ ⥤ A` to the
cochain complex which in degree `n` consists of the product,
indexed by `x : Fin (n + 1) → ι`, of the value of `P` on the product of the
objects `U (x i)` for `i : Fin (n + 1)`.  -/
CategoryTheory.cechComplexFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        [CategoryTheory.Limits.HasProducts A] →
          [CategoryTheory.Limits.HasFiniteProducts C] →
            [inst_4 : CategoryTheory.Preadditive A] →
              {ι : Type w} → (ι → C) → CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CochainComplex A ℕ)
-- Mathlib.CategoryTheory.Action.Basic
/-- Auxiliary definition for `functorCategoryEquivalence`.  -/
Action.FunctorCategoryEquivalence.functor : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] → CategoryTheory.Functor (Action V G) (CategoryTheory.Functor (CategoryTheory.SingleObj G) V)
-- Mathlib.Computability.Primrec.Basic
Primrec₂.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  (f : α → β → σ), Primrec₂ f = Primrec fun p => f p.1 p.2
-- Mathlib.Geometry.Manifold.PoincareConjecture
_private.Mathlib.Geometry.Manifold.PoincareConjecture.0.SimplyConnectedSpace.nonempty_homeomorph_sphere_three : (M : Type u_1) →
  [inst : TopologicalSpace M] →
    [T2Space M] →
      [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] →
        [SimplyConnectedSpace M] → [CompactSpace M] → ProofWanted (Nonempty (M ≃ₜ ↑(Metric.sphere 0 1)))
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rTensor_surjective_iff : ∀ {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] [Module.Invertible R M] {f : N →ₗ[R] P},
  Function.Surjective ⇑(LinearMap.rTensor M f) ↔ Function.Surjective ⇑f
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_surjective : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b), Function.Surjective (Set.projIcc a b h)
-- Mathlib.CategoryTheory.Sites.LeftExact
/-- `plusPlusSheaf` is isomorphic to an arbitrary choice of left adjoint.  -/
CategoryTheory.plusPlusSheafIsoPresheafToSheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type w) →
        [inst_1 : CategoryTheory.Category.{t, w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              {FD : D → D → Type u_1} →
                {CD : D → Type t} →
                  [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                    [inst_5 : CategoryTheory.ConcreteCategory D FD] →
                      [inst_6 :
                          ∀ (X : C),
                            CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] →
                        [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] →
                          [inst_8 :
                              ∀ {X : C} (S : J.Cover X),
                                CategoryTheory.Limits.PreservesLimitsOfShape
                                  (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] →
                            CategoryTheory.plusPlusSheaf J D ≅ CategoryTheory.presheafToSheaf J D
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.row_eq_self : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.row = Matrix.of.symm A
-- Mathlib.Algebra.Category.MonCat.Limits
/-- A choice of limit cone for a functor into `AddCommMonCat`.
(Generally, you'll just want to use `limit F`.)  -/
AddCommMonCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommMonCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- The product of two finite groups is cyclic iff
both of them are cyclic and their orders are coprime.  -/
Group.isCyclic_prod_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : Group M] [inst_1 : Group N],
  IsCyclic (M × N) ↔ IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_lt_right_iff_lt : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedRing k] [inst_3 : AddCommGroup E]
  [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k}
  [PosSMulReflectLT k E], r < 1 → ((AffineMap.lineMap a b) r < b ↔ a < b)
-- Mathlib.Logic.Hydra
Relation.cutExpand_single_add : ∀ {α : Type u_1} {r : α → α → Prop} {a' a : α}, r a' a → ∀ (s : Multiset α), Relation.CutExpand r ({a'} + s) ({a} + s)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- `p ∈ M` is a boundary point of a manifold `M` if and only if its image in the extended chart
lies on the boundary of the model space.  -/
ModelWithCorners.IsBoundaryPoint : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H → {M : Type u_4} → [inst : TopologicalSpace M] → [ChartedSpace H M] → M → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_strictMap_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D), (⊤.strictMap F).inverseImage F = ⊤
-- Mathlib.GroupTheory.Coset.Basic
mem_own_leftAddCoset : ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) (a : α), a ∈ a +ᵥ ↑s
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_inc : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β}, (G.restrict F).Inc e x ↔ G.Inc e x ∧ e ∈ F
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → t.getThenInsertIfNew? a b = t_1.getThenInsertIfNew? a b_1
-- Mathlib.Analysis.Convex.Join
convexJoin_iUnion_left : ∀ {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s : ι → Set E) (t : Set E), convexJoin 𝕜 (⋃ i, s i) t = ⋃ i, convexJoin 𝕜 (s i) t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_maxKeyD_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, k ∈ t → ∀ {fallback : α}, (compare k (t.maxKeyD fallback)).isLE = true
-- Std.Http.Transport
/-- Receives data from a channel, joining all available data up to the expected size. First does a
blocking recv, then greedily consumes available data with tryRecv until `expect` bytes are reached.
 -/
Std.Http.Internal.Mock.recvJoined : Std.CloseableChannel ByteArray → Option UInt64 → Std.Async.Async (Option ByteArray)
-- Init.Data.Iterators.Basic
Std.IterM.isPlausibleSuccessorOf_of_skip : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it it' : Std.IterM m β},
  it.IsPlausibleStep (Std.IterStep.skip it') → it'.IsPlausibleSuccessorOf it
-- Init.Data.List.Lemmas
List.ne_nil_iff_length_pos : ∀ {α : Type u_1} {l : List α}, l ≠ [] ↔ 0 < l.length
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The fully faithful embedding of `LightProfinite` in `Profinite`.  -/
lightToProfinite : CategoryTheory.Functor LightProfinite Profinite
-- Mathlib.GroupTheory.Coprod.Basic
/-- A `MulEquiv` version of `Coprod.swap`.  -/
MulEquiv.coprodComm : (M : Type u_1) →
  (N : Type u_2) → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → Monoid.Coprod M N ≃* Monoid.Coprod N M
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.instIsAffineToSchemeValOpensMemSetAffineOpens : ∀ {Y : AlgebraicGeometry.Scheme} (U : ↑Y.affineOpens), AlgebraicGeometry.IsAffine ↑↑U
-- Mathlib.Data.Real.Basic
Real.zero_lt_one : 0 < 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.ofMul_eq_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α] {a : α}, Additive.ofMul a = ⊤ ↔ a = ⊤
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcUnits_zpow : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p]
  [inst_10 : ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℤ)
  (hf : autoParam (ContinuousOn f (spectrum R a)) cfcUnits_zpow._auto_1) (ha : autoParam (p a) cfcUnits_zpow._auto_3),
  cfcUnits f a hf' hf ha ^ n = cfcUnits (f ^ n) a ⋯ ⋯ ha
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.id_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.id f =
    CategoryTheory.CatEnrichedOrdinary.Hom.mk
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CatEnrichedOrdinary.homEquiv f))
-- Mathlib.RingTheory.Adjoin.PowerBasis
/-- Let `B : PowerBasis S A` be such that `IsIntegral R B.gen`, and let `x : A` be an element
with integral coordinates in the base `B.basis`. Then `IsIntegral R ((B.basis.repr (x ^ n) i)` for
all `i` and all `n` if `minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)`. This is the case
if `R` is a GCD domain and `S` is its fraction ring.  -/
PowerBasis.repr_pow_isIntegral : ∀ {S : Type u_2} [inst : CommRing S] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Algebra R S] {A : Type u_4}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : PowerBasis S A},
  IsIntegral R B.gen →
    ∀ {x : A},
      (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
        minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen) →
          ∀ (n : ℕ) (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)
-- Init.Control.Lawful.MonadLift.Instances
ReaderT.instLawfulMonadLift : ∀ {m : Type u → Type v} [inst : Monad m] {ρ : Type u}, LawfulMonadLift m (ReaderT ρ m)
-- Mathlib.Order.Circular
/-- A circular partial order is the analogue of a partial order where you can loop around. `≤` and
`<` are replaced by ternary relations `btw` and `sbtw`. `btw` is reflexive, cyclic and
antisymmetric. `sbtw` is transitive.  -/
CircularPartialOrder : Type u_1 → Type u_1
-- Mathlib.Topology.CWComplex.Classical.Basic
_private.Mathlib.Topology.CWComplex.Classical.Basic.0.Topology.CWComplex.OfDiscreteClosed.match_3.splitter : {X : Type u_1} →
  {D : Set X} →
    (motive :
        (n : ℕ) →
          (match n with
            | 0 => ↑D
            | n.succ => PEmpty.{u_1 + 1}) →
            Sort u_2) →
      (n : ℕ) →
        (i :
            match n with
            | 0 => ↑D
            | n.succ => PEmpty.{u_1 + 1}) →
          ((i :
                match 0 with
                | 0 => ↑D
                | n.succ => PEmpty.{u_1 + 1}) →
              motive 0 i) →
            ((n : ℕ) →
                (i :
                    match n + 1 with
                    | 0 => ↑D
                    | n.succ => PEmpty.{u_1 + 1}) →
                  motive n.succ i) →
              motive n i
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_eq_of_equiv : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {H : G.Subgraph} (h : ↑(G.neighborSet v) ≃ ↑(H.neighborSet v)),
  (G.neighborSet v).Finite → H.neighborSet v = G.neighborSet v
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- Two open immersions with equal range are isomorphic.  -/
AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq : {X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      [H : AlgebraicGeometry.IsOpenImmersion f] →
        [AlgebraicGeometry.IsOpenImmersion g] → Set.range ⇑f = Set.range ⇑g → (X ≅ Y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableWithinAt.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt ℂ f s x → DifferentiableWithinAt ℂ (fun x => Complex.cos (f x)) s x
-- Batteries.Data.Fin.OfBits
Fin.val_ofBits : ∀ {n : ℕ} (f : Fin n → Bool), ↑(Fin.ofBits f) = Nat.ofBits f
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₆_det : CartanMatrix.E₆.det = 3
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.uset.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i : ℕ) (y : Lean.FVarId) (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_9) (fvarId_1 : Lean.FVarId)
  (i_1 : ℕ) (y_1 : Lean.FVarId) (k_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_9),
  (Lean.Compiler.LCNF.Code.uset fvarId i y k h = Lean.Compiler.LCNF.Code.uset fvarId_1 i_1 y_1 k_1 h_1) =
    (fvarId = fvarId_1 ∧ i = i_1 ∧ y = y_1 ∧ k = k_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_sub_pi_div_two : ∀ (x : ℝ), Real.sin (x - Real.pi / 2) = -Real.cos x
-- Mathlib.GroupTheory.Coset.Basic
/-- If `s ≤ t`, then there is a map `H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H`.  -/
Subgroup.quotientSubgroupOfMapOfLE : {α : Type u_1} →
  [inst : Group α] → {s t : Subgroup α} → (H : Subgroup α) → s ≤ t → ↥H ⧸ s.subgroupOf H → ↥H ⧸ t.subgroupOf H
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If `C` is cofiltered, and we have a left adjoint functor `L : C ⥤ D`, then `D` is cofiltered.  -/
CategoryTheory.IsCofiltered.of_isLeftAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (L : CategoryTheory.Functor C D) [L.IsLeftAdjoint],
  CategoryTheory.IsCofiltered D
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.continuousOn_rpowIntegrand₀₁ : ∀ {p x : ℝ}, p ∈ Set.Ioo 0 1 → 0 ≤ x → ContinuousOn (fun x_1 => p.rpowIntegrand₀₁ x_1 x) (Set.Ioi 0)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instRegularSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [RegularSpace α], RegularSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.isIso_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), S.g = 0 → CategoryTheory.IsIso h.i
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.nerve C).map f = TypeCat.ofHom fun x => x.whiskerLeft (SimplexCategory.toCat.map f.unop).toFunctor
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.π_comp_map_apply : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M) (x : relations.R →₀ A), solution.π (relations.map x) = 0
-- Init.Core
Not.intro : ∀ {a : Prop}, (a → False) → ¬a
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] (Q : CategoryTheory.ObjectProperty Cᵒᵖ),
  Q.IsClosedUnderLimitsOfShape J ↔ Q.unop.IsClosedUnderColimitsOfShape Jᵒᵖ
-- Mathlib.Data.Multiset.Fintype
Multiset.exists_coe : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} (p : m.ToType → Prop), (∃ x, p x) ↔ ∃ x i, p ⟨x, i⟩
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
/-- The equivalence `Mon (Type u) ≌ MonCat.{u}`
is naturally compatible with the forgetful functors to `Type u`.
 -/
monTypeEquivalenceMonForget : MonTypeEquivalenceMon.functor.comp (CategoryTheory.forget MonCat) ≅ CategoryTheory.Mon.forget (Type u)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that the action of `M` on `α` has `MeasurableVAdd` if for each `c` the map `x ↦ c +ᵥ x`
is a measurable function and for each `x` the map `c ↦ c +ᵥ x` is a measurable function.  -/
MeasurableVAdd : (M : Type u_2) → (α : Type u_3) → [VAdd M α] → [MeasurableSpace M] → [MeasurableSpace α] → Prop
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_inv_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y').HasMap
      p]
  {Z : CategoryTheory.GradedObject J D}
  (h : CategoryTheory.GradedObject.mapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.mapBifunctorMapMap F p
          (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
        h)
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- When we have `[CommSemiring R]`, the function `C` is the same as `algebraMap R R[X]`.

(But note that `C` is defined when `R` is not necessarily commutative, in which case
`algebraMap` is not available.)
 -/
Polynomial.C_eq_algebraMap : ∀ {R : Type u} [inst : CommSemiring R] (r : R), Polynomial.C r = (algebraMap R (Polynomial R)) r
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.monotone_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D), Monotone fun x => x.map F
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessResult.kind : Lean.Meta.PreprocessResult✝ → Lean.Meta.PreprocessKind✝
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.ne_zero_of_ortho : ∀ {R : Type u} {M : Type v} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M] {x : M}
  {N : Submodule R M}, (∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) → x ≠ 0