mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.forall : ∀ {α : Type u_2} [inst : TopologicalSpace α] {p : TopologicalSpace.Opens α → Prop},
  (∀ (U : TopologicalSpace.Opens α), p U) ↔ ∀ (U : Set α) (hU : IsOpen U), p { carrier := U, is_open' := hU }
-- Mathlib.GroupTheory.Perm.Fin
/-- `Fin.cycleRange i` is the cycle `(0 1 2 ... i)` leaving `(i+1 ... (n-1))` unchanged.  -/
Fin.cycleRange : {n : ℕ} → Fin n → Equiv.Perm (Fin n)
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Given a spanning set of `Γ(X, U)`, the corresponding basic open sets cover `U`.
See `IsAffineOpen.basicOpen_union_eq_self_iff` for the inverse direction for affine open sets.
 -/
AlgebraicGeometry.iSup_basicOpen_of_span_eq_top : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))),
  Ideal.span s = ⊤ → ⨆ i ∈ s, X.basicOpen i = U
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.fst_surjective : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W), Function.Surjective ⇑(Representation.IntertwiningMap.fst A ρ σ)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_left_unitor_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map f).toFunctor.map ((self.mapId a).hom.toNatTrans.app X)) h)
-- Mathlib.RingTheory.Noetherian.Defs
/-- An R-module is Noetherian iff all its submodules are finitely-generated.  -/
isNoetherian_def : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsNoetherian R M ↔ ∀ (s : Submodule R M), s.FG
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.eval₂_T_neg_n : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] (f : R →+* S) (x : Sˣ) (n : ℕ),
  (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.T (-↑n)) = ↑x⁻¹ ^ n
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.prod.instIsAddHaarMeasure : ∀ {G : Type u_3} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {x : MeasurableSpace G} {H : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : TopologicalSpace H] {x_1 : MeasurableSpace H} (μ : MeasureTheory.Measure G)
  (ν : MeasureTheory.Measure H) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] [MeasurableAdd G] [MeasurableAdd H], (μ.prod ν).IsAddHaarMeasure
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.containsThenInsert : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → Bool × Std.DHashMap.Internal.Raw₀ α β
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.let.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.LetDecl pu) (k : Lean.Compiler.LCNF.Code pu),
  sizeOf (Lean.Compiler.LCNF.Code.let decl k) = 1 + sizeOf decl + sizeOf k
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
NNReal.nndist_zero_eq_val' : ∀ (z : NNReal), nndist z 0 = z
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- A 1-morphism in one direction.  -/
CategoryTheory.Bicategory.Equivalence.hom : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → {a b : B} → CategoryTheory.Bicategory.Equivalence a b → (a ⟶ b)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.instFullSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α]
  [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat],
  ((SheafOfModules.forget R).comp (PresheafOfModules.restrictScalars α)).Full
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.congr_eq_3 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (x : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit)
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (b : Bool),
  x = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) →
    (match x with
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) ≍
      h_3 l b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_eq_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {he : t ≠ ∅}, t.minKey he = t.minKey!
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.State.mk.inj : ∀ {atoms atoms_1 : Array Lean.Expr}, { atoms := atoms } = { atoms := atoms_1 } → atoms = atoms_1
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of a `C^n` function on a domain and a constant is `C^n`.  -/
ContDiffOn.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {A : Type u_4} [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F] [IsScalarTower 𝕜 A F]
  [IsBoundedSMul A F] {s : Set E} {f : E → A}, ContDiffOn 𝕜 n f s → ∀ (v : F), ContDiffOn 𝕜 n (fun y => f y • v) s
