mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.lift_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X))
  (h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom),
  (CategoryTheory.MonoOver.lift F h).comp (CategoryTheory.MonoOver.forget X) = (CategoryTheory.MonoOver.forget Y).comp F
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A set of points is collinear if their `vectorSpan` has dimension
at most `1`.  -/
Collinear : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} → [inst : DivisionRing k] → [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → Set P → Prop
-- Mathlib.Algebra.Order.SuccPred.TypeTags
Order.succ_toAdd : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : SuccOrder X] (x : Multiplicative X),
  Order.succ (Multiplicative.toAdd x) = Multiplicative.toAdd (Order.succ x)
-- Mathlib.Algebra.Order.Field.Basic
/-- **Alias** of the forward direction of `mul_sub_mul_div_mul_nonpos_iff`. -/
div_le_div_of_mul_sub_mul_div_nonpos : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b c d : α},
  c ≠ 0 → d ≠ 0 → (a * d - b * c) / (c * d) ≤ 0 → a / c ≤ b / d
-- Mathlib.Topology.Order.Bornology
isBounded_iff_bddBelow_bddAbove : ∀ {α : Type u_1} {s : Set α} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α],
  Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalCoprimeFactorizationRing.homEquiv.eq_1 : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {n : ℕ} (m k : ℕ)
  (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Polynomial.UniversalCoprimeFactorizationRing.homEquiv S m k hn p =
    {
      toFun := fun f =>
        ⟨↑((Polynomial.UniversalFactorizationRing.homEquiv S m k hn p)
              (f.comp
                (IsScalarTower.toAlgHom R (Polynomial.UniversalFactorizationRing m k hn p)
                  (Polynomial.UniversalCoprimeFactorizationRing m k hn p)))),
          ⋯⟩,
      invFun := fun q =>
        IsLocalization.Away.liftAlgHom (Polynomial.UniversalFactorizationRing.presentation m k hn p).jacobian ⋯,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.comap_map_eq : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L},
  ↑(LieIdeal.map f I) = ⇑f '' ↑I → LieIdeal.comap f (LieIdeal.map f I) = I ⊔ f.ker
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instIsNegApply : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞}, IsNegApply (TestFunction Ω F n) E F
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLE_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ) [t.IsGE X a],
  t.IsGE ((t.truncLE b).obj X) a
-- Mathlib.Data.Set.Order
Set.strictAntiOn_iff_strictAnti : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictAntiOn f s ↔ StrictAnti fun a => f ↑a
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- Pick some representation of `x : span R w` as a linear combination in `w`,
`((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose`
 -/
Span.repr : (R : Type u_4) →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (w : Set M) → ↥(Submodule.span R w) → ↑w →₀ R
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The equalizer condition.  -/
CategoryTheory.IsRegularMono.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsRegularMono f],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsRegularMono.left f) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsRegularMono.right f)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mapEquiv_refl : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  FractionalIdeal.mapEquiv AlgEquiv.refl = RingEquiv.refl (FractionalIdeal S P)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.post_obj_hom : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T)
  (F : CategoryTheory.Functor T C) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.post L R F).obj X).hom = F.map X.hom
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instOfNatWithTopENat : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M], IsManifold I 0 M
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_toSubsemiring : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), S.op.toSubsemiring = S.op
-- Mathlib.Algebra.Ring.Equiv
/-- `Equiv.sumArrowEquivProdArrow` as a ring isomorphism.  -/
RingEquiv.sumArrowEquivProdArrow : (α : Type u_2) → (β : Type u_3) → (R : Type u_4) → [inst : NonAssocSemiring R] → (α ⊕ β → R) ≃+* (α → R) × (β → R)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.maxKey? = some km → t.getKey? km = some km
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_left_le_size_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF), m₁.size ≤ (m₁.union m₂ ⋯ ⋯).size
-- Mathlib.Data.PNat.Xgcd
/-- `IsSpecial'` is an alternative of `IsSpecial`.  -/
PNat.XgcdType.IsSpecial' : PNat.XgcdType → Prop
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- When `D` is a monoidal category,
monoid objects in `C ⥤ D` are the same thing
as functors from `C` into the monoid objects of `D`.
 -/
