mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.mem_basicOpen_top : ∀ (X : AlgebraicGeometry.Scheme) (f : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↥X),
  x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) f)
-- Mathlib.Data.Finsupp.Defs
Finsupp.fun_support_eq : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (f : α →₀ M), Function.support ⇑f = ↑f.support
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
/-- Let `K` be an object in the bounded below derived category of an abelian category `C`
with enough injectives. Assume that `K` is cohomologically `≥ n`. Then, `K`
admits an "injective resolution", in the sense that there exists a cochain
complex `L` consisting of injective object and lying in degrees `≥ n`, such that `K`
is isomorphic to the image of `L`.  -/
DerivedCategory.Plus.exists_injective_nonempty_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] [CategoryTheory.EnoughInjectives C] (K : DerivedCategory.Plus C) (n : ℤ) [K.IsGE n],
  ∃ L,
    ∃ (_ : L.obj.IsStrictlyGE n),
      Nonempty (DerivedCategory.Plus.Q.obj ((CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus.obj L) ≅ K)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- Variant of `Real.rpow_add'` that avoids having to prove `y + z = w` twice.  -/
Real.rpow_of_add_eq : ∀ {w x y z : ℝ}, 0 ≤ x → w ≠ 0 → y + z = w → x ^ w = x ^ y * x ^ z
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.top_ne_natCast : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ), ⊤ ≠ ↑n
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsSlice.exists_isSemilinearSet_setOfPred_le : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelAddMonoid M]
  [CanonicallyOrderedAdd M] {s : Set M}, IsSlice✝ s → s.Nonempty → ∃ x ∈ s, IsSemilinearSet {y | y ∈ s ∧ x ≤ y}
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.decidableLE.match_1.eq_3 : ∀ {α : Type u_1} (motive : WithTop α → WithTop α → Sort u_2) (a b : α) (h_1 : (x : WithTop α) → motive none x)
  (h_2 : (a : α) → motive (some a) none) (h_3 : (a b : α) → motive (some a) (some b)),
  (match some a, some b with
    | none, x => h_1 x
    | some a, none => h_2 a
    | some a, some b => h_3 a b) =
    h_3 a b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k k' fallback : α} {f : β → β},
  (Std.ExtDTreeMap.Const.modify t k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.toSkeleton_eq_toSkeleton_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C},
  CategoryTheory.toSkeleton X = CategoryTheory.toSkeleton Y ↔ Nonempty (X ≅ Y)
-- Mathlib.Order.LiminfLimsup
Filter.liminf_eq_iSup_iInf_of_nat' : ∀ {α : Type u_1} [inst : CompleteLattice α] {u : ℕ → α}, Filter.liminf u Filter.atTop = ⨆ n, ⨅ i, u (i + n)
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_eq_of_subset_right : ∀ {α : Type u_1} (t : Set α) {s₁ s₂ : Set α}, s₂ ⊆ s₁ → t.ite s₁ s₂ = s₁ ∩ t ∪ s₂
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.Map.Arrows.im : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  {φ : CategoryTheory.Functor C D} {hφ : Function.Injective φ.obj} {S : CategoryTheory.Subgroupoid C} {c d : C},
  ∀ f ∈ S.arrows c d, CategoryTheory.Subgroupoid.Map.Arrows φ hφ S (φ.obj c) (φ.obj d) (φ.map f)
-- Init.Data.AC
Lean.Data.AC.Context.eval_norm : ∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α) (e : Lean.Data.AC.Expr),
  Lean.Data.AC.evalList α ctx (Lean.Data.AC.norm ctx e) = Lean.Data.AC.eval α ctx e
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
/-- Define a right action of `Cᵒᵖ` on `Dᵒᵖ` from a right action of `C` on `D` via
the formula `(op d) ⊙ᵣ (op c) = op (d ⊙ᵣ c)`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
            CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- Both diagonal entries of an invertible upper-block-triangular matrix are invertible (by reading
off the diagonal entries of the inverse).  -/
Matrix.invertibleOfFromBlocksZero₂₁Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (B : Matrix m n α) →
                    (D : Matrix n n α) → [Invertible (Matrix.fromBlocks A B 0 D)] → Invertible A × Invertible D
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.nonempty' : ∀ {α : Type u_4} [inst : TopologicalSpace α] (self : TopologicalSpace.NonemptyCompacts α), self.carrier.Nonempty
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.toContinuousMultilinearMap_curryLeft : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E), (f.curryLeft x).toContinuousMultilinearMap = f.curryLeft x
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedAddGroup.mem_closure_iff : ∀ {E : Type u_4} [inst : SeminormedAddGroup E] {s : Set E} {a : E},
  a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖-a + b‖ < ε