-- Mathlib.Topology.Neighborhoods
mem_closure_iff_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∈ closure s ↔ ∃ᶠ (x : X) in nhds x, x ∈ s
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_lt_mul_iff_right₀`. -/
mul_lt_mul_iff_of_pos_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulStrictMono α]
  [PosMulReflectLT α], 0 < a → (a * b < a * c ↔ b < c)
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `nndist_eq_nnnorm_sub`. -/
nndist_eq_nnnorm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), nndist a b = ‖a - b‖₊
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
one_le_of_le_mul_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulLeftReflectLE α] {a b : α}, a ≤ a * b → 1 ≤ b
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.comp_δ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j), CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap S.g i) (hS.δ i j hij) = 0
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
CategoryTheory.CommSq.rightAdjointLiftStructEquiv.eq_1 : ∀ {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] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
  {A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y}
  (sq : CategoryTheory.CommSq u (G.map i) p v) (adj : G ⊣ F),
  sq.rightAdjointLiftStructEquiv adj =
    { toFun := fun l => { l := (adj.homEquiv B X) l.l, fac_left := ⋯, fac_right := ⋯ },
      invFun := fun l => { l := (adj.homEquiv B X).symm l.l, fac_left := ⋯, fac_right := ⋯ }, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Data.Stream.Init
Stream'.getElem?_take_succ : ∀ {α : Type u} (n : ℕ) (s : Stream' α), (Stream'.take n.succ s)[n]? = some (s.get n)
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instReflBEq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  ReflBEq (Std.ExtHashSet α)
-- Mathlib.Analysis.Complex.Trigonometric
/-- The definition of `sinh` in terms of `exp`.  -/
Real.sinh_eq : ∀ (x : ℝ), Real.sinh x = (Real.exp x - Real.exp (-x)) / 2
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k fallback : α},
  k ∉ t → l.contains k = false → (t.insertMany l).getD k fallback = fallback
-- Mathlib.Data.Holor
Holor.slice.congr_simp : ∀ {α : Type} {d : ℕ} {ds : List ℕ} (x x_1 : Holor α (d :: ds)),
  x = x_1 →
    ∀ (i i_1 : ℕ) (e_i : i = i_1) (h : i < d) (a a_1 : HolorIndex ds), a = a_1 → x.slice i h a = x_1.slice i_1 ⋯ a_1
-- Mathlib.Topology.Connected.Basic
/-- Preconnectedness of the iUnion of a family of preconnected sets
indexed by the vertices of a preconnected graph,
where two vertices are joined when the corresponding sets intersect.  -/
IsPreconnected.iUnion_of_reflTransGen : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {s : ι → Set α},
  (∀ (i : ι), IsPreconnected (s i)) →
    (∀ (i j : ι), Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j) → IsPreconnected (⋃ n, s n)
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprRaw_mathlib_1.toExpr : Substring.Raw → Lean.Expr
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight.injEq : ∀ (e : Lean.Expr) (f g : Mathlib.Tactic.BicategoryLike.Mor₁) (η : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (h : Mathlib.Tactic.BicategoryLike.Mor₁) (e_1 : Lean.Expr) (f_1 g_1 : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso) (h_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight e f g η h =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight e_1 f_1 g_1 η_1 h_1) =
    (e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ η = η_1 ∧ h = h_1)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_trans_rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (f : M ≃ₗ[R] P)
  (g : N ≃ₗ[R] Q), LinearEquiv.lTensor M g ≪≫ₗ LinearEquiv.rTensor Q f = TensorProduct.congr f g
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- Warning: This gives a diamond on `SMul R[S⁻¹] M[S⁻¹][S⁻¹]`, but we will almost never localize
at the same monoid twice.  -/
OreLocalization.instSMulOfIsScalarTower : {R : Type u_1} →
  {M : Type u_3} →
    {X : Type u_4} →
      [inst : Monoid M] →
        {S : Submonoid M} →
          [inst_1 : OreLocalization.OreSet S] →
            [inst_2 : MulAction M X] →
              [inst_3 : SMul R X] →
                [inst_4 : SMul R M] → [IsScalarTower R M X] → [IsScalarTower R M M] → SMul R (OreLocalization S X)
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instProjectiveOppositeOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : C} [CategoryTheory.Injective J],
  CategoryTheory.Projective (Opposite.op J)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Stream.nil.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α], sizeOf RBTree.RBNode.Stream.nil = 1
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_rev : ∀ {α : Sort u_1} {m n : ℕ} (xs : Fin m → α) (ys : Fin n → α) (i : Fin (m + n)),
  Fin.append xs ys i.rev = Fin.append (ys ∘ Fin.rev) (xs ∘ Fin.rev) (Fin.cast ⋯ i)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Structure witnessing that a bicone is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.Bicone.IsBilimit.isColimit : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → {B : CategoryTheory.Limits.Bicone F} → B.IsBilimit → CategoryTheory.Limits.IsColimit B.toCocone
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- This instance is useful for some measure-theoretic statements.  -/
SummationFilter.instIsCountablyGeneratedFinsetFilterUnconditionalOfCountable : ∀ (β : Type u_2) [Countable β], (SummationFilter.unconditional β).filter.IsCountablyGenerated
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
StrongDual.toStrongDual_toWeakDual : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (x : StrongDual 𝕜 E), WeakDual.toStrongDual (StrongDual.toWeakDual x) = x
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of `· - x` at `x` is `1`.  -/
meromorphicOrderAt_id_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜}, meromorphicOrderAt (fun x_1 => x_1 - x) x = 1
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` is closed under inverse.  -/
AddSubgroup.neg_mem : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x : G}, x ∈ H → -x ∈ H
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.functor_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) {i : CategoryTheory.Discrete I}
  (f : i ⟶ i), (CategoryTheory.Discrete.functor F).map f = CategoryTheory.CategoryStruct.id (F i.as)
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap_add`. -/
LinearOrderedField.inducedMap_add : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (x y : α),
  ConditionallyCompleteLinearOrderedField.inducedMap α β (x + y) =
    ConditionallyCompleteLinearOrderedField.inducedMap α β x + ConditionallyCompleteLinearOrderedField.inducedMap α β y
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.of_vadd : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (x : α) (y : β), FreeAddMonoid.of x +ᵥ y = f x y
-- Mathlib.Order.Disjoint
Codisjoint.inf_left : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderTop α] {a b c : α},
  Codisjoint a c → Codisjoint b c → Codisjoint (a ⊓ b) c
-- Lean.Meta.SizeOf
Lean.Meta.mkSizeOfSpecLemmaInstance : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under integer division.  -/
Dioph.«term_D/_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.factorₐ.congr_simp : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (hIJ : I ≤ J),
  Ideal.Quotient.factorₐ R₁ hIJ = Ideal.Quotient.factorₐ R₁ hIJ
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (X : CategoryTheory.Endofunctor.Coalgebra F),
  (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId.hom.app X).f = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.ext : ∀ {R : Type u_1} [inst : NonUnitalRing R] {p q : RingSeminorm R}, (∀ (x : R), p x = q x) → p = q
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), AddSubsemigroup.comap f ⊤ = ⊤
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioo_add_one_right_eq_Ioc_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Set.Ioo a (b + 1) = Set.Ioc a b
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_extend_one : ∀ {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [inst : One N] {f : ι → κ} {g : ι → N},
  Function.Injective f → Function.mulSupport (Function.extend f g 1) = f '' Function.mulSupport g
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.mul_closedBall : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), s * Metric.closedBall x δ = x • Metric.cthickening δ s
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)]
  [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C}
  (h : CategoryTheory.Limits.colimit (CategoryTheory.Functor.uncurry.obj F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).inv h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.uncurry.obj F) (j, k)) h
-- Lean.Declaration
/-- Returns the value of a definition. With `allowOpaque := true`, values
of theorems and opaque declarations are also returned.
 -/
Lean.ConstantInfo.value? : Lean.ConstantInfo → optParam Bool false → Option Lean.Expr
-- Init.Data.Option.Attach
Option.attach_map : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} (f : α → β),
  (Option.map f o).attach =
    Option.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      o.attach
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.divCoeffs.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.divCoeffs c =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.divCoeffs c_1) =
    (c = c_1)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.unitIso.hom.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageZeroHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : DecidableEq β] [inst_2 : Zero β]
  [inst_3 : FunLike F α β] [inst_4 : ZeroHomClass F α β] (f : F) (s : Finset α),
  (Finset.imageZeroHom f) s = Finset.image (⇑f) s
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Adjunction.mapAddGrp_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal],
  a.mapAddGrp.counit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapAddGrpCompIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapAddGrpNatTrans a.counit)
        CategoryTheory.Functor.mapAddGrpIdIso.hom)
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.cases_on : ∀ {α : Type u} {P : WithOne α → Prop} (x : WithOne α), P 1 → (∀ (a : α), P ↑a) → P x
-- Mathlib.CategoryTheory.Abelian.Subcategory
CategoryTheory.ObjectProperty.preservesMonomorphisms_ι_of_isNormalEpiCategory : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.IsNormalEpiCategory C]
  [CategoryTheory.Limits.HasZeroObject C] [P.ContainsZero] [P.IsClosedUnderKernels], P.ι.PreservesMonomorphisms
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
/-- The canonical natural isomorphism
`(whiskeringRight Cᵒᵖ A B).obj F ⋙ G₂ ≅ G₁ ⋙ sheafCompose J F`
when `F : A ⥤ B` preserves sheafification, and that `G₁` and `G₂` are
left adjoints to the forget functors `sheafToPresheaf`.  -/
CategoryTheory.sheafComposeNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u_1} →
        {B : Type u_2} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} B] →
              (F : CategoryTheory.Functor A B) →
                {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} →
                  (G₁ ⊣ CategoryTheory.sheafToPresheaf J A) →
                    {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} →
                      (G₂ ⊣ CategoryTheory.sheafToPresheaf J B) →
                        [inst_3 : J.HasSheafCompose F] →
                          [J.PreservesSheafification F] →
                            ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ≅
                              G₁.comp (CategoryTheory.sheafCompose J F)
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.germ_residue : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (x : ↥X) (hx : x ∈ U),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x hx) (X.residue x) = X.evaluation U x hx
-- Mathlib.Topology.Path
Path.cast_rfl_rfl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ.cast ⋯ ⋯ = γ
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier transform integral for `f : V → E`, with respect to a bilinear form `L : V × W → 𝕜`
and an additive character `e`.  -/
VectorFourier.fourierIntegral : {𝕜 : Type u_1} →
  [inst : CommRing 𝕜] →
    {V : Type u_2} →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module 𝕜 V] →
          [inst_3 : MeasurableSpace V] →
            {W : Type u_3} →
              [inst_4 : AddCommGroup W] →
                [inst_5 : Module 𝕜 W] →
                  {E : Type u_4} →
                    [inst_6 : NormedAddCommGroup E] →
                      [NormedSpace ℂ E] →
                        AddChar 𝕜 Circle → MeasureTheory.Measure V → (V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) → (V → E) → W → E
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.mul_eq_dfinsuppSum : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)]
  (a a' : DirectSum ι fun i => A i),
  a * a' =
    DFinsupp.sum a fun x ai => DFinsupp.sum a' fun x_1 aj => (DirectSum.of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)