CategoryTheory.Monoidal.monFunctorCategoryEquivalence : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Mon (CategoryTheory.Functor C D) ≌ CategoryTheory.Functor C (CategoryTheory.Mon D)
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.Config.toConfig : Mathlib.Tactic.RingNF.Config → Mathlib.Tactic.AtomM.Recurse.Config
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
writtenInExtChartAt_chartAt_symm_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {H : Type u_4} {M' : Type u_6} {H' : Type u_7} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  [inst_4 : TopologicalSpace H'] [inst_5 : TopologicalSpace M'] [inst_6 : ChartedSpace H' M']
  [inst_7 : ChartedSpace H H'] (x : M') {y : E},
  y ∈ (extChartAt I x).target → writtenInExtChartAt I I (↑(chartAt H' x) x) (↑(chartAt H' x).symm) y = y
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The centralizer of a set as non-unital subring.  -/
NonUnitalSubring.centralizer : {R : Type u_1} → [inst : NonUnitalRing R] → Set R → NonUnitalSubring R
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_diff_le_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑(m₁.diff m₂)).size ≤ (↑m₁).size
-- Mathlib.Algebra.BigOperators.Finprod
/-- To prove a property of a finite product, it suffices to prove that the property is
multiplicative and holds on factors.  -/
finprod_mem_induction : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α} (p : M → Prop),
  p 1 → (∀ (x y : M), p x → p y → p (x * y)) → (∀ x ∈ s, p (f x)) → p (∏ᶠ (i : α) (_ : i ∈ s), f i)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.nnreal_tsum : ∀ {α : Type u_5} {x : MeasurableSpace α} {ι : Type u_6} [Countable ι] {f : ι → α → NNReal}
  {μ : MeasureTheory.Measure α}, (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (fun x => ∑' (i : ι), f i x) μ
-- Mathlib.Analysis.SpecificLimits.Normed
/-- In a normed ring with summable geometric series, a perturbation of `1` by an element `t`
of distance less than `1` from `1` is a unit.  Here we construct its `Units` structure.  -/
Units.oneSub : {R : Type u_4} → [inst : NormedRing R] → [HasSummableGeomSeries R] → (t : R) → ‖t‖ < 1 → Rˣ
-- Batteries.Logic
/-- **Alias** of `congrFun₂`. -/
congr_fun₂ : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f g : (a : α) → (b : β a) → γ a b},
  f = g → ∀ (a : α) (b : β a), f a b = g a b
-- Std.Data.Iterators.Producers.Monadic.Empty
Std.Iterators.Types.Empty.instIterator : {m : Type w → Type w'} → {β : Type w} → [Monad m] → Std.Iterator (Std.Iterators.Types.Empty m β) m β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- Variant of `of_isColimit` for an arbitrary cocone on a diagram `WalkingSpan ⥤ C`.  -/
CategoryTheory.IsPushout.of_isColimit_cocone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  {D : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} {c : CategoryTheory.Limits.Cocone D}
  (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.IsPushout (D.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
    (D.map CategoryTheory.Limits.WalkingSpan.Hom.snd) (c.ι.app CategoryTheory.Limits.WalkingSpan.left)
    (c.ι.app CategoryTheory.Limits.WalkingSpan.right)
-- Mathlib.Analysis.Complex.Norm
Complex.nndist_self_conj : ∀ (z : ℂ), nndist z ((starRingEnd ℂ) z) = 2 * Real.nnabs z.im
-- Lean.Elab.Match
Lean.Elab.Term.ElabMatchTypeAndDiscrsResult.mk.injEq : ∀ (discrs : Array Lean.Elab.Term.Discr) (matchType : Lean.Expr) (isDep : Bool)
  (alts : Array Lean.Elab.Term.TermMatchAltView) (discrs_1 : Array Lean.Elab.Term.Discr) (matchType_1 : Lean.Expr)
  (isDep_1 : Bool) (alts_1 : Array Lean.Elab.Term.TermMatchAltView),
  ({ discrs := discrs, matchType := matchType, isDep := isDep, alts := alts } =
      { discrs := discrs_1, matchType := matchType_1, isDep := isDep_1, alts := alts_1 }) =
    (discrs = discrs_1 ∧ matchType = matchType_1 ∧ isDep = isDep_1 ∧ alts = alts_1)
-- Mathlib.LinearAlgebra.Dimension.Finite
rank_le_one : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  (v : M), (∀ (w : M), ∃ c, c • v = w) → Module.rank R M ≤ 1
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.coe_mul : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (x y : ↑(Set.Ioo 0 1)),
  ↑(x * y) = ↑x * ↑y
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_natDegree : ∀ (R : Type u) [inst : Ring R] (n : ℕ) [NoZeroDivisors R] [Nontrivial R], (descPochhammer R n).natDegree = n
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instAddCommMonoid : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_5} →
      [inst : PartialOrder Γ] → [inst_1 : SMul R V] → [inst_2 : AddCommMonoid V] → AddCommMonoid (HahnModule Γ R V)
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The proposed colimit cocone is a colimit in `Ring`.  -/
RingCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J RingCat) →
        CategoryTheory.Limits.IsColimit (RingCat.FilteredColimits.colimitCocone F)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.of_splits : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : Field K] [inst_3 : Algebra R K]
  [Algebra.IsIntegral R K] [inst_5 : Module.IsTorsionFree R K],
  (∀ (p : Polynomial R), p.Monic → Irreducible p → (Polynomial.map (algebraMap R K) p).Splits) → IsAlgClosure R K
-- Mathlib.Algebra.Group.Submonoid.Pointwise
/-- The action on a submonoid corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
Submonoid.pointwiseMulAction : {α : Type u_1} →
  {M : Type u_3} → [inst : Monoid M] → [inst_1 : Monoid α] → [MulDistribMulAction α M] → MulAction α (Submonoid M)
-- Mathlib.Algebra.Lie.Extension
/-- The Lie algebra isomorphism given by the type synonym.  -/
LieAlgebra.Extension.ofAlg : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing M] →
              [inst_4 : LieAlgebra R M] →
                [inst_5 : IsLieAbelian M] →
                  [inst_6 : LieRingModule L M] →
                    [inst_7 : LieModule R L M] →
                      (c : ↥(LieModule.Cohomology.twoCocycle R L M)) →
                        LieAlgebra.ofTwoCocycle c ≃ₗ⁅R⁆ (LieAlgebra.Extension.ofTwoCocycle c).L
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- Reinterpret `Additive G ≃+ H` as `G ≃* Multiplicative H`.  -/
AddEquiv.toMultiplicativeRight : {G : Type u_2} →
  {H : Type u_3} → [inst : MulOneClass G] → [inst_1 : AddZeroClass H] → Additive G ≃+ H ≃ (G ≃* Multiplicative H)
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instIntCast : {R : Type u_1} → [IntCast R] → IntCast Rᵃᵒᵖ
-- Init.Data.Range.Polymorphic.Basic
Std.Rco.Internal.get_elem_helper_upper_open : ∀ {α : Type u} {r : Std.Rco α} {hi a : α} [inst : LE α] [inst_1 : LT α], a ∈ r → r.upper = hi → a < hi
-- Mathlib.RingTheory.Discriminant
/-- If `b` is not linear independent, then `Algebra.discr A b = 0`.  -/
Algebra.discr_zero_of_not_linearIndependent : ∀ (A : Type u) {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : Fintype ι] [IsDomain A] {b : ι → B}, ¬LinearIndependent A b → Algebra.discr A b = 0
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmoothOfRelativeDimension_isStableUnderBaseChange : ∀ (n : ℕ), RingHom.IsStableUnderBaseChange (@RingHom.IsStandardSmoothOfRelativeDimension n)
-- Init.Data.Range.Polymorphic.PRange
Std.Rio.instDecidableMemOfDecidableLT : {α : Type u} → {r : Std.Rio α} → {a : α} → [inst : LT α] → [DecidableLT α] → Decidable (a ∈ r)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_eq_restrict_iff : ∀ {α : Type u_1} (M M' : Matroid α) (X : Set α), M.restrict X = M'.restrict X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
-- Init.Data.UInt.Lemmas
UInt16.toFin_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toFin = ⟨n, hn⟩
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.below : {L : FirstOrder.Language} →
  {α : Type u'} →
    {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsPrenex → Prop} →
      {n : ℕ} → {a : L.BoundedFormula α n} → a.IsPrenex → Prop
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffVAdd.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_6} [inst_7 : TopologicalSpace G]
  [inst_8 : ChartedSpace H G] {M : Type u_7} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M]
  [inst_11 : VAdd G M], (ContMDiff (I.prod I') I' n fun p => p.1 +ᵥ p.2) → ContMDiffVAdd I I' n G M
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.liftRel_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {r : β → γ → Prop} {x : β} {y : γ},
  r x y → Filter.Germ.LiftRel r ↑x ↑y
-- Mathlib.Data.Set.Lattice
Set.iUnion_subset_iff : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α} {t : Set α}, ⋃ i, s i ⊆ t ↔ ∀ (i : ι), s i ⊆ t
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- A coalgebra of an endofunctor; `str` stands for "structure morphism"  -/
CategoryTheory.Endofunctor.Coalgebra : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C C → Type (max u v)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_of_isUnit : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} {f : ↑(X.presheaf.obj (Opposite.op U))}, IsUnit f → X.basicOpen f = U
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpen_one : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], AlgebraicGeometry.Proj.basicOpen 𝒜 1 = ⊤
-- Mathlib.Topology.Order
induced_id : ∀ {α : Type u_1} [t : TopologicalSpace α], TopologicalSpace.induced id t = t
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.mk_vadd_mk : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  (r : R) (x : M) (hx : x ∈ s), r +ᵥ ⟨x, hx⟩ = ⟨r +ᵥ x, ⋯⟩
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeAlongCompOfHasPushoutsAlong : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) [P.IsStableUnderCobaseChangeAlong f] [P.IsStableUnderCobaseChangeAlong g] [P.HasPushoutsAlong f],
  P.IsStableUnderCobaseChangeAlong (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_congr_ae : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f g : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  (∀ᵐ (x : X) ∂μ.variation, x ∈ s → f x = g x) → ∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X) in s, g x ∂[B; μ]