-- Mathlib.Topology.Constructions.SumProd
interior_prod_eq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X) (t : Set Y),
  interior (s ×ˢ t) = interior s ×ˢ interior t
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.mk_add_mk : ∀ {K : Type u_1} [inst : Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K),
  ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
-- Mathlib.Topology.Homotopy.Lifting
/-- A covering map induces an injection on all Hom-sets of the fundamental groupoid,
in particular on the fundamental group. The first part of Proposition 1.31 of [hatcher02].  -/
IsCoveringMap.injective_path_homotopic_map : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) (e₀ e₁ : E), Function.Injective fun γ => γ.map { toFun := p, continuous_toFun := ⋯ }
-- Mathlib.Analysis.Calculus.Deriv.Basic
DifferentiableAt.derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  DifferentiableAt 𝕜 f x → UniqueDiffWithinAt 𝕜 s x → derivWithin f s x = deriv f x
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.naturality_1 : ∀ {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),
  CategoryTheory.CategoryStruct.comp (α.inv.app X) (CategoryTheory.CategoryStruct.comp (F.map f) (α.hom.app Y)) =
    G.map f
-- Mathlib.Algebra.Category.MonCat.Shrink
/-- The natural transformation `MonCat.shrinkFunctor.{w} F ⟶ MonCat.shrinkFunctor.{w} G`
induces by a natural transformation `τ : F ⟶ G` between `w`-small functors to monoids.  -/
MonCat.shrinkFunctorMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C MonCat} →
      (F ⟶ G) →
        [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] →
          [inst_2 : ∀ (X : C), Small.{w, w'} ↑(G.obj X)] →
            MonCat.shrinkFunctor.{w, w', v, u} F ⟶ MonCat.shrinkFunctor.{w, w', v, u} G
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_counitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C),
  (CategoryTheory.CostructuredArrow.ofCommaFstEquivalence F G c).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).comp
                (CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c)).obj
            x))
      ⋯
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Cached `getDecLevel type`  -/
Lean.Meta.Grind.Arith.CommRing.Semiring.u : Lean.Meta.Grind.Arith.CommRing.Semiring → Lean.Level
-- Mathlib.Order.Filter.Map
Filter.mem_seq_def : ∀ {α : Type u_1} {β : Type u_2} {f : Filter (α → β)} {g : Filter α} {s : Set β},
  s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, ∀ x ∈ u, ∀ y ∈ t, x y ∈ s
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Multiplying the second vector passed to `oangle` by a positive real does not change the
angle.  -/
Orientation.oangle_smul_right_of_pos : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ}, 0 < r → o.oangle x (r • y) = o.oangle x y
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_C : ∀ {R : Type u_1} [inst : Semiring R] (x y : R) (p : Polynomial R),
  Polynomial.evalEval x y (Polynomial.C p) = Polynomial.eval x p
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.List.forIn'_eq_foldlM.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.done b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_2 b
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (D : Set (Set α)) (s : Set α),
  DirSupInaccOn D s =
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
-- Mathlib.Order.Preorder.Chain
/-- `SuperChain s t` means that `t` is a chain that strictly includes `s`.  -/
SuperChain : {α : Type u_1} → (α → α → Prop) → Set α → Set α → Prop
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_monomial_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {d : σ →₀ ℕ} (c : R),
  m.toSyn (m.degree ((MvPolynomial.monomial d) c)) ≤ m.toSyn d
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_iff_of_countable : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} [Countable α] {p : α → Prop}, (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), μ {x} ≠ 0 → p x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂).get? k = t₁.get? k
-- Mathlib.Topology.Constructions
CofiniteTopology.isOpen_iff : ∀ {X : Type u} {s : Set (CofiniteTopology X)}, IsOpen s ↔ s.Nonempty → sᶜ.Finite
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.prime_rename_iff : ∀ {R : Type u} {σ : Type v} [inst : CommRing R] (s : Set σ) {p : MvPolynomial (↑s) R},
  Prime ((MvPolynomial.rename Subtype.val) p) ↔ Prime p