-- Mathlib.Data.Finset.Prod
/-- The product of two Finsets is nontrivial iff both are nonempty
at least one of them is nontrivial.  -/
Finset.nontrivial_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β},
  (s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) (hfg : f = g) (x : ↥X) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x) h =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap g x) h)
-- Init.Data.SInt.Lemmas
Int16.toInt8_ofInt : ∀ {n : ℤ}, (Int16.ofInt n).toInt8 = Int8.ofInt n
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The set of points for which a sequence of measurable functions converges to a given function
is measurable.  -/
MeasureTheory.measurableSet_tendsto_fun : ∀ {ι : Type u_2} {γ : Type u_3} {β : Type u_5} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] [Countable ι]
  {l : Filter ι} [l.IsCountablyGenerated] [inst_4 : TopologicalSpace γ] [SecondCountableTopology γ]
  [TopologicalSpace.PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] {f : ι → β → γ},
  (∀ (i : ι), Measurable (f i)) →
    ∀ {g : β → γ}, Measurable g → MeasurableSet {x | Filter.Tendsto (fun n => f n x) l (nhds (g x))}
-- Init.Data.String.Basic
String.isSome_utf8DecodeChar?_zero : ∀ {b : String}, b ≠ "" → (b.toByteArray.utf8DecodeChar? 0).isSome = true
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.ext : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, (∀ (x : ι → ℝ), x ∈ I ↔ x ∈ J) → I = J
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.strictAntiOn_smoothingFn : StrictAntiOn AkraBazziRecurrence.smoothingFn (Set.Ioi 1)
-- Lean.Parser.Extra
Lean.ppHardLineUnlessUngrouped.formatter : Lean.PrettyPrinter.Formatter
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.Barrier.mk.inj : ∀ {lock : Std.Mutex Std.BarrierState✝} {cvar : Std.Condvar} {numThreads : ℕ} {lock_1 : Std.Mutex Std.BarrierState✝}
  {cvar_1 : Std.Condvar} {numThreads_1 : ℕ},
  { lock := lock, cvar := cvar, numThreads := numThreads } =
      { lock := lock_1, cvar := cvar_1, numThreads := numThreads_1 } →
    lock = lock_1 ∧ cvar = cvar_1 ∧ numThreads = numThreads_1
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFDerivWithinAt.continuousMultilinearMap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] {G : Type u_4} [inst_6 : NormedAddCommGroup G]
  [inst_7 : NormedSpace 𝕜 G] [inst_8 : DecidableEq ι] {s : Set G} {x : G} {f : G → ContinuousMultilinearMap 𝕜 E F}
  {g : (i : ι) → G → E i} {f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F} {g' : (i : ι) → G →L[𝕜] E i},
  HasFDerivWithinAt f f' s x →
    (∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x) →
      HasFDerivWithinAt (fun x => (f x) fun x_1 => g x_1 x)
        ((ContinuousMultilinearMap.apply 𝕜 E F fun x_1 => g x_1 x) ∘SL f' +
          ∑ i, (f x).toContinuousLinearMap (fun x_1 => g x_1 x) i ∘SL g' i)
        s x
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.Limits.Cofan.IsColimit.desc.eq_1 : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F}
  (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A),
  CategoryTheory.Limits.Cofan.IsColimit.desc hc f = hc.desc (CategoryTheory.Limits.Cofan.mk A f)
-- Mathlib.CategoryTheory.Adjunction.Evaluation
/-- See also the file `Mathlib/CategoryTheory/Limits/FunctorCategory/EpiMono.lean`
for a similar result under a `HasPushouts` assumption.  -/
CategoryTheory.NatTrans.epi_iff_epi_app' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G),
  CategoryTheory.Epi η ↔ ∀ (c : C), CategoryTheory.Epi (η.app c)
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecsInfo.mk.sizeOf_spec : ∀ (clsName : Lean.Name) (privateSpecs : Bool) (fieldImpls : Array (Lean.Name × Lean.Name))
  (thms : Array Lean.MethodSpecTheorem✝),
  sizeOf { clsName := clsName, privateSpecs := privateSpecs, fieldImpls := fieldImpls, thms := thms } =
    1 + sizeOf clsName + sizeOf privateSpecs + sizeOf fieldImpls + sizeOf thms
-- Mathlib.Tactic.CongrExclamation
/-- Whether to require that both sides of an equality be applications of defeq functions.
That is, if true, `f a = g x` is only considered if `f` and `g` are defeq (making it be similar
to the `congr` tactic).  -/
Congr!.Config.sameFun : Congr!.Config → Bool
-- Mathlib.Order.Heyting.Basic
Codisjoint.himp_eq_left : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → a ⇨ b = b