-- Mathlib.Data.Analysis.Topology
LocallyFinite.Realizer.sets : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      {F : Ctop.Realizer α} →
        {f : β → Set α} →
          (self : LocallyFinite.Realizer F f) → (x : α) → Fintype ↑{i | (f i ∩ F.F.f ↑(self.bas x)).Nonempty}
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X G : C}
  [inst_2 : CategoryTheory.GrpObj G] (f₁ f₂ : X ⟶ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
      (CategoryTheory.GrpObj.commutator G) =
    f₁ * f₂ * f₁⁻¹ * f₂⁻¹
-- Init.Data.SInt.Lemmas
Int8.toInt_zero : Int8.toInt 0 = 0
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.eraseListₘ.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (l : List α) → (Unit → motive []) → ((hd : α) → (tl : List α) → motive (hd :: tl)) → motive l
-- Lean.Parser.Extension
Lean.Parser.throwUnknownParserCategory : {α : Type} → Lean.Name → ExceptT String Id α
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.symm_mk_nsmul : ∀ {M : Type u_1} [inst : AddMonoid M] (a : Mᵈᵃᵃ) (n : ℕ), DomAddAct.mk.symm (n • a) = n • DomAddAct.mk.symm a
-- Mathlib.Data.Fin.Tuple.Basic
/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
given by separating out the first element of the tuple.

This is `Fin.cons` as an `Equiv`.  -/
Fin.consEquiv : {n : ℕ} → (α : Fin (n + 1) → Type u_1) → α 0 × ((i : Fin n) → α i.succ) ≃ ((i : Fin (n + 1)) → α i)
-- Mathlib.Order.Filter.AtTopBot.Monoid
/-- In an ordered cancellative multiplicative monoid, if `C * f x → +∞`, then `f x → +∞`.

Earlier, this name was used for a similar lemma about ordered rings,
which is now called `Filter.Tendsto.atTop_of_const_mul₀`.  -/
Filter.Tendsto.atTop_of_const_mul : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f : α → M} (C : M), Filter.Tendsto (fun x => C * f x) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.instUniqueHomToSSetBot : {X Y : SSet} → Unique (⊥.toSSet ⟶ Y)
-- Mathlib.Logic.Function.Iterate
Function.Commute.iterate_eq_of_map_eq : ∀ {α : Type u} {f g : α → α}, Function.Commute f g → ∀ (n : ℕ) {x : α}, f x = g x → f^[n] x = g^[n] x
-- Mathlib.RingTheory.Multiplicity
emultiplicity_neg : ∀ {α : Type u_1} [inst : Ring α] (a b : α), emultiplicity a (-b) = emultiplicity a b
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is a non-unital commutative
semiring.

See note [reducible non-instances].  -/
NonUnitalAlgebra.adjoinNonUnitalCommSemiringOfComm : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] →
            [inst_4 : SMulCommClass R A A] →
              {s : Set A} → (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) → NonUnitalCommSemiring ↥(NonUnitalAlgebra.adjoin R s)
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  f₁ =ᶠ[nhdsWithin x s] f → derivWithin f₁ s =ᶠ[nhdsWithin x s] derivWithin f s
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesColimit_iff_isColimit_mapCocone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {t : CategoryTheory.Limits.Cocone K} (h : CategoryTheory.Limits.IsColimit t),
  CategoryTheory.Limits.PreservesColimit K F ↔ Nonempty (CategoryTheory.Limits.IsColimit (F.mapCocone t))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF →
    ∀ {l : List α} {k k' : α},
      cmp k k' = Ordering.eq →
        k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKey! k' = k
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.Diagnostic : Type
-- Init.Data.List.Sublist
List.subset_def : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂
-- Init.Data.Int.DivMod.Lemmas
Int.sub_ediv_of_dvd_sub : ∀ {a b c : ℤ}, c ∣ a - b → (a - b) / c = a / c - b / c
-- Mathlib.Algebra.Ring.TransferInstance
Equiv.ringEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : Add β] [inst_1 : Mul β] (a : α), e.ringEquiv a = e a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofArrowIso_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  (F : CategoryTheory.Limits.MonoFactorisation f.hom) (sq : f ⟶ g) [inst_1 : CategoryTheory.IsIso sq],
  (F.ofArrowIso sq).I = F.I
-- Mathlib.CategoryTheory.DifferentialObject
/-- The type of `C`-morphisms that can be lifted back to morphisms in the category `DifferentialObject`.
 -/
CategoryTheory.DifferentialObject.HomSubtype : (S : Type u_1) →
  [inst : AddMonoidWithOne S] →
    (C : Type (u + 1)) →
      [inst_1 : CategoryTheory.LargeCategory C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          {FC : C → C → Type u_2} →
            {CC : C → Type u_3} →
              [inst_3 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
                [CategoryTheory.ConcreteCategory C FC] →
                  [inst_5 : CategoryTheory.HasShift C S] →
                    CategoryTheory.DifferentialObject S C → CategoryTheory.DifferentialObject S C → Type (max 0 u_2)
-- Init.Data.Rat.Lemmas
Rat.le_neg_iff : ∀ {a b : ℚ}, a ≤ -b ↔ b ≤ -a
-- Lean.Meta.Offset
Lean.Meta.mkOffset : Lean.Expr → ℕ → Lean.MetaM Lean.Expr
-- Std.Do.PostCond
Std.Do.ExceptConds.entails_false : ∀ {ps : Std.Do.PostShape} {x : Std.Do.ExceptConds ps}, Std.Do.ExceptConds.false.entails x
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddSemigroup.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddSemigroup Y],
  LocallyConstant.instAddSemigroup = Function.Injective.addSemigroup DFunLike.coe ⋯ ⋯
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.LE.add.eq_1 : ∀ {n m : ℤ} (bounded : Std.Time.Internal.Bounded.LE n m) (num : ℤ), bounded.add num = ⟨↑bounded + num, ⋯⟩
-- Mathlib.Algebra.Polynomial.GroupRingAction
prodXSubSMul.monic : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Fintype G] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : MulSemiringAction G R] (x : R), (prodXSubSMul G R x).Monic
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_open_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), IsOpen hf.localInverse.source
-- Lean.MetavarContext
/-- Return true iff the local declaration `localDecl` depends on a free variable `x` s.t. `pf x`, an unassigned metavariable `?m` s.t. `pm ?m` is true.  -/
Lean.localDeclDependsOnPred : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadMCtx m] →
      Lean.LocalDecl →
        (optParam (Lean.FVarId → Bool) fun x => false) →
          (optParam (Lean.MVarId → Bool) fun x => false) → optParam Bool true → m Bool
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.lt_iff_exists_lt : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α], Order.IsSuccLimit b → (a < b ↔ ∃ c < b, a < c)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sinh_periodic : Function.Periodic Complex.sinh (2 * ↑Real.pi * Complex.I)
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- *Diagonalization theorem*, *spectral theorem*; version 2: A self-adjoint operator `T` on a
finite-dimensional inner product space `E` acts diagonally on the identification of `E` with
Euclidean space induced by an orthonormal basis of eigenvectors of `T`.  -/
LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (v : E)
  (i : Fin n),
  ((hT.eigenvectorBasis hn).repr (T v)).ofLp i = ↑(hT.eigenvalues hn i) * ((hT.eigenvectorBasis hn).repr v).ofLp i
-- Mathlib.Analysis.Complex.Basic
/-- The natural isomorphism between `𝕜` satisfying `RCLike 𝕜` and `ℂ` when
`RCLike.im RCLike.I = 1`.  -/
RCLike.complexRingEquiv : {𝕜 : Type u_2} → [inst : RCLike 𝕜] → RCLike.im RCLike.I = 1 → 𝕜 ≃+* ℂ
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.coe_ofMapBounded : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] (f : α → β)
  {h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)}, ⇑(LocallyBoundedMap.ofMapBounded f h) = f
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.Eqv.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)]
  (f f_1 : (i j : ι) → i ≤ j → G i →ₗ[R] G j),
  f = f_1 →
    ∀ {inst_4 : DecidableEq ι} [inst_5 : DecidableEq ι] (a a_1 : DirectSum ι G),
      a = a_1 →
        ∀ (a_2 a_3 : DirectSum ι G), a_2 = a_3 → Module.DirectLimit.Eqv f a a_2 = Module.DirectLimit.Eqv f_1 a_1 a_3
-- Init.Data.List.Sublist
List.prefix_append_of_prefix : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₁ <+: l₂ ++ l₃
-- Mathlib.Logic.Relation
Relation.instDecidableMapOfExistsAndEq : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        {r : α → β → Prop} →
          {f : α → γ} →
            {g : β → δ} →
              {c : γ} → {d : δ} → [Decidable (∃ a b, r a b ∧ f a = c ∧ g b = d)] → Decidable (Relation.Map r f g c d)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- A point equals its orthogonal projection if and only if it lies in the subspace.  -/
Submodule.starProjection_eq_self_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {v : E}, K.starProjection v = v ↔ v ∈ K
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y : CategoryTheory.Over X) {Z : C} (h : Y.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.snd (CategoryTheory.CategoryStruct.id X) Y.hom) h) =
    h
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.functorCategoryHasLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  [∀ (k : K), CategoryTheory.Limits.HasLimit (F.flip.obj k)], CategoryTheory.Limits.HasLimit F
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalArrayStx : {α : Type} →
  Lean.Expr → (Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)) → Lean.Term → Lean.Elab.TermElabM (Array α × Lean.Expr)